-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
@[simp]
lemma sq_sqrt : hA.sqrt ^ 2 = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
⊢ hA.sqrt ^ 2 = A

Tactic:
let E := diagonal ((↑) ∘ Real.sqrt ∘ hA.1.eigenvalues : n → 𝕜)

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ hA.sqrt ^ 2 = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ C * (E * (star C * C) * E) * star C = A

Tactic:
have : E * E = diagonal ((↑) ∘ hA.1.eigenvalues) := by
  rw [diagonal_mul_diagonal]
  congr! with v
  simp [← pow_two, ← RCLike.ofReal_pow, Real.sq_sqrt (hA.eigenvalues_nonneg v)]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
this : E * E = diagonal (RCLike.ofReal ∘ ⋯.eigenvalues)
⊢ C * (E * (star C * C) * E) * star C = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ hA.sqrt ^ 2 = A

Tactic:
let C : Matrix n n 𝕜 := hA.1.eigenvectorUnitary

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
⊢ hA.sqrt ^ 2 = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ (diagonal fun i => (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i * (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i) =
    diagonal (RCLike.ofReal ∘ ⋯.eigenvalues)

Tactic:
congr! with v

Result:
case h.e'_5.h
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
v : n
⊢ (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) v * (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) v =
    (RCLike.ofReal ∘ ⋯.eigenvalues) v

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ E * E = diagonal (RCLike.ofReal ∘ ⋯.eigenvalues)

Tactic:
rw [diagonal_mul_diagonal]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ (diagonal fun i => (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i * (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i) =
    diagonal (RCLike.ofReal ∘ ⋯.eigenvalues)

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
this : E * E = diagonal (RCLike.ofReal ∘ ⋯.eigenvalues)
⊢ C * (E * (star C * C) * E) * star C = A

Tactic:
simpa [C, this] using hA.1.spectral_theorem.symm

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ hA.sqrt ^ 2 = A

Tactic:
suffices C * (E * (star C * C) * E) * star C = A by
  rw [Matrix.PosSemidef.sqrt, pow_two]
  simpa only [← mul_assoc] using this

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
⊢ C * (E * (star C * C) * E) * star C = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
this : C * (E * (star C * C) * E) * star C = A
⊢ hA.sqrt ^ 2 = A

Tactic:
rw [Matrix.PosSemidef.sqrt, pow_two]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
this : C * (E * (star C * C) * E) * star C = A
⊢ ↑⋯.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary *
      (↑⋯.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary) =
    A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
this : C * (E * (star C * C) * E) * star C = A
⊢ ↑⋯.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary *
      (↑⋯.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary) =
    A

Tactic:
simpa only [← mul_assoc] using this

Result:
no goals

Proof state:
case h.e'_5.h
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
C : Matrix n n 𝕜 := ↑⋯.eigenvectorUnitary
E : Matrix n n 𝕜 := diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)
v : n
⊢ (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) v * (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) v =
    (RCLike.ofReal ∘ ⋯.eigenvalues) v

Tactic:
simp [← pow_two, ← RCLike.ofReal_pow, Real.sq_sqrt (hA.eigenvalues_nonneg v)]

Result:
no goals