α : Type u_1
β : Type ?u.559184
γ : Type ?u.559187
ι : Type ?u.559190
M : Type ?u.559193
M' : Type ?u.559196
N : Type ?u.559199
P : Type ?u.559202
G : Type u_2
H : Type ?u.559208
R : Type ?u.559211
S : Type ?u.559214
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support
α : Type u_1
β : Type ?u.559184
γ : Type ?u.559187
ι : Type ?u.559190
M : Type ?u.559193
M' : Type ?u.559196
N : Type ?u.559199
P : Type ?u.559202
G : Type u_2
H : Type ?u.559208
R : Type ?u.559211
S : Type ?u.559214
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support
rw [sub_eq_add_neg, ← support_neg g]
no goals
α : Type u_1
β : Type ?u.559184
γ : Type ?u.559187
ι : Type ?u.559190
M : Type ?u.559193
M' : Type ?u.559196
N : Type ?u.559199
P : Type ?u.559202
G : Type u_2
H : Type ?u.559208
R : Type ?u.559211
S : Type ?u.559214
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support
exact support_add