rw [← prod_update_one_of_mem i.prop, ← prod_update_one_of_mem (mem_attach s i)]
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x in attach s \ {i}, f ↑x = ∏ x in s \ {↑i}, f x
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j = ∏ j in s, Function.update (fun x => f x) (↑i) 1 j