-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem beth_strictMono : StrictMono beth

Proof state:
case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a < succ c
⊢ ℶ_ a < ℶ_ (succ c)

Tactic:
rw [lt_succ_iff] at h

Result:
case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a < ℶ_ (succ c)

Proof state:
case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ 2 ^ ℶ_ a ≤ ℶ_ b

Tactic:
rw [beth_limit hb, ← beth_succ]

Result:
case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ ℶ_ (succ a) ≤ ⨆ a, ℶ_ ↑a

Proof state:
case h
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
⊢ a < b → ℶ_ a < ℶ_ b

Tactic:
intro h

Result:
case h
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
⊢ ℶ_ a < ℶ_ b

Proof state:
a b : Ordinal.{u_1}
⊢ a < b → ℶ_ a < ℶ_ b

Tactic:
induction' b using Ordinal.induction with b IH generalizing a

Result:
case h
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
⊢ a < b → ℶ_ a < ℶ_ b

Proof state:
⊢ StrictMono ℶ_

Tactic:
intro a b

Result:
a b : Ordinal.{u_1}
⊢ a < b → ℶ_ a < ℶ_ b

Proof state:
case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ ℶ_ (succ a) ≤ ⨆ a, ℶ_ ↑a

Tactic:
exact le_ciSup (bddAbove_of_small _) (⟨_, hb.succ_lt h⟩ : Iio b)

Result:
no goals

Proof state:
case h.inl
a : Ordinal.{u_1}
IH : ∀ k < 0, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a < 0
⊢ ℶ_ a < ℶ_ 0

Tactic:
exact (Ordinal.not_lt_zero a h).elim

Result:
no goals

Proof state:
case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a < 2 ^ ℶ_ c

Tactic:
apply lt_of_le_of_lt _ (cantor _)

Result:
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a ≤ ℶ_ c

Proof state:
case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a < ℶ_ (succ c)

Tactic:
rw [beth_succ]

Result:
case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a < 2 ^ ℶ_ c

Proof state:
case inl
a : Ordinal.{u_1}
IH : ∀ k < succ a, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ a
⊢ ℶ_ a ≤ ℶ_ a

Tactic:
rfl

Result:
no goals

Proof state:
case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ ℶ_ a < ℶ_ b

Tactic:
apply (cantor _).trans_le

Result:
case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ 2 ^ ℶ_ a ≤ ℶ_ b

Proof state:
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ c
⊢ ℶ_ a ≤ ℶ_ c

Tactic:
rcases eq_or_lt_of_le h with (rfl | h)

Result:
case inl
a : Ordinal.{u_1}
IH : ∀ k < succ a, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a ≤ a
⊢ ℶ_ a ≤ ℶ_ a

case inr
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h✝ : a ≤ c
h : a < c
⊢ ℶ_ a ≤ ℶ_ c

Proof state:
case inr
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h✝ : a ≤ c
h : a < c
⊢ ℶ_ a ≤ ℶ_ c

Tactic:
exact (IH c (lt_succ c) h).le

Result:
no goals

Proof state:
case h
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
⊢ ℶ_ a < ℶ_ b

Tactic:
rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)

Result:
case h.inl
a : Ordinal.{u_1}
IH : ∀ k < 0, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a < 0
⊢ ℶ_ a < ℶ_ 0

case h.inr.inl.intro
a c : Ordinal.{u_1}
IH : ∀ k < succ c, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
h : a < succ c
⊢ ℶ_ a < ℶ_ (succ c)

case h.inr.inr
b : Ordinal.{u_1}
IH : ∀ k < b, ∀ ⦃a : Ordinal.{u_1}⦄, a < k → ℶ_ a < ℶ_ k
a : Ordinal.{u_1}
h : a < b
hb : b.IsLimit
⊢ ℶ_ a < ℶ_ b