∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoidWithZero M] {f g : α → M}
  (this : Fintype ↑(Function.mulSupport f ∪ Function.mulSupport g)),
  Function.mulSupport f ⊆ ↑(Function.mulSupport f ∪ Function.mulSupport g).toFinset