awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
refine_2 : ∀ (hz : b * c = 0), a ∣ b ∨ a ∣ c
refine_2₁ : ∀ (hz : b * c ≠ 0), a ∣ b ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c

Tactic:
rcases eq_or_ne (b * c) 0 with hz | hz

Premises used: HMul.hMul, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
refine_2₁ : ∀ (hbc : a ∣ b * 0) (hz : b * 0 = 0), a ∣ b ∨ a ∣ 0
⊢ a ∣ b ∨ a ∣ c

Tactic:
rcases mul_eq_zero.mp hz with (rfl | rfl)

Premises used: mul_eq_zero, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
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
⊢ a ∣ b ∨ a ∣ c

Tactic:
wlog h : c ≤ b
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
refine_2₁ : b ≤ c → a ∣ b ∨ a ∣ c
⊢ a ∣ b ∨ a ∣ c

Tactic:
cases le_total c b

Premises used: le_total
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
solve_by_elim
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 ∣ c ∨ a ∣ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
rw [or_comm]

Premises used: or_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 : b ≤ c → a ∣ c ∨ a ∣ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
cases le_total c b <;> [solve_by_elim; rw [or_comm]]

Premises used: le_total, or_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
refine_2₂ : c * b ≠ 0
refine_2₃ : b ≤ c
⊢ a ∣ c ∨ a ∣ b

Tactic:
apply_assumption
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 refine_2₁ refine_2₂ refine_2₃ : a ∣ b * c
⊢ a ∣ c * b

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 refine_2₁ refine_2₂ refine_2₃ : b * c ≠ 0
⊢ c * b ≠ 0

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a_1 a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
h₁ : a ∣ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
left
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 * c

Tactic:
have habc := le_of_dvd hz hbc
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
h₃ h₄ h₅ h₆ : ∀ (hbc : a ∣ b) (hz : b * c ≠ 0) (h : c ≤ b) (habc : a ≤ b * c), a ∣ b
⊢ a ∣ b

Tactic:
rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc

Premises used: max_def', if_pos, LE.le.trans, Cardinal.mul_eq_max'
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
rw : ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ ¬Irreducible a

Tactic:
rw [irreducible_iff, not_and_or]

Premises used: not_and_or, irreducible_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
Or.inr fun h => ?_

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
refine : ∀ (h : ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b), False
⊢ ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
refine Or.inr fun h => ?_

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
h : ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False

Tactic:
simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using
    @h a ℵ₀

Premises used: Cardinal.mul_aleph0_eq, Cardinal.one_lt_aleph0, Cardinal.isUnit_iff, LT.lt.ne', LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
⊢ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) ↔ n ∣ m

Tactic:
⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, congrArg, _private.0.Cardinal.nat_coe_dvd_iff.match_1, cast, Nat.cast, Iff.intro, Exists.intro, Nat.cast_inj._simp_1, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
refine : Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) → n ∣ m
⊢ 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⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
⊢ (↑m : Cardinal.{u_1}) < ℵ₀

Tactic:
have : ↑m < ℵ₀ := natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
this : (↑m : Cardinal.{u_1}) < ℵ₀
⊢ 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

Premises used: Cardinal.mul_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
inr₁ : ∀ (hk' : k < ℵ₀), n ∣ m
⊢ n ∣ m

Tactic:
rcases this with (h | h | ⟨-, hk'⟩)
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ m = 0

Tactic:
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Nat.cast_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
hk : m = 0
⊢ n ∣ m

Tactic:
simp [hk]
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
h : k = 0
⊢ m = 0

Tactic:
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Nat.cast_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
h : k = 0
hk : m = 0
⊢ n ∣ m

Tactic:
simp [hk]
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
hk' : k < ℵ₀
⊢ k < ℵ₀

Tactic:
hk'
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m : ℕ
k : Cardinal.{u_1}
hk : (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) * k
hk' : k < ℵ₀
inr :
  ∀ (k : ℕ) (hk : (↑m : Cardinal.{u_1}) = HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})),
    n ∣ m
⊢ n ∣ m

Tactic:
lift k to ℕ using hk'
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m k : ℕ
hk : (↑m : Cardinal.{u_1}) = HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})
⊢ n ∣ m

Tactic:
⟨k, mod_cast hk⟩

Premises used: Nat.cast_mul._simp_1, congrArg, cast, Nat.cast, Exists.intro, Nat.cast_inj._simp_1, Eq, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n m k : ℕ
hk : (↑m : Cardinal.{u_1}) = HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑k : Cardinal.{u_1})
⊢ n ∣ m

Tactic:
exact ⟨k, mod_cast hk⟩
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
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
⊢ Prime.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ Nat.Prime n

Tactic:
simp only [Prime, Nat.prime_iff]

Premises used: Nat.prime_iff, Prime
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
⊢ Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0 ↔ n ≠ 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
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
⊢ (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:
refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)

Premises used: Iff.intro, and_congr
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
refine_1 : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ ¬n = 1
⊢ ¬IsUnit.{u_1 + 1} (M := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ↔ ¬IsUnit n

Tactic:
simp only [isUnit_iff, Nat.isUnit_iff]

Premises used: Cardinal.isUnit_iff, Nat.isUnit_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
⊢ ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ ¬n = 1

Tactic:
mod_cast Iff.rfl

Premises used: congrArg, Iff.rfl, cast, Nat.cast, Iff, Nat.cast_inj._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Not, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
⊢ ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ ¬n = 1

Tactic:
exact mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
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:
mod_cast h b c (mod_cast hbc)

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, congrArg, cast, Nat.cast, congr, Or, Eq.symm, Cardinal.nat_coe_dvd_iff._simp_2, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
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:
exact mod_cast h b c (mod_cast hbc)

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, congrArg, cast, Nat.cast, Eq.symm, Cardinal.nat_coe_dvd_iff._simp_2, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
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

Tactic:
rcases lt_or_ge (b * c) ℵ₀ with h' | h'

Premises used: HMul.hMul, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
refine_3₂ : ∀ (hb : b < ℵ₀) (hc : c < ℵ₀), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c

Tactic:
rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)

Premises used: Cardinal.mul_lt_aleph0_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b : Cardinal.{u_1}
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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 < ℵ₀
⊢ b < ℵ₀

Tactic:
hb
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 < ℵ₀
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
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c

Tactic:
lift b to ℕ using hb
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 < ℵ₀
⊢ c < ℵ₀

Tactic:
hc
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 < ℵ₀
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})
⊢ Dvd.dvd.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑b : Cardinal.{u_1}) ∨ (↑n : Cardinal.{u_1}) ∣ c

Tactic:
lift c to ℕ using hc
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b 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:
mod_cast h b c (mod_cast hbc)

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, congrArg, cast, Nat.cast, congr, Or, Eq.symm, Cardinal.nat_coe_dvd_iff._simp_2, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b 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:
exact mod_cast h b c (mod_cast hbc)

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, congrArg, cast, Nat.cast, Cardinal.nat_coe_dvd_iff._simp_2, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ b ≠ 0

Tactic:
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩

Premises used: Iff.mp, Cardinal.aleph0_le_mul_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ c ≠ 0

Tactic:
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩

Premises used: Iff.mp, Cardinal.aleph0_le_mul_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ ℵ₀ ≤ b ∨ ℵ₀ ≤ c

Tactic:
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩

Premises used: Iff.mp, Cardinal.aleph0_le_mul_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ b = 0 ∨ c = 0

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
hbc₁ : b = 0 ∨ c = 0
⊢ ℵ₀ ≤ b * c

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
hbc₁ : b = 0 ∨ c = 0
h'₁ : ℵ₀ ≤ b * c
⊢ b ≠ 0

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
hbc₁ : b = 0 ∨ c = 0
h'₁ : ℵ₀ ≤ b * c
hb₁ : b ≠ 0
⊢ c ≠ 0

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
hbc₁ : b = 0 ∨ c = 0
h'₁ : ℵ₀ ≤ b * c
hb₁ : b ≠ 0
hc₁ : c ≠ 0
⊢ ℵ₀ ≤ b ∨ ℵ₀ ≤ c

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
hbc₁ : b = 0 ∨ c = 0
h'₁ : ℵ₀ ≤ b * c
hb₁ : b ≠ 0
hc₁ : c ≠ 0
hℵ₁ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Premises used: zero_dvd_iff, mul_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h_1 : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b = 0 ∨ c = 0
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
inl : b = 0 → False
inr : c = 0 → False
⊢ False

Tactic:
cases hbc
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h_1 : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
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
h_2 : b = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n : ℕ
h_1 : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
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
h_2 : c = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
⊢ 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