Theorem: Nat.Arith₁.head (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
⊢ ∀ (i : Vector ℕ (n + 1)), (↑fun v => v.get 0) i = (↑fun v => v.head) i
Tactic:
simp
State after:
no goals