-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem ord_cof_eq (r : α → α → Prop) [IsWellOrder α r] :
    ∃ S, Unbounded r S ∧ type (Subrel r (· ∈ S)) = (cof (type r)).ord

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
⊢ ∃ S, Unbounded r S ∧ type (Subrel r fun x => x ∈ S) = (type r).cof.ord

Tactic:
let ⟨s, _, e'⟩ := Cardinal.ord_eq S

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
⊢ ∃ S, Unbounded r S ∧ type (Subrel r fun x => x ∈ S) = (type r).cof.ord

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b : ↑S := ⋯.min {b | ¬r (↑b) a} this
⊢ ∃ b ∈ T, ¬r b a

Tactic:
have ba : ¬r b a := IsWellFounded.wf.min_mem _ this

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b : ↑S := ⋯.min {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
⊢ ∃ b ∈ T, ¬r b a

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b : ↑S := ⋯.min {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ∀ (b : ↑S), ⟨↑b, ⋯⟩ = b

Tactic:
intro b

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b✝ : ↑S := ⋯.min {b | ¬r (↑b) a} this
ba : ¬r (↑b✝) a
c : ↑S
h : ¬r ↑c ↑b✝
b : ↑S
⊢ ⟨↑b, ⋯⟩ = b

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r fun x => x ∈ T) ≤ (type r).cof.ord

Tactic:
rw [← e, e']

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r fun x => x ∈ T) ≤ type s

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
⊢ ∃ S, Unbounded r S ∧ type (Subrel r fun x => x ∈ S) = (type r).cof.ord

Tactic:
refine ⟨T, this, le_antisymm ?_ (Cardinal.ord_le.2 <| cof_type_le this)⟩

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r fun x => x ∈ T) ≤ (type r).cof.ord

Proof state:
case mk.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
b : ↑T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ b
⊢ s ((fun a => ⟨↑a, ⋯⟩) ⟨a, ⋯⟩) ((fun a => ⟨↑a, ⋯⟩) b)

Tactic:
rcases b with ⟨b, bS, hb⟩

Result:
case mk.intro.mk.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 ⟨b, bS⟩ → r (↑b_1) b
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ ⟨b, ⋯⟩
⊢ s ((fun a => ⟨↑a, ⋯⟩) ⟨a, ⋯⟩) ((fun a => ⟨↑a, ⋯⟩) ⟨b, ⋯⟩)

Proof state:
case mk.intro.mk.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 ⟨b, bS⟩ → r (↑b_1) b
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ ⟨b, ⋯⟩
⊢ s ((fun a => ⟨↑a, ⋯⟩) ⟨a, ⋯⟩) ((fun a => ⟨↑a, ⋯⟩) ⟨b, ⋯⟩)

Tactic:
change s ⟨a, _⟩ ⟨b, _⟩

Result:
case mk.intro.mk.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 ⟨b, bS⟩ → r (↑b_1) b
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ ⟨b, ⋯⟩
⊢ s ⟨a, ⋯⟩ ⟨b, ⋯⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b✝ : ↑S := ⋯.min {b | ¬r (↑b) a} this
ba : ¬r (↑b✝) a
c : ↑S
h : ¬r ↑c ↑b✝
b : ↑S
⊢ ⟨↑b, ⋯⟩ = b

Tactic:
cases b

Result:
case mk
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
a : α
this : {b | ¬r (↑b) a}.Nonempty
b : ↑S := ⋯.min {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
val✝ : α
property✝ : val✝ ∈ S
⊢ ⟨↑⟨val✝, property✝⟩, ⋯⟩ = ⟨val✝, property✝⟩

Proof state:
case mk.intro.mk.intro.refine_2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 ⟨b, bS⟩ → r (↑b_1) b
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ ⟨b, ⋯⟩
⊢ ¬⟨b, ⋯⟩ = ⟨a, ⋯⟩

Tactic:
intro e

Result:
case mk.intro.mk.intro.refine_2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e✝ : #↑S = (type r).cof
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : (#↑S).ord = type s
T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 ⟨b, bS⟩ → r (↑b_1) b
h : Subrel r (fun x => x ∈ T) ⟨a, ⋯⟩ ⟨b, ⋯⟩
e : ⟨b, ⋯⟩ = ⟨a, ⋯⟩
⊢ False