α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
⊢ (∑ a in f.support, if p a.fst then single a.fst (single a.snd (↑(filter (fun a => p a.fst) f) a)) else 0) =
    ∑ a in f.support, filter p (single a.fst (single a.snd (↑f a)))
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
⊢ Finsupp.curry (filter (fun a => p a.fst) f) = filter p (Finsupp.curry f)
rw [Finsupp.curry, Finsupp.curry, Finsupp.sum, Finsupp.sum, filter_sum, support_filter,
  sum_filter]
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
⊢ ∀ (x : α × β),
    x ∈ f.support →
      (if p x.fst then single x.fst (single x.snd (↑(filter (fun a => p a.fst) f) x)) else 0) =
        filter p (single x.fst (single x.snd (↑f x)))
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
⊢ (∑ a in f.support, if p a.fst then single a.fst (single a.snd (↑(filter (fun a => p a.fst) f) a)) else 0) =
    ∑ a in f.support, filter p (single a.fst (single a.snd (↑f a)))
refine' Finset.sum_congr rfl _
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p (a₁, a₂).fst then single (a₁, a₂).fst (single (a₁, a₂).snd (↑(filter (fun a => p a.fst) f) (a₁, a₂))) else 0) =
    filter p (single (a₁, a₂).fst (single (a₁, a₂).snd (↑f (a₁, a₂))))
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
⊢ ∀ (x : α × β),
    x ∈ f.support →
      (if p x.fst then single x.fst (single x.snd (↑(filter (fun a => p a.fst) f) x)) else 0) =
        filter p (single x.fst (single x.snd (↑f x)))
rintro ⟨a₁, a₂⟩ _
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p a₁ then single a₁ (single a₂ (↑(filter (fun a => p a.fst) f) (a₁, a₂))) else 0) =
    filter p (single a₁ (single a₂ (↑f (a₁, a₂))))
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p (a₁, a₂).fst then single (a₁, a₂).fst (single (a₁, a₂).snd (↑(filter (fun a => p a.fst) f) (a₁, a₂))) else 0) =
    filter p (single (a₁, a₂).fst (single (a₁, a₂).snd (↑f (a₁, a₂))))
dsimp only
case mk.inl
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : p a₁
⊢ single a₁ (single a₂ (↑(filter (fun a => p a.fst) f) (a₁, a₂))) = filter p (single a₁ (single a₂ (↑f (a₁, a₂))))

case mk.inr
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : ¬p a₁
⊢ 0 = filter p (single a₁ (single a₂ (↑f (a₁, a₂))))
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p a₁ then single a₁ (single a₂ (↑(filter (fun a => p a.fst) f) (a₁, a₂))) else 0) =
    filter p (single a₁ (single a₂ (↑f (a₁, a₂))))
split_ifs with h
no goals
case mk.inl
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : p a₁
⊢ single a₁ (single a₂ (↑(filter (fun a => p a.fst) f) (a₁, a₂))) = filter p (single a₁ (single a₂ (↑f (a₁, a₂))))
rw [filter_apply_pos, filter_single_of_pos] <;> exact h
no goals
case mk.inr
α : Type u_2
β : Type u_1
γ : Type ?u.549060
ι : Type ?u.549063
M : Type u_3
M' : Type ?u.549069
N : Type ?u.549072
P : Type ?u.549075
G : Type ?u.549078
H : Type ?u.549081
R : Type ?u.549084
S : Type ?u.549087
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
p : α → Prop
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : ¬p a₁
⊢ 0 = filter p (single a₁ (single a₂ (↑f (a₁, a₂))))
rwa [filter_single_of_neg]