case inl
b p : ℕ
hab : coprime 0 b
⊢ p ∈ factors (0 * b) ↔ p ∈ factors 0 ∪ factors b

case inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
a b : ℕ
hab : coprime a b
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
rcases a.eq_zero_or_pos with (rfl | ha)
case inr.inl
a p : ℕ
ha : a > 0
hab : coprime a 0
⊢ p ∈ factors (a * 0) ↔ p ∈ factors a ∪ factors 0

case inr.inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
case inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
rcases b.eq_zero_or_pos with (rfl | hb)
no goals
case inr.inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
rw [mem_factors_mul ha.ne' hb.ne', List.mem_union]
no goals
case inl
b p : ℕ
hab : coprime 0 b
⊢ p ∈ factors (0 * b) ↔ p ∈ factors 0 ∪ factors b
simp [(coprime_zero_left _).mp hab]
no goals
case inr.inl
a p : ℕ
ha : a > 0
hab : coprime a 0
⊢ p ∈ factors (a * 0) ↔ p ∈ factors a ∪ factors 0
simp [(coprime_zero_right _).mp hab]