a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∨ p ∈ factors b
rw [mem_factors (mul_ne_zero ha hb), mem_factors ha, mem_factors hb, ← and_or_left]
no goals
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
simpa only [and_congr_right_iff] using Prime.dvd_mul