case mk
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ ↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n) =
    Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
a : (i : ι) × η i
n : N
⊢ ↑sigmaFinsuppEquivDfinsupp (single a n) = Dfinsupp.single a.fst (single a.snd n)
obtain ⟨i, a⟩ := a
case mk.h.h
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
case mk
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ ↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n) =
    Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)
ext (j b)
case pos
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b

case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
case mk.h.h
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
by_cases h : i = j
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
suffices Finsupp.single (⟨i, a⟩ : Σi, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
have H : (⟨i, a⟩ : Σi, η i) ≠ ⟨j, b⟩ := by simp [h]
no goals
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
classical rw [Finsupp.single_apply, if_neg H]
case pos
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
case pos
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
subst h
no goals
case pos
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
classical simp [split_apply, Finsupp.single_apply]
no goals
case pos
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
simp [split_apply, Finsupp.single_apply]
no goals
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this : ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(Dfinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
simp [split_apply, dif_neg h, this]
no goals
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ { fst := i, snd := a } ≠ { fst := j, snd := b }
simp [h]
no goals
case neg
ι : Type u_1
R : Type ?u.70785
M : Type ?u.70788
η : ι → Type u_3
N : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
rw [Finsupp.single_apply, if_neg H]