no goals
ι : Type ?u.859388
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommGroup β
inst✝ : DecidableEq α
a : α
h : a ∈ s
⊢ ∏ x in erase s a, f x = (∏ x in s, f x) / f a
rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]