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

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

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