-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_curry (f : α × β →₀ M) (p : α → Prop) [DecidablePred p] :
    (f.filter fun a : α × β => p a.1).curry = f.curry.filter p

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ x ∈ f.support,
    (if p x.1 then single x.1 (single x.2 ((filter (fun a => p a.1) f) x)) else 0) =
      filter p (single x.1 (single x.2 (f x)))

Tactic:
rintro ⟨a₁, a₂⟩ _

Result:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p (a₁, a₂).1 then single (a₁, a₂).1 (single (a₁, a₂).2 ((filter (fun a => p a.1) f) (a₁, a₂))) else 0) =
    filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (∑ a ∈ f.support, if p a.1 then single a.1 (single a.2 ((filter (fun a => p a.1) f) a)) else 0) =
    ∑ a ∈ f.support, filter p (single a.1 (single a.2 (f a)))

Tactic:
refine Finset.sum_congr rfl ?_

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ x ∈ f.support,
    (if p x.1 then single x.1 (single x.2 ((filter (fun a => p a.1) f) x)) else 0) =
      filter p (single x.1 (single x.2 (f x)))

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter (fun a => p a.1) f).curry = filter p f.curry

Tactic:
rw [Finsupp.curry, Finsupp.curry, Finsupp.sum, Finsupp.sum, filter_sum, support_filter,
  sum_filter]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (∑ a ∈ f.support, if p a.1 then single a.1 (single a.2 ((filter (fun a => p a.1) f) a)) else 0) =
    ∑ a ∈ f.support, filter p (single a.1 (single a.2 (f a)))

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : ¬p (a₁, a₂).1
⊢ 0 = filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))

Tactic:
rwa [filter_single_of_neg]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : p (a₁, a₂).1
⊢ single (a₁, a₂).1 (single (a₁, a₂).2 ((filter (fun a => p a.1) f) (a₁, a₂))) =
    filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))

Tactic:
rw [filter_apply_pos, filter_single_of_pos] <;> exact h

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
⊢ (if p (a₁, a₂).1 then single (a₁, a₂).1 (single (a₁, a₂).2 ((filter (fun a => p a.1) f) (a₁, a₂))) else 0) =
    filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : p (a₁, a₂).1
⊢ single (a₁, a₂).1 (single (a₁, a₂).2 ((filter (fun a => p a.1) f) (a₁, a₂))) =
    filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a₁ : α
a₂ : β
a✝ : (a₁, a₂) ∈ f.support
h : ¬p (a₁, a₂).1
⊢ 0 = filter p (single (a₁, a₂).1 (single (a₁, a₂).2 (f (a₁, a₂))))