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

Goal state before:
pp: case inr.inl
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1

pp: case inr.inr
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
·

Goal state after:
case inr.inl
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_1
ι : 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
⊢ range P.reflection ⊆ ↑((Equiv.weightHom P).domRestrict P.weylGroup).range

pp: case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ range P.reflection ⊆ ↑((Equiv.weightHom P).domRestrict P.weylGroup).range
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)

Tactic:
·

Goal state after:
case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inr
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
·

Goal state after:
case inr.inr
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_1
ι : 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
⊢ range (MulOpposite.op ∘ P.coreflection) ⊆ ↑((Equiv.coweightHom P).domRestrict P.weylGroup).range

pp: case refine_2
ι : 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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ range (MulOpposite.op ∘ P.coreflection) ⊆ ↑((Equiv.coweightHom P).domRestrict P.weylGroup).range
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inr.refine_1
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
⊢ ↑(chainTopCoeff (⇑α) β) - ↑n ≤ ↑(chainTopCoeff (⇑α) β) ∧ -(↑(chainTopCoeff (⇑α) β) - ↑n) ≤ ↑(chainBotCoeff (⇑α) β)

pp: case inr.inr.refine_2
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
this : rootSpace H✝ ((↑(chainTopCoeff (⇑α) β) - ↑n) • ⇑α + ⇑β) ≠ ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
·

Goal state after:
case inr.inr.refine_1
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 : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
⊢ ↑(chainTopCoeff (⇑α) β) - ↑n ≤ ↑(chainTopCoeff (⇑α) β) ∧ -(↑(chainTopCoeff (⇑α) β) - ↑n) ≤ ↑(chainBotCoeff (⇑α) β)
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2
ι : 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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
·

Goal state after:
case refine_2
ι : 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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_1
ι : 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
⊢ range P.reflectionPerm ⊆ ↑P.weylGroupToPerm.range

pp: case refine_2
ι : 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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflectionPerm)

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ range P.reflectionPerm ⊆ ↑P.weylGroupToPerm.range
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2
ι : 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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflectionPerm)

Tactic:
·

Goal state after:
case refine_2
ι : 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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflectionPerm)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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 : K
h : ⇑β = k • ⇑α
hα : α.IsZero
⊢ β = -α ∨ β = α

pp: case neg
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 : K
h : ⇑β = k • ⇑α
hα : ¬α.IsZero
⊢ β = -α ∨ β = α

Tactic:
·

Goal state after:
case pos
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 : K
h : ⇑β = k • ⇑α
hα : α.IsZero
⊢ β = -α ∨ β = α
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.inl
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
hα : ¬α.IsZero
h : ⇑β = -1 • ⇑α
⊢ β = -α ∨ β = α

pp: case neg.inr.inl
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
hα : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α

pp: case neg.inr.inr
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
hα : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
·

Goal state after:
case neg.inl
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
hα : ¬α.IsZero
h : ⇑β = -1 • ⇑α
⊢ β = -α ∨ β = α
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
h : Nontrivial ↥ρ.invtSubmodule
⊢ Nontrivial V

pp: case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule

Tactic:
·

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
h : Nontrivial ↥ρ.invtSubmodule
⊢ Nontrivial V
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule

Tactic:
·

Goal state after:
case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (m_1 : G),
    ((ofModule M).asAlgebraHom ((of k G) m_1)) m =
      (RestrictScalars.addEquiv k k[G] M).symm ((of k G) m_1 • (RestrictScalars.addEquiv k k[G] M) m)

pp: case add
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (x y : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom y) m =
          (RestrictScalars.addEquiv k k[G] M).symm (y • (RestrictScalars.addEquiv k k[G] M) m) →
        ((ofModule M).asAlgebraHom (x + y)) m =
          (RestrictScalars.addEquiv k k[G] M).symm ((x + y) • (RestrictScalars.addEquiv k k[G] M) m)

pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
·

Goal state after:
case of
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (m_1 : G),
    ((ofModule M).asAlgebraHom ((of k G) m_1)) m =
      (RestrictScalars.addEquiv k k[G] M).symm ((of k G) m_1 • (RestrictScalars.addEquiv k k[G] M) m)
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (x y : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom y) m =
          (RestrictScalars.addEquiv k k[G] M).symm (y • (RestrictScalars.addEquiv k k[G] M) m) →
        ((ofModule M).asAlgebraHom (x + y)) m =
          (RestrictScalars.addEquiv k k[G] M).symm ((x + y) • (RestrictScalars.addEquiv k k[G] M) m)

pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
·

Goal state after:
case add
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (x y : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom y) m =
          (RestrictScalars.addEquiv k k[G] M).symm (y • (RestrictScalars.addEquiv k k[G] M) m) →
        ((ofModule M).asAlgebraHom (x + y)) m =
          (RestrictScalars.addEquiv k k[G] M).symm ((x + y) • (RestrictScalars.addEquiv k k[G] M) m)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.inr.inl
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
hα : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α

pp: case neg.inr.inr
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
hα : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
·

Goal state after:
case neg.inr.inl
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
hα : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
·

Goal state after:
case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.inr.inr
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
hα : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
·

Goal state after:
case neg.inr.inr
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
hα : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (m : G) (t : k), (t • (of k G) m) • v = t • (of k G) m • v

pp: case add
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v

pp: case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (r : k) (x : k[G]), (∀ (t : k), (t • x) • v = t • x • v) → ∀ (t : k), (t • r • x) • v = t • (r • x) • v

Tactic:
·

Goal state after:
case of
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (m : G) (t : k), (t • (of k G) m) • v = t • (of k G) m • v
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v

pp: case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (r : k) (x : k[G]), (∀ (t : k), (t • x) • v = t • x • v) → ∀ (t : k), (t • r • x) • v = t • (r • x) • v

Tactic:
·

Goal state after:
case add
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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α : α.IsZero
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥

pp: case neg
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α : ¬α.IsZero
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥

Tactic:
·

Goal state after:
case pos
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α : α.IsZero
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥