case h => simp [this]
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ p < (map (fun b => (hd, b)) L2).length
no goals