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

State before:
m : Type ?u.23145
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
⊢ (N.conjTranspose * M * N).PosSemidef
Tactic:
refine' ⟨isHermitian_conjTranspose_mul_mul _ hM.1, _⟩
State after:
m : Type ?u.23145
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
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x

State before:
m : Type ?u.23145
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
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
intro x
State after:
m : Type ?u.23145
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
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x

State before:
m : Type ?u.23145
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
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
convert hM.2 (N.mulVec x) using 1
State after:
case h.e'_4
m : Type ?u.23145
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
x : n → 𝕜
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)

State before:
case h.e'_4
m : Type ?u.23145
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
x : n → 𝕜
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Tactic:
rw [mul_assoc, mulVec_mulVec, ← mulVec_mulVec, dotProduct_mulVec, star_mulVec]
State after:
no goals