-- 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:
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

Tactic:
obtain ⟨a⟩ := mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero)

Result:
case intro.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
⊢ ∃ a, type r = succ a

Proof state:
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', aS⟩

Tactic:
have := le_one_iff_subsingleton.1 (le_of_eq e)

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
this : Subsingleton ↑S
⊢ ↑a = ↑⟨a', aS⟩

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
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

Tactic:
convert this

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, (RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a) ⋯) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x

Proof state:
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
this : Subsingleton ↑S
⊢ ↑a = ↑⟨a', aS⟩

Tactic:
congr!

Result:
no goals

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, Sum.rec Subtype.val (fun x => ↑a) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
simp

Result:
no goals

Proof state:
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'

Tactic:
change (a : α) = ↑(⟨a', aS⟩ : S)

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', aS⟩

Proof state:
case intro.intro.intro.refine_3
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 ∨ ∃ x_1, ↑a = x

Tactic:
rcases trichotomous_of r x a with (h | h | h)

Result:
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

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

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

Proof state:
case intro.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
⊢ ∃ a, type r = succ a

Tactic:
refine
  ⟨typein r a,
    Eq.symm <|
      Quotient.sound
        ⟨RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ fun x y => ?_) fun x => ?_⟩⟩

Result:
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} → α

case intro.intro.intro.refine_2
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 y : { x // r x ↑a } ⊕ PUnit.{u + 1}
⊢ Sum.Lex (Subrel r fun x => r x ↑a) EmptyRelation x y →
    r (?intro.intro.intro.refine_1 x) (?intro.intro.intro.refine_1 y)

case intro.intro.intro.refine_3
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 : α
⊢ ∃ a_1, (RelEmbedding.ofMonotone ?intro.intro.intro.refine_1 ⋯) a_1 = x

Proof state:
case intro.intro.intro.refine_2
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 y : { x // r x ↑a } ⊕ PUnit.{u + 1}
⊢ Sum.Lex (Subrel r fun x => r x ↑a) EmptyRelation x y →
    r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)

Tactic:
rcases x with (x | ⟨⟨⟨⟩⟩⟩) <;> rcases y with (y | ⟨⟨⟨⟩⟩⟩) <;>
  simp [Subrel, Order.Preimage, EmptyRelation]

Result:
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

Proof state:
case intro.intro.intro.refine_3
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 : α
⊢ ∃ a_1, (RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a) ⋯) a_1 = x

Tactic:
suffices r x a ∨ ∃ _ : PUnit.{u}, ↑a = x by
  convert this
  dsimp [RelEmbedding.ofMonotone]; simp

Result:
case intro.intro.intro.refine_3
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 ∨ ∃ 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 x ↑a ∨ ∃ x_1, ↑a = x

Tactic:
refine absurd h ?_

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 (↑a) x