awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
inl : ∀ (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}
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀
have inl : max a b ≤ max (max a b) ℵ₀
Tactic: rw [add_eq_max ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
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}
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}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀
have inr : max a b ≤ max (max a b) ℵ₀
Tactic: rw [add_comm, add_eq_max hb, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b + max a b < c
have rw : max a b < c
Tactic: rw [add_eq_self h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b = c
have a₁ : b ≤ c
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
a₁ : b ≤ c
⊢ b = c
have a₂ : c ≤ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c
have a₁ : b ≤ a + b
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b
have a₁ : ¬b < c
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False
have this : a + b < c
Tactic: have : a + b < c := add_lt_of_lt hc ha hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a
have rw : max a b = a
Tactic: rw [add_eq_max ha, 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
rw : max a b = a
⊢ a + b = a
have rw₁ : a = a
Tactic: rw [add_eq_max ha, 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
⊢ a + b = b
have rw : b + a = b
Tactic: rw [add_comm, add_eq_left hb ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
rw : b + a = b
⊢ a + b = b
have rw₁ : b = b
Tactic: rw [add_comm, add_eq_left hb ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0
have rw : a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
have refine_1 : ∀ (h : a + b = a), ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
have refine_2 : ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
have refine_1 : ∀ (ha : ℵ₀ ≤ a), ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
have refine_1₁ : ∀ (ha : a < ℵ₀), ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
have refine_1 : ℵ₀ ≤ a ∧ b ≤ a
Tactic: left
-- 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
have right : b ≤ a
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
⊢ b ≤ a
have right : ¬a < b
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
have apply : ∀ (hb : a < b), a < a + b
Tactic: apply fun hb => ne_of_gt _ 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
have refine_1 : b = 0
Tactic: right
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ b = 0
have ha₁ : (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
Tactic: rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
⊢ b = 0
have refine_1 : ∀ (n m : ℕ) (h : HAdd.hAdd (α := 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}) 0
Tactic: rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
Cleared hypotheses: a, b, h, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h : HAdd.hAdd (α := 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}) 0
have refine_1 : ∀ (h : n + m = n), m = 0
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h : n + m = n
⊢ m = 0
have refine_1 : n + m = n + 0
Tactic: rw [← add_right_inj, h, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h : n + m = n
refine_1 : n + m = n + 0
refine_1₁ : ℕ
⊢ m = 0
have refine_1₂ : n = n + 0
Tactic: rw [← add_right_inj, h, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m : ℕ
h : n + m = n
refine_1 : n + m = n + 0
refine_1₁ : ℕ
refine_1₂ : n = n + 0
⊢ m = 0
have refine_1₃ : n = n
Tactic: rw [← add_right_inj, h, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a
have refine_2 : max a b = a
Tactic: rw [add_eq_max h1, max_eq_left h2]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
refine_2 : max a b = a
⊢ a + b = a
have refine_2₁ : a = a
Tactic: rw [add_eq_max h1, max_eq_left h2]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a
have refine_2 : a + 0 = a
Tactic: rw [h3, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
h3 : b = 0
refine_2 : a + 0 = a
⊢ a + b = a
have refine_2₁ : a = a
Tactic: rw [h3, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0
have rw : b + a = b ↔ max ℵ₀ a ≤ b ∨ a = 0
Tactic: rw [add_comm, add_eq_left_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u_1}
rw : b + a = b ↔ max ℵ₀ a ≤ b ∨ a = 0
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0
have rw₁ : max ℵ₀ a ≤ b ∨ a = 0 ↔ max ℵ₀ a ≤ b ∨ a = 0
Tactic: rw [add_comm, add_eq_left_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ (↑n : Cardinal.{u_1}) + a = a
have rw : a + (↑n : Cardinal.{u_1}) = a
Tactic: rw [add_comm, add_nat_eq n ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
rw : a + (↑n : Cardinal.{u_1}) = a
⊢ (↑n : Cardinal.{u_1}) + a = a
have rw₁ : a = a
Tactic: rw [add_comm, add_nat_eq n ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
i : α
h : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
hα : ℵ₀ ≤ #α
⊢ #(↑(Iic i) : Type u_1) < #α
have rw : #(↑(Iio i) : Type u_1) + 1 < #α
Tactic: rw [← Iio_insert, mk_insert self_notMem_Iio]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
⊢ b = c
have inl : ∀ (hb : ℵ₀ ≤ b), b = c
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
inl : ∀ (hb : ℵ₀ ≤ b), b = c
⊢ b = c
have inr : ∀ (hb : b < ℵ₀), b = c
Tactic: rcases le_or_gt ℵ₀ b with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b = c
have this : a < b
Tactic: have : a < b := ha.trans_le hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
have h₁ : a + c = b
Tactic: rw [add_eq_right hb this.le, eq_comm] at h
Cleared hypotheses: h, ha, hb, this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
have inl : b = b
Tactic: rw [eq_of_add_eq_of_aleph0_le h this hb]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ c < ℵ₀
have rw : ¬ℵ₀ ≤ c
Tactic: rw [← not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ False
have apply : ℵ₀ < ℵ₀
Tactic: apply lt_irrefl ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ ℵ₀ < ℵ₀
have apply : a + c < ℵ₀
Tactic: apply (hc.trans (self_le_add_left _ a)).trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀
have rw : a + b < ℵ₀
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c
have hc : c < ℵ₀
Tactic: have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ b = c
have ha₁ : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
Tactic: rw [lt_aleph0] at *
Cleared hypotheses: ha, hb, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
ha₁ : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
⊢ b = c
have hb₁ : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
Tactic: rw [lt_aleph0] at *
Cleared hypotheses: ha, hb, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
ha₁ : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
hb₁ : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
⊢ b = c
have hc₁ : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
Tactic: rw [lt_aleph0] at *
Cleared hypotheses: ha, hb, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
hb : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
hc : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
⊢ b = c
have inr : ∀ (n : ℕ) (h : (↑n : Cardinal.{u_1}) + b = (↑n : Cardinal.{u_1}) + c), b = c
Tactic: rcases ha with ⟨n, rfl⟩
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
b c : Cardinal.{u_1}
hb : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
hc : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
n : ℕ
h : (↑n : Cardinal.{u_1}) + b = (↑n : Cardinal.{u_1}) + c
⊢ b = c
have inr : ∀ (m : ℕ) (h : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) + c),
  (↑m : Cardinal.{u_1}) = c
Tactic: rcases hb with ⟨m, rfl⟩
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
n m : ℕ
h : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) + c
⊢ (↑m : Cardinal.{u_1}) = c
have inr : ∀ (k : ℕ)
  (h :
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) =
      HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})),
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑k : Cardinal.{u_1})
Tactic: rcases hc with ⟨k, rfl⟩
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
n m k : ℕ
h :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) =
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑k : Cardinal.{u_1})
have inr : ∀ (h : n + m = n + k), m = k
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c
have h₁ : b + a = b + c
Tactic: rw [add_comm a b, add_comm c b] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : Infinite α
⊢ ∃ (r : α → α → Prop), (∀ (x : α), #{ y : α // ¬r x y } < #α) ∧ ∀ (y : α), #{ x : α // r x y } < #α
have obtain : ∀ (α_1 : LinearOrder α) (w : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2),
  ∃ (r : α → α → Prop), (∀ (x : α), #{ y : α // ¬r x y } < #α) ∧ ∀ (y : α), #{ x : α // r x y } < #α
Tactic: obtain ⟨α, _, hα⟩ := exists_ord_eq_type_lt α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
inst : Infinite α_1
α : LinearOrder α_1
w : WellFoundedLT α_1
hα : (#α_1).ord = type fun (x1 x2 : α_1) ↦ x1 < x2
⊢ ∃ (r : α_1 → α_1 → Prop), (∀ (x : α_1), #{ y : α_1 // ¬r x y } < #α_1) ∧ ∀ (y : α_1), #{ x : α_1 // r x y } < #α_1
have refine : ∀ (x : α_1), #{ y : α_1 // ¬x < y } < #α_1
Tactic: refine ⟨LT.lt, fun x ↦ ?_, fun y ↦ mk_Iio_lt _ hα⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
i : ι
⊢ f i + c ≤ (⨆ (i : ι), f i) + c
have grw : iSup f + c ≤ iSup f + c
Tactic: grw [le_ciSup hf i]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c
have this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
Tactic: have (i : ι) : f i + c ≤ (⨆ i, f i) + c := by grw [le_ciSup hf i]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
⊢ (⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c
have refine : (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
Tactic: refine le_antisymm ?_ (ciSup_le' this)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
have bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
Tactic: have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
have inl : ∀ (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}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
inl : ∀ (hs : ⨆ (i : ι), f i < ℵ₀), (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
have inr : ∀ (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}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
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 inl : ∀ (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}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
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 inr : LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i + c) ∧ c ≤ ⨆ (i : ι), f i + c
Tactic: rw [add_eq_max hs, max_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
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 [add_comm, Cardinal.ciSup_add f hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst : Nonempty ι
inst_1 : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ HAdd.hAdd (α := 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_add f hf, Cardinal.add_ciSup g hg]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have inl : IsEmpty ι → (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
inl : IsEmpty ι → (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have inr : Nonempty ι → (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have inr : HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) 0 = ⨆ (i : ι), f i * 0
Tactic: obtain rfl | h0 := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
inr : HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) 0 = ⨆ (i : ι), f i * 0
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have inr₁ : ∀ (h0 : c ≠ 0), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
Tactic: obtain rfl | h0 := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have pos : ∀ (hf : BddAbove (range f)), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
Tactic: by_cases hf : BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
pos : ∀ (hf : BddAbove (range f)), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have neg : ∀ (hf : ¬BddAbove (range f)), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
Tactic: by_cases hf : BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have hfc : ¬BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
Tactic: have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd 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)
i : ι
⊢ f i * c ≤ (⨆ (i : ι), f i) * c
have grw : f i * c ≤ f i * c
Tactic: grw [← le_ciSup hf i]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
Tactic: have (i : ι) : f i * c ≤ (⨆ i, f i) * c := by grw [← le_ciSup hf 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
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
have pos : (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
Tactic: refine le_antisymm ?_ (ciSup_le' this)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
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
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
have bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
Tactic: have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
-- 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)
⊢ (⨆ (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) ℵ₀