ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
x_eq_y :
  get l { val := indexOf x l, isLt := (_ : indexOf x l < length l) } =
    get l { val := indexOf y l, isLt := (_ : indexOf y l < length l) }
⊢ x = y
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
⊢ x = y
have x_eq_y :
    get l ⟨indexOf x l, indexOf_lt_length.2 hx⟩ =
    get l ⟨indexOf y l, indexOf_lt_length.2 hy⟩ := by
  simp only [h]
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
x_eq_y : x = y
⊢ x = y
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
x_eq_y :
  get l { val := indexOf x l, isLt := (_ : indexOf x l < length l) } =
    get l { val := indexOf y l, isLt := (_ : indexOf y l < length l) }
⊢ x = y
simp only [indexOf_get] at x_eq_y
no goals
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
x_eq_y : x = y
⊢ x = y
exact x_eq_y
no goals
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : indexOf x l = indexOf y l
⊢ get l { val := indexOf x l, isLt := (_ : indexOf x l < length l) } =
    get l { val := indexOf y l, isLt := (_ : indexOf y l < length l) }
simp only [h]
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x : α
hx hy : x ∈ l
⊢ indexOf x l = indexOf x l
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : x = y
⊢ indexOf x l = indexOf y l
subst h
no goals
ι : Type ?u.94752
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x : α
hx hy : x ∈ l
⊢ indexOf x l = indexOf x l
rfl