α : Type u_1
β : Type u_2
γ : Type ?u.552201
ι : Type ?u.552204
M : Type u_3
M' : Type ?u.552210
N : Type ?u.552213
P : Type ?u.552216
G : Type ?u.552219
H : Type ?u.552222
R : Type ?u.552225
S : Type ?u.552228
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (Finsupp.curry f).support ⊆ Finset.biUnion f.support fun a => {a.fst}
α : Type u_1
β : Type u_2
γ : Type ?u.552201
ι : Type ?u.552204
M : Type u_3
M' : Type ?u.552210
N : Type ?u.552213
P : Type ?u.552216
G : Type ?u.552219
H : Type ?u.552222
R : Type ?u.552225
S : Type ?u.552228
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (Finsupp.curry f).support ⊆ image Prod.fst f.support
rw [← Finset.biUnion_singleton]
α : Type u_1
β : Type u_2
γ : Type ?u.552201
ι : Type ?u.552204
M : Type u_3
M' : Type ?u.552210
N : Type ?u.552213
P : Type ?u.552216
G : Type ?u.552219
H : Type ?u.552222
R : Type ?u.552225
S : Type ?u.552228
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (Finset.biUnion f.support fun a => (single a.fst (single a.snd (↑f a))).support) ⊆
    Finset.biUnion f.support fun a => {a.fst}
α : Type u_1
β : Type u_2
γ : Type ?u.552201
ι : Type ?u.552204
M : Type u_3
M' : Type ?u.552210
N : Type ?u.552213
P : Type ?u.552216
G : Type ?u.552219
H : Type ?u.552222
R : Type ?u.552225
S : Type ?u.552228
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (Finsupp.curry f).support ⊆ Finset.biUnion f.support fun a => {a.fst}
refine' Finset.Subset.trans support_sum _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.552201
ι : Type ?u.552204
M : Type u_3
M' : Type ?u.552210
N : Type ?u.552213
P : Type ?u.552216
G : Type ?u.552219
H : Type ?u.552222
R : Type ?u.552225
S : Type ?u.552228
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (Finset.biUnion f.support fun a => (single a.fst (single a.snd (↑f a))).support) ⊆
    Finset.biUnion f.support fun a => {a.fst}
refine' Finset.biUnion_mono fun a _ => support_single_subset