no goals
ι : Type ?u.795937
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : a ∈ s
⊢ (∏ x in erase s a, f x) * f a = ∏ x in s, f x
rw [mul_comm, mul_prod_erase s f h]