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

State before:
n : ℕ
α : Type u
a : α
⊢ (fun x => a) = ![a]
Tactic:
funext x
State after:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0)
⊢ a = ![a] x

State before:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0)
⊢ a = ![a] x
Tactic:
simp
State after:
no goals