no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type ?u.651010
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
⊢ δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
exact x
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(sigmaUncurry (single i (single j x))) { fst := i', snd := j' } =
    ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
⊢ sigmaUncurry (single i (single j x)) = single { fst := i, snd := j } x
ext ⟨i', j'⟩
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(sigmaUncurry (single i (single j x))) { fst := i', snd := j' } =
    ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(sigmaUncurry (single i (single j x))) { fst := i', snd := j' } =
    ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
dsimp only
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(↑(single i (single j x)) i') j' = ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(sigmaUncurry (single i (single j x))) { fst := i', snd := j' } =
    ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
rw [sigmaUncurry_apply]
case h.mk.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ↑(↑(single i (single j x)) i) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }

case h.mk.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ ↑(↑(single i (single j x)) i') j' = ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
case h.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ↑(↑(single i (single j x)) i') j' = ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
obtain rfl | hi := eq_or_ne i i'
case h.mk.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ↑(single j x) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }
case h.mk.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ↑(↑(single i (single j x)) i) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }
rw [single_eq_same]
case h.mk.inl.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
⊢ ↑(single j x) j = ↑(single { fst := i, snd := j } x) { fst := i, snd := j }

case h.mk.inl.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
hj : j ≠ j'
⊢ ↑(single j x) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }
case h.mk.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ↑(single j x) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }
obtain rfl | hj := eq_or_ne j j'
no goals
case h.mk.inl.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
⊢ ↑(single j x) j = ↑(single { fst := i, snd := j } x) { fst := i, snd := j }
rw [single_eq_same, single_eq_same]
case h.mk.inl.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
hj : j ≠ j'
⊢ { fst := i, snd := j } ≠ { fst := i, snd := j' }
case h.mk.inl.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
hj : j ≠ j'
⊢ ↑(single j x) j' = ↑(single { fst := i, snd := j } x) { fst := i, snd := j' }
rw [single_eq_of_ne hj, single_eq_of_ne]
no goals
case h.mk.inl.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
j' : α i
hj : j ≠ j'
⊢ { fst := i, snd := j } ≠ { fst := i, snd := j' }
simpa using hj
case h.mk.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ { fst := i, snd := j } ≠ { fst := i', snd := j' }
case h.mk.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ ↑(↑(single i (single j x)) i') j' = ↑(single { fst := i, snd := j } x) { fst := i', snd := j' }
rw [single_eq_of_ne hi, single_eq_of_ne, zero_apply]
no goals
case h.mk.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.651005
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : (i : ι) → (j : α i) → Zero (δ i j)
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ { fst := i, snd := j } ≠ { fst := i', snd := j' }
simp [hi]