∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) [inst_1 : Decidable (Function.mulSupport f).Finite],
  ∏ᶠ (i : α), f i = if h : (Function.mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1