simp only [erase_eq]
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in erase (attach s) i, f ↑j = ∏ j in erase s ↑i, f j
ι : 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