no goals
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ support f \ support g ⊆ support (f - g)
simp (config := { contextual := true }) [subset_iff]