awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : Cardinal.lift.{u_1, u_1} #ι ≤ Cardinal.lift.{u_1, u_1} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ card (⨆ (i : ι), f i) ≤ c

Tactic:
simpa using card_iSup_le_lift hι hf

Premises used: Ordinal.card_iSup_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
apply : Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, v} c
⊢ card (⨆ (i : (↑(Iio o) : Type (u + 1))), f i) ≤ c

Tactic:
apply card_iSup_le_lift _ hf

Premises used: Ordinal.card_iSup_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
rw : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
| Cardinal.lift.{u + 1, v} c

Tactic:
rw [← Cardinal.lift_lift.{u, u + 1}]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
conv_rhs : Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, v} c

Tactic:
conv_rhs => rw [← Cardinal.lift_lift.{u, u + 1}]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
rwa :
  Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
rwa₁ : Cardinal.lift.{max (u + 1) v, u} o.card ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
rwa₂ :
  Cardinal.lift.{u + 1, max v u} (Cardinal.lift.{v, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
rwa₃ rwa₄ rwa₅ rwa₆ : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)

Tactic:
rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]

Premises used: Cardinal.lift_lift, Cardinal.mk_Iio_ordinal, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : (↑(Iio o) : Type (u_1 + 1)) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : (↑(Iio o) : Type (u_1 + 1))), (f i).card ≤ c
⊢ Cardinal.lift.{u_1, u_1} o.card ≤ Cardinal.lift.{u_1, u_1} c

Tactic:
rw [← Cardinal.lift_le] at hι

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : (↑(Iio o) : Type (u_1 + 1)) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : (↑(Iio o) : Type (u_1 + 1))), (f i).card ≤ c
hι₁ : Cardinal.lift.{u_1, u_1} o.card ≤ Cardinal.lift.{u_1, u_1} c
⊢ ∀ (i : (↑(Iio o) : Type (u_1 + 1))), (f i).card ≤ c

Tactic:
rw [← Cardinal.lift_le] at hι

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : (↑(Iio o) : Type (u_1 + 1)) → Ordinal.{u_1}
hι : Cardinal.lift.{u_1, u_1} o.card ≤ Cardinal.lift.{u_1, u_1} c
hf : ∀ (i : (↑(Iio o) : Type (u_1 + 1))), (f i).card ≤ c
⊢ card (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), f i) ≤ c

Tactic:
simpa using card_iSup_Iio_le_of_lift hι hf

Premises used: Ordinal.card_iSup_Iio_le_of_lift
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
rw : card (⨆ (a : (↑s : Type (u + 1))), (↑a : Ordinal.{u})) ≤ c
⊢ (sSup s).card ≤ c

Tactic:
rw [sSup_eq_iSup']

Premises used: sSup_eq_iSup'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
hι : Cardinal.lift.{u, u + 1} #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hf : ∀ (i : (↑s : Type (u + 1))), (↑i : Ordinal.{u}).card ≤ c
⊢ card (⨆ (a : (↑s : Type (u + 1))), (↑a : Ordinal.{u})) ≤ c

Tactic:
apply card_iSup_le_lift

Premises used: Ordinal.card_iSup_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
hι hι₁ hι₂ hι₃ : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
⊢ Cardinal.lift.{u, u + 1} #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c

Tactic:
rwa [Cardinal.lift_id'.{u, u + 1}]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ ∀ (i : (↑s : Type (u + 1))), (↑i : Ordinal.{u}).card ≤ c

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
⊢ (HPow.hPow (β := Ordinal.{u_1}) a 0).card ≤ max a.card (card 0)

Tactic:
simpa using one_lt_omega0.le.trans ha

Premises used: LT.lt.le, LE.le.trans, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : max a.card (a ^ b).card ≤ max a.card (b.card + 1)
add_one₁ : (a ^ b).card ≠ 0
add_one₂ : ℵ₀ ≤ a.card
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card

Tactic:
rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]

Premises used: Ordinal.card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, Ordinal.card_mul, Ordinal.opow_add_one, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : max a.card (max a.card b.card) ≤ max a.card (b.card + 1)
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)

Tactic:
grw [IH]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : max a.card b.card ≤ max a.card (b.card + 1)
⊢ max a.card (max a.card b.card) ≤ max a.card (b.card + 1)

Tactic:
rw [← max_assoc, max_self]

Premises used: max_self, max_assoc
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one add_one₁ : max a.card b.card ≤ max a.card b.card
⊢ max a.card b.card ≤ max a.card (b.card + 1)

Tactic:
grw [← le_self_add]

Premises used: le_self_add
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : ¬(a = 0 ∧ b ≠ 0)
⊢ (a ^ b).card ≠ 0

Tactic:
rw [ne_eq, card_eq_zero, opow_eq_zero]

Premises used: Ordinal.card_eq_zero, ne_eq, Ordinal.opow_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
ha : ω ≤ 0
IH : (HPow.hPow (α := Ordinal.{u_1}) 0 b).card ≤ max (card 0) b.card
⊢ False

Tactic:
cases omega0_pos.not_ge ha

Premises used: Ordinal.omega0_pos, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one add_one₁ add_one₂ add_one₃ : ω ≤ a
⊢ ℵ₀ ≤ a.card

Tactic:
rwa [aleph0_le_card]

Premises used: Ordinal.aleph0_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
hb : Order.IsSuccLimit b
IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card
limit : card (⨆ (b_1 : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑b_1 : Ordinal.{u_1})) ≤ max a.card b.card
⊢ (a ^ b).card ≤ max a.card b.card

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

Premises used: Order.IsNormal.apply_of_isSuccLimit, Ordinal.isNormal_opow, LT.lt.trans_le, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
hb : Order.IsSuccLimit b
IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card
⊢ card (⨆ (b_1 : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑b_1 : Ordinal.{u_1})) ≤ max a.card b.card

Tactic:
card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

Premises used: le_max_right, max_le_max_left, Ordinal.card_le_card, LT.lt.le, Ordinal.card_iSup_Iio_le, Ordinal.card, LE.le.trans, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
hb : Order.IsSuccLimit b
IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card
⊢ card (⨆ (b_1 : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑b_1 : Ordinal.{u_1})) ≤ max a.card b.card

Tactic:
exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

Premises used: le_max_right, max_le_max_left, Ordinal.card_le_card, LT.lt.le, Ordinal.card_iSup_Iio_le, Ordinal.card, LE.le.trans, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
zero : (HPow.hPow (β := Ordinal.{u_1}) a 0).card ≤ max a.card (card 0)
add_one : ∀ (b : Ordinal.{u_1}) (IH : (a ^ b).card ≤ max a.card b.card), (a ^ (b + 1)).card ≤ max a.card (b + 1).card
limit :
  ∀ (b : Ordinal.{u_1}) (hb : Order.IsSuccLimit b) (IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card),
    (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

Premises used: Ordinal.card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, Ordinal.card_eq_zero, LT.lt.le, max_self, ne_eq, Ordinal.aleph0_le_card, Ordinal.card_mul, Ordinal.zero, Ordinal.opow_add_one, max_assoc, LE.le.trans, le_self_add, Ordinal.one_lt_omega0, rfl, Ordinal.opow_eq_zero, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
hb : ω ≤ b
inl : ∀ (n : ℕ), (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
inr : ∀ (ha : ω ≤ a), (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a

Premises used: Ordinal.eq_natCast_or_omega0_le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
inl : (ω ^ b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card

Tactic:
apply (card_le_card <| opow_le_opow_left b (natCast_lt_omega0 n).le).trans

Premises used: Ordinal.card_le_card, LT.lt.le, Ordinal.natCast_lt_omega0, LE.le.trans, Ordinal.opow_le_opow_left
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
inl : max ω.card b.card ≤ max (card (↑n : Ordinal.{u_1})) b.card
⊢ (ω ^ b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card

Tactic:
apply (card_opow_le_of_omega0_le_left le_rfl _).trans

Premises used: le_rfl, Ordinal.card_opow_le_of_omega0_le_left, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ max ω.card b.card ≤ max (card (↑n : Ordinal.{u_1})) b.card

Tactic:
simp [hb]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
card_opow_le_of_omega0_le_left ha b

Premises used: Ordinal.card_opow_le_of_omega0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
exact card_opow_le_of_omega0_le_left ha b

Premises used: Ordinal.card_opow_le_of_omega0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
inl :
  ∀ (n : ℕ),
    (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
inr : ∀ (ha : ω ≤ a), (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a

Premises used: Ordinal.eq_natCast_or_omega0_le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
n : ℕ
inl :
  ∀ (m : ℕ),
    (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑m : Ordinal.{u_1})).card ≤
      max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
inl₁ :
  ∀ (hb : ω ≤ b),
    (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)

Tactic:
obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b

Premises used: Ordinal.eq_natCast_or_omega0_le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
n m : ℕ
inl : (↑(n ^ m) : Cardinal.{u_1}) ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
⊢ (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑m : Ordinal.{u_1})).card ≤
    max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))

Tactic:
rw [opow_natCast, ← natCast_pow, card_nat]

Premises used: Ordinal.natCast_pow, Ordinal.opow_natCast, Ordinal.card_nat
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
n m : ℕ
⊢ (↑(n ^ m) : Cardinal.{u_1}) ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))

Tactic:
le_max_of_le_left natCast_le_aleph0

Premises used: le_max_of_le_left, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
n m : ℕ
⊢ (↑(n ^ m) : Cardinal.{u_1}) ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))

Tactic:
exact le_max_of_le_left natCast_le_aleph0

Premises used: le_max_of_le_left, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)

Tactic:
(card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

Premises used: le_max_right, Ordinal.card_opow_le_of_omega0_le_right, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)

Tactic:
exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

Premises used: le_max_right, Ordinal.card_opow_le_of_omega0_le_right, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
(card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

Premises used: le_max_right, Ordinal.card_opow_le_of_omega0_le_left, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

Premises used: le_max_right, Ordinal.card_opow_le_of_omega0_le_left, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
apply : a.card ≤ (a ^ b).card
apply₁ : b.card ≤ (a ^ b).card
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _)

Premises used: LE.le.antisymm, max_le, Ordinal.card_opow_le_of_omega0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
a₁ : a ≤ a ^ b
⊢ a.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
a₁ : b ≤ a ^ b
⊢ b.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b

Tactic:
left_le_opow a hb

Premises used: Ordinal.left_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b

Tactic:
exact left_le_opow a hb

Premises used: Ordinal.left_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b

Tactic:
right_le_opow b (one_lt_omega0.trans_le ha)

Premises used: Ordinal.right_le_opow, LT.lt.trans_le, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b

Tactic:
exact right_le_opow b (one_lt_omega0.trans_le ha)

Premises used: Ordinal.right_le_opow, LT.lt.trans_le, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
apply : a.card ≤ (a ^ b).card
apply₁ : b.card ≤ (a ^ b).card
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _)

Premises used: LE.le.antisymm, Ordinal.card_opow_le_of_omega0_le_right, max_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
a₁ : a ≤ a ^ b
⊢ a.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
a₁ : b ≤ a ^ b
⊢ b.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

Tactic:
left_le_opow a (omega0_pos.trans_le hb)

Premises used: Ordinal.omega0_pos, LT.lt.trans_le, Ordinal.left_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

Tactic:
exact left_le_opow a (omega0_pos.trans_le hb)

Premises used: Ordinal.omega0_pos, LT.lt.trans_le, Ordinal.left_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b

Tactic:
right_le_opow b ha

Premises used: Ordinal.right_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b

Tactic:
exact right_le_opow b ha

Premises used: Ordinal.right_le_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
rw : max ω.card a.card = max ℵ₀ a.card
rw₁ rw₂ : max ℵ₀ a.card = max ℵ₀ a.card
⊢ (ω ^ a).card = max ℵ₀ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]

Premises used: le_rfl, Ordinal.card_omega0, Ordinal.card_opow_eq_of_omega0_le_left, Ne.bot_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
h : 1 < a
rw : max a.card ω.card = max ℵ₀ a.card
rw₁ : max a.card ℵ₀ = max ℵ₀ a.card
rw₂ rw₃ : max ℵ₀ a.card = max ℵ₀ a.card
⊢ (a ^ ω).card = max ℵ₀ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]

Premises used: le_rfl, Ordinal.card_omega0, Ordinal.card_opow_eq_of_omega0_le_right, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
inr :
  ∀ (ho : 0 < o),
    IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)

Tactic:
obtain rfl | ho := eq_zero_or_pos o

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
inl : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ω
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)

Tactic:
rw [omega_zero]

Premises used: Ordinal.omega_zero
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ω

Tactic:
isPrincipal_opow_omega0

Premises used: Ordinal.isPrincipal_opow_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ω

Tactic:
exact isPrincipal_opow_omega0

Premises used: Ordinal.isPrincipal_opow_omega0
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
hb : b < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
inr :
  ∀ (ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
    (hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o),
    card ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ LT.lt (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b : Ordinal.{u_1})
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})

Tactic:
rw [lt_omega_iff_card_lt] at ha hb ⊢

Premises used: Cardinal.lt_omega_iff_card_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
apply : ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ card ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))

Premises used: max_lt, LE.le.trans_lt, Ordinal.card_opow_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
rwa :
  LT.lt (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < o
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rwa [← aleph_zero, aleph_lt_aleph]

Premises used: Cardinal.aleph_lt_aleph, Cardinal.aleph_zero
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
obtain :
  ∀ (a : Ordinal.{u_1}) (h : IsInitial.{u_1} ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a))
    (ho : ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a),
    IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) o

Tactic:
obtain ⟨a, rfl⟩ := mem_range_omega_iff.2 ⟨ho, h⟩

Premises used: Iff.mpr, Ordinal.mem_range_omega_iff, And.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
h : IsInitial.{u_1} ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
ho : ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)

Tactic:
isPrincipal_opow_omega a

Premises used: Ordinal.isPrincipal_opow_omega
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
a : Ordinal.{u_1}
h : IsInitial.{u_1} ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
ho : ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)

Tactic:
exact isPrincipal_opow_omega a

Premises used: Ordinal.isPrincipal_opow_omega
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
apply : ω ≤ c.ord
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) c.ord

Tactic:
apply (isInitial_ord c).isPrincipal_opow

Premises used: Ordinal.isInitial_ord, Ordinal.IsInitial.isPrincipal_opow
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc rwa rwa₁ rwa₂ rwa₃ : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
rwa [omega0_le_ord]

Premises used: Cardinal.omega0_le_ord