awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
ind : ∀ (hq : #(↑(Iio q) : Type u_1) < ℵ₀), #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
have ind₁ : ∀ (hq : ℵ₀ ≤ #(↑(Iio q) : Type u_1)), #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
Tactic: rcases lt_or_ge #(Iio q) ℵ₀ with hq | hq
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #(↑(Iio q) : Type u_1)
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
have this₁ : #(↑(Iio q) : Type u_1) < #α
Tactic: have := mk_Iio_lt q hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ HMul.hMul (α := 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.mul_eq_max (aleph0_le_aleph o₁) (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})
⊢ HMul.hMul (α := 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.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), aleph_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c
have rw : a * b ≤ c * c
Tactic: rw [← Cardinal.mul_eq_self hc]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ a * b < c
have apply : max a b * max a b < c
Tactic: apply (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ max a b * max a b < c
have inl : ∀ (h : max a b < ℵ₀), max a b * max a b < c
Tactic: obtain h | h := lt_or_ge (max a b) ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
inl : ∀ (h : max a b < ℵ₀), max a b * max a b < c
⊢ max a b * max a b < c
have inr : ∀ (h : ℵ₀ ≤ max a b), max a b * max a b < c
Tactic: obtain h | h := lt_or_ge (max a b) ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c
have inr : max a b < c
Tactic: rw [mul_eq_self h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b
have h₁ : max a b = max a b * max a b
Tactic: convert! mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ max a b = max a b * max a b
have h₁ : ℵ₀ ≤ max a b
Tactic: rw [mul_eq_self]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
⊢ a * b = max a b
have inl : ∀ (hb : ℵ₀ ≤ b), a * b = max a b
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
inl : ∀ (hb : ℵ₀ ≤ b), a * b = max a b
⊢ a * b = max a b
have inr : ∀ (hb : b < ℵ₀), a * b = max a b
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = max a b
have inr : max a b ≤ a * b
Tactic: refine (mul_le_max_of_aleph0_le_left h).antisymm ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ max a b ≤ a * b
have this : b ≤ a
Tactic: have : b ≤ a := hb.le.trans h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ max a b ≤ a * b
have inr : a ≤ a * b
Tactic: rw [max_eq_left this]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b
have h₁ : a = a * 1
Tactic: convert! mul_le_mul_right (Cardinal.one_le_iff_ne_zero.mpr h') a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a = a * 1
have h₁ : a = a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b
have rw : b * a = max b a
Tactic: rw [mul_comm, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = max a b
have inl : ∀ (ha : a ≠ 0) (hb : b ≠ 0) (ha' : ℵ₀ ≤ a), a * b = max a b
Tactic: rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
inl : ∀ (ha : a ≠ 0) (hb : b ≠ 0) (ha' : ℵ₀ ≤ a), a * b = max a b
⊢ a * b = max a b
have inr : ∀ (ha : a ≠ 0) (hb : b ≠ 0) (hb' : ℵ₀ ≤ b), a * b = max a b
Tactic: rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a * b ≤ max (max a b) ℵ₀
have inl : 0 * b ≤ max (max 0 b) ℵ₀
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
inl : 0 * b ≤ max (max 0 b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
have inr : ∀ (ha0 : a ≠ 0), a * b ≤ max (max a b) ℵ₀
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
have inr : a * 0 ≤ max (max a 0) ℵ₀
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
inr : a * 0 ≤ max (max a 0) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
have inr₁ : ∀ (hb0 : b ≠ 0), a * b ≤ max (max a b) ℵ₀
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
have inr : ∀ (ha : ℵ₀ ≤ a), a * b ≤ max (max a b) ℵ₀
Tactic: rcases le_or_gt ℵ₀ a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
inr : ∀ (ha : ℵ₀ ≤ a), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
have inr₁ : ∀ (ha : a < ℵ₀), a * b ≤ max (max a b) ℵ₀
Tactic: rcases le_or_gt ℵ₀ a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀
have inr : max a b ≤ max (max a b) ℵ₀
Tactic: rw [mul_eq_max_of_aleph0_le_left ha hb0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
have inr : ∀ (hb : ℵ₀ ≤ b), a * b ≤ max (max a b) ℵ₀
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
inr : ∀ (hb : ℵ₀ ≤ b), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
have inr₁ : ∀ (hb : b < ℵ₀), a * b ≤ max (max a b) ℵ₀
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀
have inr : max a b ≤ max (max a b) ℵ₀
Tactic: rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ a * b = a
have rw : max a b = a
Tactic: rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
rw : max a b = a
⊢ a * b = a
have rw₁ : a = a
Tactic: rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ a * b = b
have rw : b * a = b
Tactic: rw [mul_comm, mul_eq_left hb ha ha']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
rw : b * a = b
⊢ a * b = b
have rw₁ : b = b
Tactic: rw [mul_comm, mul_eq_left hb ha ha']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
have h₁ : a = 1 * a
Tactic: convert! mul_le_mul_left (Cardinal.one_le_iff_ne_zero.mpr h) a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = 1 * a
have h₁ : a = a
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b
have rw : a ≤ b * a
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have rw : a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Tactic: rw [max_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_1 : ∀ (h : a * b = a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
refine_1 : ∀ (h : a * b = a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_2 : (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_1 : ∀ (ha : ℵ₀ ≤ a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Tactic: rcases le_or_gt ℵ₀ a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
refine_1 : ∀ (ha : ℵ₀ ≤ a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_1₁ : ∀ (ha : a < ℵ₀), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Tactic: rcases le_or_gt ℵ₀ a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have this : a ≠ 0
Tactic: have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_1 : (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
have refine_1 : ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
Tactic: rw [and_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
have right : b ≤ a ∧ b ≠ 0
Tactic: use ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0
have right : b ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
right : b ≤ a
⊢ b ≤ a ∧ b ≠ 0
have right₁ : b ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a
have right : ¬a < b
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False
have right : a = 0
Tactic: apply this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0
have h₁ : 0 = a
Tactic: rw [mul_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have refine_1 : b = 1 ∨ a = 0
Tactic: right
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0
have pos : ∀ (h2a : a = 0), b = 1 ∨ a = 0
Tactic: by_cases h2a : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
pos : ∀ (h2a : a = 0), b = 1 ∨ a = 0
⊢ b = 1 ∨ a = 0
have neg : ∀ (h2a : ¬a = 0), b = 1 ∨ a = 0
Tactic: by_cases h2a : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False
have apply : a = 0
Tactic: apply h2a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0
have h₁ : 0 = a
Tactic: rw [mul_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0
have hb : b ≠ 0
Tactic: have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0
have neg : b = 1
Tactic: left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
have ha₁ : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
Tactic: rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
Cleared hypotheses: ha, h2a, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
have neg : ∀ (h : 0 * b = 0) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), b = 1
Tactic: rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
Cleared hypotheses: a, h, ha, h2a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
h2a : ¬a = 0
hb : b ≠ 0
neg : ∀ (h : 0 * b = 0) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), b = 1
⊢ b = 1
have neg₁ : ∀ (h : a * 0 = a) (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 1
Tactic: rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
Cleared hypotheses: b, h, ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
h2a : ¬a = 0
hb : b ≠ 0
neg : ∀ (h : 0 * b = 0) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), b = 1
neg₁ : ∀ (h : a * 0 = a) (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 1
⊢ b = 1
have neg₂ : ∀ (n : ℕ) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (m : ℕ)
  (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0)
  (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
Tactic: rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
Cleared hypotheses: a, b, h, ha, h2a, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n : ℕ
h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
m : ℕ
hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
have neg : ∀ (h2a : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (m : ℕ)
  (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0)
  (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
Tactic: rw [← Ne] at h2a
Cleared hypotheses: h2a, m, hb, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n : ℕ
h2a : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
m : ℕ
hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
have neg : ∀ (h2a : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})) (m : ℕ)
  (hb : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑m : Cardinal.{u_1}))
  (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
Tactic: rw [← Cardinal.one_le_iff_ne_zero] at h2a hb
Cleared hypotheses: h2a, m, hb, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n : ℕ
h2a : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})
m : ℕ
hb : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑m : Cardinal.{u_1})
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
have neg : ∀ (h2a : 1 ≤ n) (hb : 1 ≤ m) (h : n * m = n), m = 1
Tactic: norm_cast at h2a hb h ⊢
Cleared hypotheses: h2a, hb, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1
have apply : m ≤ 1
Tactic: apply le_antisymm _ hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1
have rw : ¬1 < m
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
have apply : ∀ (h2b : 1 < m), n < n * m
Tactic: apply fun h2b => ne_of_gt _ h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
| n < n * m
have left : n
Tactic: left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
| n
have rw : n * 1
Tactic: rw [← mul_one n]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
| n < n * m
have rw : n * 1
Tactic: left; rw [← mul_one n]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ∀ (h2b : 1 < m), n < n * m
have conv_rhs : ∀ (a : 1 < m), n * 1 < n * m
Tactic: conv_rhs => left; rw [← mul_one n]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ∀ (a : 1 < m), n * 1 < n * m
have rw : ∀ (a : 1 < m), 1 < m
Tactic: rw [Nat.mul_lt_mul_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
rw : ∀ (a : 1 < m), 1 < m
⊢ ∀ (a : 1 < m), n * 1 < n * m
have rw₁ : 0 < n
Tactic: rw [Nat.mul_lt_mul_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a
have refine_2 : max a b = a
Tactic: rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
refine_2 : max a b = a
⊢ a * b = a
have refine_2₁ : a = a
Tactic: rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ a + b = max a b
have rw : b + a = max a b
Tactic: rw [add_comm, max_comm, add_eq_max ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
rw : b + a = max a b
⊢ a + b = max a b
have rw₁ : b + a = max b a
Tactic: rw [add_comm, max_comm, add_eq_max ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
rw : b + a = max a b
rw₁ : b + a = max b a
⊢ a + b = max a b
have rw₂ : max b a = max b a
Tactic: rw [add_comm, max_comm, add_eq_max ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀
have inl : ∀ (ha : ℵ₀ ≤ a), a + b ≤ max (max a b) ℵ₀
Tactic: rcases le_or_gt ℵ₀ a with ha | ha