-- 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 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)

Tactic:
rw [← dotProduct_mulVec]

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)

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
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
refine fun h => ⟨h.1, fun 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 → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Proof state:
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
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
constructor

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
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef

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
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

Proof state:
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)

Tactic:
apply hA.posSemidef.2

Result:
no goals

Proof state:
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
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
rw [PosSemidef, IsHermitian.fromBlocks₁₁ _ _ hA.1]

Result:
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
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (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 → 𝕜
this : 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x

Tactic:
exact this

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
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

Tactic:
refine fun h => ⟨h.1, fun x => ?_⟩

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 ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x