Theorem: Matrix.PosSemidef.sqrt_mul_sqrt (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ ⋯.sqrt * ⋯.sqrt =
    ⋯.eigenvectorMatrix *
        ((diagonal fun i => (⋯.eigenvalues i).sqrt) * (⋯.eigenvectorMatrix.transpose * ⋯.eigenvectorMatrix) *
          diagonal fun i => (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.transpose
Tactic:
simp [IsHermitian.sqrt, Matrix.mul_assoc]
State after:
no goals

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ ⋯.eigenvectorMatrix *
        ((diagonal fun i => (⋯.eigenvalues i).sqrt) * (⋯.eigenvectorMatrix.transpose * ⋯.eigenvectorMatrix) *
          diagonal fun i => (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.transpose =
    A
Tactic:
rw [← conjTranspose_eq_transpose, hA.1.conjTranspose_eigenvectorMatrix,
  hA.1.eigenvectorMatrix_inv_mul, Matrix.mul_one, diagonal_mul_diagonal,
  ← hA.1.conjTranspose_eigenvectorMatrix]
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ (⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt * (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.conjTranspose =
    A

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ (⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt * (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.conjTranspose =
    A
Tactic:
convert hA.1.spectral_theorem''
State after:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ (⋯.eigenvalues x✝).sqrt * (⋯.eigenvalues x✝).sqrt = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝

State before:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ (⋯.eigenvalues x✝).sqrt * (⋯.eigenvalues x✝).sqrt = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Tactic:
rw [← Real.sqrt_mul (hA.eigenvalues_nonneg _), Real.sqrt_mul_self (hA.eigenvalues_nonneg _)]
State after:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ ⋯.eigenvalues x✝ = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝

State before:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ ⋯.eigenvalues x✝ = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Tactic:
simp
State after:
no goals