List.Mem as Or?

Stream: mathlib4

[Arien Malec]

In data.prod.tprod we have hj : j ∈ i :: l and then hj.resolve_left which seems like hj is being coerced to an or but I haven't been able to see where that coercion is happening in mathlib. Post mathport, this doesn't work at all. What's going on on in mathlib and what's the mathlib 4 equivalent?

[Chris Hughes]

The definition of j in i :: l in Lean3 is j=i or j in l. In lean4 the definition changed so you have to write (mem_cons.2 hj).resolve_left

[Arien Malec]

mem_cons.mp rather than mem_cons.mpr at it happens.