no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
x✝ : Nodup []
i : Fin (length [])
⊢ next [] (get [] i) (_ : get [] { val := ↑i, isLt := (_ : ↑i < length []) } ∈ []) =
    get [] { val := (↑i + 1) % length [], isLt := (_ : (↑i + 1) % length [] < length []) }
simpa using i.2
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
x head✝ : α
x✝¹ : Nodup [head✝]
x✝ : Fin (length [head✝])
⊢ next [head✝] (get [head✝] x✝) (_ : get [head✝] { val := ↑x✝, isLt := (_ : ↑x✝ < length [head✝]) } ∈ [head✝]) =
    get [head✝] { val := (↑x✝ + 1) % length [head✝], isLt := (_ : (↑x✝ + 1) % length [head✝] < length [head✝]) }
simp
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := 0, isLt := h0 })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := 0, isLt := h0 }, isLt := (_ : ↑{ val := 0, isLt := h0 } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
⊢ next (x :: y :: l) (get (x :: y :: l) { val := 0, isLt := h0 })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := 0, isLt := h0 }, isLt := (_ : ↑{ val := 0, isLt := h0 } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
have h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x := by simp
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ y =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := 0, isLt := h0 })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := 0, isLt := h0 }, isLt := (_ : ↑{ val := 0, isLt := h0 } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
rw [next_cons_cons_eq' _ _ _ _ _ h₁]
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ y =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
simp
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
⊢ get (x :: y :: l) { val := 0, isLt := h0 } = x
simp
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
have hx' : (x :: y :: l).get ⟨i+1, hi⟩ ≠ x := by
  intro H
  suffices (i + 1 : ℕ) = 0 by simpa
  rw [nodup_iff_injective_get] at hn
  refine' Fin.veq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ _)
  simpa using H
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi' : i ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
have hi' : i ≤ l.length := Nat.le_of_lt_succ (Nat.succ_lt_succ_iff.1 hi)
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i = length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi' : i ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
rcases hi'.eq_or_lt with (hi' | hi')
no goals
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
. rw [next_ne_head_ne_getLast _ _ _ _ _ hx']
  simp only [get_cons_succ]
  rw [next_get (y::l), ← get_cons_succ (a := x)]
  congr
  dsimp
  rw [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'),
    Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 (Nat.succ_lt_succ_iff.2 hi'))]
  . simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), Nat.succ_eq_add_one, hi']
  . exact hn.of_cons
  . rw [getLast_eq_get]
    intro h
    have := nodup_iff_injective_get.1 hn h
    simp at this; simp [this] at hi'
  . rw [get_cons_succ]; exact get_mem _ _ _
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ False
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
intro H
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ False
suffices (i + 1 : ℕ) = 0 by simpa
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
rw [nodup_iff_injective_get] at hn
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := 0, isLt := (_ : 0 < Nat.succ (length l + 1)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
refine' Fin.veq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ _)
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := 0, isLt := (_ : 0 < Nat.succ (length l + 1)) }
simpa using H
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
this : i + 1 = 0
⊢ False
simpa
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ 0 < length (x :: y :: l)
simp
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := length l + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := length l + 1, isLt := hi },
              isLt := (_ : ↑{ val := length l + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i = length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
subst hi'
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ x =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ∈ y :: l

case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x

case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := length l + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := length l + 1, isLt := hi },
              isLt := (_ : ↑{ val := length l + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
rw [next_getLast_cons]
case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x

case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ∈ y :: l

case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x

case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
. rw [get_cons_succ]; exact get_mem _ _ _
case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x

case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
. exact hx'
case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
. simp [getLast_eq_get]
no goals
case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
. exact hn.of_cons
no goals
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ x =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
simp [hi', get]
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (y :: l) { val := length l, isLt := (_ : length l < length (y :: l)) } ∈ y :: l
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ∈ y :: l
rw [get_cons_succ]
no goals
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (y :: l) { val := length l, isLt := (_ : length l < length (y :: l)) } ∈ y :: l
exact get_mem _ _ _
no goals
case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
exact hx'
no goals
case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
simp [getLast_eq_get]
no goals
case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
exact hn.of_cons
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ : get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
rw [next_ne_head_ne_getLast _ _ _ _ _ hx']
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) })
      (_ : get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l) =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ : get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
simp only [get_cons_succ]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l)
      { val := (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1, isLt := ?m.114397 } =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) })
      (_ : get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l) =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
rw [next_get (y::l), ← get_cons_succ (a := x)]
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 = (i + 1 + 1) % length (x :: y :: l)

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l)
      { val := (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1, isLt := ?m.114397 } =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
congr
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (i + 1) % Nat.succ (length l) + 1 = (i + 1 + 1) % Nat.succ (Nat.succ (length l))

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 = (i + 1 + 1) % length (x :: y :: l)

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
dsimp
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (i + 1) % Nat.succ (length l) + 1 = (i + 1 + 1) % Nat.succ (Nat.succ (length l))

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
rw [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'),
  Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 (Nat.succ_lt_succ_iff.2 hi'))]
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)

case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
. simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), Nat.succ_eq_add_one, hi']
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)

case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
. exact hn.of_cons
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])

α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
. rw [getLast_eq_get]
  intro h
  have := nodup_iff_injective_get.1 hn h
  simp at this; simp [this] at hi'
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
. rw [get_cons_succ]; exact get_mem _ _ _
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)
simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), Nat.succ_eq_add_one, hi']
no goals
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)
exact hn.of_cons
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
rw [getLast_eq_get]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
intro h
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this :
  { val := i + 1, isLt := hi } =
    { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
have := nodup_iff_injective_get.1 hn h
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this : i = length l
⊢ False
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this :
  { val := i + 1, isLt := hi } =
    { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
simp at this
no goals
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this : i = length l
⊢ False
simp [this] at hi'
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
rw [get_cons_succ]
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l
exact get_mem _ _ _