no goals
ι : Type ?u.270424
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ ∏ x in {a, b}, f x = f a * f b
rw [prod_insert (not_mem_singleton.2 h), prod_singleton]