α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum (sum f fun p c => single p.fst (single p.snd c)) fun a f => sum f (g a)) = sum f fun p c => g p.fst p.snd c
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum (Finsupp.curry f) fun a f => sum f (g a)) = sum f fun p c => g p.fst p.snd c
rw [Finsupp.curry]
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum (sum f fun p c => single p.fst (single p.snd c)) fun a f => sum f (g a)) = ?m.540167

α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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.540167 = sum f fun p c => g p.fst p.snd c

α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum (sum f fun p c => single p.fst (single p.snd c)) fun a f => sum f (g a)) = sum f fun p c => g p.fst p.snd c
trans
case e_g
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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 => sum (single a.fst (single a.snd b)) fun a f => sum f (g a)) = fun p c => g p.fst p.snd c
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum f fun a b => sum (single a.fst (single a.snd b)) fun a f => sum f (g a)) = sum f fun p c => g p.fst p.snd c
congr
case e_g.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
⊢ (sum (single p.fst (single p.snd c)) fun a f => sum f (g a)) = g p.fst p.snd c
case e_g
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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 => sum (single a.fst (single a.snd b)) fun a f => sum f (g a)) = fun p c => g p.fst p.snd c
funext p c
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
⊢ (sum (single p.fst (single p.snd c)) fun a f => sum f (g a)) = ?m.541818

α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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.541818 = g p.fst p.snd c

α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
case e_g.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
⊢ (sum (single p.fst (single p.snd c)) fun a f => sum f (g a)) = g p.fst p.snd c
trans
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
⊢ sum (single p.snd c) (g p.fst) = g p.fst p.snd c
exact sum_single_index (hg₀ _ _)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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₁
⊢ (sum (sum f fun p c => single p.fst (single p.snd c)) fun a f => sum f (g a)) = ?m.540167
exact
  sum_sum_index (fun a => sum_zero_index) fun a b₀ b₁ =>
    sum_add_index' (fun a => hg₀ _ _) fun c d₀ d₁ => hg₁ _ _ _ _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.536703
ι : Type ?u.536706
M : Type u_3
M' : Type ?u.536712
N : Type u_4
P : Type ?u.536718
G : Type ?u.536721
H : Type ?u.536724
R : Type ?u.536727
S : Type ?u.536730
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
⊢ (sum (single p.fst (single p.snd c)) fun a f => sum f (g a)) = ?m.541818
exact sum_single_index sum_zero_index