Theorem: LDL.lowerInv_diagonal (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
i : n
⊢ lowerInv hS i i = 1
Tactic:
simp only [lowerInv_eq_gramSchmidtBasis, 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
i : n
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1

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
i : n
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
letI := NormedAddCommGroup.ofMatrix hS.transpose
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
i : n
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1

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
i : n
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
letI := InnerProductSpace.ofMatrix hS.transpose
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
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1

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
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
rw [Basis.coe_mk, ← @repr_gramSchmidt_diagonal 𝕜 (n → 𝕜) _ _ _ n _ _ _ i (Pi.basisFun 𝕜 n)]
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
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix (gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n))).transpose i i =
    ((Pi.basisFun 𝕜 n).repr (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n)) i)) i

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
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix (gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n))).transpose i i =
    ((Pi.basisFun 𝕜 n).repr (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n)) i)) i
Tactic:
simp [Basis.toMatrix]
State after:
no goals