<commit_before>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>
-/
import set_theory.cardinal_ordinal
/-!
# Cofinality

This file contains the definition of cofinality of a ordinal number and regular cardinals

## Main Definitions

* `ordinal.cof o` is the cofinality of the ordinal `o`.
  If `o` is the order type of the relation `<` on `α`, then `o.cof` is the smallest cardinality of a
  subset `s` of α that is *cofinal* in `α`, i.e. `∀ x : α, ∃ y ∈ s, ¬ y < x`.
* `cardinal.is_limit c` means that `c` is a (weak) limit cardinal: `c ≠ 0 ∧ ∀ x < c, succ x < c`.
* `cardinal.is_strong_limit c` means that `c` is a strong limit cardinal:
  `c ≠ 0 ∧ ∀ x < c, 2 ^ x < c`.
* `cardinal.is_regular c` means that `c` is a regular cardinal: `ω ≤ c ∧ c.ord.cof = c`.
* `cardinal.is_inaccessible c` means that `c` is strongly inaccessible:
  `ω < c ∧ is_regular c ∧ is_strong_limit c`.

## Main Statements

* `ordinal.infinite_pigeonhole_card`: the infinite pigeonhole principle
* `cardinal.lt_power_cof`: A consequence of König's theorem stating that `c < c ^ c.ord.cof` for
  `c ≥ ω`
* `cardinal.univ_inaccessible`: The type of ordinals in `Type u` form an inaccessible cardinal
  (in `Type v` with `v > u`). This shows (externally) that in `Type u` there are at least `u`
  inaccessible cardinals.

## Implementation Notes

* The cofinality is defined for ordinals.
  If `c` is a cardinal number, its cofinality is `c.ord.cof`.

## Tags

cofinality, regular cardinals, limits cardinals, inaccessible cardinals,
infinite pigeonhole principle


-/
noncomputable theory

open function cardinal set
open_locale classical cardinal

universes u v w
variables {α : Type*} {r : α → α → Prop}

/-! ### Cofinality of orders -/

namespace order
/-- Cofinality of a reflexive order `≼`. This is the smallest cardinality
  of a subset `S : set α` such that `∀ a, ∃ b ∈ S, a ≼ b`. -/
def cof (r : α → α → Prop) [is_refl α r] : cardinal :=
@cardinal.min {S : set α // ∀ a, ∃ b ∈ S, r a b}
  ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
  (λ S, #S)

lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) :
  order.cof r ≤ #S :=
le_trans (cardinal.min_le _ ⟨S, h⟩) le_rfl

lemma le_cof {r : α → α → Prop} [is_refl α r] (c : cardinal) :
  c ≤ order.cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ #S :=
by { rw [order.cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }

end order

theorem rel_iso.cof.aux {α : Type u} {β : Type v} {r s}
  [is_refl α r] [is_refl β s] (f : r ≃r s) :
  cardinal.lift.{(max u v)} (order.cof r) ≤
  cardinal.lift.{(max u v)} (order.cof s) :=
begin
  rw [order.cof, order.cof, lift_min, lift_min, cardinal.le_min],
  intro S, cases S with S H, simp only [comp, coe_sort_coe_base, subtype.coe_mk],
  refine le_trans (min_le _ _) _,
  { exact ⟨f ⁻¹' S, λ a,
    let ⟨b, bS, h⟩ := H (f a) in ⟨f.symm b, by simp [bS, ← f.map_rel_iff, h,
      -coe_fn_coe_base, -coe_fn_coe_trans, principal_seg.coe_coe_fn', initial_seg.coe_coe_fn]⟩⟩ },
  { exact lift_mk_le.{u v (max u v)}.2
    ⟨⟨λ ⟨x, h⟩, ⟨f x, h⟩, λ ⟨x, h₁⟩ ⟨y, h₂⟩ h₃,
      by congr; injection h₃ with h'; exact f.to_equiv.injective h'⟩⟩ }
end

theorem rel_iso.cof {α : Type u} {β : Type v} {r s}
  [is_refl α r] [is_refl β s] (f : r ≃r s) :
  cardinal.lift.{(max u v)} (order.cof r) =
  cardinal.lift.{(max u v)} (order.cof s) :=
le_antisymm (rel_iso.cof.aux f) (rel_iso.cof.aux f.symm)

def strict_order.cof (r : α → α → Prop) [h : is_irrefl α r] : cardinal :=
@order.cof α (λ x y, ¬ r y x) ⟨h.1⟩

/-! ### Cofinality of ordinals -/

namespace ordinal

/-- Cofinality of an ordinal. This is the smallest cardinal of a
  subset `S` of the ordinal which is unbounded, in the sense
  `∀ a, ∃ b ∈ S, a ≤ b`. It is defined for all ordinals, but
  `cof 0 = 0` and `cof (succ o) = 1`, so it is only really
  interesting on limit ordinals (when it is an infinite cardinal). -/
def cof (o : ordinal.{u}) : cardinal.{u} :=
quot.lift_on o (λ a, by exactI strict_order.cof a.r)
begin
  rintros ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩,
  rw ← cardinal.lift_inj,
  apply rel_iso.cof ⟨f, _⟩,
  simp [hf]
end

lemma cof_type (r : α → α → Prop) [is_well_order α r] : (type r).cof = strict_order.cof r := rfl

theorem le_cof_type [is_well_order α r] {c} : c ≤ cof (type r) ↔
  ∀ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) → c ≤ #S :=
by dsimp [cof, strict_order.cof, order.cof, type, quotient.mk, quot.lift_on];
   rw [cardinal.le_min, subtype.forall]; refl

theorem cof_type_le [is_well_order α r] (S : set α) (h : ∀ a, ∃ b ∈ S, ¬ r b a) :
  cof (type r) ≤ #S :=
le_cof_type.1 le_rfl S h

theorem lt_cof_type [is_well_order α r] (S : set α) (hl : #S < cof (type r)) :
  ∃ a, ∀ b ∈ S, r b a :=
not_forall_not.1 $ λ h, not_le_of_lt hl $ cof_type_le S (λ a, not_ball.1 (h a))

theorem cof_eq (r : α → α → Prop) [is_well_order α r] :
  ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ #S = cof (type r) :=
begin
  have : ∃ i, cof (type r) = _,
  { dsimp [cof, order.cof, type, quotient.mk, quot.lift_on],
    apply cardinal.min_eq },
  exact let ⟨⟨S, hl⟩, e⟩ := this in ⟨S, hl, e.symm⟩,
end

theorem ord_cof_eq (r : α → α → Prop) [is_well_order α r] :
  ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ type (subrel r S) = (cof (type r)).ord :=
let ⟨S, hS, e⟩ := cof_eq r, ⟨s, _, e'⟩ := cardinal.ord_eq S,
    T : set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a} in
begin
  resetI, suffices,
  { refine ⟨T, this,
      le_antisymm _ (cardinal.ord_le.2 $ cof_type_le T this)⟩,
    rw [← e, e'],
    refine type_le'.2 ⟨rel_embedding.of_monotone
      (λ a, ⟨a, let ⟨aS, _⟩ := a.2 in aS⟩) (λ a b h, _)⟩,
    rcases a with ⟨a, aS, ha⟩, rcases b with ⟨b, bS, hb⟩,
    change s ⟨a, _⟩ ⟨b, _⟩,
    refine ((trichotomous_of s _ _).resolve_left (λ hn, _)).resolve_left _,
    { exact asymm h (ha _ hn) },
    { intro e, injection e with e, subst b,
      exact irrefl _ h } },
  { intro a,
    have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
    let b := (is_well_order.wf).min _ this,
    have ba : ¬r b a := (is_well_order.wf).min_mem _ this,
    refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
    rw [show ∀b:S, (⟨b, b.2⟩:S) = b, by intro b; cases b; refl],
    exact (is_well_order.wf).not_lt_min _ this
      (is_order_connected.neg_trans h ba) }
end

/-! ### Cofinality of suprema and least strict upper bounds -/

private theorem card_mem_cof {o} : ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = o.card :=
⟨_, _, lsub_typein o, mk_ordinal_out o⟩

/-- The set in the `lsub` characterization of `cof` is nonempty. -/
theorem cof_lsub_def_nonempty (o) :
  {a : cardinal | ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = a}.nonempty :=
⟨_, card_mem_cof⟩

theorem cof_eq_Inf_lsub (o : ordinal.{u}) :
  cof o = Inf {a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = a} :=
begin
  refine le_antisymm (le_cInf (cof_lsub_def_nonempty o) _) (cInf_le' _),
  { rintros a ⟨ι, f, hf, rfl⟩,
    rw ←type_lt o,
    refine (cof_type_le _ (λ a, _)).trans (@mk_le_of_injective _ _
      (λ s : (typein ((<) : o.out.α → o.out.α → Prop))⁻¹' (set.range f), classical.some s.prop)
      (λ s t hst, let H := congr_arg f hst in by rwa [classical.some_spec s.prop,
        classical.some_spec t.prop, typein_inj, subtype.coe_inj] at H)),
    have := typein_lt_self a,
    simp_rw [←hf, lt_lsub_iff] at this,
    cases this with i hi,
    refine ⟨enum (<) (f i) _, _, _⟩,
    { rw [type_lt, ←hf], apply lt_lsub },
    { rw [mem_preimage, typein_enum], exact mem_range_self i },
    { rwa [←typein_le_typein, typein_enum] } },
  { rcases cof_eq (<) with ⟨S, hS, hS'⟩,
    let f : S → ordinal := λ s, typein (<) s.val,
    refine ⟨S, f, le_antisymm (lsub_le (λ i, typein_lt_self i)) (le_of_forall_lt (λ a ha, _)),
      by rwa type_lt o at hS'⟩,
    rw ←type_lt o at ha,
    rcases hS (enum (<) a ha) with ⟨b, hb, hb'⟩,
    rw [←typein_le_typein, typein_enum] at hb',
    exact hb'.trans_lt (lt_lsub.{u u} f ⟨b, hb⟩) }
end

theorem lift_cof (o) : (cof o).lift = cof o.lift :=
induction_on o $ begin introsI α r _,
  cases lift_type r with _ e, rw e,
  apply le_antisymm,
  { unfreezingI { refine le_cof_type.2 (λ S H, _) },
    have : (#(ulift.up ⁻¹' S)).lift ≤ #S :=
     ⟨⟨λ ⟨⟨x, h⟩⟩, ⟨⟨x⟩, h⟩,
       λ ⟨⟨x, h₁⟩⟩ ⟨⟨y, h₂⟩⟩ e, by simp at e; congr; injection e⟩⟩,
    refine le_trans (cardinal.lift_le.2 $ cof_type_le _ _) this,
    exact λ a, let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩ in ⟨b, bs, br⟩ },
  { rcases cof_eq r with ⟨S, H, e'⟩,
    have : #(ulift.down ⁻¹' S) ≤ (#S).lift :=
     ⟨⟨λ ⟨⟨x⟩, h⟩, ⟨⟨x, h⟩⟩,
       λ ⟨⟨x⟩, h₁⟩ ⟨⟨y⟩, h₂⟩ e, by simp at e; congr; injections⟩⟩,
    rw e' at this,
    unfreezingI { refine le_trans (cof_type_le _ _) this },
    exact λ ⟨a⟩, let ⟨b, bs, br⟩ := H a in ⟨⟨b⟩, bs, br⟩ }
end

theorem cof_le_card (o) : cof o ≤ card o :=
by { rw cof_eq_Inf_lsub, exact cInf_le' card_mem_cof }

theorem cof_ord_le (c : cardinal) : cof c.ord ≤ c :=
by simpa using cof_le_card c.ord

theorem ord_cof_le (o : ordinal.{u}) : o.cof.ord ≤ o :=
(ord_le_ord.2 (cof_le_card o)).trans (ord_card_le o)

theorem exists_lsub_cof (o : ordinal) : ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = cof o :=
by { rw cof_eq_Inf_lsub, exact Inf_mem (cof_lsub_def_nonempty o) }

theorem cof_lsub_le {ι} (f : ι → ordinal) : cof (lsub.{u u} f) ≤ #ι :=
by { rw cof_eq_Inf_lsub, exact cInf_le' ⟨ι, f, rfl, rfl⟩ }

theorem cof_lsub_le_lift {ι} (f : ι → ordinal) : cof (lsub f) ≤ cardinal.lift.{v u} (#ι) :=
begin
  rw ←mk_ulift,
  convert cof_lsub_le (λ i : ulift ι, f i.down),
  exact lsub_eq_of_range_eq.{u (max u v) max u v}
    (set.ext (λ x, ⟨λ ⟨i, hi⟩, ⟨ulift.up i, hi⟩, λ ⟨i, hi⟩, ⟨_, hi⟩⟩))
end

theorem le_cof_iff_lsub {o : ordinal} {a : cardinal} :
  a ≤ cof o ↔ ∀ {ι} (f : ι → ordinal), lsub.{u u} f = o → a ≤ #ι :=
begin
  rw cof_eq_Inf_lsub,
  exact (le_cInf_iff'' (cof_lsub_def_nonempty o)).trans ⟨λ H ι f hf, H _ ⟨ι, f, hf, rfl⟩,
    λ H b ⟨ι, f, hf, hb⟩, ( by { rw ←hb, exact H _ hf} )⟩
end

theorem lsub_lt_ord_lift {ι} {f : ι → ordinal} {c : ordinal} (hι : cardinal.lift (#ι) < c.cof)
  (hf : ∀ i, f i < c) : lsub.{u v} f < c :=
lt_of_le_of_ne (lsub_le hf) (λ h, by { subst h, exact (cof_lsub_le_lift f).not_lt hι })

theorem lsub_lt_ord {ι} {f : ι → ordinal} {c : ordinal} (hι : #ι < c.cof) :
  (∀ i, f i < c) → lsub.{u u} f < c :=
lsub_lt_ord_lift (by rwa (#ι).lift_id)

theorem cof_sup_le_lift {ι} {f : ι → ordinal} (H : ∀ i, f i < sup f) : cof (sup f) ≤ (#ι).lift :=
by { rw ←sup_eq_lsub_iff_lt_sup at H, rw H, exact cof_lsub_le_lift f }

theorem cof_sup_le {ι} {f : ι → ordinal} (H : ∀ i, f i < sup.{u u} f) : cof (sup.{u u} f) ≤ #ι :=
by { rw ←(#ι).lift_id, exact cof_sup_le_lift H }

theorem sup_lt_ord_lift {ι} {f : ι → ordinal} {c : ordinal} (hι : cardinal.lift (#ι) < c.cof)
  (hf : ∀ i, f i < c) : sup.{u v} f < c :=
(sup_le_lsub.{u v} f).trans_lt (lsub_lt_ord_lift hι hf)

theorem sup_lt_ord {ι} {f : ι → ordinal} {c : ordinal} (hι : #ι < c.cof) :
  (∀ i, f i < c) → sup.{u u} f < c :=
sup_lt_ord_lift (by rwa (#ι).lift_id)

theorem sup_lt_lift {ι} {f : ι → cardinal} {c : cardinal} (hι : cardinal.lift (#ι) < c.ord.cof)
  (hf : ∀ i, f i < c) : cardinal.sup.{u v} f < c :=
by { rw [←ord_lt_ord, ←sup_ord], refine sup_lt_ord_lift hι (λ i, _), rw ord_lt_ord, apply hf }

theorem sup_lt {ι} {f : ι → cardinal} {c : cardinal} (hι : #ι < c.ord.cof) :
  (∀ i, f i < c) → cardinal.sup.{u u} f < c :=
sup_lt_lift (by rwa (#ι).lift_id)

theorem exists_blsub_cof (o : ordinal) : ∃ (f : Π a < (cof o).ord, ordinal), blsub.{u u} _ f = o :=
begin
  rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩,
  rcases cardinal.ord_eq ι with ⟨r, hr, hι'⟩,
  rw ←@blsub_eq_lsub' ι r hr at hf,
  rw [←hι, hι'],
  exact ⟨_, hf⟩
end

theorem le_cof_iff_blsub {b : ordinal} {a : cardinal} :
  a ≤ cof b ↔ ∀ {o} (f : Π a < o, ordinal), blsub.{u u} o f = b → a ≤ o.card :=
le_cof_iff_lsub.trans ⟨λ H o f hf, by simpa using H _ hf, λ H ι f hf, begin
  rcases cardinal.ord_eq ι with ⟨r, hr, hι'⟩,
  rw ←@blsub_eq_lsub' ι r hr at hf,
  simpa using H _ hf
end⟩

theorem cof_blsub_le_lift {o} (f : Π a < o, ordinal) :
  cof (blsub o f) ≤ cardinal.lift.{v u} (o.card) :=
by { convert cof_lsub_le_lift _, exact (mk_ordinal_out o).symm }

theorem cof_blsub_le {o} (f : Π a < o, ordinal) : cof (blsub.{u u} o f) ≤ o.card :=
by { rw ←(o.card).lift_id, exact cof_blsub_le_lift f }

theorem blsub_lt_ord_lift {o : ordinal} {f : Π a < o, ordinal} {c : ordinal}
  (ho : o.card.lift < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u v} o f < c :=
lt_of_le_of_ne (blsub_le hf) (λ h, not_le_of_lt ho
  (by simpa [sup_ord, hf, h] using cof_blsub_le_lift.{u} f))

theorem blsub_lt_ord {o : ordinal} {f : Π a < o, ordinal} {c : ordinal} (ho : o.card < c.cof)
  (hf : ∀ i hi, f i hi < c) : blsub.{u u} o f < c :=
blsub_lt_ord_lift (by rwa (o.card).lift_id) hf

theorem cof_bsup_le_lift {o : ordinal} {f : Π a < o, ordinal} (H : ∀ i h, f i h < bsup o f) :
  cof (bsup o f) ≤ o.card.lift :=
by { rw ←bsup_eq_blsub_iff_lt_bsup at H, rw H, exact cof_blsub_le_lift f }

theorem cof_bsup_le {o : ordinal} {f : Π a < o, ordinal} :
  (∀ i h, f i h < bsup.{u u} o f) → cof (bsup.{u u} o f) ≤ o.card :=
by { rw ←(o.card).lift_id, exact cof_bsup_le_lift }

theorem bsup_lt_ord_lift {o : ordinal} {f : Π a < o, ordinal} {c : ordinal}
  (ho : o.card.lift < c.cof) (hf : ∀ i hi, f i hi < c) : bsup.{u v} o f < c :=
(bsup_le_blsub f).trans_lt (blsub_lt_ord_lift ho hf)

theorem bsup_lt_ord {o : ordinal} {f : Π a < o, ordinal} {c : ordinal} (ho : o.card < c.cof) :
  (∀ i hi, f i hi < c) → bsup.{u u} o f < c :=
bsup_lt_ord_lift (by rwa (o.card).lift_id)

/-! ### Basic results -/

@[simp] theorem cof_zero : cof 0 = 0 :=
(cof_le_card 0).antisymm (cardinal.zero_le _)

@[simp] theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
⟨induction_on o $ λ α r _ z, by exactI
  let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_is_empty.2 $
  ⟨λ a, let ⟨b, h, _⟩ := hl a in
    (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
λ e, by simp [e]⟩

@[simp] theorem cof_succ (o) : cof (succ o) = 1 :=
begin
  apply le_antisymm,
  { refine induction_on o (λ α r _, _),
    change cof (type _) ≤ _,
    rw [← (_ : #_ = 1)], apply cof_type_le,
    { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
      rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
    { rw [cardinal.mk_fintype, set.card_singleton], simp } },
  { rw [← cardinal.succ_zero, cardinal.succ_le],
    simpa [lt_iff_le_and_ne, cardinal.zero_le] using
      λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
end

@[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
⟨induction_on o $ λ α r _ z, begin
  resetI,
  rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
  cases mk_ne_zero_iff.1 (by rw e; exact one_ne_zero) with a,
  refine ⟨typein r a, eq.symm $ quotient.sound
    ⟨rel_iso.of_surjective (rel_embedding.of_monotone _
      (λ x y, _)) (λ x, _)⟩⟩,
  { apply sum.rec; [exact subtype.val, exact λ _, a] },
  { rcases x with x|⟨⟨⟨⟩⟩⟩; rcases y with y|⟨⟨⟨⟩⟩⟩;
      simp [subrel, order.preimage, empty_relation],
    exact x.2 },
  { suffices : r x a ∨ ∃ (b : punit), ↑a = x, {simpa},
    rcases trichotomous_of r x a with h|h|h,
    { exact or.inl h },
    { exact or.inr ⟨punit.star, h.symm⟩ },
    { rcases hl x with ⟨a', aS, hn⟩,
      rw (_ : ↑a = a') at h, {exact absurd h hn},
      refine congr_arg subtype.val (_ : a = ⟨a', aS⟩),
      haveI := le_one_iff_subsingleton.1 (le_of_eq e),
      apply subsingleton.elim } }
end, λ ⟨a, e⟩, by simp [e]⟩

@[simp] theorem cof_add (a b : ordinal) : b ≠ 0 → cof (a + b) = cof b :=
induction_on a $ λ α r _, induction_on b $ λ β s _ b0, begin
  resetI,
  change cof (type _) = _,
  refine eq_of_forall_le_iff (λ c, _),
  rw [le_cof_type, le_cof_type],
  split; intros H S hS,
  { refine le_trans (H {a | sum.rec_on a (∅:set α) S} (λ a, _)) ⟨⟨_, _⟩⟩,
    { cases a with a b,
      { cases type_ne_zero_iff_nonempty.1 b0 with b,
        rcases hS b with ⟨b', bs, _⟩,
        exact ⟨sum.inr b', bs, by simp⟩ },
      { rcases hS b with ⟨b', bs, h⟩,
        exact ⟨sum.inr b', bs, by simp [h]⟩ } },
    { exact λ a, match a with ⟨sum.inr b, h⟩ := ⟨b, h⟩ end },
    { exact λ a b, match a, b with
        ⟨sum.inr a, h₁⟩, ⟨sum.inr b, h₂⟩, h := by congr; injection h
      end } },
  { refine le_trans (H (sum.inr ⁻¹' S) (λ a, _)) ⟨⟨_, _⟩⟩,
    { rcases hS (sum.inr a) with ⟨a'|b', bs, h⟩; simp at h,
      { cases h }, { exact ⟨b', bs, h⟩ } },
    { exact λ ⟨a, h⟩, ⟨_, h⟩ },
    { exact λ ⟨a, h₁⟩ ⟨b, h₂⟩ h,
        by injection h with h; congr; injection h } }
end

@[simp] theorem cof_cof (o : ordinal) : cof (cof o).ord= cof o :=
le_antisymm (le_trans (cof_le_card _) (by simp)) $
induction_on o $ λ α r _, by exactI
let ⟨S, hS, e₁⟩ := ord_cof_eq r,
    ⟨T, hT, e₂⟩ := cof_eq (subrel r S) in begin
  rw e₁ at e₂, rw ← e₂,
  refine le_trans (cof_type_le {a | ∃ h, (subtype.mk a h : S) ∈ T} (λ a, _)) ⟨⟨_, _⟩⟩,
  { rcases hS a with ⟨b, bS, br⟩,
    rcases hT ⟨b, bS⟩ with ⟨⟨c, cS⟩, cT, cs⟩,
    exact ⟨c, ⟨cS, cT⟩, is_order_connected.neg_trans cs br⟩ },
  { exact λ ⟨a, h⟩, ⟨⟨a, h.fst⟩, h.snd⟩ },
  { exact λ ⟨a, ha⟩ ⟨b, hb⟩ h,
      by injection h with h; congr; injection h },
end

theorem omega_le_cof {o} : ω ≤ cof o ↔ is_limit o :=<commit_msg>feat(set_theory/cofinality): Every ordinal has a fundamental sequence (#12317)<commit_after>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>
-/
import set_theory.cardinal_ordinal
/-!
# Cofinality

This file contains the definition of cofinality of a ordinal number and regular cardinals

## Main Definitions

* `ordinal.cof o` is the cofinality of the ordinal `o`.
  If `o` is the order type of the relation `<` on `α`, then `o.cof` is the smallest cardinality of a
  subset `s` of α that is *cofinal* in `α`, i.e. `∀ x : α, ∃ y ∈ s, ¬ y < x`.
* `cardinal.is_limit c` means that `c` is a (weak) limit cardinal: `c ≠ 0 ∧ ∀ x < c, succ x < c`.
* `cardinal.is_strong_limit c` means that `c` is a strong limit cardinal:
  `c ≠ 0 ∧ ∀ x < c, 2 ^ x < c`.
* `cardinal.is_regular c` means that `c` is a regular cardinal: `ω ≤ c ∧ c.ord.cof = c`.
* `cardinal.is_inaccessible c` means that `c` is strongly inaccessible:
  `ω < c ∧ is_regular c ∧ is_strong_limit c`.

## Main Statements

* `ordinal.infinite_pigeonhole_card`: the infinite pigeonhole principle
* `cardinal.lt_power_cof`: A consequence of König's theorem stating that `c < c ^ c.ord.cof` for
  `c ≥ ω`
* `cardinal.univ_inaccessible`: The type of ordinals in `Type u` form an inaccessible cardinal
  (in `Type v` with `v > u`). This shows (externally) that in `Type u` there are at least `u`
  inaccessible cardinals.

## Implementation Notes

* The cofinality is defined for ordinals.
  If `c` is a cardinal number, its cofinality is `c.ord.cof`.

## Tags

cofinality, regular cardinals, limits cardinals, inaccessible cardinals,
infinite pigeonhole principle


-/
noncomputable theory

open function cardinal set
open_locale classical cardinal

universes u v w
variables {α : Type*} {r : α → α → Prop}

/-! ### Cofinality of orders -/

namespace order
/-- Cofinality of a reflexive order `≼`. This is the smallest cardinality
  of a subset `S : set α` such that `∀ a, ∃ b ∈ S, a ≼ b`. -/
def cof (r : α → α → Prop) [is_refl α r] : cardinal :=
@cardinal.min {S : set α // ∀ a, ∃ b ∈ S, r a b}
  ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
  (λ S, #S)

lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) :
  order.cof r ≤ #S :=
le_trans (cardinal.min_le _ ⟨S, h⟩) le_rfl

lemma le_cof {r : α → α → Prop} [is_refl α r] (c : cardinal) :
  c ≤ order.cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ #S :=
by { rw [order.cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }

end order

theorem rel_iso.cof.aux {α : Type u} {β : Type v} {r s}
  [is_refl α r] [is_refl β s] (f : r ≃r s) :
  cardinal.lift.{(max u v)} (order.cof r) ≤
  cardinal.lift.{(max u v)} (order.cof s) :=
begin
  rw [order.cof, order.cof, lift_min, lift_min, cardinal.le_min],
  intro S, cases S with S H, simp only [comp, coe_sort_coe_base, subtype.coe_mk],
  refine le_trans (min_le _ _) _,
  { exact ⟨f ⁻¹' S, λ a,
    let ⟨b, bS, h⟩ := H (f a) in ⟨f.symm b, by simp [bS, ← f.map_rel_iff, h,
      -coe_fn_coe_base, -coe_fn_coe_trans, principal_seg.coe_coe_fn', initial_seg.coe_coe_fn]⟩⟩ },
  { exact lift_mk_le.{u v (max u v)}.2
    ⟨⟨λ ⟨x, h⟩, ⟨f x, h⟩, λ ⟨x, h₁⟩ ⟨y, h₂⟩ h₃,
      by congr; injection h₃ with h'; exact f.to_equiv.injective h'⟩⟩ }
end

theorem rel_iso.cof {α : Type u} {β : Type v} {r s}
  [is_refl α r] [is_refl β s] (f : r ≃r s) :
  cardinal.lift.{(max u v)} (order.cof r) =
  cardinal.lift.{(max u v)} (order.cof s) :=
le_antisymm (rel_iso.cof.aux f) (rel_iso.cof.aux f.symm)

def strict_order.cof (r : α → α → Prop) [h : is_irrefl α r] : cardinal :=
@order.cof α (λ x y, ¬ r y x) ⟨h.1⟩

/-! ### Cofinality of ordinals -/

namespace ordinal

/-- Cofinality of an ordinal. This is the smallest cardinal of a
  subset `S` of the ordinal which is unbounded, in the sense
  `∀ a, ∃ b ∈ S, a ≤ b`. It is defined for all ordinals, but
  `cof 0 = 0` and `cof (succ o) = 1`, so it is only really
  interesting on limit ordinals (when it is an infinite cardinal). -/
def cof (o : ordinal.{u}) : cardinal.{u} :=
quot.lift_on o (λ a, by exactI strict_order.cof a.r)
begin
  rintros ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩,
  rw ← cardinal.lift_inj,
  apply rel_iso.cof ⟨f, _⟩,
  simp [hf]
end

lemma cof_type (r : α → α → Prop) [is_well_order α r] : (type r).cof = strict_order.cof r := rfl

theorem le_cof_type [is_well_order α r] {c} : c ≤ cof (type r) ↔
  ∀ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) → c ≤ #S :=
by dsimp [cof, strict_order.cof, order.cof, type, quotient.mk, quot.lift_on];
   rw [cardinal.le_min, subtype.forall]; refl

theorem cof_type_le [is_well_order α r] (S : set α) (h : ∀ a, ∃ b ∈ S, ¬ r b a) :
  cof (type r) ≤ #S :=
le_cof_type.1 le_rfl S h

theorem lt_cof_type [is_well_order α r] (S : set α) (hl : #S < cof (type r)) :
  ∃ a, ∀ b ∈ S, r b a :=
not_forall_not.1 $ λ h, not_le_of_lt hl $ cof_type_le S (λ a, not_ball.1 (h a))

theorem cof_eq (r : α → α → Prop) [is_well_order α r] :
  ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ #S = cof (type r) :=
begin
  have : ∃ i, cof (type r) = _,
  { dsimp [cof, order.cof, type, quotient.mk, quot.lift_on],
    apply cardinal.min_eq },
  exact let ⟨⟨S, hl⟩, e⟩ := this in ⟨S, hl, e.symm⟩,
end

theorem ord_cof_eq (r : α → α → Prop) [is_well_order α r] :
  ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ type (subrel r S) = (cof (type r)).ord :=
let ⟨S, hS, e⟩ := cof_eq r, ⟨s, _, e'⟩ := cardinal.ord_eq S,
    T : set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a} in
begin
  resetI, suffices,
  { refine ⟨T, this,
      le_antisymm _ (cardinal.ord_le.2 $ cof_type_le T this)⟩,
    rw [← e, e'],
    refine type_le'.2 ⟨rel_embedding.of_monotone
      (λ a, ⟨a, let ⟨aS, _⟩ := a.2 in aS⟩) (λ a b h, _)⟩,
    rcases a with ⟨a, aS, ha⟩, rcases b with ⟨b, bS, hb⟩,
    change s ⟨a, _⟩ ⟨b, _⟩,
    refine ((trichotomous_of s _ _).resolve_left (λ hn, _)).resolve_left _,
    { exact asymm h (ha _ hn) },
    { intro e, injection e with e, subst b,
      exact irrefl _ h } },
  { intro a,
    have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
    let b := (is_well_order.wf).min _ this,
    have ba : ¬r b a := (is_well_order.wf).min_mem _ this,
    refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
    rw [show ∀b:S, (⟨b, b.2⟩:S) = b, by intro b; cases b; refl],
    exact (is_well_order.wf).not_lt_min _ this
      (is_order_connected.neg_trans h ba) }
end

/-! ### Cofinality of suprema and least strict upper bounds -/

private theorem card_mem_cof {o} : ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = o.card :=
⟨_, _, lsub_typein o, mk_ordinal_out o⟩

/-- The set in the `lsub` characterization of `cof` is nonempty. -/
theorem cof_lsub_def_nonempty (o) :
  {a : cardinal | ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = a}.nonempty :=
⟨_, card_mem_cof⟩

theorem cof_eq_Inf_lsub (o : ordinal.{u}) :
  cof o = Inf {a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = a} :=
begin
  refine le_antisymm (le_cInf (cof_lsub_def_nonempty o) _) (cInf_le' _),
  { rintros a ⟨ι, f, hf, rfl⟩,
    rw ←type_lt o,
    refine (cof_type_le _ (λ a, _)).trans (@mk_le_of_injective _ _
      (λ s : (typein ((<) : o.out.α → o.out.α → Prop))⁻¹' (set.range f), classical.some s.prop)
      (λ s t hst, let H := congr_arg f hst in by rwa [classical.some_spec s.prop,
        classical.some_spec t.prop, typein_inj, subtype.coe_inj] at H)),
    have := typein_lt_self a,
    simp_rw [←hf, lt_lsub_iff] at this,
    cases this with i hi,
    refine ⟨enum (<) (f i) _, _, _⟩,
    { rw [type_lt, ←hf], apply lt_lsub },
    { rw [mem_preimage, typein_enum], exact mem_range_self i },
    { rwa [←typein_le_typein, typein_enum] } },
  { rcases cof_eq (<) with ⟨S, hS, hS'⟩,
    let f : S → ordinal := λ s, typein (<) s.val,
    refine ⟨S, f, le_antisymm (lsub_le (λ i, typein_lt_self i)) (le_of_forall_lt (λ a ha, _)),
      by rwa type_lt o at hS'⟩,
    rw ←type_lt o at ha,
    rcases hS (enum (<) a ha) with ⟨b, hb, hb'⟩,
    rw [←typein_le_typein, typein_enum] at hb',
    exact hb'.trans_lt (lt_lsub.{u u} f ⟨b, hb⟩) }
end

theorem lift_cof (o) : (cof o).lift = cof o.lift :=
induction_on o $ begin introsI α r _,
  cases lift_type r with _ e, rw e,
  apply le_antisymm,
  { unfreezingI { refine le_cof_type.2 (λ S H, _) },
    have : (#(ulift.up ⁻¹' S)).lift ≤ #S :=
     ⟨⟨λ ⟨⟨x, h⟩⟩, ⟨⟨x⟩, h⟩,
       λ ⟨⟨x, h₁⟩⟩ ⟨⟨y, h₂⟩⟩ e, by simp at e; congr; injection e⟩⟩,
    refine le_trans (cardinal.lift_le.2 $ cof_type_le _ _) this,
    exact λ a, let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩ in ⟨b, bs, br⟩ },
  { rcases cof_eq r with ⟨S, H, e'⟩,
    have : #(ulift.down ⁻¹' S) ≤ (#S).lift :=
     ⟨⟨λ ⟨⟨x⟩, h⟩, ⟨⟨x, h⟩⟩,
       λ ⟨⟨x⟩, h₁⟩ ⟨⟨y⟩, h₂⟩ e, by simp at e; congr; injections⟩⟩,
    rw e' at this,
    unfreezingI { refine le_trans (cof_type_le _ _) this },
    exact λ ⟨a⟩, let ⟨b, bs, br⟩ := H a in ⟨⟨b⟩, bs, br⟩ }
end

theorem cof_le_card (o) : cof o ≤ card o :=
by { rw cof_eq_Inf_lsub, exact cInf_le' card_mem_cof }

theorem cof_ord_le (c : cardinal) : cof c.ord ≤ c :=
by simpa using cof_le_card c.ord

theorem ord_cof_le (o : ordinal.{u}) : o.cof.ord ≤ o :=
(ord_le_ord.2 (cof_le_card o)).trans (ord_card_le o)

theorem exists_lsub_cof (o : ordinal) : ∃ {ι} (f : ι → ordinal), lsub.{u u} f = o ∧ #ι = cof o :=
by { rw cof_eq_Inf_lsub, exact Inf_mem (cof_lsub_def_nonempty o) }

theorem cof_lsub_le {ι} (f : ι → ordinal) : cof (lsub.{u u} f) ≤ #ι :=
by { rw cof_eq_Inf_lsub, exact cInf_le' ⟨ι, f, rfl, rfl⟩ }

theorem cof_lsub_le_lift {ι} (f : ι → ordinal) : cof (lsub f) ≤ cardinal.lift.{v u} (#ι) :=
begin
  rw ←mk_ulift,
  convert cof_lsub_le (λ i : ulift ι, f i.down),
  exact lsub_eq_of_range_eq.{u (max u v) max u v}
    (set.ext (λ x, ⟨λ ⟨i, hi⟩, ⟨ulift.up i, hi⟩, λ ⟨i, hi⟩, ⟨_, hi⟩⟩))
end

theorem le_cof_iff_lsub {o : ordinal} {a : cardinal} :
  a ≤ cof o ↔ ∀ {ι} (f : ι → ordinal), lsub.{u u} f = o → a ≤ #ι :=
begin
  rw cof_eq_Inf_lsub,
  exact (le_cInf_iff'' (cof_lsub_def_nonempty o)).trans ⟨λ H ι f hf, H _ ⟨ι, f, hf, rfl⟩,
    λ H b ⟨ι, f, hf, hb⟩, ( by { rw ←hb, exact H _ hf} )⟩
end

theorem lsub_lt_ord_lift {ι} {f : ι → ordinal} {c : ordinal} (hι : cardinal.lift (#ι) < c.cof)
  (hf : ∀ i, f i < c) : lsub.{u v} f < c :=
lt_of_le_of_ne (lsub_le hf) (λ h, by { subst h, exact (cof_lsub_le_lift f).not_lt hι })

theorem lsub_lt_ord {ι} {f : ι → ordinal} {c : ordinal} (hι : #ι < c.cof) :
  (∀ i, f i < c) → lsub.{u u} f < c :=
lsub_lt_ord_lift (by rwa (#ι).lift_id)

theorem cof_sup_le_lift {ι} {f : ι → ordinal} (H : ∀ i, f i < sup f) : cof (sup f) ≤ (#ι).lift :=
by { rw ←sup_eq_lsub_iff_lt_sup at H, rw H, exact cof_lsub_le_lift f }

theorem cof_sup_le {ι} {f : ι → ordinal} (H : ∀ i, f i < sup.{u u} f) : cof (sup.{u u} f) ≤ #ι :=
by { rw ←(#ι).lift_id, exact cof_sup_le_lift H }

theorem sup_lt_ord_lift {ι} {f : ι → ordinal} {c : ordinal} (hι : cardinal.lift (#ι) < c.cof)
  (hf : ∀ i, f i < c) : sup.{u v} f < c :=
(sup_le_lsub.{u v} f).trans_lt (lsub_lt_ord_lift hι hf)

theorem sup_lt_ord {ι} {f : ι → ordinal} {c : ordinal} (hι : #ι < c.cof) :
  (∀ i, f i < c) → sup.{u u} f < c :=
sup_lt_ord_lift (by rwa (#ι).lift_id)

theorem sup_lt_lift {ι} {f : ι → cardinal} {c : cardinal} (hι : cardinal.lift (#ι) < c.ord.cof)
  (hf : ∀ i, f i < c) : cardinal.sup.{u v} f < c :=
by { rw [←ord_lt_ord, ←sup_ord], refine sup_lt_ord_lift hι (λ i, _), rw ord_lt_ord, apply hf }

theorem sup_lt {ι} {f : ι → cardinal} {c : cardinal} (hι : #ι < c.ord.cof) :
  (∀ i, f i < c) → cardinal.sup.{u u} f < c :=
sup_lt_lift (by rwa (#ι).lift_id)

theorem exists_blsub_cof (o : ordinal) : ∃ (f : Π a < (cof o).ord, ordinal), blsub.{u u} _ f = o :=
begin
  rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩,
  rcases cardinal.ord_eq ι with ⟨r, hr, hι'⟩,
  rw ←@blsub_eq_lsub' ι r hr at hf,
  rw [←hι, hι'],
  exact ⟨_, hf⟩
end

theorem le_cof_iff_blsub {b : ordinal} {a : cardinal} :
  a ≤ cof b ↔ ∀ {o} (f : Π a < o, ordinal), blsub.{u u} o f = b → a ≤ o.card :=
le_cof_iff_lsub.trans ⟨λ H o f hf, by simpa using H _ hf, λ H ι f hf, begin
  rcases cardinal.ord_eq ι with ⟨r, hr, hι'⟩,
  rw ←@blsub_eq_lsub' ι r hr at hf,
  simpa using H _ hf
end⟩

theorem cof_blsub_le_lift {o} (f : Π a < o, ordinal) :
  cof (blsub o f) ≤ cardinal.lift.{v u} (o.card) :=
by { convert cof_lsub_le_lift _, exact (mk_ordinal_out o).symm }

theorem cof_blsub_le {o} (f : Π a < o, ordinal) : cof (blsub.{u u} o f) ≤ o.card :=
by { rw ←(o.card).lift_id, exact cof_blsub_le_lift f }

theorem blsub_lt_ord_lift {o : ordinal} {f : Π a < o, ordinal} {c : ordinal}
  (ho : o.card.lift < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u v} o f < c :=
lt_of_le_of_ne (blsub_le hf) (λ h, not_le_of_lt ho
  (by simpa [sup_ord, hf, h] using cof_blsub_le_lift.{u} f))

theorem blsub_lt_ord {o : ordinal} {f : Π a < o, ordinal} {c : ordinal} (ho : o.card < c.cof)
  (hf : ∀ i hi, f i hi < c) : blsub.{u u} o f < c :=
blsub_lt_ord_lift (by rwa (o.card).lift_id) hf

theorem cof_bsup_le_lift {o : ordinal} {f : Π a < o, ordinal} (H : ∀ i h, f i h < bsup o f) :
  cof (bsup o f) ≤ o.card.lift :=
by { rw ←bsup_eq_blsub_iff_lt_bsup at H, rw H, exact cof_blsub_le_lift f }

theorem cof_bsup_le {o : ordinal} {f : Π a < o, ordinal} :
  (∀ i h, f i h < bsup.{u u} o f) → cof (bsup.{u u} o f) ≤ o.card :=
by { rw ←(o.card).lift_id, exact cof_bsup_le_lift }

theorem bsup_lt_ord_lift {o : ordinal} {f : Π a < o, ordinal} {c : ordinal}
  (ho : o.card.lift < c.cof) (hf : ∀ i hi, f i hi < c) : bsup.{u v} o f < c :=
(bsup_le_blsub f).trans_lt (blsub_lt_ord_lift ho hf)

theorem bsup_lt_ord {o : ordinal} {f : Π a < o, ordinal} {c : ordinal} (ho : o.card < c.cof) :
  (∀ i hi, f i hi < c) → bsup.{u u} o f < c :=
bsup_lt_ord_lift (by rwa (o.card).lift_id)

/-! ### Basic results -/

@[simp] theorem cof_zero : cof 0 = 0 :=
(cof_le_card 0).antisymm (cardinal.zero_le _)

@[simp] theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
⟨induction_on o $ λ α r _ z, by exactI
  let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_is_empty.2 $
  ⟨λ a, let ⟨b, h, _⟩ := hl a in
    (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
λ e, by simp [e]⟩

@[simp] theorem cof_succ (o) : cof (succ o) = 1 :=
begin
  apply le_antisymm,
  { refine induction_on o (λ α r _, _),
    change cof (type _) ≤ _,
    rw [← (_ : #_ = 1)], apply cof_type_le,
    { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
      rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
    { rw [cardinal.mk_fintype, set.card_singleton], simp } },
  { rw [← cardinal.succ_zero, cardinal.succ_le],
    simpa [lt_iff_le_and_ne, cardinal.zero_le] using
      λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
end

@[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
⟨induction_on o $ λ α r _ z, begin
  resetI,
  rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
  cases mk_ne_zero_iff.1 (by rw e; exact one_ne_zero) with a,
  refine ⟨typein r a, eq.symm $ quotient.sound
    ⟨rel_iso.of_surjective (rel_embedding.of_monotone _
      (λ x y, _)) (λ x, _)⟩⟩,
  { apply sum.rec; [exact subtype.val, exact λ _, a] },
  { rcases x with x|⟨⟨⟨⟩⟩⟩; rcases y with y|⟨⟨⟨⟩⟩⟩;
      simp [subrel, order.preimage, empty_relation],
    exact x.2 },
  { suffices : r x a ∨ ∃ (b : punit), ↑a = x, {simpa},
    rcases trichotomous_of r x a with h|h|h,
    { exact or.inl h },
    { exact or.inr ⟨punit.star, h.symm⟩ },
    { rcases hl x with ⟨a', aS, hn⟩,
      rw (_ : ↑a = a') at h, {exact absurd h hn},
      refine congr_arg subtype.val (_ : a = ⟨a', aS⟩),
      haveI := le_one_iff_subsingleton.1 (le_of_eq e),
      apply subsingleton.elim } }
end, λ ⟨a, e⟩, by simp [e]⟩

@[simp] theorem cof_add (a b : ordinal) : b ≠ 0 → cof (a + b) = cof b :=
induction_on a $ λ α r _, induction_on b $ λ β s _ b0, begin
  resetI,
  change cof (type _) = _,
  refine eq_of_forall_le_iff (λ c, _),
  rw [le_cof_type, le_cof_type],
  split; intros H S hS,
  { refine le_trans (H {a | sum.rec_on a (∅:set α) S} (λ a, _)) ⟨⟨_, _⟩⟩,
    { cases a with a b,
      { cases type_ne_zero_iff_nonempty.1 b0 with b,
        rcases hS b with ⟨b', bs, _⟩,
        exact ⟨sum.inr b', bs, by simp⟩ },
      { rcases hS b with ⟨b', bs, h⟩,
        exact ⟨sum.inr b', bs, by simp [h]⟩ } },
    { exact λ a, match a with ⟨sum.inr b, h⟩ := ⟨b, h⟩ end },
    { exact λ a b, match a, b with
        ⟨sum.inr a, h₁⟩, ⟨sum.inr b, h₂⟩, h := by congr; injection h
      end } },
  { refine le_trans (H (sum.inr ⁻¹' S) (λ a, _)) ⟨⟨_, _⟩⟩,
    { rcases hS (sum.inr a) with ⟨a'|b', bs, h⟩; simp at h,
      { cases h }, { exact ⟨b', bs, h⟩ } },
    { exact λ ⟨a, h⟩, ⟨_, h⟩ },
    { exact λ ⟨a, h₁⟩ ⟨b, h₂⟩ h,
        by injection h with h; congr; injection h } }
end

/-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
    `a`. We provide `o` explicitly in order to avoid type rewrites. -/
def is_fundamental_sequence (a o : ordinal.{u}) (f : Π b < o, ordinal.{u}) : Prop :=
o ≤ a.cof.ord ∧ (∀ {i j} (hi hj), i < j → f i hi < f j hj) ∧ blsub.{u u} o f = a

section fundamental_sequence
variables {a o : ordinal.{u}} {f : Π b < o, ordinal.{u}} (hf : is_fundamental_sequence a o f)

theorem is_fundamental_sequence.cof_eq : a.cof.ord = o :=
hf.1.antisymm' (by { rw ←hf.2.2, exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o) })

theorem is_fundamental_sequence.strict_mono :
  ∀ {i j : ordinal} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj :=
hf.2.1

theorem is_fundamental_sequence.blsub_eq : blsub.{u u} o f = a :=
hf.2.2

include hf
theorem is_fundamental_sequence.monotone {i j : ordinal} (hi : i < o) (hj : j < o) (hij : i ≤ j) :
  f i hi ≤ f j hj :=
begin
  rcases lt_or_eq_of_le hij with hij | rfl,
  { exact le_of_lt (hf.2.1 hi hj hij) },
  { refl }
end

end fundamental_sequence

theorem is_fundamental_sequence.trans {a o o' : ordinal.{u}} {f : Π b < o, ordinal.{u}}
  (hf : is_fundamental_sequence a o f) {g : Π b < o', ordinal.{u}}
  (hg : is_fundamental_sequence o o' g) :
  is_fundamental_sequence a o' (λ i hi, f (g i hi) (by { rw ←hg.2.2, apply lt_blsub })) :=
begin
  refine ⟨_, λ i j _ _ h, hf.2.1 _ _ (hg.2.1 _ _ h), _⟩,
  { rw hf.cof_eq,
    exact hg.1.trans (ord_cof_le o) },
  { rw @blsub_comp.{u u u} o _ f (@is_fundamental_sequence.monotone _ _ f hf),
    exact hf.2.2 }
end

/-- Every ordinal has a fundamental sequence. -/
theorem exists_fundamental_sequence (a : ordinal.{u}) :
  ∃ f, is_fundamental_sequence a a.cof.ord f :=
begin
  suffices : ∃ o f, is_fundamental_sequence a o f,
  { rcases this with ⟨o, f, hf⟩,
    convert exists.intro f hf;
    rw hf.cof_eq },
  rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩,
  rcases ord_eq ι with ⟨r, wo, hr⟩,
  haveI := wo,
  let r' := subrel r {i | ∀ j, r j i → f j < f i},
  let hrr' : r' ↪r r := subrel.rel_embedding _ _,
  haveI := hrr'.is_well_order,
  refine ⟨_, _, (type_le'.2 ⟨hrr'⟩).trans _, λ i j _ h _, (enum r' j h).prop _ _,
    le_antisymm (blsub_le (λ i hi, lsub_le_iff.1 hf.le _)) _⟩,
  { rw [←hι, hr] },
  { change r (hrr'.1 _ ) (hrr'.1 _ ),
    rwa [hrr'.2, @enum_lt_enum _ r'] },
  { rw [←hf, lsub_le_iff],
    intro i,
    suffices : ∃ i' hi', f i ≤ bfamily_of_family' r' (λ i, f i) i' hi',
    { rcases this with ⟨i', hi', hfg⟩,
      exact hfg.trans_lt (lt_blsub _ _ _) },
    by_cases h : ∀ j, r j i → f j < f i,
    { refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, _⟩,
      rw bfamily_of_family'_typein,
      refl },
    { push_neg at h,
      cases wo.wf.min_mem _ h with hji hij,
      refine ⟨typein r' ⟨_, λ k hkj, lt_of_lt_of_le _ hij⟩, typein_lt_type _ _, _⟩,
      { by_contra' H,
        exact (wo.wf.not_lt_min _ h ⟨is_trans.trans _ _ _ hkj hji, H⟩) hkj },
      { rwa bfamily_of_family'_typein } } }
end

@[simp] theorem cof_cof (a : ordinal.{u}) : cof (cof a).ord = cof a :=
begin
  cases exists_fundamental_sequence a with f hf,
  cases exists_fundamental_sequence a.cof.ord with g hg,
  exact ord_injective ((hf.trans hg).cof_eq.symm)
end

theorem omega_le_cof {o} : ω ≤ cof o ↔ is_limit o :=
{'fraction_non_alphanumeric': 0.16839748604105415, 'fraction_numerical': 0.0031559355865454644, 'mean_word_length': 2.937758895379713, 'pattern_counts': {'":': 0, '<': 139, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5084784', 'n_tokens_mistral': 18428, 'n_tokens_neox': 18179, 'n_words': 5813}