awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ x.PosDef
have this : ((↑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⁻¹))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have 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
Tactic: rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have 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
Tactic: rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have 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
Tactic: rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have 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
Tactic: rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have 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
Tactic: rwa [← star_eq_conjTranspose, ← mul_assoc, ← mul_assoc, ← star_mul, mul_assoc,
    Units.mul_inv, mul_one, star_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have rwa₅ : ∀ (this : (star 1 * x * 1).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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have rwa₆ : ∀ (this : (star 1 * 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have rwa₇ : ∀ (this : (1 * 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ x.PosDef
have rwa₈ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
have have : ∀ (this : Fintype n), (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
Tactic: have := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
have rw : ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
  (D - Bᴴ * A⁻¹ * B).PosSemidef
Tactic: rw [posSemidef_iff_dotProduct_mulVec, IsHermitian.fromBlocks₁₁ _ _ hA.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have mp : ((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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (D - Bᴴ * A⁻¹ * B).PosSemidef
have mpr : (D - Bᴴ * A⁻¹ * B).PosSemidef →
  (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have 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
Tactic: refine fun h => .of_dotProduct_mulVec_nonneg h.1 fun x => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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 x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have this₁ : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
Tactic: have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have 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
Tactic: rwa [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_cancel, dotProduct_zero,
      zero_add, ← dotProduct_mulVec] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have 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
Tactic: rwa [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_cancel, dotProduct_zero,
      zero_add, ← dotProduct_mulVec] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have mp₂ : ∀ (this : 0 ≤ star 0 ᵥ* A ⬝ᵥ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have mp₃ : ∀ (this : 0 ≤ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have mp₄ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
have mp₅ : ∀ (this : 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
Cleared hypotheses: this