-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_succ {c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c) :=
  ⟨h.trans (le_succ c),
    succ_le_of_lt
      (by
        have αe := Cardinal.mk_out (succ c)
        set α := (succ c).out
        rcases ord_eq α with ⟨r, wo, re⟩
        have := isLimit_ord (h.trans (le_succ _))
        rw [← αe, re] at this ⊢
        rcases cof_eq' r this with ⟨S, H, Se⟩
        rw [← Se]
        apply lt_imp_lt_of_le_imp_le fun h => mul_le_mul_right' h c
        rw [mul_eq_self h, ← succ_le_iff, ← αe, ← sum_const']
        refine le_trans ?_ (sum_le_sum (fun (x : S) => card (typein r (x : α))) _ fun i => ?_)
        · simp only [← card_typein, ← mk_sigma]
          exact
            ⟨Embedding.ofSurjective (fun x => x.2.1) fun a =>
                let ⟨b, h, ab⟩ := H a
                ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩⟩
        · rw [← lt_succ_iff, ← lt_ord, ← αe, re]
          apply typein_lt_type)⟩

Proof state:
c : Cardinal.{u}
h : ℵ₀ ≤ c
⊢ c < (succ c).ord.cof

Tactic:
have αe := Cardinal.mk_out (succ c)

Result:
c : Cardinal.{u}
h : ℵ₀ ≤ c
αe : #(Quotient.out (succ c)) = succ c
⊢ c < (succ c).ord.cof

Proof state:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ #α ≤ sum fun x => ((typein r).toRelEmbedding ↑x).card

Tactic:
simp only [← card_typein, ← mk_sigma]

Result:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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) × { y // r y ↑i })

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

Tactic:
rw [← αe, re] at this ⊢

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

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c < (type r).cof

Tactic:
rw [← Se]

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c < #↑S

Proof state:
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
⊢ c < (succ c).ord.cof

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

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

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c * c < #↑S * c

Tactic:
rw [mul_eq_self h, ← succ_le_iff, ← αe, ← sum_const']

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ #α ≤ sum fun x => c

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

Tactic:
have := isLimit_ord (h.trans (le_succ _))

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

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ #α ≤ sum fun x => c

Tactic:
refine le_trans ?_ (sum_le_sum (fun (x : S) => card (typein r (x : α))) _ fun i => ?_)

Result:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ #α ≤ sum fun x => ((typein r).toRelEmbedding ↑x).card

case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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 x => ((typein r).toRelEmbedding ↑x).card) i ≤ c

Proof state:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ (typein r).toRelEmbedding ↑i < type r

Tactic:
apply typein_lt_type

Result:
no goals

Proof state:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c < #↑S

Tactic:
apply lt_imp_lt_of_le_imp_le fun h => mul_le_mul_right' h c

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c * c < #↑S * c

Proof state:
c : Cardinal.{u}
h : ℵ₀ ≤ c
αe : #(Quotient.out (succ c)) = succ c
⊢ c < (succ c).ord.cof

Tactic:
set α := (succ c).out

Result:
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
⊢ c < (succ c).ord.cof

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

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

Result:
case intro.intro.intro.intro
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ c < (type r).cof

Proof state:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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 x => ((typein r).toRelEmbedding ↑x).card) i ≤ c

Tactic:
rw [← lt_succ_iff, ← lt_ord, ← αe, re]

Result:
case intro.intro.intro.intro.refine_2
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
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
⊢ (typein r).toRelEmbedding ↑i < type r