rw [List.get_product_fin_pair]
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ (L1 ×ˢ L2).get (Fin.cast ⋯ (left.pair right)) = (L1.get left, L2.get right)
case hp
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ ↑(Fin.cast ⋯ (left.pair right)) = ↑(left.pair right)