case mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
⊢ sigmaCurry (single { fst := i, snd := j } x) = single { fst := i, snd := j }.fst (single { fst := i, snd := j }.snd x)
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ ij.fst ij.snd
⊢ sigmaCurry (single ij x) = single ij.fst (single ij.snd x)
obtain ⟨i, j⟩ := ij
case mk.h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
i' : ι
j' : α i'
⊢ ↑(↑(sigmaCurry (single { fst := i, snd := j } x)) i') j' =
    ↑(↑(single { fst := i, snd := j }.fst (single { fst := i, snd := j }.snd x)) i') j'
case mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
⊢ sigmaCurry (single { fst := i, snd := j } x) = single { fst := i, snd := j }.fst (single { fst := i, snd := j }.snd x)
ext (i' j')
case mk.h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
i' : ι
j' : α i'
⊢ ↑(↑(sigmaCurry (single { fst := i, snd := j } x)) i') j' = ↑(↑(single i (single j x)) i') j'
case mk.h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
i' : ι
j' : α i'
⊢ ↑(↑(sigmaCurry (single { fst := i, snd := j } x)) i') j' =
    ↑(↑(single { fst := i, snd := j }.fst (single { fst := i, snd := j }.snd x)) i') j'
dsimp only
case mk.h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
i' : ι
j' : α i'
⊢ ↑(single { fst := i, snd := j } x) { fst := i', snd := j' } = ↑(↑(single i (single j x)) i') j'
case mk.h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
i' : ι
j' : α i'
⊢ ↑(↑(sigmaCurry (single { fst := i, snd := j } x)) i') j' = ↑(↑(single i (single j x)) i') j'
rw [sigmaCurry_apply]
case mk.h.h.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.625564
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ { fst := i, snd := j }.fst { fst := i, snd := j }.snd
j' : α i
⊢ ↑(single { fst := i, snd := j } x) { fst := i, snd := j' } = ↑(↑(single i (single j x)) i) j'

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

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