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

State before:
n : ℕ
α : Type u
a b : α
s : Fin n → α
⊢ a :> s <: b = (a :> s) <: b
Tactic:
funext x
State after:
case h
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin n.succ.succ
⊢ (a :> s <: b) x = ((a :> s) <: b) x

State before:
case h
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin n.succ.succ
⊢ (a :> s <: b) x = ((a :> s) <: b) x
Tactic:
cases' x using Fin.cases with x <;> simp
State after:
case h.succ
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin (n + 1)
⊢ (s <: b) x = ((a :> s) <: b) x.succ

State before:
case h.succ
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin (n + 1)
⊢ (s <: b) x = ((a :> s) <: b) x.succ
Tactic:
cases x using Fin.lastCases <;> simp[Fin.succ_castSucc]
State after:
no goals