awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Fintype m
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
⊢ (A * Aᴴ).PosDef

Tactic:
classical
  simpa using mul_mul_conjTranspose_same .one hA

Premises used: Matrix.PosDef.one, Matrix.PosDef.mul_mul_conjTranspose_same
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : QuadraticMap.PosDef M.toQuadraticForm'
⊢ M.PosDef

Tactic:
of_dotProduct_mulVec_pos hM fun x hx ↦ ?_

Premises used: Matrix.PosDef.of_dotProduct_mulVec_pos
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : QuadraticMap.PosDef M.toQuadraticForm'
refine : ∀ (x : n → ℝ) (hx : x ≠ 0), 0 < star x ⬝ᵥ M *ᵥ x
⊢ M.PosDef

Tactic:
refine of_dotProduct_mulVec_pos hM fun x hx ↦ ?_

Premises used: Matrix.PosDef.of_dotProduct_mulVec_pos
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : QuadraticMap.PosDef M.toQuadraticForm'
x : n → ℝ
hx : x ≠ 0
⊢ ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x

Tactic:
simp only [toQuadraticForm', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply,
    toLinearMap₂'_apply'] at hMq

Premises used: Matrix.toQuadraticForm', Matrix.toLinearMap₂'_apply', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
x : n → ℝ
hx : x ≠ 0
hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
apply hMq x hx
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
simp : 0 < x ⬝ᵥ M *ᵥ x
⊢ LT.lt (α := ℝ) (0 : ℝ) ((M.toQuadraticForm' : (a : n → ℝ) → ℝ) x : ℝ)

Tactic:
simp only [Matrix.toQuadraticForm', LinearMap.BilinMap.toQuadraticMap_apply,
    toLinearMap₂'_apply']

Premises used: Matrix.toQuadraticForm', Matrix.toLinearMap₂'_apply', LinearMap.BilinMap.toQuadraticMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ M *ᵥ x

Tactic:
apply hM.dotProduct_mulVec_pos hx

Premises used: Matrix.PosDef.dotProduct_mulVec_pos
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Nontrivial R
inst_5 : IsOrderedCancelAddMonoid R
inst_6 : Nonempty n
A : Matrix n n R
hA : A.PosDef
⊢ 0 < A.trace

Tactic:
Finset.sum_pos (fun _ _ ↦ hA.diag_pos) Finset.univ_nonempty

Premises used: Matrix.PosDef.diag_pos, Finset.sum_pos, Finset.univ_nonempty, Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
by_contra : ∀ (h : ¬IsUnit M), False
⊢ IsUnit M

Tactic:
by_contra h
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
obtain : ∀ (a b : n → K) (ha : M *ᵥ a = M *ᵥ b ∧ a ≠ b), ∃ (a : n → K), a ≠ 0 ∧ M *ᵥ a = 0
⊢ ∃ (a : n → K), a ≠ 0 ∧ M *ᵥ a = 0

Tactic:
obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h

Premises used: Iff.mpr, Iff.not, Iff.mp, Matrix.mulVec_injective_iff_isUnit, Function.not_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
a b : n → K
ha : M *ᵥ a = M *ᵥ b ∧ a ≠ b
⊢ a - b ≠ 0 ∧ M *ᵥ (a - b) = 0

Tactic:
simp [sub_eq_zero, ha, mulVec_sub]

Premises used: sub_eq_zero, Matrix.mulVec_sub
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
a b : n → K
ha : M *ᵥ a = M *ᵥ b ∧ a ≠ b
⊢ ∃ (a : n → K), a ≠ 0 ∧ M *ᵥ a = 0

Tactic:
exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
obtain : ∀ (a : n → K) (ha : a ≠ 0) (ha2 : M *ᵥ a = 0), False
⊢ False

Tactic:
obtain ⟨a, ha, ha2⟩ : ∃ a ≠ 0, M *ᵥ a = 0 := by
    obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
a : n → K
ha : a ≠ 0
ha2 : M *ᵥ a = 0
⊢ False

Tactic:
simpa [ha2] using hM.dotProduct_mulVec_pos ha

Premises used: Matrix.PosDef.dotProduct_mulVec_pos
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
refine_2 : ∀ (this : (M⁻¹ * M * M⁻¹ᴴ).PosDef), M⁻¹.PosDef
refine_1 : Function.Injective (β := n → K) fun (v : n → K) ↦ v ᵥ* M⁻¹
⊢ M⁻¹.PosDef

Tactic:
have := hM.mul_mul_conjTranspose_same (B := M⁻¹) ?_
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
this : (M⁻¹ * M * M⁻¹ᴴ).PosDef
x : Invertible M := IsUnit.invertible ⋯
⊢ M⁻¹.PosDef

Tactic:
simpa using this.conjTranspose

Premises used: Matrix.PosDef.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
hM : M.PosDef
⊢ Function.Injective (β := n → K) fun (v : n → K) ↦ v ᵥ* M⁻¹

Tactic:
simp only [Matrix.vecMul_injective_iff_isUnit, isUnit_nonsing_inv_iff, hM.isUnit]

Premises used: Matrix.PosDef.isUnit, Matrix.vecMul_injective_iff_isUnit, Matrix.isUnit_nonsing_inv_iff
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
inst : Fintype n
K : Type u_5
inst_1 : Field K
inst_2 : PartialOrder K
inst_3 : StarRing K
inst_4 : DecidableEq n
M : Matrix n n K
⊢ M⁻¹.PosDef ↔ M.PosDef

Tactic:
⟨fun h =>
    letI := (Matrix.isUnit_nonsing_inv_iff.1 <| h.isUnit).invertible
    Matrix.inv_inv_of_invertible M ▸ h.inv, (·.inv)⟩

Premises used: Eq.rec, Iff.intro, Matrix.PosDef.inv, Matrix.inv_inv_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
⊢ (star U * x * U).PosDef ↔ x.PosDef

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same <| mulVec_injective_of_isUnit hU⟩

Premises used: Matrix.PosDef.conjTranspose_mul_mul_same, Matrix.mulVec_injective_of_isUnit, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
refine : ∀ (h : (star U * x * U).PosDef), x.PosDef
⊢ (star U * x * U).PosDef ↔ x.PosDef

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same <| mulVec_injective_of_isUnit hU⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosDef
⊢ IsUnit U

Tactic:
hU
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosDef
lift : ∀ (U : (Matrix n n R)ˣ) (h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosDef), x.PosDef
⊢ x.PosDef

Tactic:
lift U to (Matrix n n R)ˣ using hU

Premises used: Matrix
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosDef
⊢ ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosDef

Tactic:
have := h.conjTranspose_mul_mul_same (mulVec_injective_of_isUnit (Units.isUnit U⁻¹))
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosDef
this : ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosDef
rwa :
  ∀
    (this :
      (star (↑U⁻¹ : Matrix n n R) * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) *
          (↑U⁻¹ : Matrix n n R)).PosDef),
    x.PosDef
rwa₁ :
  ∀
    (this :
      (star (↑U⁻¹ : Matrix n n R) * (star (↑U : Matrix n n R) * x) * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosDef),
    x.PosDef
rwa₂ :
  ∀
    (this :
      (star (↑U⁻¹ : Matrix n n R) * star (↑U : Matrix n n R) * x * (↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)).PosDef),
    x.PosDef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)).PosDef),
    x.PosDef
rwa₄ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R))).PosDef),
    x.PosDef
rwa₅ : ∀ (this : (star 1 * x * 1).PosDef), x.PosDef
rwa₆ : ∀ (this : (star 1 * x).PosDef), x.PosDef
rwa₇ : ∀ (this : (1 * x).PosDef), x.PosDef
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : ∀ (this : x.PosDef), x.PosDef
⊢ x.PosDef

Tactic:
rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this

Premises used: Matrix.star_eq_conjTranspose, mul_assoc, Units.mul_inv, StarMul.star_mul, mul_one, one_mul, star_one
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosDef ↔ x.PosDef

Tactic:
simpa using hU.star.posDef_star_left_conjugate_iff

Premises used: IsUnit.star, Matrix.IsUnit.posDef_star_left_conjugate_iff
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
have : ∀ (this : Fintype n), (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
rw :
  ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (D - Bᴴ * A⁻¹ * B).PosSemidef
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

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

Premises used: And.left, Matrix.posSemidef_iff_dotProduct_mulVec, Matrix.IsHermitian.fromBlocks₁₁
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
mp :
  ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef
mpr :
  (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
fun h => .of_dotProduct_mulVec_nonneg h.1 fun x => ?_

Premises used: And.left, Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
mp :
  ∀ (h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) (x : n → R'),
    0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
refine fun h => .of_dotProduct_mulVec_nonneg h.1 fun x => ?_
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
⊢ 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)

Tactic:
have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this_1 : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
mp :
  ∀ (this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)),
    0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
mp₁ :
  ∀
    (this :
      0 ≤
        star (-((A⁻¹ * B) *ᵥ x) + (A⁻¹ * B) *ᵥ x) ᵥ* A ⬝ᵥ (-((A⁻¹ * B) *ᵥ x) + (A⁻¹ * B) *ᵥ x) +
          star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x),
    0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
mp₂ : ∀ (this : 0 ≤ star 0 ᵥ* A ⬝ᵥ 0 + star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x), 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
mp₃ : ∀ (this : 0 ≤ 0 + star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x), 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
mp₄ : ∀ (this : 0 ≤ star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x), 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
mp₅ mp₆ mp₇ mp₈ : ∀ (this : 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x), 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

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

Premises used: zero_add, Matrix.schur_complement_eq₁₁, neg_add_cancel, And.left, dotProduct_zero, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

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

Premises used: And.left, And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
mpr : ∀ (h : (D - Bᴴ * A⁻¹ * B).PosSemidef) (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

Tactic:
refine fun h => ⟨h.1, fun x => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
mpr :
  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
⊢ 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]

Premises used: Matrix.schur_complement_eq₁₁, And.left, Sum.elim_comp_inl_inr, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
mpr : 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
mpr₁ : 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
⊢ 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

Premises used: le_add_of_nonneg_of_le
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
mpr : 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ⬝ᵥ A *ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)

Tactic:
rw [← dotProduct_mulVec]

Premises used: Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ⬝ᵥ A *ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)

Tactic:
apply (posSemidef_iff_dotProduct_mulVec.mp hA.posSemidef).2

Premises used: And.right, Matrix.PosDef.posSemidef, Matrix.posSemidef_iff_dotProduct_mulVec, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
mpr : 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

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

Premises used: Function.comp, Sum.inr, Matrix.dotProduct_mulVec, Star.star
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr

Tactic:
apply (posSemidef_iff_dotProduct_mulVec.mp h).2

Premises used: And.right, Matrix.posSemidef_iff_dotProduct_mulVec, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
rw : (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
    fromBlocks_submatrix_sum_swap_sum_swap]

Premises used: Matrix.fromBlocks_submatrix_sum_swap_sum_swap, Equiv.sumComm, Equiv.sumComm_apply, Matrix.posSemidef_submatrix_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
⊢ (fromBlocks D Bᴴ Bᴴᴴ A).PosSemidef ↔ (A - Bᴴᴴ * D⁻¹ * Bᴴ).PosSemidef

Tactic:
fromBlocks₁₁ Bᴴ A hD

Premises used: Matrix.PosDef.fromBlocks₁₁, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
h : B = Bᴴᴴ
h₁ : B = Bᴴᴴ
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
convert! fromBlocks₁₁ Bᴴ A hD

Premises used: Matrix.PosDef.fromBlocks₁₁, Matrix.conjTranspose