-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
    sInf { a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a }

Proof state:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
let f : S → Ordinal := fun s => typein LT.lt s.val

Result:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ f i ∈ Iio (lsub f)

Tactic:
apply lt_lsub

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
⊢ ∀ b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}, o.cof ≤ b

Tactic:
rintro a ⟨ι, f, hf, rfl⟩

Result:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ o.cof ≤ #ι

Proof state:
o : Ordinal.{u}
⊢ o.cof = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)

Result:
case refine_1
o : Ordinal.{u}
⊢ ∀ b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}, o.cof ≤ b

case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ f i ∈ range f

Tactic:
exact mem_range_self i

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ (enum fun x1 x2 => x1 < x2) ⟨f i, ⋯⟩ ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f

Tactic:
rw [mem_preimage, typein_enum]

Result:
case refine_1.intro.intro.intro.intro.refine_2
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ f i ∈ range f

Proof state:
case refine_2.intro.intro.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < type fun x1 x2 => x1 < x2
b : o.toType
hb : b ∈ S
hb' : ¬(fun x1 x2 => x1 < x2) b ((enum fun x1 x2 => x1 < x2) ⟨a, ha⟩)
⊢ a < lsub f

Tactic:
rw [← typein_le_typein, typein_enum] at hb'

Result:
case refine_2.intro.intro.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < type fun x1 x2 => x1 < x2
b : o.toType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f

Proof state:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
s t : ↑(⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f)
hst : (fun s => Classical.choose ⋯) s = (fun s => Classical.choose ⋯) t
⊢ s = t

Tactic:
let H := congr_arg f hst

Result:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
s t : ↑(⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f)
hst : (fun s => Classical.choose ⋯) s = (fun s => Classical.choose ⋯) t
H : f ((fun s => Classical.choose ⋯) s) = f ((fun s => Classical.choose ⋯) t) := congr_arg f hst
⊢ s = t

Proof state:
case refine_1.intro.intro.intro.intro.refine_3
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ ¬(enum fun x1 x2 => x1 < x2) ⟨f i, ⋯⟩ < a

Tactic:
rwa [← typein_le_typein, typein_enum]

Result:
no goals

Proof state:
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
⊢ #↑S = o.cof

Tactic:
rwa [type_toType o] at hS'

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ f i ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
rw [type_toType, ← hf]

Result:
case refine_1.intro.intro.intro.intro.refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ f i ∈ Iio (lsub f)

Proof state:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ o.cof ≤ #ι

Tactic:
rw [← type_toType o]

Result:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ (type fun x1 x2 => x1 < x2).cof ≤ #ι

Proof state:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
this : ∃ i, (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a

Tactic:
obtain ⟨i, hi⟩ := this

Result:
case refine_1.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
i : ι
hi : (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a

Proof state:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < o
⊢ a < lsub f

Tactic:
rw [← type_toType o] at ha

Result:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < type fun x1 x2 => x1 < x2
⊢ a < lsub f

Proof state:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
s t : ↑(⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f)
hst : (fun s => Classical.choose ⋯) s = (fun s => Classical.choose ⋯) t
H : f ((fun s => Classical.choose ⋯) s) = f ((fun s => Classical.choose ⋯) t) := congr_arg f hst
⊢ s = t

Tactic:
rwa [Classical.choose_spec s.prop, Classical.choose_spec t.prop, typein_inj,
  Subtype.coe_inj] at H

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < type fun x1 x2 => x1 < x2
b : o.toType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f

Tactic:
exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
this : (typein fun x1 x2 => x1 < x2).toRelEmbedding a < o
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a

Tactic:
simp_rw [← hf, lt_lsub_iff] at this

Result:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
this : ∃ i, (typein fun x1 x2 => x1 < x2).toRelEmbedding a ≤ f i
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a