-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
  ⟨inductionOn o fun α r _ z => by
      rcases cof_eq r with ⟨S, hl, e⟩; rw [z] at e
      obtain ⟨a⟩ := mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero)
      refine
        ⟨typein r a,
          Eq.symm <|
            Quotient.sound
              ⟨RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ fun x y => ?_) fun x => ?_⟩⟩
      · apply Sum.rec <;> [exact Subtype.val; exact fun _ => a]
      · rcases x with (x | ⟨⟨⟨⟩⟩⟩) <;> rcases y with (y | ⟨⟨⟨⟩⟩⟩) <;>
          simp [Subrel, Order.Preimage, EmptyRelation]
        exact x.2
      · suffices r x a ∨ ∃ _ : PUnit.{u}, ↑a = x by
          convert this
          dsimp [RelEmbedding.ofMonotone]; simp
        rcases trichotomous_of r x a with (h | h | h)
        · exact Or.inl h
        · exact Or.inr ⟨PUnit.unit, h.symm⟩
        · rcases hl x with ⟨a', aS, hn⟩
          refine absurd h ?_
          convert hn
          change (a : α) = ↑(⟨a', aS⟩ : S)
          have := le_one_iff_subsingleton.1 (le_of_eq e)
          congr!,
    fun ⟨a, e⟩ => by simp [e]⟩

Proof state:
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
⊢ #?m.47881 ≠ 0

Tactic:
rw [e]

Result:
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
⊢ 1 ≠ 0

Proof state:
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
⊢ ∃ a, type r = succ a

Tactic:
rcases cof_eq r with ⟨S, hl, e⟩

Result:
case intro.intro
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = (type r).cof
⊢ ∃ a, type r = succ a

Proof state:
case a
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1, (RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a) ⋯) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
dsimp [RelEmbedding.ofMonotone]

Result:
case a
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1, Sum.rec Subtype.val (fun x => ↑a) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x

Proof state:
case intro.intro.intro.refine_3.inr.inr.intro.intro
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ ¬r (↑a) x

Tactic:
convert hn

Result:
case h.e'_1.h.e'_1
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ ↑a = a'

Proof state:
case intro.intro.intro.refine_3.inl
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : r x ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
⊢ { x // r x ↑a } ⊕ PUnit.{u + 1} → α

Tactic:
apply Sum.rec <;> [exact Subtype.val; exact fun _ => a]

Result:
no goals

Proof state:
case intro.intro.intro.refine_3.inr.inl
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : x = ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
exact Or.inr ⟨PUnit.unit, h.symm⟩

Result:
no goals

Proof state:
case intro.intro
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = (type r).cof
⊢ ∃ a, type r = succ a

Tactic:
rw [z] at e

Result:
case intro.intro
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
⊢ ∃ a, type r = succ a

Proof state:
o : Ordinal.{u}
x✝ : ∃ a, o = succ a
a : Ordinal.{u}
e : o = succ a
⊢ o.cof = 1

Tactic:
simp [e]

Result:
no goals

Proof state:
case intro.intro.intro.refine_3.inr.inr
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : r (↑a) x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
rcases hl x with ⟨a', aS, hn⟩

Result:
case intro.intro.intro.refine_3.inr.inr.intro.intro
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

Proof state:
case intro.intro.intro.refine_2.inl.inr.unit
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : (type r).cof = 1
S : Set α
hl : Unbounded r S
e : #↑S = 1
a : ↑S
x : { x // r x ↑a }
⊢ r ↑x ↑a

Tactic:
exact x.2

Result:
no goals