-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordinal) :
    (a ^ b).card ≤ max a.card b.card

Proof state:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Tactic:
rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isLimit hb]

Result:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (⨆ a_1, a ^ ↑a_1).card ≤ a.card ⊔ b.card

Proof state:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ b.card ≤ a.card ⊔ (b.card + 1)

Tactic:
exact max_le_max_left _ le_self_add

Result:
no goals

Proof state:
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ⨆ a_1, (a ^ ↑a_1).card ≤ a.card ⊔ b.card

Tactic:
apply ciSup_le'

Result:
case h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ∀ (i : ↑(Iio b)), (a ^ ↑i).card ≤ a.card ⊔ b.card

Proof state:
case refine_3.h.refine_1
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ BddAbove (range fun a_1 => (a ^ ↑a_1).card)

Tactic:
exact Cardinal.bddAbove_of_small _

Result:
no goals

Proof state:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (⨆ a_1, a ^ ↑a_1).card ≤ a.card ⊔ b.card

Tactic:
apply (card_iSup_Iio_le_card_mul_iSup _).trans

Result:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ Cardinal.lift.{u_1, u_1} b.card * ⨆ a_1, (a ^ ↑a_1).card ≤ a.card ⊔ b.card

Proof state:
case refine_2.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ ¬(a = 0 ∧ b ≠ 0)

Tactic:
rintro ⟨rfl, -⟩

Result:
case refine_2.h'.intro
b✝ b : Ordinal.{u_1}
ha : ω ≤ 0
IH : (0 ^ b).card ≤ card 0 ⊔ b.card
⊢ False

Proof state:
case refine_3.h.refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ℵ₀ ≤ (a ^ ↑⟨1, ⋯⟩).card

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ (a ^ b).card ≤ a.card ⊔ (b.card + 1)

Tactic:
apply (max_le_max_left _ IH).trans

Result:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ (a.card ⊔ b.card) ≤ a.card ⊔ (b.card + 1)

Proof state:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ (a.card ⊔ b.card) ≤ a.card ⊔ (b.card + 1)

Tactic:
rw [← max_assoc, max_self]

Result:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ b.card ≤ a.card ⊔ (b.card + 1)

Proof state:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}), (a ^ o).card ≤ a.card ⊔ o.card → (a ^ succ o).card ≤ a.card ⊔ (succ o).card

Tactic:
intro b IH

Result:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ (a ^ succ b).card ≤ a.card ⊔ (succ b).card

Proof state:
case refine_2.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ (a ^ b).card ≠ 0

Tactic:
rw [ne_eq, card_eq_zero, opow_eq_zero]

Result:
case refine_2.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ ¬(a = 0 ∧ b ≠ 0)

Proof state:
case refine_2.h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ ℵ₀ ≤ a.card

Tactic:
rwa [aleph0_le_card]

Result:
no goals

Proof state:
case refine_3.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ b.card ≠ 0

Tactic:
simpa using hb.pos.ne'

Result:
no goals

Proof state:
case refine_3.h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ℵ₀ ≤ ⨆ a_1, (a ^ ↑a_1).card

Tactic:
refine le_ciSup_of_le ?_ ⟨1, one_lt_omega0.trans_le <| omega0_le_of_isLimit hb⟩ ?_

Result:
case refine_3.h.refine_1
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ BddAbove (range fun a_1 => (a ^ ↑a_1).card)

case refine_3.h.refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ℵ₀ ≤ (a ^ ↑⟨1, ⋯⟩).card

Proof state:
case refine_2.h'.intro
b✝ b : Ordinal.{u_1}
ha : ω ≤ 0
IH : (0 ^ b).card ≤ card 0 ⊔ b.card
⊢ False

Tactic:
cases omega0_pos.not_le ha

Result:
no goals

Proof state:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ (a ^ succ b).card ≤ a.card ⊔ (succ b).card

Tactic:
rw [opow_succ, card_mul, card_succ, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]

Result:
case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ a.card ⊔ (a ^ b).card ≤ a.card ⊔ (b.card + 1)

case refine_2.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ (a ^ b).card ≠ 0

case refine_2.h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
IH : (a ^ b).card ≤ a.card ⊔ b.card
⊢ ℵ₀ ≤ a.card

Proof state:
case refine_1
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ 0).card ≤ a.card ⊔ card 0

Tactic:
simpa using one_lt_omega0.le.trans ha

Result:
no goals

Proof state:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Tactic:
refine limitRecOn b ?_ ?_ ?_

Result:
case refine_1
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ 0).card ≤ a.card ⊔ card 0

case refine_2
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}), (a ^ o).card ≤ a.card ⊔ o.card → (a ^ succ o).card ≤ a.card ⊔ (succ o).card

case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}), o.IsLimit → (∀ o' < o, (a ^ o').card ≤ a.card ⊔ o'.card) → (a ^ o).card ≤ a.card ⊔ o.card

Proof state:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}), o.IsLimit → (∀ o' < o, (a ^ o').card ≤ a.card ⊔ o'.card) → (a ^ o).card ≤ a.card ⊔ o.card

Tactic:
intro b hb IH

Result:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Proof state:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (⨆ a_1, (a ^ ↑a_1).card) ⊔ b.card ≤ a.card ⊔ b.card

Tactic:
apply max_le _ (le_max_right _ _)

Result:
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ⨆ a_1, (a ^ ↑a_1).card ≤ a.card ⊔ b.card

Proof state:
case h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
c : ↑(Iio b)
⊢ (a ^ ↑c).card ≤ a.card ⊔ b.card

Tactic:
exact (IH c.1 c.2).trans (max_le_max_left _ (card_le_card c.2.le))

Result:
no goals