∀ {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
  (s : Finset ι) (f : ι → κ → M₀), (Function.support fun j => ∏ i ∈ s, f i j) = ⋂ i ∈ s, Function.support (f i)