simp [prod_update_of_mem hi]
ι : Type u_1
β : Type u
α : Type v
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
hi : i ∈ s
f : α → β
⊢ ∏ j in s, Function.update f i 1 j = ∏ j in s \ {i}, f j
no goals