n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (toList (reverse v)) (↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ head (reverse v) = last v
rw [← get_zero, last_def, get_eq_get, get_eq_get]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (List.reverse (toList v)) (↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (toList (reverse v)) (↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
simp_rw [toList_reverse]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get? (toList v)
      (List.length (toList v) - 1 - ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0)) =
    List.get? (toList v) ↑(↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))

case h
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) < List.length (toList v)
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (List.reverse (toList v)) (↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
rw [← Option.some_inj, ← List.get?_eq_get, ← List.get?_eq_get, List.get?_reverse]
case e_a
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.length (toList v) - 1 - ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    ↑(↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get? (toList v)
      (List.length (toList v) - 1 - ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0)) =
    List.get? (toList v) ↑(↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
congr
no goals
case e_a
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.length (toList v) - 1 - ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    ↑(↑(Fin.cast (_ : n + 1 = List.length (toList v))) (Fin.last n))
simp
no goals
case h
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ↑(↑(Fin.cast (_ : Nat.succ n = List.length (toList (reverse v)))) 0) < List.length (toList v)
simp