Theorem: Matrix.PosSemidef.fromBlocks₂₂ (CvxLean/Lib/Math/SchurComplement.lean)

State before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (A.fromBlocks B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
Tactic:
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap]
State after:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (D.fromBlocks B.conjTranspose B A).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef

State before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (D.fromBlocks B.conjTranspose B A).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
Tactic:
convert @PosSemidef.fromBlocks₁₁ m n 𝕜 _ _ _ _ _ _ _ hD _ <;>
rw [conjTranspose_conjTranspose]
State after:
no goals