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

State before:
n : ℕ
α : Type u
α✝ : Type u_1
s : Fin n → α✝
a : α✝
i : Fin n
⊢ (s <: a) i.castSucc = s i
Tactic:
simp[vecConsLast]
State after:
no goals