mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ ?m.73

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ ?m.73
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosDef
hB : B.PosSemidef
x : m →₀ R
hx : x ≠ 0
⊢ 0 < x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * (A + B) i j * xj

Tactic:
simpa using

Goal state after:
m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosDef
hB : B.PosSemidef
x : m →₀ R
hx : x ≠ 0
⊢ 0 <
    (x.sum fun a b ↦ x.sum fun a_1 ↦ HMul.hMul (star b * A a a_1)) +
      x.sum fun a b ↦ x.sum fun a_1 ↦ HMul.hMul (star b * B a a_1)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
α : Type u_5
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : StarRing α
inst✝³ : StarOrderedRing α
inst✝² : Algebra α R
inst✝¹ : StarModule α R
inst✝ : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
y : n →₀ R
hy : y ≠ 0
⊢ 0 < y.sum fun i xi ↦ y.sum fun j xj ↦ star xi * (a • x) i j * xj

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
α : Type u_5
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : StarRing α
inst✝³ : StarOrderedRing α
inst✝² : Algebra α R
inst✝¹ : StarModule α R
inst✝ : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
y : n →₀ R
hy : y ≠ 0
⊢ 0 < a • y.sum fun a b ↦ y.sum fun a_1 ↦ HMul.hMul (star b * x a a_1)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
x✝ : Mᴴ.PosDef
⊢ M.PosDef

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
x✝ : Mᴴ.PosDef
⊢ M.PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : Nontrivial R
A : Matrix n n R
hA : A.PosDef
i : n
⊢ 0 < A i i

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : Nontrivial R
A : Matrix n n R
hA : A.PosDef
i : n
⊢ 0 < A i i
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : 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 using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : 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
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix m n R
⊢ (B * A * Bᴴ).PosSemidef

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix m n R
⊢ (B * A * Bᴴ).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k : ℕ
⊢ (M ^ 1).PosSemidef

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k : ℕ
⊢ M.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ ↑n).PosSemidef

Tactic:
simpa using

Goal state after:
case inl
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ n).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inr
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ (-↑n)).PosSemidef

Tactic:
simpa using

Goal state after:
case inr
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ n)⁻¹.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : Finite m
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).PosSemidef

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : Finite m
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
R : Type u_5
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
⊢ (A * Aᴴ).trace = 0 ↔ A = 0

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
R : Type u_5
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
⊢ (A * Aᴴ).trace = 0 ↔ A = 0
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U x : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosSemidef ↔ x.PosSemidef

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U x : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosSemidef ↔ x.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : 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 using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : 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
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective fun x ↦ Bᴴ *ᵥ x
⊢ (B * A * Bᴴ).PosDef

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective fun x ↦ Bᴴ *ᵥ x
⊢ (B * A * Bᴴ).PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective A.mulVec
⊢ (Aᴴ * A).PosDef

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective A.mulVec
⊢ (Aᴴ * A).PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective fun v ↦ v ᵥ* A
⊢ (A * Aᴴ).PosDef

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective fun v ↦ v ᵥ* A
⊢ (A * Aᴴ).PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
inst✝⁵ : Fintype n
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : TrivialStar R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.IsSymm
hMq : QuadraticMap.PosDef M.toQuadraticForm'
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
simpa using

Goal state after:
n : Type u_2
inst✝⁵ : Fintype n
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : TrivialStar R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.IsSymm
hMq : QuadraticMap.PosDef M.toQuadraticForm'
x : n → R
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ M *ᵥ x
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
inst✝⁵ : Fintype n
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : TrivialStar R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ 0 < M.toQuadraticForm' x

Tactic:
simpa using

Goal state after:
n : Type u_2
inst✝⁵ : Fintype n
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : TrivialStar R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ M *ᵥ x
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case refine_2
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : (LinearMap.BilinMap.toQuadraticMap B).PosDef
v : n →₀ R
hv : v ≠ 0
⊢ 0 < v.sum fun i xi ↦ v.sum fun j xj ↦ star xi * (LinearMap.BilinForm.toMatrix b) B i j * xj

Tactic:
simpa using

Goal state after:
case refine_2
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : (LinearMap.BilinMap.toQuadraticMap B).PosDef
v : n →₀ R
hv : v ≠ 0
⊢ 0 < v.sum fun i xi ↦ v.sum fun j xj ↦ xi * (B (b i)) (b j) * xj
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (B ((Finsupp.linearCombination R ⇑b) (b.repr v))) ((Finsupp.linearCombination R ⇑b) (b.repr v))

Tactic:
simpa using

Goal state after:
case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (b.repr v).sum fun a b_1 ↦ (b.repr v).sum fun a_1 c ↦ b_1 * (c * (B (b a_1)) (b a))
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : 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 using

Goal state after:
n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
a : n → K
ha : a ≠ 0
ha2 : M *ᵥ a = 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case refine_2
n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
this : (M⁻¹ * M * M⁻¹ᴴ).PosDef
x✝ : Invertible M := ⋯.invertible
⊢ M⁻¹.PosDef

Tactic:
simpa using

Goal state after:
case refine_2
n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
this : (M⁻¹ * M * M⁻¹ᴴ).PosDef
x✝ : Invertible M := ⋯.invertible
⊢ M⁻¹.PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosDef ↔ x.PosDef

Tactic:
simpa using

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
⊢ (U * x * star U).PosDef ↔ x.PosDef
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
i : ι
⊢ 0 < d i * A i i

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
i : ι
⊢ 0 < d i * A i i
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
hρ : HasEigenvalue (toLin' N) (μ - ρ)
⊢ ∃ v, N *ᵥ v = (μ - ρ) • v ∧ v ≠ 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
hρ : HasEigenvalue (toLin' N) (μ - ρ)
⊢ ∃ v, N *ᵥ v = (μ - ρ) • v ∧ ¬v = 0
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hv₀ : |v| ≠ 0
⊢ 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j|

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hv₀ : |v| ≠ 0
⊢ 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j|
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ False

Tactic:
refine (not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ ∃ s g, ∑ i ∈ s, g i • P.root ↑i = 0 ∧ ∃ i ∈ s, g i ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
i j : ↥b.support
h : i ≠ j
⊢ |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j

Tactic:
simpa using

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
i j : ↥b.support
h : i ≠ j
⊢ b.cartanMatrix i j ≤ 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
i j : ↥b.support
⊢ (algebraMap ℤ R) (b.cartanMatrix i j) * (P.RootForm (P.root ↑j)) (P.root ↑j) =
    (algebraMap ℤ R) 2 * (P.RootForm ↑(b.toWeightBasisInt i)) ↑(b.toWeightBasisInt j)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
i j : ↥b.support
⊢ ↑(b.cartanMatrix i j) * (P.RootForm (P.root ↑j)) (P.root ↑j) = 2 * (P.RootForm (P.root ↑i)) (P.root ↑j)
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ { toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ⋯ } ∈ root

Tactic:
simpa using

Goal state after:
case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ ¬b.baseSupp i = 0