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

Proof state:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)

Result:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Proof state:
case mpr.hbc
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]

Result:
case mpr.hbc
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr

Proof state:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
rw [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_cancel, dotProduct_zero,
  zero_add] at this

Result:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

Tactic:
rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]

Result:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Proof state:
case mpr.hbc
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr

Tactic:
apply h.2

Result:
no goals

Proof state:
case mpr
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
apply le_add_of_nonneg_of_le

Result:
case mpr.ha
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)

case mpr.hbc
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Proof state:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
rw [dotProduct_mulVec]

Result:
case mp
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x