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

State before:
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ (N.conjTranspose * M * N).PosDef
Tactic:
refine' ⟨isHermitian_conjTranspose_mul_mul _ hM.1, _⟩
State after:
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x

State before:
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
intros x hx
State after:
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x

State before:
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
convert
  hM.2 (N.mulVec x) (fun h => hx (eq_zero_of_mulVec_eq_zero hN h)) using 1
State after:
case h.e'_4
m : Type ?u.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ 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.28307
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Tactic:
rw [Matrix.mul_assoc, mulVec_mulVec, ← mulVec_mulVec, dotProduct_mulVec,
  star_mulVec]
State after:
no goals