p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ Int.natAbs a ∨ p ∣ Int.natAbs b
⊢ ↑p ∣ a ∨ ↑p ∣ b
p : ℕ
hp : Prime p
a b : ℤ
h : ↑p ∣ a * b
⊢ ↑p ∣ a ∨ ↑p ∣ b
rw [← Int.dvd_natAbs, Int.coe_nat_dvd, Int.natAbs_mul, hp.dvd_mul] at h
no goals
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ Int.natAbs a ∨ p ∣ Int.natAbs b
⊢ ↑p ∣ a ∨ ↑p ∣ b
rwa [← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
no goals
p : ℕ
hp : _root_.Prime ↑p
h : p = 1
⊢ False
simp [h, not_prime_one] at hp
no goals
p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
simpa only [Int.coe_nat_dvd, (Int.ofNat_mul _ _).symm] using hp.2.2 a b