l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ transposeᵣ A i j = Aᵀ i j
simp_rw [transposeᵣ, transposeᵣ_eq]
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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

case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
refine' i.cases _ fun i => _
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
dsimp
no goals
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
rw [FinVec.map_eq, Function.comp_apply]
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
simp only [of_apply, Matrix.cons_val_succ]
no goals
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.8461
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
rfl