case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = getLast (y :: l) (_ : y :: l ≠ [])
hl : Nodup l
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = getLast (y :: l) (_ : y :: l ≠ [])
hl : Nodup l
⊢ next (y :: l) x h = y
rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = getLast (y :: l) (_ : y :: l ≠ [])
hl : Nodup l
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
subst hx
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
⊢ False
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
intro H
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.zero, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False

case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
⊢ False
obtain ⟨⟨_ | k, hk⟩, hk'⟩ := get_of_mem H
case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ Nat.succ k = length l
case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
suffices k.succ = l.length by simp [this] at hk
case h.intro.mk.succ.nil
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hl : Nodup []
h✝ : getLast [y] (_ : [y] ≠ []) ∈ []
h : getLast [y] (_ : [y] ≠ []) ∈ [y]
hy : getLast [y] (_ : [y] ≠ []) ≠ y
H : getLast [y] (_ : [y] ≠ []) ∈ dropLast [y]
hk : Nat.succ k < length (dropLast [y])
hk' : get (dropLast [y]) { val := Nat.succ k, isLt := hk } = getLast [y] (_ : [y] ≠ [])
⊢ Nat.succ k = length []

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Nodup (hd :: tl)
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ Nat.succ k = length l
cases' l with hd tl
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : some (get (dropLast (y :: l)) { val := Nat.zero, isLt := hk }) = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ False
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.zero, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
rw [← Option.some_inj] at hk'
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : y = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False

case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : some (get (dropLast (y :: l)) { val := Nat.zero, isLt := hk }) = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ False
rw [← get?_eq_get, dropLast_eq_take, get?_take, get?_zero, head?_cons,
  Option.some_inj] at hk'
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : y = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False

case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
exact hy (Eq.symm hk')
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ 0 < length l
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
rw [Nat.zero_eq, length_cons, Nat.pred_succ]
no goals
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ 0 < length l
exact length_pos_of_mem (by assumption)
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ ?m.71152 ∈ l
assumption
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
this : Nat.succ k = length l
⊢ False
simp [this] at hk
no goals
case h.intro.mk.succ.nil
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hl : Nodup []
h✝ : getLast [y] (_ : [y] ≠ []) ∈ []
h : getLast [y] (_ : [y] ≠ []) ∈ [y]
hy : getLast [y] (_ : [y] ≠ []) ≠ y
H : getLast [y] (_ : [y] ≠ []) ∈ dropLast [y]
hk : Nat.succ k < length (dropLast [y])
hk' : get (dropLast [y]) { val := Nat.succ k, isLt := hk } = getLast [y] (_ : [y] ≠ [])
⊢ Nat.succ k = length []
simp at hk
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Nodup (hd :: tl)
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
rw [nodup_iff_injective_get] at hl
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ k = length tl
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
rw [length, Nat.succ_inj']
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ k = length tl
refine' Fin.veq_of_eq (@hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩ ⟨tl.length, by simp⟩ _)
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  some (get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk }) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
rw [← Option.some_inj] at hk'
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' : get (hd :: tl) { val := k, isLt := ?h.intro.mk.succ.cons } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  some (get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk }) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
rw [← get?_eq_get, dropLast_eq_take, get?_take, get?, get?_eq_get, Option.some_inj] at hk'
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' :
  get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' : get (hd :: tl) { val := k, isLt := ?h.intro.mk.succ.cons } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
rw [hk']
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' :
  get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }

case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
simp [getLast_eq_get]
no goals
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
simpa using hk
no goals
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k < length (hd :: tl)
simpa using hk
no goals
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ length tl < length (hd :: tl)
simp