Theorem: Matrix.PosSemidef.mul_mul_of_IsHermitian (CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean)

State before:
m : Type ?u.45085
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.IsHermitian
⊢ (N * M * N).PosSemidef
Tactic:
convert hM.conjTranspose_mul_mul M N
State after:
case h.e'_8.h.e'_5.h.e'_5
m : Type ?u.45085
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.IsHermitian
⊢ N = N.conjTranspose

State before:
case h.e'_8.h.e'_5.h.e'_5
m : Type ?u.45085
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.IsHermitian
⊢ N = N.conjTranspose
Tactic:
exact hN.symm
State after:
no goals