Theorem: Matrix.fun_eq_vec₄ (Arithmetization/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
v : Fin 4 → α
⊢ v = ![v 0, v 1, v 2, v 3]
Tactic:
funext x
State after:
case h
α : Type u_1
v : Fin 4 → α
x : Fin 4
⊢ v x = ![v 0, v 1, v 2, v 3] x

State before:
case h
α : Type u_1
v : Fin 4 → α
x : Fin 4
⊢ v x = ![v 0, v 1, v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
State after:
case h.succ
α : Type u_1
v : Fin 4 → α
x : Fin 3
⊢ v x.succ = ![v 1, v 2, v 3] x

State before:
case h.succ
α : Type u_1
v : Fin 4 → α
x : Fin 3
⊢ v x.succ = ![v 1, v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
State after:
case h.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 2
⊢ v x.succ.succ = ![v 2, v 3] x

State before:
case h.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 2
⊢ v x.succ.succ = ![v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
State after:
case h.succ.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 1
⊢ v (Fin.succ 2) = v 3

State before:
case h.succ.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 1
⊢ v (Fin.succ 2) = v 3
Tactic:
rfl
State after:
no goals