Theorem: Matrix.PosSemidef₂₂_of_PosSemidef_toBlock (CvxLean/Lib/Math/LogDet.lean)

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).PosSemidef
x : n → ℝ
⊢ 0 ≤ star x ⬝ᵥ D.mulVec x
Tactic:
simpa [Matrix.fromBlocks_mulVec, star] using h.2 (Sum.elim 0 x)
State after:
no goals