a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
⊢ a ∣ b
a b : ℕ
⊢ (∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p) ↔ a ∣ b
refine' ⟨fun h => _, fun hab p => ord_compl_dvd_ord_compl_of_dvd hab p⟩
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p
⊢ a ∣ 0

case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
⊢ a ∣ b
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
⊢ a ∣ b
rcases eq_or_ne b 0 with (rfl | hb0)
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b

case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
⊢ a ∣ b
by_cases pa : a.Prime
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b

case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
case neg => simpa [pa] using h a
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b

case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b
by_cases pb : b.Prime
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b

case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
case neg => simpa [pb] using h b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b
rw [prime_dvd_prime_iff_eq pa pb]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b
by_contra hab
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False
apply pa.ne_one
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]
no goals
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b
no goals
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p
⊢ a ∣ 0
simp
no goals
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
simpa [pa] using h a
no goals
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
simpa [pb] using h b