-- Mathlib/Data/Finsupp/Basic.lean
theorem curry_apply (f : α × β →₀ M) (x : α) (y : β) : f.curry x y = f (x, y)

Proof state:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ ((single (b₁, b₂).1 (single (b₁, b₂).2 (f (b₁, b₂)))) x) y = if (b₁, b₂) = (x, y) then f (b₁, b₂) else 0

Tactic:
simp only [ne_eq, single_apply, Prod.ext_iff, ite_and]

Result:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ (if b₁ = x then single b₂ (f (b₁, b₂)) else 0) y = if b₁ = x then if b₂ = y then f (b₁, b₂) else 0 else 0

Proof state:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
a✝ : f (x, y) = 0
⊢ ((single (x, y).1 (single (x, y).2 0)) x) y = 0

Tactic:
rw [single_zero, single_zero, coe_zero, Pi.zero_apply, coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
b : α × β
a✝ : f b ≠ 0
b_ne : b ≠ (x, y)
⊢ ((single b.1 (single b.2 (f b))) x) y = 0

Tactic:
rw [this b, if_neg b_ne]

Result:
no goals

Proof state:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ ∀ (b : α × β), f b ≠ 0 → b ≠ (x, y) → ((single b.1 (single b.2 (f b))) x) y = 0

Tactic:
intro b _ b_ne

Result:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
b : α × β
a✝ : f b ≠ 0
b_ne : b ≠ (x, y)
⊢ ((single b.1 (single b.2 (f b))) x) y = 0

Proof state:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ f (x, y) = 0 → ((single (x, y).1 (single (x, y).2 0)) x) y = 0

Tactic:
intro _

Result:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
a✝ : f (x, y) = 0
⊢ ((single (x, y).1 (single (x, y).2 0)) x) y = 0

Proof state:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ (if b₁ = x then single b₂ (f (b₁, b₂)) else 0) y = if b₁ = x then if b₂ = y then f (b₁, b₂) else 0 else 0

Tactic:
split_ifs <;> simp [single_apply, *]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ (f.curry x) y = f (x, y)

Tactic:
rw [Finsupp.curry, sum_apply, sum_apply, sum_eq_single, this, if_pos rfl]

Result:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ ∀ (b : α × β), f b ≠ 0 → b ≠ (x, y) → ((single b.1 (single b.2 (f b))) x) y = 0

case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ f (x, y) = 0 → ((single (x, y).1 (single (x, y).2 0)) x) y = 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
⊢ ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0

Tactic:
rintro ⟨b₁, b₂⟩

Result:
case mk
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ ((single (b₁, b₂).1 (single (b₁, b₂).2 (f (b₁, b₂)))) x) y = if (b₁, b₂) = (x, y) then f (b₁, b₂) else 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
⊢ (f.curry x) y = f (x, y)

Tactic:
have : ∀ b : α × β, single b.fst (single b.snd (f b)) x y = if b = (x, y) then f b else 0 := by
  rintro ⟨b₁, b₂⟩
  simp only [ne_eq, single_apply, Prod.ext_iff, ite_and]
  split_ifs <;> simp [single_apply, *]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ((single b.1 (single b.2 (f b))) x) y = if b = (x, y) then f b else 0
⊢ (f.curry x) y = f (x, y)