induction la with
| nil => exact .nil
| cons a la IH =>
  specialize IH la_nodup.tail
  conv =>
    arg 1
    dsimp [List.product, List.bind]
    change lb.map (Prod.mk a) ++ la.product lb
  refine Nodup.append ?_ IH ?_
  . apply lb_nodup.map
    intro b₁ b₂; exact congrArg Prod.snd
  . intro x
    let ⟨_,b⟩ := x
    simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
    intro _ ha h; cases ha
    exact la_nodup.head h.1
α : Type u
β : Type v
la : List α
lb : List β
la_nodup : Nodup la
lb_nodup : Nodup lb
⊢ Nodup (List.product la lb)
no goals