simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ (fst✝, b) ∈ List.map (Prod.mk a) lb → ¬(fst✝, b) ∈ List.product la lb
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ b ∈ lb → a = fst✝ → ¬(fst✝ ∈ la ∧ b ∈ lb)