case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ (factorization (a * b)).support ↔ q ∈ (factorization a).support ∪ (factorization b).support
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (factorization (a * b)).support = (factorization a).support ∪ (factorization b).support
ext q
case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ factors (a * b) ↔ q ∈ factors a ∨ q ∈ factors b
case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ (factorization (a * b)).support ↔ q ∈ (factorization a).support ∪ (factorization b).support
simp only [Finset.mem_union, factor_iff_mem_factorization]
no goals
case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ factors (a * b) ↔ q ∈ factors a ∨ q ∈ factors b
exact mem_factors_mul ha hb