-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} :=
  le_antisymm (cof_le_card _)
    (by
      refine le_of_forall_lt fun c h => ?_
      rcases lt_univ'.1 h with ⟨c, rfl⟩
      rcases @cof_eq Ordinal.{u} (· < ·) _ with ⟨S, H, Se⟩
      rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]
      refine lt_of_not_ge fun h => ?_
      obtain ⟨a, e⟩ := Cardinal.mem_range_lift_of_le h
      refine Quotient.inductionOn a (fun α e => ?_) e
      obtain ⟨f⟩ := Quotient.exact e
      have f := Equiv.ulift.symm.trans f
      let g a := (f a).1
      let o := succ (iSup g)
      rcases H o with ⟨b, h, l⟩
      refine l (lt_succ_iff.2 ?_)
      rw [← show g (f.symm ⟨b, h⟩) = b by simp [g]]
      apply Ordinal.le_iSup)

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
⊢ False

Tactic:
obtain ⟨f⟩ := Quotient.exact e

Result:
case intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f : ULift.{u + 1, u} α ≃ ↑S
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
b : Ordinal.{u}
h : b ∈ S
l : ¬(fun x1 x2 => x1 < x2) b o
⊢ b ≤ iSup g

Tactic:
rw [← show g (f.symm ⟨b, h⟩) = b by simp [g]]

Result:
case intro.intro.intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
b : Ordinal.{u}
h : b ∈ S
l : ¬(fun x1 x2 => x1 < x2) b o
⊢ g (f.symm ⟨b, h⟩) ≤ iSup g

Proof state:
case intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
⊢ False

Tactic:
let o := succ (iSup g)

Result:
case intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
⊢ False

Proof state:
case intro.intro.intro
c : Cardinal.{u}
h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
⊢ Cardinal.lift.{u + 1, u} c < #↑S

Tactic:
refine lt_of_not_ge fun h => ?_

Result:
case intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
⊢ False

Proof state:
case intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
⊢ False

Tactic:
rcases H o with ⟨b, h, l⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
b : Ordinal.{u}
h : b ∈ S
l : ¬(fun x1 x2 => x1 < x2) b o
⊢ False

Proof state:
case intro.intro.intro
c : Cardinal.{u}
h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
⊢ Cardinal.lift.{max (u + 1) v, u} c < univ.{u, v}.cof

Tactic:
rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]

Result:
case intro.intro.intro
c : Cardinal.{u}
h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
⊢ Cardinal.lift.{u + 1, u} c < #↑S

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e : Cardinal.lift.{u + 1, u} a = #↑S
⊢ False

Tactic:
refine Quotient.inductionOn a (fun α e => ?_) e

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
⊢ False

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < Cardinal.univ.{u, v}
⊢ c < univ.{u, v}.cof

Tactic:
rcases lt_univ'.1 h with ⟨c, rfl⟩

Result:
case intro
c : Cardinal.{u}
h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
⊢ Cardinal.lift.{max (u + 1) v, u} c < univ.{u, v}.cof

Proof state:
⊢ Cardinal.univ.{u, v} ≤ univ.{u, v}.cof

Tactic:
refine le_of_forall_lt fun c h => ?_

Result:
c : Cardinal.{max (u + 1) v}
h : c < Cardinal.univ.{u, v}
⊢ c < univ.{u, v}.cof

Proof state:
case intro.intro.intro.intro.intro.intro.intro
c : Cardinal.{u}
h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
S : Set Ordinal.{u}
H : Unbounded (fun x1 x2 => x1 < x2) S
Se : #↑S = (type fun x1 x2 => x1 < x2).cof
h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S
a : Cardinal.{u}
e✝ : Cardinal.lift.{u + 1, u} a = #↑S
α : Type u
e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S
f✝ : ULift.{u + 1, u} α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal.{u} := fun a => ↑(f a)
o : Ordinal.{u} := succ (iSup g)
b : Ordinal.{u}
h : b ∈ S
l : ¬(fun x1 x2 => x1 < x2) b o
⊢ g (f.symm ⟨b, h⟩) ≤ iSup g

Tactic:
apply Ordinal.le_iSup

Result:
no goals