[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ IsUnit a ↔ a = 1
[PROOFSTEP]
refine'
  ⟨fun h => _, by
    rintro rfl
    exact isUnit_one⟩
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ a = 1 → IsUnit a
[PROOFSTEP]
rintro rfl
[GOAL]
b : Cardinal.{u}
n m : ℕ
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
a b : Cardinal.{u}
n m : ℕ
h : IsUnit a
⊢ a = 1
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
b : Cardinal.{u}
n m : ℕ
h : IsUnit 0
⊢ 0 = 1
[PROOFSTEP]
exact (not_isUnit_zero h).elim
[GOAL]
case inr
a b : Cardinal.{u}
n m : ℕ
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
[PROOFSTEP]
rw [isUnit_iff_forall_dvd] at h 
[GOAL]
case inr
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1
[PROOFSTEP]
cases' h 1 with t ht
[GOAL]
case inr.intro
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
⊢ a = 1
[PROOFSTEP]
rw [eq_comm, mul_eq_one_iff'] at ht 
[GOAL]
case inr.intro
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1
[PROOFSTEP]
exact ht.1
[GOAL]
case inr.intro.ha
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a
[PROOFSTEP]
exact one_le_iff_ne_zero.mpr ha
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
[PROOFSTEP]
apply one_le_iff_ne_zero.mpr
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ t ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ False
[PROOFSTEP]
rw [h, mul_zero] at ht 
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 0 = 1
h : t = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one ht
[GOAL]
a✝ b✝ : Cardinal.{u}
n m : ℕ
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
⊢ a ≤ x
[PROOFSTEP]
simpa only [hab, mul_one] using
  mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab )) a
[GOAL]
a✝ b✝ : Cardinal.{u}
n m : ℕ
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
h : b = 0
⊢ x = 0
[PROOFSTEP]
rwa [h, mul_zero] at hab 
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ Prime a
[PROOFSTEP]
refine' ⟨(aleph0_pos.trans_le ha).ne', _, fun b c hbc => _⟩
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a
[PROOFSTEP]
rw [isUnit_iff]
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬a = 1
[PROOFSTEP]
exact (one_lt_aleph0.trans_le ha).ne'
[GOAL]
case refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases' eq_or_ne (b * c) 0 with hz hz
[GOAL]
case refine'_2.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
rcases mul_eq_zero.mp hz with (rfl | rfl)
[GOAL]
case refine'_2.inl.inl
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inl.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
wlog h : c ≤ b
[GOAL]
case refine'_2.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases le_total c b <;> [skip; rw [or_comm]]
[GOAL]
case refine'_2.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases le_total c b
[GOAL]
case refine'_2.inr.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
skip
[GOAL]
case refine'_2.inr.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
rw [or_comm]
[GOAL]
case refine'_2.inr.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
apply_assumption
[GOAL]
case refine'_2.inr.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c ∨ a ∣ b
[PROOFSTEP]
apply_assumption
[GOAL]
case refine'_2.inr.inr.inl.b
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ Cardinal.{u}
case refine'_2.inr.inr.inl.n
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inl.m
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inl.ha
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℵ₀ ≤ a
case refine'_2.inr.inr.inl.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ a ∣ b * c
case refine'_2.inr.inr.inl.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ b * c ≠ 0
case refine'_2.inr.inr.inl.h
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ c ≤ b
case refine'_2.inr.inr.inr.b
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ Cardinal.{u}
case refine'_2.inr.inr.inr.n
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inr.m
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inr.ha
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℵ₀ ≤ a
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
case refine'_2.inr.inr.inr.h
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ b ≤ c
[PROOFSTEP]
assumption'
[GOAL]
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
[PROOFSTEP]
all_goals rwa [mul_comm]
[GOAL]
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
left
[GOAL]
case h
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b
[PROOFSTEP]
have habc := le_of_dvd hz hbc
[GOAL]
case h
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b
[PROOFSTEP]
rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc 
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a
[PROOFSTEP]
rw [irreducible_iff, not_and_or]
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
[PROOFSTEP]
refine' Or.inr fun h => _
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
[PROOFSTEP]
simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using h a ℵ₀
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m
[PROOFSTEP]
refine' ⟨_, fun ⟨h, ht⟩ => ⟨h, by exact_mod_cast ht⟩⟩
[GOAL]
a b : Cardinal.{u}
n m : ℕ
x✝ : n ∣ m
h : ℕ
ht : m = n * h
⊢ ↑m = ↑n * ↑h
[PROOFSTEP]
exact_mod_cast ht
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
⊢ n ∣ m
[PROOFSTEP]
have : ↑m < ℵ₀ := nat_lt_aleph0 m
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
rw [hk, mul_lt_aleph0_iff] at this 
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
rcases this with (h | h | ⟨-, hk'⟩)
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk ; simp [hk]
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk 
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
h : ↑n = 0
hk : m = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp [hk]
[GOAL]
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk 
[GOAL]
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
h : k = 0
hk : m = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp [hk]
[GOAL]
case intro.inr.inr.intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
lift k to ℕ using hk'
[GOAL]
case intro.inr.inr.intro.intro
a b : Cardinal.{u}
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m
[PROOFSTEP]
exact ⟨k, by exact_mod_cast hk⟩
[GOAL]
a b : Cardinal.{u}
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ m = n * k
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ Prime ↑n ↔ Nat.Prime n
[PROOFSTEP]
simp only [Prime, Nat.prime_iff]
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ (↑n ≠ 0 ∧ ¬IsUnit ↑n ∧ ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b) ↔
    n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
[PROOFSTEP]
refine' and_congr (by simp) (and_congr _ ⟨fun h b c hbc => _, fun h b c hbc => _⟩)
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
⊢ ¬IsUnit ↑n ↔ ¬IsUnit n
[PROOFSTEP]
simp only [isUnit_iff, Nat.isUnit_iff]
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
⊢ ¬↑n = 1 ↔ ¬n = 1
[PROOFSTEP]
exact_mod_cast Iff.rfl
[GOAL]
case refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b
b c : ℕ
hbc : n ∣ b * c
⊢ n ∣ b ∨ n ∣ c
[PROOFSTEP]
exact_mod_cast h b c (by exact_mod_cast hbc)
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b
b c : ℕ
hbc : n ∣ b * c
⊢ ↑n ∣ ↑b * ↑c
[PROOFSTEP]
exact_mod_cast hbc
[GOAL]
case refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
cases' lt_or_le (b * c) ℵ₀ with h' h'
[GOAL]
case refine'_3.inl
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
[GOAL]
case refine'_3.inl.inl
a b : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hbc : ↑n ∣ 0 * c
h' : 0 * c < ℵ₀
⊢ ↑n ∣ 0 ∨ ↑n ∣ c
[PROOFSTEP]
simp
[GOAL]
case refine'_3.inl.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b : Cardinal.{u_1}
hbc : ↑n ∣ b * 0
h' : b * 0 < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_3.inl.inr.inr.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
lift b to ℕ using hb
[GOAL]
case refine'_3.inl.inr.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hc : c < ℵ₀
b : ℕ
hbc : ↑n ∣ ↑b * c
h' : ↑b * c < ℵ₀
⊢ ↑n ∣ ↑b ∨ ↑n ∣ c
[PROOFSTEP]
lift c to ℕ using hc
[GOAL]
case refine'_3.inl.inr.inr.intro.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : ℕ
hbc : ↑n ∣ ↑b * ↑c
h' : ↑b * ↑c < ℵ₀
⊢ ↑n ∣ ↑b ∨ ↑n ∣ ↑c
[PROOFSTEP]
exact_mod_cast h b c (by exact_mod_cast hbc)
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : ℕ
hbc : ↑n ∣ ↑b * ↑c
h' : ↑b * ↑c < ℵ₀
⊢ n ∣ b * c
[PROOFSTEP]
exact_mod_cast hbc
[GOAL]
case refine'_3.inr
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
[GOAL]
case refine'_3.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
have hn : (n : Cardinal) ≠ 0 := by
  intro h
  rw [h, zero_dvd_iff, mul_eq_zero] at hbc 
  cases hbc <;> contradiction
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ≠ 0
[PROOFSTEP]
intro h
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False
[PROOFSTEP]
rw [h, zero_dvd_iff, mul_eq_zero] at hbc 
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h✝ : ∀ (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 : ↑n = 0
⊢ False
[PROOFSTEP]
cases hbc
[GOAL]
case inl
a b✝ : Cardinal.{u}
n m : ℕ
h✝¹ : ∀ (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 : ↑n = 0
h✝ : b = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case inr
a b✝ : Cardinal.{u}
n m : ℕ
h✝¹ : ∀ (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 : ↑n = 0
h✝ : c = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case refine'_3.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
wlog hℵ₀b : ℵ₀ ≤ b
[GOAL]
case refine'_3.inr.intro.intro.inr
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
refine' (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_1
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_1
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℕ
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℕ
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rwa [mul_comm] at hbc 
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rwa [mul_comm] at h' 
[GOAL]
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
exact Or.inl (dvd_of_le_of_aleph0_le hn ((nat_lt_aleph0 n).le.trans hℵ₀b) hℵ₀b)
[GOAL]
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with h h
[GOAL]
case inl
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
simp [h]
[GOAL]
case inr
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
lift a to ℕ using id h
[GOAL]
case inr.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
simp [not_le.mpr h]
[GOAL]
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
by_cases h : ℵ₀ ≤ a
[GOAL]
case pos
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simp [h, (prime_of_aleph0_le h).isPrimePow]
[GOAL]
case neg
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simp only [h, Nat.cast_inj, exists_eq_left', false_or_iff, isPrimePow_nat_iff]
[GOAL]
case neg
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ∃ n, a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
lift a to ℕ using not_le.mp h
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [isPrimePow_def]
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' ⟨_, fun ⟨n, han, p, k, hp, hk, h⟩ => ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact_mod_cast h⟩⟩
[GOAL]
a✝ b : Cardinal.{u}
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑a
[PROOFSTEP]
rw [han]
[GOAL]
a✝ b : Cardinal.{u}
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) → ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, hpk⟩
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
have key : p ^ 1 ≤ ↑a := by rw [← hpk]; apply power_le_power_left hp.ne_zero; exact_mod_cast hk
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ ↑a
[PROOFSTEP]
rw [← hpk]
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k
[PROOFSTEP]
apply power_le_power_left hp.ne_zero
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ 1 ≤ ↑k
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ^ 1 ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [power_one] at key 
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
lift p to ℕ using key.trans_lt (nat_lt_aleph0 a)
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ p ^ k = a
[PROOFSTEP]
exact_mod_cast hpk
