Theorem: Finset.prod_update_one_of_mem (ForML/FDerivProd.lean)

State before:
ι : 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
Tactic:
simp [prod_update_of_mem hi]
State after:
no goals