-- Mathlib/Data/Finsupp/Basic.lean
theorem sum_curry_index (f : α × β →₀ M) (g : α → β → M → N) (hg₀ : ∀ a b, g a b 0 = 0)
    (hg₁ : ∀ a b c₀ c₁, g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
    (f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ (f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c

Tactic:
rw [Finsupp.curry]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ ((f.sum fun p c => single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c

Proof state:
case e_g.h.h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ ((single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = g p.1 p.2 c

Tactic:
trans

Result:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ ((single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = ?m.213211

α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ ?m.213211 = g p.1 p.2 c

α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ N

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ (single p.2 c).sum (g p.1) = g p.1 p.2 c

Tactic:
exact sum_single_index (hg₀ _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ (f.sum fun a b => (single a.1 (single a.2 b)).sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c

Tactic:
congr

Result:
case e_g
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ (fun a b => (single a.1 (single a.2 b)).sum fun a f => f.sum (g a)) = fun p c => g p.1 p.2 c

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ ((single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = ?m.213211

Tactic:
exact sum_single_index sum_zero_index

Result:
no goals

Proof state:
case e_g
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ (fun a b => (single a.1 (single a.2 b)).sum fun a f => f.sum (g a)) = fun p c => g p.1 p.2 c

Tactic:
funext p c

Result:
case e_g.h.h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
p : α × β
c : M
⊢ ((single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = g p.1 p.2 c

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ ((f.sum fun p c => single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = ?m.212084

Tactic:
exact
  sum_sum_index (fun a => sum_zero_index) fun a b₀ b₁ =>
    sum_add_index' (fun a => hg₀ _ _) fun c d₀ d₁ => hg₁ _ _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ ((f.sum fun p c => single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c

Tactic:
trans

Result:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ ((f.sum fun p c => single p.1 (single p.2 c)).sum fun a f => f.sum (g a)) = ?m.212084

α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ ?m.212084 = f.sum fun p c => g p.1 p.2 c

α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
hg₀ : ∀ (a : α) (b : β), g a b 0 = 0
hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁
⊢ N