-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem IsHermitian.fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜)
    (D : Matrix n n 𝕜) (hA : A.IsHermitian) :
    (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Proof state:
case hA
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

Tactic:
apply hA.inv

Result:
no goals

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian

Tactic:
refine ⟨hA, rfl, conjTranspose_conjTranspose B, ?_⟩

Result:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ D.IsHermitian

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := by
  apply isHermitian_conjTranspose_mul_mul
  apply hA.inv

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Proof state:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian
⊢ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
apply IsHermitian.sub h.2.2.2 hBAB

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
apply isHermitian_conjTranspose_mul_mul

Result:
case hA
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ (D - ?mpr + ?mpr).IsHermitian

case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ Matrix n n 𝕜

Tactic:
apply IsHermitian.add h hBAB

Result:
no goals

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ (D - Bᴴ * A⁻¹ * B).IsHermitian → A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian

Tactic:
intro h

Result:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
constructor

Result:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian → (D - Bᴴ * A⁻¹ * B).IsHermitian

case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ (D - Bᴴ * A⁻¹ * B).IsHermitian → A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian

Proof state:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian → (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
intro h

Result:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian
⊢ (D - Bᴴ * A⁻¹ * B).IsHermitian

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ D.IsHermitian

Tactic:
rw [← sub_add_cancel D]

Result:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ (D - ?mpr + ?mpr).IsHermitian

case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
h : (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ Matrix n n 𝕜

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
rw [isHermitian_fromBlocks_iff]

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian