Cannot find instance

Stream: general

[AHan]

In mathlib/data/finsupp.lean the instance has_add of finsupp structure was already proved,
but in t he following example, it failed to synthesize type class instance for has_add...
Don't understand what instance I missed...

import data.finsupp
variables {α : Type*} {β : Type*} [has_zero α] [has_zero β] [add_monoid α] [add_monoid β]
variables [decidable_eq α] [decidable_eq β]

lemma support_contain_a' (a b : α →₀ β) : a.support ⊆ (a + b).support := sorry