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

Goal state before:
pp: n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ Aᴴ ^ n = Aᴴ ^ n

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ x ≠ 0 → 0 < x.sum fun x' v' ↦ x.sum fun x v ↦ star v * Mᵀ x x' * v'

Tactic:
]

Goal state after:
n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ x ≠ 0 → 0 < x.sum fun x' v' ↦ x.sum fun x v ↦ star v * Mᵀ x x' * v'
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (Aᴴ ^ (n + 1))⁻¹ = (Aᴴ ^ (n + 1))⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ A ^ k = A ^ k

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case insert
m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
ι : Type u_5
inst✝ : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : hi.Nonempty → (∀ i ∈ hi, (A i).PosDef) → (∑ i ∈ hi, A i).PosDef
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
]

Goal state after:
case insert
m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
ι : Type u_5
inst✝ : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : hi.Nonempty → (∀ i ∈ hi, (A i).PosDef) → (∑ i ∈ hi, A i).PosDef
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
⊢ (A i + ∑ x ∈ hi, A x).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✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef

Tactic:
]

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 pos
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
]

Goal state after:
case pos
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case neg
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef 0

Tactic:
]

Goal state after:
case neg
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef 0
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 m
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x

Tactic:
]

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 m
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x
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 = 0 ↔ A = 0

Tactic:
]

Goal state after:
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 : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : x.PosSemidef
⊢ x.PosSemidef

Tactic:
]

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 : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : x.PosSemidef
⊢ x.PosSemidef
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:
]

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 ((Finsupp.linearCombination R ⇑b) (b.repr v))) ((Finsupp.linearCombination R ⇑b) (b.repr v))
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 : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : x.PosDef
⊢ x.PosDef

Tactic:
]

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 : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : x.PosDef
⊢ x.PosDef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : 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
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : 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'
this : 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
]

Goal state after:
case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : 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'
this : 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
]

Goal state after:
case mpr
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mpr.ha
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ⬝ᵥ A *ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)

Tactic:
]

Goal state after:
case mpr.ha
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ⬝ᵥ A *ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr

Tactic:
]

Goal state after:
case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr
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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ B.form.Nondegenerate

Tactic:
]

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ B.form.Nondegenerate
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
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:
]

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.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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : (2 • (LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form).Nondegenerate
⊢ ∀ a ∈ Finset.univ, (B.form (P.root ↑a)) (P.root ↑a) ≠ 0

Tactic:
]

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : (2 • (LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form).Nondegenerate
⊢ ∀ a ∈ Finset.univ, (B.form (P.root ↑a)) (P.root ↑a) ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef

Tactic:
]

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef
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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : ¬(cartanMatrixIn S b).det = 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
]

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : ¬(cartanMatrixIn S b).det = 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate
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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : ¬(cartanMatrixIn S b).det = 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).det ≠ 0

Tactic:
]

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : ¬(cartanMatrixIn S b).det = 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef
⊢ Q.toMatrix'.PosDef

Tactic:
]

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef
⊢ Q.toMatrix'.PosDef
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inl R L₁ L₂)).range = (↑(snd R L₁ L₂)).ker

Tactic:
]

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inl R L₁ L₂)).range = (↑(snd R L₁ L₂)).ker
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
i j : ↥b.support
⊢ P.pairing ↑i ↑j = 0 ↔ P.pairing ↑i ↑j = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (inl R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker

Tactic:
by
  rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
    ker_toSubmodule]
  exact LinearMap.range_inl R L₁ L₂

Goal state after:
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inr R L₁ L₂)).range = (↑(fst R L₁ L₂)).ker

Tactic:
]

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inr R L₁ L₂)).range = (↑(fst R L₁ L₂)).ker
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
h : i ≠ j
⊢ ¬i = j

Tactic:
]

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
h : i ≠ j
⊢ ¬i = j
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
h₁ : 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j|
⊢ ∑ i, μ * (d i * |v i| ^ 2) = ∑ i, |v i| * (d i * μ) * |v i|

Tactic:
]

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
h₁ : 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j|
⊢ ∑ i, μ * (d i * |v i| ^ 2) = ∑ i, |v i| * (d i * μ) * |v i|