awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
z : ℤ
⊢ (M ^ z).PosSemidef
have inl : ∀ (n_1 : ℕ), (HPow.hPow (β := ℤ) M (↑n_1 : ℤ)).PosSemidef
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
z : ℤ
inl : ∀ (n_1 : ℕ), (HPow.hPow (β := ℤ) M (↑n_1 : ℤ)).PosSemidef
⊢ (M ^ z).PosSemidef
have inr : ∀ (n_1 : ℕ), (HPow.hPow (β := ℤ) M (-(↑n_1 : ℤ))).PosSemidef
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).PosSemidef
have have : ∀ (this : Fintype n), (Aᴴ * A).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_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
⊢ (Aᴴ * A).PosSemidef
have refine : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x
Tactic: refine .of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_self _) fun x => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x
have rw : 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x
Tactic: rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : Fintype m
R : Type u_5
inst_2 : PartialOrder R
inst_3 : NonUnitalRing R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
⊢ (Aᴴ * A).trace = 0 ↔ A = 0
have rw : star A.vec ⬝ᵥ A.vec = 0 ↔ A = 0
Tactic: rw [← star_vec_dotProduct_vec, dotProduct_star_self_eq_zero, vec_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : Fintype m
R : Type u_5
inst_2 : PartialOrder R
inst_3 : NonUnitalRing R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
rw : star A.vec ⬝ᵥ A.vec = 0 ↔ A = 0
⊢ (Aᴴ * A).trace = 0 ↔ A = 0
have rw₁ : A.vec = 0 ↔ A = 0
Tactic: rw [← star_vec_dotProduct_vec, dotProduct_star_self_eq_zero, vec_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : Fintype m
R : Type u_5
inst_2 : PartialOrder R
inst_3 : NonUnitalRing R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
rw : star A.vec ⬝ᵥ A.vec = 0 ↔ A = 0
rw₁ : A.vec = 0 ↔ A = 0
⊢ (Aᴴ * A).trace = 0 ↔ A = 0
have rw₂ : A = 0 ↔ A = 0
Tactic: rw [← star_vec_dotProduct_vec, dotProduct_star_self_eq_zero, vec_eq_zero_iff]
-- 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
U x : Matrix n n R
hU : IsUnit U
⊢ (star U * x * U).PosSemidef ↔ x.PosSemidef
have refine : ∀ (h : (star U * x * U).PosSemidef), x.PosSemidef
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same _⟩
-- 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
U x : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosSemidef
⊢ x.PosSemidef
have lift : ∀ (U : (Matrix n n R)ˣ) (h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosSemidef), x.PosSemidef
Tactic: lift U to (Matrix n n R)ˣ using hU
Cleared hypotheses: U, hU, h
-- 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)).PosSemidef
⊢ x.PosSemidef
have this : ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
Tactic: have := h.conjTranspose_mul_mul_same ((U⁻¹ : (Matrix n n R)ˣ) : Matrix n n R)
-- 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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
⊢ x.PosSemidef
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)).PosSemidef),
  x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
⊢ x.PosSemidef
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)).PosSemidef),
  x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
⊢ x.PosSemidef
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)).PosSemidef),
  x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
⊢ x.PosSemidef
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)).PosSemidef),
  x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosSemidef),
    x.PosSemidef
⊢ x.PosSemidef
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))).PosSemidef),
  x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosSemidef),
    x.PosSemidef
rwa₄ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x *
          ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R))).PosSemidef),
    x.PosSemidef
⊢ x.PosSemidef
have rwa₅ : ∀ (this : (star 1 * x * 1).PosSemidef), x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosSemidef),
    x.PosSemidef
rwa₄ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x *
          ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R))).PosSemidef),
    x.PosSemidef
rwa₅ : ∀ (this : (star 1 * x * 1).PosSemidef), x.PosSemidef
⊢ x.PosSemidef
have rwa₆ : ∀ (this : (star 1 * x).PosSemidef), x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosSemidef),
    x.PosSemidef
rwa₄ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x *
          ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R))).PosSemidef),
    x.PosSemidef
rwa₅ : ∀ (this : (star 1 * x * 1).PosSemidef), x.PosSemidef
rwa₆ : ∀ (this : (star 1 * x).PosSemidef), x.PosSemidef
⊢ x.PosSemidef
have rwa₇ : ∀ (this : (1 * x).PosSemidef), x.PosSemidef
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)).PosSemidef
this :
  ((↑U⁻¹ : Matrix n n R)ᴴ * (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)) * (↑U⁻¹ : Matrix n n R)).PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
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)).PosSemidef),
    x.PosSemidef
rwa₃ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x * (↑U : Matrix n n R) *
          (↑U⁻¹ : Matrix n n R)).PosSemidef),
    x.PosSemidef
rwa₄ :
  ∀
    (this :
      (star ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R)) * x *
          ((↑U : Matrix n n R) * (↑U⁻¹ : Matrix n n R))).PosSemidef),
    x.PosSemidef
rwa₅ : ∀ (this : (star 1 * x * 1).PosSemidef), x.PosSemidef
rwa₆ : ∀ (this : (star 1 * x).PosSemidef), x.PosSemidef
rwa₇ : ∀ (this : (1 * x).PosSemidef), x.PosSemidef
⊢ x.PosSemidef
have rwa₈ : ∀ (this : x.PosSemidef), x.PosSemidef
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 (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
M : Matrix n n R
⊢ M.PosDef ↔ M.IsHermitian ∧ ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M *ᵥ x
have this : ∀ (x : n →₀ R), x = 0 ↔ Eq (α := n → R) ((Finsupp.equivFunOnFinite : (a : n →₀ R) → n → R) x : n → R) (0 : n → R)
Tactic: have (x : n →₀ R) : x = 0 ↔ Finsupp.equivFunOnFinite x = 0 :=
    ⟨fun h1 ↦ Finsupp.coe_eq_zero.mpr h1,fun h2 ↦ Finsupp.coe_eq_zero.mp h2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
⊢ (Bᴴ * A * B).PosDef
have refine : ∀ (x : m → R) (hx : x ≠ 0), 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
Tactic: refine of_dotProduct_mulVec_pos (isHermitian_conjTranspose_mul_mul _ hA.1) fun x hx => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
have this : B *ᵥ x ≠ 0
Tactic: have : B *ᵥ x ≠ 0 := fun h => hx <| hB.eq_iff' (mulVec_zero _) |>.1 h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (β := n → R) fun (v : m → R) ↦ v ᵥ* B
⊢ (B * A * Bᴴ).PosDef
have hB₁ : Function.Injective (α := m → R) (β := n → R) (star ∘ (fun (v : m → R) ↦ v ᵥ* B) ∘ star)
Tactic: replace hB := star_injective.comp <| hB.comp star_injective
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (α := m → R) (β := n → R) (star ∘ (fun (v : m → R) ↦ v ᵥ* B) ∘ star)
⊢ (B * A * Bᴴ).PosDef
have hB₁ : Function.Injective (β := n → R) fun (x : m → R) ↦ Bᴴ *ᵥ x
Tactic: simp_rw [Function.comp_def, star_vecMul, star_star] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have refine : ∀ (x : n → ℝ) (hx : x ≠ 0), 0 < star x ⬝ᵥ M *ᵥ x
Tactic: refine of_dotProduct_mulVec_pos hM fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ 0 < star x ⬝ᵥ M *ᵥ x
have hMq₁ : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x
Tactic: simp only [toQuadraticForm', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply,
    toLinearMap₂'_apply'] at hMq
Cleared hypotheses: hMq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((M.toQuadraticForm' : (a : n → ℝ) → ℝ) x : ℝ)
have simp : 0 < x ⬝ᵥ M *ᵥ x
Tactic: simp only [Matrix.toQuadraticForm', LinearMap.BilinMap.toQuadraticMap_apply,
    toLinearMap₂'_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ IsUnit M
have by_contra : ∀ (h : ¬IsUnit M), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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), a ≠ 0 ∧ M *ᵥ a = 0
have obtain : ∀ (a b : n → K) (ha : M *ᵥ a = M *ᵥ b ∧ a ≠ b), ∃ (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ False
have obtain : ∀ (a : n → K) (ha : a ≠ 0) (ha2 : M *ᵥ a = 0), 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]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ M⁻¹.PosDef
have refine_2 : ∀ (this : (M⁻¹ * M * M⁻¹ᴴ).PosDef), M⁻¹.PosDef
Tactic: have := hM.mul_mul_conjTranspose_same (B := M⁻¹) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ M⁻¹.PosDef
have refine_1 : Function.Injective (β := n → K) fun (v : n → K) ↦ v ᵥ* M⁻¹
Tactic: have := hM.mul_mul_conjTranspose_same (B := M⁻¹) ?_
-- 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 U : Matrix n n R
hU : IsUnit U
⊢ (star U * x * U).PosDef ↔ x.PosDef
have refine : ∀ (h : (star U * x * U).PosDef), x.PosDef
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same <| mulVec_injective_of_isUnit hU⟩
-- 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 U : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosDef
⊢ x.PosDef
have lift : ∀ (U : (Matrix n n R)ˣ) (h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosDef), x.PosDef
Tactic: lift U to (Matrix n n R)ˣ using hU
Cleared hypotheses: U, hU, h