case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.604100
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
⊢ ↑(↑(sigmaCurry 0) i) j = ↑(↑0 i) j
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.604100
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
⊢ sigmaCurry 0 = 0
ext (i j)
case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.604100
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
⊢ ↑0 { fst := i, snd := j } = ↑(↑0 i) j
case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.604100
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
⊢ ↑(↑(sigmaCurry 0) i) j = ↑(↑0 i) j
rw [sigmaCurry_apply]
no goals
case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.604100
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
⊢ ↑0 { fst := i, snd := j } = ↑(↑0 i) j
rfl