Lemmas allowing locating an element based on index in a List

Stream: mathlib4

[Zhuanhao Wu]

Given a Nodup List l and two elements i and j that are both members of the list, we know that we can split l into l = fr ++ j :: tail. Assume i's index is less than j in l, we can be sure that i is in fr. This can be stated in the attached lemma.

I'm wondering if there is a way to get this result within one/two steps; if not is it worth adding to mathlib?

The context is that I need to construct a swap of two elements in a list based off their indices.

lemma List.mem_front_of_index {α: Type*} [DecidableEq α]
  (l fr jtail: List α)
  (i j: α)
  (h_nd: List.Nodup (fr ++ j :: jtail))
  (h: fr ++ j :: jtail = l)
  (hij: List.indexOf i l < List.indexOf j l): i ∈ fr := by sorry

[Miyahara Kō]

I'm working on now...

[Miyahara Kō]

Done!

import Mathlib

namespace List

lemma mem_front_of_index {α: Type*} [DecidableEq α]
    (l fr jtail : List α)
    (i j : α)
    (hnd : Nodup (fr ++ j :: jtail))
    (hl : fr ++ j :: jtail = l)
    (hidx : indexOf i l < indexOf j l) : i ∈ fr := by
  subst hl
  by_contra hnm
  rw [nodup_append, disjoint_cons_right] at hnd
  simp [indexOf_append_of_not_mem hnm, indexOf_append_of_not_mem hnd.2.2.1] at hidx

end List

[Zhuanhao Wu]

Thanks! this is much cleaner than what I could have done!