Theorem: Matrix.eq_vecCons (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
C : Type u_1
s : Fin (n + 1) → C
⊢ s 0 = (s 0 :> s ∘ succ) 0
Tactic:
simp
State after:
no goals

State before:
n : ℕ
α : Type u
C : Type u_1
s : Fin (n + 1) → C
⊢ ∀ (i : Fin n), s i.succ = (s 0 :> s ∘ succ) i.succ
Tactic:
simp
State after:
no goals