Theorem: Vector.get_one (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.tail.head
Tactic:
rw[←Vector.get_zero, Vector.get_tail_succ]
State after:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.get (Fin.succ 0)

State before:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.get (Fin.succ 0)
Tactic:
rfl
State after:
no goals