-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lt_power_cof {c : Cardinal.{u}} : ℵ₀ ≤ c → c < (c^cof c.ord) :=
  Cardinal.inductionOn c fun α h => by
    rcases ord_eq α with ⟨r, wo, re⟩
    have := isLimit_ord h
    rw [re] at this ⊢
    rcases cof_eq' r this with ⟨S, H, Se⟩
    have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_
    · simp only [Cardinal.prod_const, Cardinal.lift_id, ← Se, ← mk_sigma, power_def] at this ⊢
      refine lt_of_le_of_lt ?_ this
      refine ⟨Embedding.ofSurjective ?_ ?_⟩
      · exact fun x => x.2.1
      · exact fun a =>
          let ⟨b, h, ab⟩ := H a
          ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩
    · have := typein_lt_type r i
      rwa [← re, lt_ord] at this

Proof state:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (#α).ord.IsLimit
⊢ #α < #α ^ (#α).ord.cof

Tactic:
rw [re] at this ⊢

Result:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
⊢ #α < #α ^ (type r).cof

Proof state:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ #α < #(↑S → α)

Tactic:
refine lt_of_le_of_lt ?_ this

Result:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ #α ≤ #((i : ↑S) × { x // r x ↑i })

Proof state:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
⊢ #α < #α ^ (type r).cof

Tactic:
rcases cof_eq' r this with ⟨S, H, Se⟩

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
⊢ #α < #α ^ (type r).cof

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
⊢ #α < #α ^ (type r).cof

Tactic:
have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_

Result:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : (sum fun a => #{ x // r x ↑a }) < prod fun x => #α
⊢ #α < #α ^ (type r).cof

case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
i : ↑S
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i

Proof state:
case intro.intro.intro.intro.refine_2.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ Surjective fun x => ↑x.snd

Tactic:
exact fun a =>
  let ⟨b, h, ab⟩ := H a
  ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : (sum fun a => #{ x // r x ↑a }) < prod fun x => #α
⊢ #α < #α ^ (type r).cof

Tactic:
simp only [Cardinal.prod_const, Cardinal.lift_id, ← Se, ← mk_sigma, power_def] at this ⊢

Result:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ #α < #(↑S → α)

Proof state:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
i : ↑S
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i

Tactic:
have := typein_lt_type r i

Result:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
i : ↑S
this : (typein r).toRelEmbedding ↑i < type r
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i

Proof state:
case intro.intro.intro.intro.refine_2.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ (i : ↑S) × { x // r x ↑i } → α

Tactic:
exact fun x => x.2.1

Result:
no goals

Proof state:
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof

Tactic:
rcases ord_eq α with ⟨r, wo, re⟩

Result:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
⊢ #α < #α ^ (#α).ord.cof

Proof state:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
⊢ #α < #α ^ (#α).ord.cof

Tactic:
have := isLimit_ord h

Result:
case intro.intro
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (#α).ord.IsLimit
⊢ #α < #α ^ (#α).ord.cof

Proof state:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
i : ↑S
this : (typein r).toRelEmbedding ↑i < type r
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i

Tactic:
rwa [← re, lt_ord] at this

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ #α ≤ #((i : ↑S) × { x // r x ↑i })

Tactic:
refine ⟨Embedding.ofSurjective ?_ ?_⟩

Result:
case intro.intro.intro.intro.refine_2.refine_1
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ (i : ↑S) × { x // r x ↑i } → α

case intro.intro.intro.intro.refine_2.refine_2
c : Cardinal.{u}
α : Type u
h : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this✝ : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
this : #((i : ↑S) × { x // r x ↑i }) < #(↑S → α)
⊢ Surjective ?intro.intro.intro.intro.refine_2.refine_1