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

State before:
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
⊢ appendr ![] w = w
Tactic:
funext i
State after:
case h
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
i : Fin (m + 0)
⊢ appendr ![] w i = w i

State before:
case h
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
i : Fin (m + 0)
⊢ appendr ![] w i = w i
Tactic:
simp [appendr]
State after:
no goals