Theorem: LDL.lower_eq_to_matrix (CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean)

State before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ lower hS = ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose
Tactic:
simp only [lower, lowerInv_eq_gramSchmidtBasis]
State after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose⁻¹ =
    ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose

State before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose⁻¹ =
    ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose
Tactic:
apply Matrix.inv_eq_left_inv
State after:
case h
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose *
      ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose =
    1

State before:
case h
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose *
      ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose =
    1
Tactic:
rw [← transpose_mul, Basis.toMatrix_mul_toMatrix_flip, transpose_one]
State after:
no goals