Theorem: Matrix.IsHermitian₂₂_of_IsHermitian_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).IsHermitian
⊢ D.IsHermitian
Tactic:
ext i j
State after:
case a
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).IsHermitian
i j : n
⊢ D.conjTranspose i j = D i j

State before:
case a
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).IsHermitian
i j : n
⊢ D.conjTranspose i j = D i j
Tactic:
simpa using congr_fun (congr_fun h (Sum.inr i)) (Sum.inr j)
State after:
no goals