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
⊢ A.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
⊢ A.conjTranspose i j = A 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
⊢ A.conjTranspose i j = A i j
Tactic:
simpa using congr_fun (congr_fun h (Sum.inl i)) (Sum.inl j)
State after:
no goals