∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι)
  (b : (x : ι) → a = x → M), (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1