case pos
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j

case neg
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
by_cases hji : j = i
case pos
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ TProd.elim (TProd.mk (j :: is) f) hj = f j
case pos
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
subst hji
no goals
case pos
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ TProd.elim (TProd.mk (j :: is) f) hj = f j
simp
no goals
case neg
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]