no goals
α : Type ?u.174780
β : Type ?u.174783
ι : Type ?u.174786
G : Type ?u.174789
M : Type u_1
N : Type ?u.174795
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
⊢ (∏ᶠ (_ : f a ≠ 1), f a) = f a
rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]