awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1
have inr : ∀ (t : Cardinal.{u}) (ht : 1 = a * t), a = 1
Tactic: obtain ⟨t, ht⟩ := h 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
⊢ a = 1
have inr : ∀ (ht : a = 1 ∧ t = 1), a = 1
Tactic: rw [eq_comm, mul_eq_one_iff_of_one_le] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
inr : ∀ (ht : a = 1 ∧ t = 1), a = 1
⊢ a = 1
have inr₁ : ∀ (ht : a * t = 1), 1 ≤ a
Tactic: rw [eq_comm, mul_eq_one_iff_of_one_le] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
inr : ∀ (ht : a = 1 ∧ t = 1), a = 1
inr₁ : ∀ (ht : a * t = 1), 1 ≤ a
⊢ a = 1
have inr₂ : ∀ (ht : a * t = 1), 1 ≤ t
Tactic: rw [eq_comm, mul_eq_one_iff_of_one_le] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
have inr : t ≠ 0
Tactic: apply Cardinal.one_le_iff_ne_zero.mpr
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
a : Cardinal.{u}
h_1 : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ False
have ht₁ : Eq.{u + 2} (α := Cardinal.{u}) 0 1
Tactic: rw [h, mul_zero] at ht
Cleared hypotheses: ht, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a b : Cardinal.{u_1}
hb : b ≠ 0
hdiv : a ∣ b
⊢ a ≤ b
have obtain : ∀ (b : Cardinal.{u_1}) (hb : a * b ≠ 0), a ≤ a * b
Tactic: obtain ⟨b, rfl⟩ := hdiv
Cleared hypotheses: b, hb, hdiv
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a b : Cardinal.{u_1}
hb : a * b ≠ 0
⊢ a ≤ a * b
have h : b ≠ 0
Tactic: apply le_mul_right
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ Prime a
have refine_1 : ¬IsUnit a
Tactic: refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
refine_1 : ¬IsUnit a
⊢ Prime a
have refine_2 : ∀ (b c : Cardinal.{u}) (hbc : a ∣ b * c), a ∣ b ∨ a ∣ c
Tactic: refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a
have refine_1 : ¬a = 1
Tactic: rw [isUnit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
⊢ a ∣ b ∨ a ∣ c
have refine_2 : ∀ (hz : b * c = 0), a ∣ b ∨ a ∣ c
Tactic: rcases eq_or_ne (b * c) 0 with hz | hz
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
refine_2 : ∀ (hz : b * c = 0), a ∣ b ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c
have refine_2₁ : ∀ (hz : b * c ≠ 0), a ∣ b ∨ a ∣ c
Tactic: rcases eq_or_ne (b * c) 0 with hz | hz
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
⊢ a ∣ b ∨ a ∣ c
have refine_2 : ∀ (hbc : a ∣ 0 * c) (hz : 0 * c = 0), a ∣ 0 ∨ a ∣ c
Tactic: rcases mul_eq_zero.mp hz with (rfl | rfl)
Cleared hypotheses: b, hbc, hz
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
refine_2 : ∀ (hbc : a ∣ 0 * c) (hz : 0 * c = 0), a ∣ 0 ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c
have refine_2₁ : ∀ (hbc : a ∣ b * 0) (hz : b * 0 = 0), a ∣ b ∨ a ∣ 0
Tactic: rcases mul_eq_zero.mp hz with (rfl | rfl)
Cleared hypotheses: c, hbc, hz
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
⊢ a ∣ b ∨ a ∣ c
have refine_2 : ∀
  (this :
    ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b),
      a ∣ b ∨ a ∣ c)
  (h : ¬c ≤ b), a ∣ b ∨ a ∣ c
Tactic: wlog h : c ≤ b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
refine_2 :
  ∀
    (this :
      ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b),
        a ∣ b ∨ a ∣ c)
    (h : ¬c ≤ b), a ∣ b ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c
have wlog : ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
Tactic: wlog h : c ≤ b
Cleared hypotheses: ha, b, c, hbc, hz
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
have refine_2 : c ≤ b → a ∣ b ∨ a ∣ c
Tactic: cases le_total c b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
refine_2 : c ≤ b → a ∣ b ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c
have refine_2₁ : b ≤ c → a ∣ b ∨ a ∣ c
Tactic: cases le_total c b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h_1 : b ≤ c
⊢ a ∣ b ∨ a ∣ c
have refine_2 : a ∣ c ∨ a ∣ b
Tactic: rw [or_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
have refine_2 : b ≤ c → a ∣ c ∨ a ∣ b
Tactic: cases le_total c b <;> [solve_by_elim; rw [or_comm]]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h_1 : b ≤ c
refine_2 : ℵ₀ ≤ a
⊢ a ∣ c ∨ a ∣ b
have refine_2₁ : a ∣ c * b
Tactic: apply_assumption
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} (ha : ℵ₀ ≤ a) (b c : Cardinal.{u}) (hbc : a ∣ b * c) (hz : b * c ≠ 0) (h : c ≤ b), a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h_1 : b ≤ c
refine_2 : ℵ₀ ≤ a
refine_2₁ : a ∣ c * b
⊢ a ∣ c ∨ a ∣ b
have refine_2₂ : c * b ≠ 0
Tactic: apply_assumption
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c
have h₁ : a ∣ b
Tactic: left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b
have habc : a ≤ b * c
Tactic: have habc := le_of_dvd hz hbc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b
have h₁ : ∀ (hbc : a ∣ max b c) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
Tactic: rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc
Cleared hypotheses: hbc, hz, h, habc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
h₁ : ∀ (hbc : a ∣ max b c) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
⊢ a ∣ b
have h₂ : ∀ (hbc : a ∣ if c ≤ b then b else c) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
Tactic: rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc
Cleared hypotheses: hbc, hz, h, habc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
h₁ : ∀ (hbc : a ∣ max b c) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
h₂ : ∀ (hbc : a ∣ if c ≤ b then b else c) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
⊢ a ∣ b
have h₃ : ∀ (hbc : a ∣ b) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
Tactic: rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc
Cleared hypotheses: hbc, hz, h, habc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a
have rw : ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
Tactic: rw [irreducible_iff, not_and_or]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
have refine : ∀ (h : ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b), False
Tactic: refine Or.inr fun h => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n m : ℕ
⊢ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) ↔ n ∣ m
have refine : Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) → n ∣ m
Tactic: refine ⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
⊢ n ∣ m
have this : (↑m : Cardinal.{u_1}) < ℵ₀
Tactic: have : ↑m < ℵ₀ := natCast_lt_aleph0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
this : (↑m : Cardinal.{u_1}) < ℵ₀
⊢ n ∣ m
have this₁ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ k = 0 ∨ (↑n : Cardinal.{u_1}) < ℵ₀ ∧ k < ℵ₀
Tactic: rw [hk, mul_lt_aleph0_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
this : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ k = 0 ∨ (↑n : Cardinal.{u_1}) < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
have inl : ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0), n ∣ m
Tactic: rcases this with (h | h | ⟨-, hk'⟩)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
this : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ k = 0 ∨ (↑n : Cardinal.{u_1}) < ℵ₀ ∧ k < ℵ₀
inl : ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0), n ∣ m
⊢ n ∣ m
have inr : ∀ (h : k = 0), n ∣ m
Tactic: rcases this with (h | h | ⟨-, hk'⟩)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
this : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ k = 0 ∨ (↑n : Cardinal.{u_1}) < ℵ₀ ∧ k < ℵ₀
inl : ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0), n ∣ m
inr : ∀ (h : k = 0), n ∣ m
⊢ n ∣ m
have inr₁ : ∀ (hk' : k < ℵ₀), n ∣ m
Tactic: rcases this with (h | h | ⟨-, hk'⟩)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
⊢ n ∣ m
have hk₁ : m = 0
Tactic: simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
h : k = 0
⊢ n ∣ m
have hk₁ : m = 0
Tactic: simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
hk' : k < ℵ₀
⊢ n ∣ m
have inr : ∀ (k : ℕ) (hk : (↑m : Cardinal.{u_1}) = HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})),
  n ∣ m
Tactic: lift k to ℕ using hk'
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
⊢ Prime.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ Nat.Prime n
have simp : (Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∧
    ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∀ (a b : Cardinal.{u_1}), (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b) ↔
  n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
Tactic: simp only [Prime, Nat.prime_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
⊢ (Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∧
      ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
        ∀ (a b : Cardinal.{u_1}),
          (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b) ↔
    n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
have refine_1 : ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ ¬IsUnit n
Tactic: refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
refine_1 : ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ ¬IsUnit n
⊢ (Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∧
      ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
        ∀ (a b : Cardinal.{u_1}),
          (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b) ↔
    n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
have refine_2 : ∀ (h : ∀ (a b : Cardinal.{u_1}), (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b)
  (b c : ℕ) (hbc : n ∣ b * c), n ∣ b ∨ n ∣ c
Tactic: refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
refine_1 : ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ ¬IsUnit n
refine_2 :
  ∀
    (h :
      ∀ (a b : Cardinal.{u_1}), (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b)
    (b c : ℕ) (hbc : n ∣ b * c), n ∣ b ∨ n ∣ c
⊢ (Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∧
      ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
        ∀ (a b : Cardinal.{u_1}),
          (↑n : Cardinal.{u_1}) ∣ a * b → (↑n : Cardinal.{u_1}) ∣ a ∨ (↑n : Cardinal.{u_1}) ∣ b) ↔
    n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
have refine_3 : ∀ (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c),
  (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
⊢ ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ ¬IsUnit n
have refine_1 : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ ¬n = 1
Tactic: simp only [isUnit_iff, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3 : ∀ (h' : b * c < ℵ₀), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: rcases lt_or_ge (b * c) ℵ₀ with h' | h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
refine_3 : ∀ (h' : b * c < ℵ₀), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3₁ : ∀ (h' : ℵ₀ ≤ b * c), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: rcases lt_or_ge (b * c) ℵ₀ with h' | h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : b * c < ℵ₀
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3 : ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ 0 * c) (h' : 0 * c < ℵ₀),
  Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
Cleared hypotheses: b, hbc, h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : b * c < ℵ₀
refine_3 :
  ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ 0 * c) (h' : 0 * c < ℵ₀),
    Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ (↑n : Cardinal.{u_1}) ∣ c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3₁ : ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ b * 0) (h' : b * 0 < ℵ₀),
  (↑n : Cardinal.{u_1}) ∣ b ∨ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
Tactic: rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
Cleared hypotheses: c, hbc, h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : b * c < ℵ₀
refine_3 :
  ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ 0 * c) (h' : 0 * c < ℵ₀),
    Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ∨ (↑n : Cardinal.{u_1}) ∣ c
refine_3₁ :
  ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ b * 0) (h' : b * 0 < ℵ₀),
    (↑n : Cardinal.{u_1}) ∣ b ∨ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3₂ : ∀ (hb : b < ℵ₀) (hc : c < ℵ₀), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : b * c < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3 : ∀ (b : ℕ) (hbc : (↑n : Cardinal.{u_1}) ∣ (↑b : Cardinal.{u_1}) * c) (h' : (↑b : Cardinal.{u_1}) * c < ℵ₀),
  Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑b : Cardinal.{u_1}) ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: lift b to ℕ using hb
Cleared hypotheses: b, hbc, h', hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hc : c < ℵ₀
b : ℕ
hbc : (↑n : Cardinal.{u_1}) ∣ (↑b : Cardinal.{u_1}) * c
h' : (↑b : Cardinal.{u_1}) * c < ℵ₀
⊢ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑b : Cardinal.{u_1}) ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3 : ∀ (c : ℕ) (hbc : (↑n : Cardinal.{u_1}) ∣ HMul.hMul (α := Cardinal.{u_1}) (↑b : Cardinal.{u_1}) (↑c : Cardinal.{u_1}))
  (h' : HMul.hMul (α := Cardinal.{u_1}) (↑b : Cardinal.{u_1}) (↑c : Cardinal.{u_1}) < ℵ₀),
  Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑b : Cardinal.{u_1}) ∨
    Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑c : Cardinal.{u_1})
Tactic: lift c to ℕ using hc
Cleared hypotheses: c, hc, hbc, h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have hb : b ≠ 0
Tactic: rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have hc : c ≠ 0
Tactic: rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
Tactic: rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n : ℕ
h_1 : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
⊢ False
have hbc₁ : b = 0 ∨ c = 0
Tactic: rw [h, zero_dvd_iff, mul_eq_zero] at hbc
Cleared hypotheses: hbc, h', hb, hc, hℵ₀, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
Tactic: have hn : (n : Cardinal) ≠ 0 := by
    intro h
    rw [h, zero_dvd_iff, mul_eq_zero] at hbc
    cases hbc <;> contradiction
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have refine_3 : ∀
  (this :
    ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
      (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
      (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
      (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c)
  (hℵ₀b : ¬ℵ₀ ≤ b), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: wlog hℵ₀b : ℵ₀ ≤ b