simp only [a1_right] at s1
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ map f xs_tl
⊢ x1 = x2
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ ys_tl
⊢ x1 = x2