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✝¹ : Fintype n
inst✝ : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
⊢ (star U * x * U).PosDef ↔ x.PosDef

Tactic:
by

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

Tactic:
by

Goal state after:
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
P : RootPairing ι R M N
inst✝ : P.IsValuedIn S
b : P.Base
i j : ↥b.support
⊢ (algebraMap S R) (cartanMatrixIn S b i j) = P.pairing ↑i ↑j

Tactic:
by

Goal state after:
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
P : RootPairing ι R M N
inst✝¹ : P.IsValuedIn S
b : P.Base
inst✝ : FaithfulSMul S R
i : ↥b.support
⊢ (algebraMap S R) (cartanMatrixIn S b i i) = (algebraMap S R) 2

Tactic:
by

Goal state after:
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
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsValuedIn S
B : P.InvariantForm
b : P.Base
inst✝ : DecidableEq ι
⊢ ((cartanMatrixIn S b).map ⇑(algebraMap S R) * Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)) =
    2 • (LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form

Tactic:
by

Goal state after:
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
⊢ (2 • (LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form).Nondegenerate

Tactic:
by

Goal state after:
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
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
by

Goal state after:
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 A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
by

Goal state after:
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 : ι
⊢ Finsupp.single i 1 ≠ 0

Tactic:
by

Goal state after:
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
⊢ (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate

Tactic:
by

Goal state after:
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 < A i i

Tactic:
by

Goal state after:
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
i j : ι
⊢ 0 ≤ N i j

Tactic:
by

Goal state after:
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
⊢ HasEigenvalue (toLin' N) (μ - ρ)

Tactic:
by

Goal state after:
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
⊢ QuadraticMap.PosDef Q

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : QuadraticMap.PosDef Q
⊢ Q.toMatrix'.PosDef

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅(x + y).1, z.1⁆, ⁅(x + y).2, z.2⁆) = (⁅x.1, z.1⁆, ⁅x.2, z.2⁆) + (⁅y.1, z.1⁆, ⁅y.2, z.2⁆)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅x.1, (y + z).1⁆, ⁅x.2, (y + z).2⁆) = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆) + (⁅x.1, z.1⁆, ⁅x.2, z.2⁆)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x : L₁ × L₂), (⁅x.1, x.1⁆, ⁅x.2, x.2⁆) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂),
    (⁅x.1, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).1⁆, ⁅x.2, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).2⁆) =
      (⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).1, z.1⁆, ⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).2, z.2⁆) +
        (⁅y.1, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).1⁆, ⁅y.2, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).2⁆)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
x✝² : R
x✝¹ x✝ : L₁ × L₂
⊢ ⁅x✝¹, x✝² • x✝⁆ = x✝² • ⁅x✝¹, x✝⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (LinearMap.fst R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.fst R L₁ L₂).toFun x, (LinearMap.fst R L₁ L₂).toFun y⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (LinearMap.snd R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.snd R L₁ L₂).toFun x, (LinearMap.snd R L₁ L₂).toFun y⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁},
    (LinearMap.inl R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.inl R L₁ L₂).toFun x, (LinearMap.inl R L₁ L₂).toFun y⁆

Tactic:
by

Goal state after:
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, N *ᵥ v = (μ - ρ) • v ∧ v ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₂},
    (LinearMap.inr R L₁ L₂).toFun ⁅x, y⁆ = ⁅(LinearMap.inr R L₁ L₂).toFun x, (LinearMap.inr R L₁ L₂).toFun y⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
f : L →ₗ⁅R⁆ L₁
g : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L}, ((↑f).prod ↑g).toFun ⁅x, y⁆ = ⁅((↑f).prod ↑g).toFun x, ((↑f).prod ↑g).toFun y⁆

Tactic:
by

Goal state after:
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
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
by

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₂
x✝ : L₁
⊢ ∀ ⦃a₂ : L₁⦄, (inl R L₁ L₂) x✝ = (inl R L₁ L₂) a₂ → x✝ = a₂

Tactic:
by

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₂
x✝ : L₂
⊢ ∀ ⦃a₂ : L₂⦄, (inr R L₁ L₂) x✝ = (inr R L₁ L₂) a₂ → x✝ = a₂

Tactic:
by

Goal state after:
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
hv₀ : v ≠ 0
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
⊢ |v| ≠ 0

Tactic:
by

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

Goal state after:
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
⊢ b.cartanMatrix i j = 0 ↔ P.pairing ↑i ↑j = 0

Tactic:
by

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 = LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker

Tactic:
by

Goal state after:
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
i j : ↥b.support
⊢ b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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
this : P.pairingIn ℤ ↑i ↑j ≠ -4
⊢ P.pairingIn ℤ ↑i ↑j ∈ {-3, -2, -1, 0}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
⊢ f = g ↔ f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂) ∧ f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)

Tactic:
by

Goal state after:
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.pairingIn ℤ ↑i ↑j = -4
⊢ P.pairingIn ℤ ↑j ↑i = -1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
hl : f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂)
hr : f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L₁
inst✝¹² : LieAlgebra R L₁
inst✝¹¹ : LieRing L₂
inst✝¹⁰ : LieAlgebra R L₂
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : LieRing L₃
inst✝⁶ : LieAlgebra R L₃
inst✝⁵ : LieRing L₄
inst✝⁴ : LieAlgebra R L₄
inst✝³ : LieRing L₅
inst✝² : LieAlgebra R L₅
inst✝¹ : LieRing L₆
inst✝ : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    (↑(LinearEquiv.prodComm R L₁ L₂)).toFun ⁅x, y⁆ =
      ⁅(↑(LinearEquiv.prodComm R L₁ L₂)).toFun x, (↑(LinearEquiv.prodComm R L₁ L₂)).toFun y⁆

Tactic:
by

Goal state after:
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
⊢ {i, j}.Nodup

Tactic:
by

Goal state after:
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 : ι
x✝ : i ∈ Finset.univ
⊢ μ * (d i * |v i| ^ 2) = |v i| * (d i * μ) * |v i|

Tactic:
by

Goal state after:
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
⊢ b.cartanMatrix i j ∈ {-3, -2, -1, 0}

Tactic:
by

Goal state after: