simp [Eq.symm right, left]
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
left : y ∈ xs
right : (x, y) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs