Theorem: Matrix.constant_eq_singleton' (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
v : Fin 1 → α
⊢ v = ![v 0]
Tactic:
funext x
State after:
case h
n : ℕ
α : Type u
v : Fin 1 → α
x : Fin 1
⊢ v x = ![v 0] x

State before:
case h
n : ℕ
α : Type u
v : Fin 1 → α
x : Fin 1
⊢ v x = ![v 0] x
Tactic:
simp[Fin.eq_zero]
State after:
no goals