no goals
α : Type u_1
β : Type ?u.5479
γ : Type ?u.5482
M : Type u_2
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x : α, f x = f a * f b
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;>
  exact fun hc => (hc (Finset.mem_univ _)).elim