Lean4
/-- Given an element of the iterated product `l.Prod α`, take a projection into direction `i`.
If `i` appears multiple times in `l`, this chooses the first component in direction `i`. -/
protected def elim : ∀ {l : List ι} (_ : TProd α l) {i : ι} (_ : i ∈ l), α i
| i :: is, v, j, hj =>
if hji : j = i then by
subst hji
exact v.1
else TProd.elim v.2 ((List.mem_cons.mp hj).resolve_left hji)