case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ factors 0
⊢ p ∈ factors (0 * b)

case inr
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ factors (a * b)
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
⊢ p ∈ factors (a * b)
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inr
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ factors (a * b)
apply (mem_factors_mul ha hb).2 (Or.inl hpa)
no goals
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ factors 0
⊢ p ∈ factors (0 * b)
simp at hpa