α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ↑(↑(Finsupp.curry f) x) y = ↑f (x, y)
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
⊢ ↑(↑(Finsupp.curry f) x) y = ↑f (x, y)
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 [single_apply, ite_apply, Prod.ext_iff, ite_and]
  split_ifs <;> simp [single_apply, *]
case h₀
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ∀ (b : α × β), b ∈ f.support → b ≠ (x, y) → ↑(↑(single b.fst (single b.snd (↑f b))) x) y = 0

case h₁
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ¬(x, y) ∈ f.support → ↑(↑(single (x, y).fst (single (x, y).snd (↑f (x, y)))) x) y = 0
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ↑(↑(Finsupp.curry f) x) y = ↑f (x, y)
rw [Finsupp.curry, sum_apply, sum_apply, Finsupp.sum, Finset.sum_eq_single, this, if_pos rfl]
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ ↑(↑(single (b₁, b₂).fst (single (b₁, b₂).snd (↑f (b₁, b₂)))) x) y = if (b₁, b₂) = (x, y) then ↑f (b₁, b₂) else 0
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
⊢ ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
rintro ⟨b₁, b₂⟩
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
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
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
b₁ : α
b₂ : β
⊢ ↑(↑(single (b₁, b₂).fst (single (b₁, b₂).snd (↑f (b₁, b₂)))) x) y = if (b₁, b₂) = (x, y) then ↑f (b₁, b₂) else 0
simp [single_apply, ite_apply, Prod.ext_iff, ite_and]
no goals
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
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
split_ifs <;> simp [single_apply, *]
case h₀
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
b : α × β
a✝ : b ∈ f.support
b_ne : b ≠ (x, y)
⊢ ↑(↑(single b.fst (single b.snd (↑f b))) x) y = 0
case h₀
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ∀ (b : α × β), b ∈ f.support → b ≠ (x, y) → ↑(↑(single b.fst (single b.snd (↑f b))) x) y = 0
intro b _ b_ne
no goals
case h₀
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
b : α × β
a✝ : b ∈ f.support
b_ne : b ≠ (x, y)
⊢ ↑(↑(single b.fst (single b.snd (↑f b))) x) y = 0
rw [this b, if_neg b_ne]
case h₁
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
hxy : ¬(x, y) ∈ f.support
⊢ ↑(↑(single (x, y).fst (single (x, y).snd (↑f (x, y)))) x) y = 0
case h₁
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
⊢ ¬(x, y) ∈ f.support → ↑(↑(single (x, y).fst (single (x, y).snd (↑f (x, y)))) x) y = 0
intro hxy
no goals
case h₁
α : Type u_2
β : Type u_1
γ : Type ?u.528340
ι : Type ?u.528343
M : Type u_3
M' : Type ?u.528349
N : Type ?u.528352
P : Type ?u.528355
G : Type ?u.528358
H : Type ?u.528361
R : Type ?u.528364
S : Type ?u.528367
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α × β →₀ M
x : α
y : β
this : ∀ (b : α × β), ↑(↑(single b.fst (single b.snd (↑f b))) x) y = if b = (x, y) then ↑f b else 0
hxy : ¬(x, y) ∈ f.support
⊢ ↑(↑(single (x, y).fst (single (x, y).snd (↑f (x, y)))) x) y = 0
rw [this (x, y), if_pos rfl, not_mem_support_iff.mp hxy]