no goals
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support
simp (config := { contextual := true }) only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
  Ne.def, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]