a b : Ordinal
⊢ a < b → beth a < beth b
⊢ StrictMono beth
intro a b
case h
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
⊢ a < b → beth a < beth b
a b : Ordinal
⊢ a < b → beth a < beth b
induction' b using Ordinal.induction with b IH generalizing a
case h
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
⊢ beth a < beth b
case h
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
⊢ a < b → beth a < beth b
intro h
case h.inl
a✝ a : Ordinal
IH : ∀ (k : Ordinal), k < 0 → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a < 0
⊢ beth a < beth 0

case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a < succ c
⊢ beth a < beth (succ c)

case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ beth a < beth b
case h
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
⊢ beth a < beth b
rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)
no goals
case h.inl
a✝ a : Ordinal
IH : ∀ (k : Ordinal), k < 0 → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a < 0
⊢ beth a < beth 0
exact (Ordinal.not_lt_zero a h).elim
case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < beth (succ c)
case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a < succ c
⊢ beth a < beth (succ c)
rw [lt_succ_iff] at h
case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < 2 ^ beth c
case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < beth (succ c)
rw [beth_succ]
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a ≤ beth c
case h.inr.inl.intro
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < 2 ^ beth c
apply lt_of_le_of_lt _ (cantor _)
case inl
a✝ a : Ordinal
IH : ∀ (k : Ordinal), k < succ a → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ a
⊢ beth a ≤ beth a

case inr
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h✝ : a ≤ c
h : a < c
⊢ beth a ≤ beth c
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a ≤ beth c
rcases eq_or_lt_of_le h with (rfl | h)
no goals
case inr
a✝ a c : Ordinal
IH : ∀ (k : Ordinal), k < succ c → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h✝ : a ≤ c
h : a < c
⊢ beth a ≤ beth c
exact (IH c (lt_succ c) h).le
no goals
case inl
a✝ a : Ordinal
IH : ∀ (k : Ordinal), k < succ a → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
h : a ≤ a
⊢ beth a ≤ beth a
rfl
case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ 2 ^ beth a ≤ beth b
case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ beth a < beth b
apply (cantor _).trans_le
case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ beth (succ a) ≤ ⨆ (a : ↑(Iio b)), beth ↑a
case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ 2 ^ beth a ≤ beth b
rw [beth_limit hb, ← beth_succ]
no goals
case h.inr.inr
a✝ b : Ordinal
IH : ∀ (k : Ordinal), k < b → ∀ ⦃a : Ordinal⦄, a < k → beth a < beth k
a : Ordinal
h : a < b
hb : Ordinal.IsLimit b
⊢ beth (succ a) ≤ ⨆ (a : ↑(Iio b)), beth ↑a
exact le_ciSup (bddAbove_of_small _) (⟨_, hb.succ_lt h⟩ : Iio b)