mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) =
    ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) =
    ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0

Tactic:
]

Goal state after:
case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ x₁ = 0 ∧ x₂ = 0

Tactic:
]

Goal state after:
case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ x₁ = 0 ∧ x₂ = 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R P
inst✝ : Invertible 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ⅟2 • LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      ⅟2 • LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂) =
    LinearMap.compl₁₂ (⅟2 • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ (⅟2 • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)

Tactic:
]

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R P
inst✝ : Invertible 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ⅟2 • LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      ⅟2 • LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂) =
    LinearMap.compl₁₂ (⅟2 • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ (⅟2 • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ (Q i) m = (Q i) m

pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Q (m i) = Q (m i)

pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
⊢ (Pi.single i Q j) (m j) = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
⊢ (Pi.single i Q j) (m j) = 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ n ≤ ↑(chainBotCoeff (⇑(-α)) β)

Tactic:
]

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ n ≤ ↑(chainBotCoeff (⇑(-α)) β)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥

Tactic:
]

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
this : x = 0
⊢ x = 0

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
this : x = 0
⊢ x = 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ n ≤ ↑(chainTopCoeff (⇑α) β)

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ n ≤ ↑(chainTopCoeff (⇑α) β)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℕ
hk : n = ↑(chainTopCoeff (⇑α) β) - ↑k
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥

Tactic:
]

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℕ
hk : n = ↑(chainTopCoeff (⇑α) β) - ↑k
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
j : ι
a✝ : j ∈ Finset.univ
x : Mᵢ j
hx : (Q j) x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
Pi.single_eq_of_ne hji,

Goal state after:
case neg
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ (Q j) 0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
k : ℕ
h₁ : ↑(chainTopCoeff (⇑α) β) - ↑k ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : k ≤ chainLength α β
this : rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥

Tactic:
]

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
k : ℕ
h₁ : ↑(chainTopCoeff (⇑α) β) - ↑k ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : k ≤ chainLength α β
this : rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Injective ⇑(dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Injective ⇑(dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective ⇑(↑e.symm ∘ₗ dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective ⇑(↑e.symm ∘ₗ dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
⊢ (Q i) x = (Q i) x

pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) (Pi.single i x j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
Pi.single_eq_of_ne hji,

Goal state after:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) 0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective (Prod.map ⇑id ⇑(Module.Dual.eval R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective (Prod.map ⇑id ⇑(Module.Dual.eval R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)