generalize hleft : Fin.pair_left _ = left
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
⊢ (L1 ×ˢ L2).get i = (L1.get (Fin.cast ⋯ i).pair_left, L2.get (Fin.cast ⋯ i).pair_right)
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get (Fin.cast ⋯ i).pair_right)