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

State before:
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
⊢ appendr (x :> v) w = x :> appendr v w
Tactic:
funext i
State after:
case h
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
i : Fin (m + n.succ)
⊢ appendr (x :> v) w i = (x :> appendr v w) i

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