[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)
[PROOFSTEP]
simp_rw [seq, seq_eq]
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
refine' i.cases _ fun i => _
[GOAL]
case refine'_1
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
rw [Matrix.cons_val_succ]
[GOAL]
case refine'_2
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x
[PROOFSTEP]
simp only [Forall, Fin.forall_fin_zero_pi]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim
[PROOFSTEP]
rfl
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin (Nat.succ n) → α), P x
[PROOFSTEP]
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0' ↔ P finZeroElim
[PROOFSTEP]
rfl
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ sum a = ∑ i : Fin (n + 2), a i
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, sum, sum_eq]
