awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
pos : ∀ (hs : ⨆ (i : ι), f i < ℵ₀), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
have pos₁ : ∀ (hs : ℵ₀ ≤ ⨆ (i : ι), f i), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
Tactic: obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ⨆ (i : ι), f i < ℵ₀
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
have pos : ∀ (i : ι) (hi : f i = ⨆ (i : ι), f i), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
Tactic: obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
have pos : LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c
Tactic: rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c
have pos : ∀ (i : ι) (hi : 1 < f i),
  LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c
Tactic: obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i
have rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i * c) (⨆ (i : ι), c * f i)
Tactic: rw [mul_comm, Cardinal.ciSup_mul f]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (j : ι'), g j) = ⨆ (i : ι), ⨆ (j : ι'), f i * g j
have simp_rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i * ⨆ (j : ι'), g j) (⨆ (i : ι), ⨆ (j : ι'), f i * g j)
Tactic: simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ (i : ι), f i)
⊢ sum f = lift.{u, v} (⨆ (i : ι), f i)
have h₁ : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
Tactic: rw [lift_iSup bddAbove_of_small] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ sum f = lift.{u, v} (⨆ (i : ι), f i)
have apply : sum f ≤ lift.{u, v} (⨆ (i : ι), f i)
Tactic: apply (lift_iSup_le_sum f).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ sum f ≤ lift.{u, v} (⨆ (i : ι), f i)
have h₁ : lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
Tactic: convert! sum_le_lift_mk_mul_iSup_lift f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
have h₁ : lift.{u, v} (⨆ (i : ι), f i) = max (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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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))
⊢ lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
have h₂ : lift.{u, v} (⨆ (i : ι), f i) = ⨆ (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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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)
⊢ lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
have h₃ : Eq (α := Cardinal.{max v u}) (⨆ (i : ι), lift.{u, v} (f i)) (⨆ (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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
⊢ sum f = ⨆ (i : ι), f i
have rw : sum f = lift.{u, max u v} (⨆ (i : ι), f i)
Tactic: rw [← lift_id'.{u, v} (iSup _)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
⊢ sum f = lift.{u, max u v} (⨆ (i : ι), f i)
have apply : lift.{max u v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)
Tactic: apply sum_eq_lift_iSup_of_lift_mk_le_lift_iSup hι
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), f i
⊢ lift.{max u v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)
have rwa : lift.{v, u} #ι ≤ lift.{u, max u v} (⨆ (i : ι), f i)
Tactic: rwa [lift_umax, lift_id'.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
o₁ o₂ : Ordinal.{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₂)
have 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})
Tactic: rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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})
⊢ 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₂)
have 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})
Tactic: rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β
have refine : ∀ (h : α + γ ≤ β + γ), α ≤ β
Tactic: refine ⟨fun h => ?_, fun h => by gcongr⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β
have contrapose : ∀ (h : ¬α ≤ β), ¬α + γ ≤ β + γ
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ
have rw : ∀ (h : β ≤ α ∧ ¬β = α), β + γ ≤ α + γ ∧ ¬β + γ = α + γ
Tactic: rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ
have grw : α + γ ≤ α + γ
Tactic: grw [h.1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b
have mp : a + c < b + c → a < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
mp : a + c < b + c → a < b
⊢ a + c < b + c ↔ a < b
have mpr : a < b → a + c < b + c
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c → a < b
have mp : b ≤ a → b + c ≤ a + c
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a < b → a + c < b + c
have mpr : b + c ≤ a + c → b ≤ a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inl : ∀ (hinf : ℵ₀ ≤ κ₂ + μ₂), κ₁ + μ₁ < κ₂ + μ₂
Tactic: rcases le_or_gt ℵ₀ (κ₂ + μ₂) with hinf | hfin
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
inl : ∀ (hinf : ℵ₀ ≤ κ₂ + μ₂), κ₁ + μ₁ < κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inr : ∀ (hfin : κ₂ + μ₂ < ℵ₀), κ₁ + μ₁ < κ₂ + μ₂
Tactic: rcases le_or_gt ℵ₀ (κ₂ + μ₂) with hinf | hfin
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inl : κ₁ < κ₂ + μ₂
Tactic: refine add_lt_of_lt hinf ?_ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : κ₁ < κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inl₁ : μ₁ < κ₂ + μ₂
Tactic: refine add_lt_of_lt hinf ?_ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : κ₁ < κ₂
⊢ κ₁ < κ₂ + μ₂
have inl₁ : κ₂ ≤ κ₂ + μ₂
Tactic: apply lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
inl : μ₁ < μ₂
⊢ μ₁ < κ₂ + μ₂
have inl₁ : μ₂ ≤ κ₂ + μ₂
Tactic: apply lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂
have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
Tactic: have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀ := add_lt_aleph0_iff.1 hfin
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inr : κ₁ + μ₁ ≤ κ₂ + μ₁
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
inr : κ₁ + μ₁ ≤ κ₂ + μ₁
⊢ κ₁ + μ₁ < κ₂ + μ₂
have inr₁ : κ₂ + μ₁ < κ₂ + μ₂
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n_1 : ℕ
hn : n_1 ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ 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) μ)
have 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) * μ
Tactic: push_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 + 1) * a
have rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 + 1) * a <
    (HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 + 1) * μ
have 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) * μ
Tactic: conv_lhs => rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 + 1) * μ
have rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 + 1) * μ
have conv_rhs : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a + a <
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ + μ
Tactic: conv_rhs => rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 * μ + μ
have refine : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * a <
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 * μ
Tactic: refine Cardinal.add_lt_add ?_ hlt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ μ : Cardinal.{u}
H1_1 : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = (↑n : Cardinal.{u})
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑Nat.zero : Cardinal.{u}) ≤ ⟦α⟧
have grw : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 0 ≤ ⟦α⟧
Tactic: grw [Nat.cast_zero, power_zero, one_lt_aleph0, H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ μ : Cardinal.{u}
H1_1 : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = (↑n : Cardinal.{u})
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
grw : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 0 ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑Nat.zero : Cardinal.{u}) ≤ ⟦α⟧
have grw₁ : 1 ≤ ⟦α⟧
Tactic: grw [Nat.cast_zero, power_zero, one_lt_aleph0, H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
κ μ : Cardinal.{u}
H1_1 : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = (↑n : Cardinal.{u})
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
grw : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 0 ≤ ⟦α⟧
grw₁ : 1 ≤ ⟦α⟧
grw₂ : ℵ₀ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑Nat.zero : Cardinal.{u}) ≤ ⟦α⟧
have grw₃ : ⟦α⟧ ≤ ⟦α⟧
Tactic: grw [Nat.cast_zero, power_zero, one_lt_aleph0, H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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}) ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧
have grw : ⟦α⟧ ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 ≤ ⟦α⟧
Tactic: grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧
have grw₁ : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n : Cardinal.{u}) * HPow.hPow (β := Cardinal.{u}) ⟦α⟧ 1 ≤ ⟦α⟧
Tactic: grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧
have grw₂ : HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n : Cardinal.{u}) * ⟦α⟧ ≤ ⟦α⟧
Tactic: grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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}) * ⟦α⟧ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧
have grw₃ : ⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
Tactic: grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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₃ : ⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
⊢ HPow.hPow (β := Cardinal.{u}) ⟦α⟧ (↑n.succ : Cardinal.{u}) ≤ ⟦α⟧
have grw₄ : ⟦α⟧ ≤ ⟦α⟧
Tactic: grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^ c = HPow.hPow (α := Cardinal.{u_1}) 2 c
have apply : HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ c ^ c
Tactic: apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
apply : HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ c ^ c
⊢ c ^ c = HPow.hPow (α := Cardinal.{u_1}) 2 c
have apply₁ : HPow.hPow (α := Cardinal.{u_1}) 2 c ^ c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
Tactic: apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 c ^ c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
have rw : HPow.hPow (α := Cardinal.{u_1}) 2 (c * c) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
Tactic: rw [← power_mul, mul_eq_self h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : HPow.hPow (α := Cardinal.{u_1}) 2 (c * c) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 c ^ c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
have rw₁ : HPow.hPow (α := Cardinal.{u_1}) 2 c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 c
Tactic: rw [← power_mul, mul_eq_self h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ prod c = HPow.hPow (α := Cardinal.{max u v}) 2 (lift.{v, u} #ι)
have rw : (prod fun (i : ι) ↦ lift.{u, v} (c i)) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
Tactic: rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 #ι)
have a : (prod fun (i : ι) ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 #ι)
⊢ (prod fun (i : ι) ↦ lift.{u, v} (c i)) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a₁ : lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 #ι)
have a : (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
Tactic: refine (prod_le_prod _ _ h₂).trans_eq ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a : lift.{u, max u v} (lift.{v, u} #ι) ^ lift.{max u 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}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 #ι)
⊢ (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a₁ : lift.{max v u, u} #ι ^ lift.{max u 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}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 #ι)
⊢ (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a₂ : lift.{max u 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}]