no goals
ι : Type u_1
α : Type u_2
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
inst✝ : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support
simp (config := { contextual := true }) [subset_iff]