awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
h₁ : lift.{u, v} (⨆ (i : ι), f i) = max (lift.{v, u} #ι) (⨆ (i : ι), lift.{u, v} (f i))
h₂ : lift.{u, v} (⨆ (i : ι), f i) = ⨆ (i : ι), lift.{u, v} (f i)
h₃ h₄ : Eq (α := Cardinal.{max v u}) (⨆ (i : ι), lift.{u, v} (f i)) (⨆ (i : ι), lift.{u, v} (f i))
⊢ lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h,
    lift_iSup bddAbove_of_small]

Premises used: Iff.mpr, Cardinal.lift_iSup, Cardinal.mul_eq_max, Cardinal.aleph0_le_lift, max_eq_right, Cardinal.bddAbove_of_small, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
rw : sum f = lift.{u, max u v} (⨆ (i : ι), f i)
⊢ sum f = ⨆ (i : ι), f i

Tactic:
rw [← lift_id'.{u, v} (iSup _)]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
apply : lift.{max u v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)
⊢ sum f = lift.{u, max u v} (⨆ (i : ι), f i)

Tactic:
apply sum_eq_lift_iSup_of_lift_mk_le_lift_iSup hι

Premises used: Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
rwa : lift.{v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)
rwa₁ rwa₂ rwa₃ rwa₄ : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
⊢ lift.{max u v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)

Tactic:
rwa [lift_umax, lift_id'.{u, v}]

Premises used: Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{u}
hι : ℵ₀ ≤ #ι
h : #ι ≤ iSup f
⊢ sum f = ⨆ (i : ι), f i

Tactic:
sum_eq_iSup_of_lift_mk_le_iSup hι ((lift_id #ι).symm ▸ h)

Premises used: Cardinal.mk, Eq.rec, Eq.symm, Cardinal.lift_id, Cardinal.sum_eq_iSup_of_lift_mk_le_iSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
o₁ o₂ : Ordinal.{u_1}
rw :
  Eq (α := Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (max o₁ o₂) : Cardinal.{u_1})
rw₁ rw₂ :
  Eq (α := Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (β := Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁ : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂ : Cardinal.{u_1}) =
    (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (max o₁ o₂)

Tactic:
rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]

Premises used: Cardinal.aleph_max, Cardinal.add_eq_max, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ = β + γ ↔ α = β

Tactic:
⟨fun h => Cardinal.eq_of_add_eq_add_right h γ₀, fun h => congr_arg (· + γ) h⟩

Premises used: Cardinal.eq_of_add_eq_add_right, congr_arg, HAdd.hAdd, Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Cardinal.{u_1}
n : ℕ
⊢ α + (↑n : Cardinal.{u_1}) = β + (↑n : Cardinal.{u_1}) ↔ α = β

Tactic:
add_right_inj_of_lt_aleph0 natCast_lt_aleph0

Premises used: Cardinal.add_right_inj_of_lt_aleph0, Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Cardinal.{u_1}
⊢ α + 1 = β + 1 ↔ α = β

Tactic:
add_right_inj_of_lt_aleph0 one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, Cardinal.add_right_inj_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α ≤ β
⊢ α + γ ≤ β + γ

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
refine : ∀ (h : α + γ ≤ β + γ), α ≤ β
⊢ α + γ ≤ β + γ ↔ α ≤ β

Tactic:
refine ⟨fun h => ?_, fun h => by gcongr⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
contrapose : ∀ (h : ¬α ≤ β), ¬α + γ ≤ β + γ
⊢ α ≤ β

Tactic:
contrapose h
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
rw : ∀ (h : β ≤ α ∧ ¬β = α), β + γ ≤ α + γ ∧ ¬β + γ = α + γ
⊢ ¬α + γ ≤ β + γ

Tactic:
rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢

Premises used: not_le, lt_iff_le_and_ne, Ne
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
grw grw₁ : α + γ ≤ α + γ
⊢ β + γ ≤ α + γ

Tactic:
grw [h.1]

Premises used: And.left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ

Tactic:
exact ⟨by grw [h.1], mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Cardinal.{u_1}
n : ℕ
⊢ α + (↑n : Cardinal.{u_1}) ≤ β + (↑n : Cardinal.{u_1}) ↔ α ≤ β

Tactic:
add_le_add_iff_of_lt_aleph0 natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Cardinal.{u_1}
⊢ α + 1 ≤ β + 1 ↔ α ≤ β

Tactic:
add_le_add_iff_of_lt_aleph0 one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
mp : a + c < b + c → a < b
mpr : a < b → a + c < b + c
⊢ a + c < b + c ↔ a < b

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
mp : b ≤ a → b + c ≤ a + c
⊢ a + c < b + c → a < b

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
mpr : b + c ≤ a + c → b ≤ a
⊢ a < b → a + c < b + c

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b ≤ a → b + c ≤ a + c

Tactic:
simp [add_le_add_iff_of_lt_aleph0 hc]

Premises used: Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b + c ≤ a + c → b ≤ a

Tactic:
simp [add_le_add_iff_of_lt_aleph0 hc]

Premises used: Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ c + a < c + b ↔ a < b

Tactic:
simpa [add_comm] using add_lt_add_iff_of_right_lt_aleph0 (a := a) (b := b) hc

Premises used: add_comm, Cardinal.add_lt_add_iff_of_right_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
inl : ∀ (hinf : ℵ₀ ≤ κ₂ + μ₂), κ₁ + μ₁ < κ₂ + μ₂
inr : ∀ (hfin : κ₂ + μ₂ < ℵ₀), κ₁ + μ₁ < κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
rcases le_or_gt ℵ₀ (κ₂ + μ₂) with hinf | hfin

Premises used: Cardinal.aleph0, le_or_gt, HAdd.hAdd
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
add_lt_of_lt hinf ?_ ?_

Premises used: Cardinal.add_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : κ₁ < κ₂ + μ₂
inl₁ : μ₁ < κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
refine add_lt_of_lt hinf ?_ ?_

Premises used: Cardinal.add_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : κ₁ < κ₂
inl₁ : κ₂ ≤ κ₂ + μ₂
inl₂ : Cardinal.{u_1}
⊢ κ₁ < κ₂ + μ₂

Tactic:
apply lt_of_lt_of_le

Premises used: lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : μ₁ < μ₂
inl₁ : μ₂ ≤ κ₂ + μ₂
inl₂ : Cardinal.{u_1}
⊢ μ₁ < κ₂ + μ₂

Tactic:
apply lt_of_lt_of_le

Premises used: lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂

Tactic:
assumption
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂

Tactic:
solve | assumption | simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₂ ≤ κ₂ + μ₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₂ ≤ κ₂ + μ₂

Tactic:
solve | assumption | simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < μ₂

Tactic:
assumption
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < μ₂

Tactic:
solve | assumption | simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₂ ≤ κ₂ + μ₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₂ ≤ κ₂ + μ₂

Tactic:
solve | assumption | simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
⊢ κ₂ < ℵ₀ ∧ μ₂ < ℵ₀

Tactic:
have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀ := add_lt_aleph0_iff.1 hfin
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
inr : κ₁ + μ₁ ≤ κ₂ + μ₁
inr₁ : κ₂ + μ₁ < κ₂ + μ₂
inr₂ : Cardinal.{u_1}
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ ≤ κ₂ + μ₁

Tactic:
(add_le_add_iff_of_lt_aleph0 (hμ.trans hfin_.right)).mpr hκ.le

Premises used: Iff.mpr, LT.lt.le, And.right, LT.lt.trans, Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ ≤ κ₂ + μ₁

Tactic:
exact (add_le_add_iff_of_lt_aleph0 (hμ.trans hfin_.right)).mpr hκ.le

Premises used: Iff.mpr, LT.lt.le, And.right, LT.lt.trans, Cardinal.add_le_add_iff_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₂ + μ₁ < κ₂ + μ₂

Tactic:
simpa [add_comm] using (add_lt_add_iff_of_right_lt_aleph0 hfin_.left).mpr hμ

Premises used: Iff.mpr, add_comm, And.left, Cardinal.add_lt_add_iff_of_right_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
hn : n ≠ 0
h : Ne (α := ℕ) 1 0
⊢ StrictMono (β := Cardinal.{u_1}) fun (a : Cardinal.{u_1}) ↦ (↑1 : Cardinal.{u_1}) * a

Tactic:
simpa using strictMono_id

Premises used: strictMono_id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
push_cast :
  (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * a <
    (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) ((fun (a : Cardinal.{u_1}) ↦ (↑(n + 1 + 1) : Cardinal.{u_1}) * a) a)
    ((fun (a : Cardinal.{u_1}) ↦ (↑(n + 1 + 1) : Cardinal.{u_1}) * a) μ)

Tactic:
push_cast
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a
| (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * a

Tactic:
rw [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
conv_lhs :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
    (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ
⊢ (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * a <
    (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ

Tactic:
conv_lhs => rw [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ
| (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ

Tactic:
rw [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
conv_rhs :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
    (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ

Tactic:
conv_rhs => rw [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ

Tactic:
Cardinal.add_lt_add ?_ hlt

Premises used: Cardinal.add_lt_add
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
refine :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a <
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ

Tactic:
refine Cardinal.add_lt_add ?_ hlt

Premises used: Cardinal.add_lt_add
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a <
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ

Tactic:
simpa using (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictMono (β := Cardinal.{u_1}) fun (a : Cardinal.{u_1}) ↦ (↑n : Cardinal.{u_1}) * a

Tactic:
match n, hn with
  | 1, _ => simpa using strictMono_id
  | (n + 1) + 1, hneq1 =>
    intro a μ hlt
    push_cast
    conv_lhs => rw [add_mul, one_mul]
    conv_rhs => rw [add_mul, one_mul]
    refine Cardinal.add_lt_add ?_ hlt
    simpa using (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
hn : n ≠ 0
x x_1 : Cardinal.{u_1}
hlt : x < x_1
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) ((fun (a : Cardinal.{u_1}) ↦ a * (↑n : Cardinal.{u_1})) x)
    ((fun (a : Cardinal.{u_1}) ↦ a * (↑n : Cardinal.{u_1})) x_1)

Tactic:
simpa [mul_comm] using natCast_mul_strictMono hn hlt

Premises used: Cardinal.natCast_mul_strictMono, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ (↑n : Cardinal.{u_1}) * a = (↑n : Cardinal.{u_1}) * b ↔ a = b

Tactic:
(natCast_mul_strictMono hn).injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Cardinal.natCast_mul_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ a * (↑n : Cardinal.{u_1}) = b * (↑n : Cardinal.{u_1}) ↔ a = b

Tactic:
(mul_natCast_strictMono hn).injective.eq_iff

Premises used: Cardinal.mul_natCast_strictMono, Function.Injective.eq_iff, StrictMono.injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ (↑n : Cardinal.{u_1}) * a ≤ (↑n : Cardinal.{u_1}) * b ↔ a ≤ b

Tactic:
(natCast_mul_strictMono hn).le_iff_le

Premises used: Cardinal.natCast_mul_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ a * (↑n : Cardinal.{u_1}) ≤ b * (↑n : Cardinal.{u_1}) ↔ a ≤ b

Tactic:
(mul_natCast_strictMono hn).le_iff_le

Premises used: Cardinal.mul_natCast_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ (↑n : Cardinal.{u_1}) * a < (↑n : Cardinal.{u_1}) * b ↔ a < b

Tactic:
(natCast_mul_strictMono hn).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Cardinal.natCast_mul_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
a b : Cardinal.{u_1}
hn : n ≠ 0
⊢ a * (↑n : Cardinal.{u_1}) < b * (↑n : Cardinal.{u_1}) ↔ a < b

Tactic:
(mul_natCast_strictMono hn).lt_iff_lt

Premises used: Cardinal.mul_natCast_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ μ : Cardinal.{u}
H1_1 : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = (↑n : Cardinal.{u})
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
grw : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 0 ≤ ⟦α⟧
grw₁ : 1 ≤ ⟦α⟧
grw₂ : ℵ₀ ≤ ⟦α⟧
grw₃ grw₄ : ⟦α⟧ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑Nat.zero : Cardinal.{u}) ≤ ⟦α⟧

Tactic:
grw [Nat.cast_zero, power_zero, one_lt_aleph0, H1]

Premises used: Cardinal.one_lt_aleph0, Cardinal.power_zero, Nat.cast_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ μ : Cardinal.{u}
H1_1 : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n_1 : ℕ
H3 : μ = (↑n_1 : Cardinal.{u})
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n : Cardinal.{u}) ≤ ⟦α⟧
grw : ⟦α⟧ ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 ≤ ⟦α⟧
grw₁ : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n : Cardinal.{u}) * HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 1 ≤ ⟦α⟧
grw₂ : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n : Cardinal.{u}) * ⟦α⟧ ≤ ⟦α⟧
grw₃ : ⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
grw₄ grw₅ : ⟦α⟧ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧

Tactic:
grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]

Premises used: Nat.cast_succ, Cardinal.power_add, Cardinal.mul_eq_self, Cardinal.power_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
κ μ : Cardinal.{u}
H1 : ℵ₀ ≤ κ
H2 : 1 ≤ μ
H3 : μ < ℵ₀
⊢ κ ^ μ = κ

Tactic:
(pow_le H1 H3).antisymm <| self_le_power κ H2

Premises used: Cardinal.self_le_power, Cardinal.pow_le, LE.le.antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
apply : HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ c ^ c
apply₁ : HPow.hPow (α := Cardinal.{u_1}) 2 c ^ c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
⊢ c ^ c = HPow.hPow (α := Cardinal.{u_1}) 2 c

Tactic:
apply ((power_le_power_right <| (cantor c).le).trans _).antisymm

Premises used: Cardinal.power_le_power_right, LE.le.antisymm, LT.lt.le, Cardinal.cantor, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ c ^ c

Tactic:
power_le_power_right (natCast_le_aleph0.trans h)

Premises used: Cardinal.power_le_power_right, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ c ^ c

Tactic:
exact power_le_power_right (natCast_le_aleph0.trans h)

Premises used: Cardinal.power_le_power_right, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : HPow.hPow (α := Cardinal.{u_1}) 2 (c * c) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
rw₁ rw₂ : HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 c ^ c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c

Tactic:
rw [← power_mul, mul_eq_self h]

Premises used: Cardinal.power_mul, Cardinal.mul_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
rw : (prod fun (i : ι) ↦ lift.{u, v} (c i)) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
⊢ prod c = HPow.hPow (α := Cardinal.{max u v}) 2 (lift.{v, u} #ι)

Tactic:
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]

Premises used: Cardinal.lift_prod, Cardinal.lift_two_power
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : (prod fun (i : ι) ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₁ : lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
⊢ (prod fun (i : ι) ↦ lift.{u, v} (c i)) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun (i : ι) ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)

Tactic:
(prod_le_prod _ _ h₂).trans_eq ?_

Premises used: LE.le.trans_eq, Cardinal.prod_le_prod
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
⊢ (prod fun (i : ι) ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)

Tactic:
refine (prod_le_prod _ _ h₂).trans_eq ?_

Premises used: LE.le.trans_eq, Cardinal.prod_le_prod
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : lift.{u, max u v} (lift.{v, u} #ι) ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₁ : lift.{max v u, u} #ι ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₂ : lift.{max u v, u} (#ι ^ #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₃ : lift.{max u v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₄ a₅ : lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
⊢ (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)

Tactic:
rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]

Premises used: Cardinal.lift_lift, Cardinal.prod_const, Cardinal.power_self_eq, Cardinal.lift_power, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : (prod fun (i : ι) ↦ lift.{v, u} 2) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
⊢ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)

Tactic:
rw [← prod_const', lift_prod]

Premises used: Cardinal.lift_prod, Cardinal.prod_const'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun (i : ι) ↦ lift.{v, u} 2) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)

Tactic:
prod_le_prod _ _ fun i => ?_

Premises used: Cardinal.prod_le_prod
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : ∀ (i : ι), lift.{v, u} 2 ≤ lift.{u, v} (c i)
⊢ (prod fun (i : ι) ↦ lift.{v, u} 2) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)

Tactic:
refine prod_le_prod _ _ fun i => ?_

Premises used: Cardinal.prod_le_prod