no goals
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Finset γ
f : γ → α
g : γ → β
this : DecidableEq γ
⊢ ∀ ⦃a : γ⦄ {s : Finset γ},
    ¬a ∈ s →
      (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x) →
        (∏ x in insert a s, f x, ∏ x in insert a s, g x) = ∏ x in insert a s, (f x, g x)
simp (config := { contextual := true }) [Prod.ext_iff]