-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem sigmaFinsuppEquivDFinsupp_single [DecidableEq ι] [Zero N] (a : Σi, η i) (n : N) :
    sigmaFinsuppEquivDFinsupp (Finsupp.single a n) =
      @DFinsupp.single _ (fun i => η i →₀ N) _ _ a.1 (Finsupp.single a.2 n)

Proof state:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Tactic:
rw [Finsupp.single_apply, if_neg H]

Result:
no goals

Proof state:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Tactic:
classical rw [Finsupp.single_apply, if_neg H]

Result:
no goals

Proof state:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Tactic:
have H : (⟨i, a⟩ : Σi, η i) ≠ ⟨j, b⟩ := by simp [h]

Result:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Proof state:
case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
subst h

Result:
case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) i) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) i) b

Proof state:
case mk
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n) = DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)

Tactic:
ext j b

Result:
case mk.h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Proof state:
case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) i) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) i) b

Tactic:
simp [split_apply, Finsupp.single_apply]

Result:
no goals

Proof state:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
suffices Finsupp.single (⟨i, a⟩ : Σi, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]

Result:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ⟨i, a⟩ ≠ ⟨j, b⟩

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this : (single ⟨i, a⟩ n) ⟨j, b⟩ = 0
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
simp [split_apply, dif_neg h, this]

Result:
no goals

Proof state:
case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) i) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) i) b

Tactic:
classical simp [split_apply, Finsupp.single_apply]

Result:
no goals

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
a : (i : ι) × η i
n : N
⊢ sigmaFinsuppEquivDFinsupp (single a n) = DFinsupp.single a.fst (single a.snd n)

Tactic:
obtain ⟨i, a⟩ := a

Result:
case mk
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n) = DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)

Proof state:
case mk.h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
by_cases h : i = j

Result:
case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b