m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)
simp_rw [seq, seq_eq]
case refine'_1
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)

case refine'_2
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) (Fin.succ i) =
    f (Fin.succ i) (v (Fin.succ i))
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
refine' i.cases _ fun i => _
no goals
case refine'_1
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)
rfl
case refine'_2
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f (Fin.succ i) (v (Fin.succ i))
case refine'_2
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) (Fin.succ i) =
    f (Fin.succ i) (v (Fin.succ i))
rw [Matrix.cons_val_succ]
no goals
case refine'_2
m n✝ : ℕ
α : Type u_2
β : Type u_1
γ : Type ?u.1470
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f (Fin.succ i) (v (Fin.succ i))
rfl