no goals
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ i :: l
hji : j ≠ i
v : TProd α (i :: l)
⊢ TProd.elim v hj = TProd.elim v.snd (_ : j ∈ l)
simp [TProd.elim, hji]