awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M : Matrix n n R
hM : M.PosSemidef
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
(posSemidef_iff_dotProduct_mulVec.mp hM).2

Premises used: And.right, Matrix.posSemidef_iff_dotProduct_mulVec, Iff.mp
-- 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
M : Matrix n n R
hM1 : M.IsHermitian
hM2 : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x
⊢ M.PosSemidef

Tactic:
posSemidef_iff_dotProduct_mulVec.mpr ⟨hM1, hM2⟩

Premises used: Iff.mpr, And.intro, Matrix.posSemidef_iff_dotProduct_mulVec
-- 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 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
have : ∀ (this : Fintype m), (Bᴴ * A * B).PosSemidef
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
have := Fintype.ofFinite m
-- 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 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
this : Fintype m
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_mul B hA.1) fun x ↦ ?_

Premises used: Matrix.isHermitian_conjTranspose_mul_mul, 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_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
this : Fintype m
refine : ∀ (x : m → R), 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
refine of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_mul B hA.1) fun x ↦ ?_

Premises used: Matrix.isHermitian_conjTranspose_mul_mul, 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_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
this : Fintype m
x : m → R
⊢ 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Tactic:
simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using
      hA.dotProduct_mulVec_nonneg (B *ᵥ x)

Premises used: Matrix.PosSemidef.dotProduct_mulVec_nonneg, Matrix.vecMul_vecMul, Matrix.mulVec, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- 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 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix m n R
⊢ (B * A * Bᴴ).PosSemidef

Tactic:
simpa only [conjTranspose_conjTranspose] using hA.conjTranspose_mul_mul_same Bᴴ

Premises used: Matrix.PosSemidef.conjTranspose_mul_mul_same, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose
-- 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 : StarOrderedRing R
inst_5 : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k : ℕ
⊢ (HPow.hPow (β := ℕ) M 1).PosSemidef

Tactic:
simpa using hM
-- 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 : StarOrderedRing R
inst_5 : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k_1 k : ℕ
rw : (M * M ^ k * M).PosSemidef
⊢ (M ^ (k + 2)).PosSemidef

Tactic:
rw [pow_succ, pow_succ']

Premises used: pow_succ, pow_succ'
-- 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 : StarOrderedRing R
inst_5 : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k_1 k : ℕ
⊢ (M * M ^ k * M).PosSemidef

Tactic:
simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.eq, Matrix.PosSemidef.mul_mul_conjTranspose_same
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
pos : ∀ (h : IsUnit M.det), M⁻¹.PosSemidef
neg : ∀ (h : ¬IsUnit M.det), M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
by_cases h : IsUnit M.det

Premises used: IsUnit, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
⊢ (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef

Tactic:
have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
pos : ∀ (this : M⁻¹ᴴᴴ.PosSemidef), M⁻¹.PosSemidef
pos₁ pos₂ pos₃ pos₄ : ∀ (this : M⁻¹.PosSemidef), M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this

Premises used: Matrix.mul_nonsing_inv_cancel_right, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
neg : PosSemidef.{u_2, u_4} (n := n) (R := R') 0
⊢ M⁻¹.PosSemidef

Tactic:
rw [nonsing_inv_apply_not_isUnit _ h]

Premises used: Matrix.nonsing_inv_apply_not_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef.{u_2, u_4} (n := n) (R := R') 0

Tactic:
.zero

Premises used: Matrix.PosSemidef.zero
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef.{u_2, u_4} (n := n) (R := R') 0

Tactic:
exact .zero
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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
inr : ∀ (n_1 : ℕ), (HPow.hPow (β := ℤ) M (-(↑n_1 : ℤ))).PosSemidef
⊢ (M ^ z).PosSemidef

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n_1 : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n_1
inst_4 : StarOrderedRing R'
inst_5 : DecidableEq n_1
M : Matrix n_1 n_1 R'
hM : M.PosSemidef
n : ℕ
⊢ (HPow.hPow (β := ℤ) M (↑n : ℤ)).PosSemidef

Tactic:
simpa using hM.pow n

Premises used: Matrix.PosSemidef.pow
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n_1 : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n_1
inst_4 : StarOrderedRing R'
inst_5 : DecidableEq n_1
M : Matrix n_1 n_1 R'
hM : M.PosSemidef
n : ℕ
⊢ (HPow.hPow (β := ℤ) M (-(↑n : ℤ))).PosSemidef

Tactic:
simpa using (hM.pow n).inv

Premises used: Matrix.PosSemidef.pow, Matrix.PosSemidef.inv
-- 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 : AddLeftMono R
A : Matrix n n R
hA : A.PosSemidef
⊢ 0 ≤ A.trace

Tactic:
Fintype.sum_nonneg fun _ ↦ hA.diag_nonneg

Premises used: Matrix.trace, Fintype.sum_nonneg, Matrix.PosSemidef.diag_nonneg
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
have : ∀ (this : Fintype n), (Aᴴ * A).PosSemidef
⊢ (Aᴴ * A).PosSemidef

Tactic:
have := Fintype.ofFinite n
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
⊢ (Aᴴ * A).PosSemidef

Tactic:
.of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_self _) fun x => ?_

Premises used: Matrix.isHermitian_conjTranspose_mul_self, Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
refine : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x
⊢ (Aᴴ * A).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_self _) fun x => ?_
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
rw : 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x

Tactic:
rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]

Premises used: star_star, Matrix.vecMul_conjTranspose, Matrix.dotProduct_mulVec, Matrix.mulVec_mulVec
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x

Tactic:
Finset.sum_nonneg fun i _ => star_mul_self_nonneg _

Premises used: dotProduct, Finset.sum_nonneg, star_mul_self_nonneg, Matrix.mulVec
-- 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 m
inst_4 : Finite n
inst_5 : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x

Tactic:
exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _

Premises used: Finset.sum_nonneg, star_mul_self_nonneg
-- 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 : Finite m
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).PosSemidef

Tactic:
simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ

Premises used: Matrix.posSemidef_conjTranspose_mul_self, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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
rw₂ rw₃ : A = 0 ↔ A = 0
⊢ (Aᴴ * A).trace = 0 ↔ A = 0

Tactic:
rw [← star_vec_dotProduct_vec, dotProduct_star_self_eq_zero, vec_eq_zero_iff]

Premises used: dotProduct_star_self_eq_zero, Matrix.star_vec_dotProduct_vec, Matrix.vec_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
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

Tactic:
simpa using trace_conjTranspose_mul_self_eq_zero_iff (A := Aᴴ)

Premises used: Matrix.trace_conjTranspose_mul_self_eq_zero_iff
-- 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
U x : Matrix n n R
hU : IsUnit U
⊢ (star U * x * U).PosSemidef ↔ x.PosSemidef

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same _⟩

Premises used: Matrix.PosSemidef.conjTranspose_mul_mul_same, 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
U x : Matrix n n R
hU : IsUnit U
refine : ∀ (h : (star U * x * U).PosSemidef), x.PosSemidef
⊢ (star U * x * U).PosSemidef ↔ x.PosSemidef

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.conjTranspose_mul_mul_same _⟩
-- 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
U x : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosSemidef
⊢ 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
U x : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosSemidef
lift : ∀ (U : (Matrix n n R)ˣ) (h : (star (↑U : Matrix n n R) * x * (↑U : Matrix n n R)).PosSemidef), x.PosSemidef
⊢ x.PosSemidef

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)).PosSemidef
⊢ ((↑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)
-- 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)).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
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : ∀ (this : x.PosSemidef), 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

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
U x : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosSemidef ↔ x.PosSemidef

Tactic:
simpa using hU.star.posSemidef_star_left_conjugate_iff

Premises used: IsUnit.star, Matrix.IsUnit.posSemidef_star_left_conjugate_iff
-- 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 : Finite n
inst_4 : StarOrderedRing R
a : n → R
⊢ (vecMulVec a (star a)).PosSemidef

Tactic:
simp [vecMulVec_eq Unit, ← conjTranspose_replicateCol, posSemidef_self_mul_conjTranspose]

Premises used: Matrix.posSemidef_self_mul_conjTranspose, Matrix.vecMulVec_eq, Unit, Matrix.conjTranspose_replicateCol
-- 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 : Finite n
inst_4 : StarOrderedRing R
a : n → R
⊢ (vecMulVec (star a) a).PosSemidef

Tactic:
simp [vecMulVec_eq Unit, ← conjTranspose_replicateRow, posSemidef_conjTranspose_mul_self]

Premises used: Matrix.posSemidef_conjTranspose_mul_self, Matrix.conjTranspose_replicateRow, Matrix.vecMulVec_eq, Unit
-- 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
M : Matrix n n R
⊢ ∀ (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⟩
-- 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
M : Matrix n n R
this : ∀ (x : n →₀ R), x = 0 ↔ Eq (α := n → R) ((Finsupp.equivFunOnFinite : (a : n →₀ R) → n → R) x : n → R) (0 : n → R)
⊢ M.PosDef ↔ M.IsHermitian ∧ ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
simp [PosDef, ← Finsupp.equivFunOnFinite.forall_congr_right, dotProduct, mulVec,
    Finsupp.sum_fintype, Finset.mul_sum, mul_assoc, this]

Premises used: Finset.mul_sum, dotProduct, Finsupp.sum_fintype, mul_assoc, Finsupp.equivFunOnFinite, Matrix.PosDef, Equiv.forall_congr_right, Matrix.mulVec
-- 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
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
(posDef_iff_dotProduct_mulVec.mp hM).2 hx

Premises used: Matrix.posDef_iff_dotProduct_mulVec, And.right, Iff.mp
-- 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
M : Matrix n n R
hM1 : M.IsHermitian
hM2 : ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M *ᵥ x
⊢ M.PosDef

Tactic:
posDef_iff_dotProduct_mulVec.mpr ⟨hM1, hM2⟩

Premises used: Iff.mpr, Matrix.posDef_iff_dotProduct_mulVec, And.intro
-- 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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
⊢ (Bᴴ * A * B).PosDef

Tactic:
of_dotProduct_mulVec_pos (isHermitian_conjTranspose_mul_mul _ hA.1) fun x hx => ?_

Premises used: Matrix.isHermitian_conjTranspose_mul_mul, And.left, Matrix.PosDef.of_dotProduct_mulVec_pos
-- 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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
refine : ∀ (x : m → R) (hx : x ≠ 0), 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
⊢ (Bᴴ * A * B).PosDef

Tactic:
refine of_dotProduct_mulVec_pos (isHermitian_conjTranspose_mul_mul _ hA.1) fun x hx => ?_

Premises used: Matrix.isHermitian_conjTranspose_mul_mul, And.left, Matrix.PosDef.of_dotProduct_mulVec_pos
-- 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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
x : m → R
hx : x ≠ 0
⊢ B *ᵥ x ≠ 0

Tactic:
have : B *ᵥ x ≠ 0 := fun h => hx <| hB.eq_iff' (mulVec_zero _) |>.1 h
-- 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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
x : m → R
hx : x ≠ 0
this : B *ᵥ x ≠ 0
⊢ 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Tactic:
simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.dotProduct_mulVec_pos this

Premises used: Matrix.vecMul_vecMul, Matrix.PosDef.dotProduct_mulVec_pos, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- 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
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (β := n → R) fun (v : m → R) ↦ v ᵥ* B
⊢ Function.Injective (α := m → R) (β := n → R) (star ∘ (fun (v : m → R) ↦ v ᵥ* B) ∘ star)

Tactic:
replace hB := star_injective.comp <| hB.comp star_injective
-- 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
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)
⊢ Function.Injective (β := n → R) fun (x : m → R) ↦ Bᴴ *ᵥ x

Tactic:
simp_rw [Function.comp_def, star_vecMul, star_star] at hB

Premises used: star_star, Matrix.star_vecMul, Function.comp_def
-- 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
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (β := n → R) fun (x : m → R) ↦ Bᴴ *ᵥ x
⊢ (B * A * Bᴴ).PosDef

Tactic:
simpa using hA.conjTranspose_mul_mul_same (B := Bᴴ) hB

Premises used: Matrix.PosDef.conjTranspose_mul_mul_same
-- 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 A.mulVec
⊢ (Aᴴ * A).PosDef

Tactic:
simpa using conjTranspose_mul_mul_same .one hA

Premises used: Matrix.PosDef.conjTranspose_mul_mul_same, Matrix.PosDef.one
-- 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 A.mulVec
⊢ (Aᴴ * A).PosDef

Tactic:
classical
  simpa using conjTranspose_mul_mul_same .one hA

Premises used: Matrix.PosDef.conjTranspose_mul_mul_same, Matrix.PosDef.one
-- 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:
simpa using mul_mul_conjTranspose_same .one hA

Premises used: Matrix.PosDef.one, Matrix.PosDef.mul_mul_conjTranspose_same