case inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
⊢ Finset.prod (toFinset (factors (gcd m 0))) f * Finset.prod (toFinset (factors (m * 0))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors 0)) f

case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
rcases eq_or_ne n 0 with (rfl | hm0)
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd 0 n))) f * Finset.prod (toFinset (factors (0 * n))) f =
    Finset.prod (toFinset (factors 0)) f * Finset.prod (toFinset (factors n)) f

case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
rcases eq_or_ne m 0 with (rfl | hn0)
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (m * n))) f * Finset.prod (toFinset (factors (gcd m n))) f =
    (∏ x in toFinset (factors m) ∪ toFinset (factors n), f x) * ∏ x in toFinset (factors m) ∩ toFinset (factors n), f x
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
rw [← @Finset.prod_union_inter _ _ m.factors.toFinset n.factors.toFinset, mul_comm]
case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (m * n)) = toFinset (factors m) ∪ toFinset (factors n)

case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (gcd m n)) = toFinset (factors m) ∩ toFinset (factors n)
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (m * n))) f * Finset.prod (toFinset (factors (gcd m n))) f =
    (∏ x in toFinset (factors m) ∪ toFinset (factors n), f x) * ∏ x in toFinset (factors m) ∩ toFinset (factors n), f x
congr
no goals
case inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
⊢ Finset.prod (toFinset (factors (gcd m 0))) f * Finset.prod (toFinset (factors (m * 0))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors 0)) f
simp
no goals
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd 0 n))) f * Finset.prod (toFinset (factors (0 * n))) f =
    Finset.prod (toFinset (factors 0)) f * Finset.prod (toFinset (factors n)) f
simp
no goals
case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (m * n)) = toFinset (factors m) ∪ toFinset (factors n)
apply factors_mul_toFinset <;> assumption
no goals
case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (gcd m n)) = toFinset (factors m) ∩ toFinset (factors n)
simp only [← support_factorization, factorization_gcd hn0 hm0, Finsupp.support_inf]