[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
[PROOFSTEP]
simp only [Forall, FinVec.forall_iff, forall_iff]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin (Nat.add m 0)) (Fin n) α), P (↑of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
[PROOFSTEP]
exact Iff.symm Fin.forall_fin_succ_pi
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, FinVec.exists_iff, exists_iff]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ x x_1, P (↑of (vecCons x x_1))) ↔ ∃ x, P x
[PROOFSTEP]
exact Iff.symm Fin.exists_fin_succ_pi
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ transposeᵣ A i j = Aᵀ i j
[PROOFSTEP]
simp_rw [transposeᵣ, transposeᵣ_eq]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) i j = Aᵀ i j
[PROOFSTEP]
refine' i.cases _ fun i => _
[GOAL]
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) 0 j = Aᵀ 0 j
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ FinVec.map (fun v => v 0) A j = A j 0
[PROOFSTEP]
rw [FinVec.map_eq, Function.comp_apply]
[GOAL]
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) (Fin.succ i) j = Aᵀ (Fin.succ i) j
[PROOFSTEP]
simp only [of_apply, Matrix.cons_val_succ]
[GOAL]
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (submatrix A id Fin.succ)ᵀ i j = Aᵀ (Fin.succ i) j
[PROOFSTEP]
rfl
[GOAL]
l m✝ n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b
[PROOFSTEP]
simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq, Function.comp_apply]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ mulᵣ A B = A * B
[PROOFSTEP]
simp [mulᵣ, Function.comp, Matrix.transpose]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ (↑of fun x x_1 => A x ⬝ᵥ ↑of (fun x y => B y x) x_1) = A * B
[PROOFSTEP]
rfl
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ mulVecᵣ A v = mulVec A v
[PROOFSTEP]
simp [mulVecᵣ, Function.comp]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ (fun x => A x ⬝ᵥ v) = mulVec A v
[PROOFSTEP]
rfl
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = vecMul v A
[PROOFSTEP]
simp [vecMulᵣ, Function.comp]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun x => v ⬝ᵥ Aᵀ x) = vecMul v A
[PROOFSTEP]
rfl
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ etaExpand A = A
[PROOFSTEP]
simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of, Equiv.refl_apply]
