mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W
x✝² x✝¹ : G
x✝ : V
⊢ (W.mapQ W (ρ (x✝² * x✝¹)) ⋯ ∘ₗ W.mkQ) x✝ = ((W.mapQ W (ρ x✝²) ⋯ * W.mapQ W (ρ x✝¹) ⋯) ∘ₗ W.mkQ) x✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W
x✝² x✝¹ : G
x✝ : V
⊢ (W.mapQ W (ρ (x✝² * x✝¹)) ⋯ ∘ₗ W.mkQ) x✝ = ((W.mapQ W (ρ x✝²) ⋯ * W.mapQ W (ρ x✝¹) ⋯) ∘ₗ W.mkQ) x✝
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
α β : ↥LieSubalgebra.root
h : (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) β
⊢ α = β

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
α β : ↥LieSubalgebra.root
h : (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) β
⊢ α = β
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
α β : ↥LieSubalgebra.root
h : (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) β
x : ↥H
⊢ ↑α x = ↑β x

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
α β : ↥LieSubalgebra.root
h : (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) β
x : ↥H
⊢ ↑α x = ↑β x
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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
h : (coroot ∘ Subtype.val) ⟨α, hα⟩ = (coroot ∘ Subtype.val) ⟨β, hβ⟩
⊢ ⟨α, hα⟩ = ⟨β, hβ⟩

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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
h : (coroot ∘ Subtype.val) ⟨α, hα⟩ = (coroot ∘ Subtype.val) ⟨β, hβ⟩
⊢ ⟨α, hα⟩ = ⟨β, hβ⟩
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h : (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x
x✝ : Fin (n + 1)
⊢ Fin.init (fun j ↦ (ρ (g ^ ↑j)) x) x✝ = (ρ (g ^ ↑x✝)) x

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h : (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x
x✝ : Fin (n + 1)
⊢ Fin.init (fun j ↦ (ρ (g ^ ↑j)) x) x✝ = (ρ (g ^ ↑x✝)) x
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
x✝ : ι
⊢ (indexEquiv 1) x✝ = 1 x✝

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
x✝ : ι
⊢ (indexEquiv 1) x✝ = 1 x✝
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case e'_6
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
⊢ Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } = Weight.toLinear K (↥H) L '' {α | α.IsNonZero}

Tactic:
;

Goal state after:
case e'_6
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
⊢ Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } = Weight.toLinear K (↥H) L '' {α | α.IsNonZero}
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
x y : P.End
x✝ : ι
⊢ (x * y).indexEquiv x✝ = (x.indexEquiv * y.indexEquiv) x✝

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
x y : P.End
x✝ : ι
⊢ (x * y).indexEquiv x✝ = (x.indexEquiv * y.indexEquiv) x✝
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case e'_6
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
x✝ : Dual K ↥H
⊢ x✝ ∈ Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } ↔
    x✝ ∈ Weight.toLinear K (↥H) L '' {α | α.IsNonZero}

Tactic:
;

Goal state after:
case e'_6
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
x✝ : Dual K ↥H
⊢ x✝ ∈ Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } ↔
    x✝ ∈ Weight.toLinear K (↥H) L '' {α | α.IsNonZero}
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
x✝ : ι
⊢ x✝ ∈ {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} ↔ x✝ ∈ univ

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
x✝ : ι
⊢ x✝ ∈ {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} ↔ x✝ ∈ univ
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x✝ a✝ : H
⊢ (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ 1 • x) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ lsingle x✝)
          1).coeff
      a✝ =
    ((1 ∘ₗ lsingle x✝) 1).coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x✝ a✝ : H
⊢ (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ 1 • x) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ lsingle x✝)
          1).coeff
      a✝ =
    ((1 ∘ₗ lsingle x✝) 1).coeff a✝
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : G
x✝ a✝ : H
⊢ (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ (x * y) • x_1) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝ =
    (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ x • x_1) ∘ₗ ↑(coeffLinearEquiv k) *
              ↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ y • x) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝

Tactic:
;

Goal state after:
k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : G
x✝ a✝ : H
⊢ (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ (x * y) • x_1) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝ =
    (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ x • x_1) ∘ₗ ↑(coeffLinearEquiv k) *
              ↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ y • x) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝ : A
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) 1;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝ =
    1 x✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝ : A
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) 1;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝ =
    1 x✝
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
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSubmodule α = H.toLieSubmodule

Tactic:
suffices ⨆ α : Weight K H L, ⨆ (_ : α.IsNonZero), corootSpace α = ⊤ from
    le_antisymm (by simp) (by simp [← LieSubmodule.map_iSup, this])

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
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSpace ⇑α = ⊤
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝ y✝ : G
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) (x✝ * y✝);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    (let __src := (DistribMulAction.toAddMonoidEnd G A) x✝;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) *
      let __src := (DistribMulAction.toAddMonoidEnd G A) y✝;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝ y✝ : G
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) (x✝ * y✝);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    (let __src := (DistribMulAction.toAddMonoidEnd G A) x✝;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) *
      let __src := (DistribMulAction.toAddMonoidEnd G A) y✝;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝¹ y✝ : G
x✝ : A
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) (x✝¹ * y✝);
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝ =
    ((let __src := (DistribMulAction.toAddMonoidEnd G A) x✝¹;
        { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) *
        let __src := (DistribMulAction.toAddMonoidEnd G A) y✝;
        { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
A : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x✝¹ y✝ : G
x✝ : A
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) (x✝¹ * y✝);
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝ =
    ((let __src := (DistribMulAction.toAddMonoidEnd G A) x✝¹;
        { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) *
        let __src := (DistribMulAction.toAddMonoidEnd G A) y✝;
        { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      x✝
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
y : k[G]
g a✝ : G
⊢ (((ofMulAction k G G).asAlgebraHom ((of k G) g)) y).coeff a✝ = ((of k G) g * y).coeff a✝

Tactic:
;

Goal state after:
case of
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
y : k[G]
g a✝ : G
⊢ (((ofMulAction k G G).asAlgebraHom ((of k G) g)) y).coeff a✝ = ((of k G) g * y).coeff a✝
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s ∈ S

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s ∈ S
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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
x : ↥H
⊢ β x = (u • ⇑α) x

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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
x : ↥H
⊢ β x = (u • ⇑α) x
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
x y : P.Equiv P
x✝ : M
⊢ (weightEquiv P P (x.comp y)) x✝ = (weightEquiv P P y ≪≫ₗ weightEquiv P P x) x✝

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
x y : P.Equiv P
x✝ : M
⊢ (weightEquiv P P (x.comp y)) x✝ = (weightEquiv P P y ≪≫ₗ weightEquiv P P x) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
x y : P.Equiv P
x✝ : N
⊢ (coweightEquiv P P (x.comp y)) x✝ = (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) x✝

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
x y : P.Equiv P
x✝ : N
⊢ (coweightEquiv P P (x.comp y)) x✝ = (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) x✝
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
⊢ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩

Tactic:
;

Goal state after:
case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
⊢ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
x : ↥H
⊢ ((rootSystem H).root ⟨α, hα⟩) x = (-(rootSystem H).root ⟨β, hβ⟩) x

Tactic:
;

Goal state after:
case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
x : ↥H
⊢ ((rootSystem H).root ⟨α, hα⟩) x = (-(rootSystem H).root ⟨β, hβ⟩) x
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩

Tactic:
;

Goal state after:
case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
x : ↥H
⊢ ((rootSystem H).root ⟨α, hα⟩) x = ((rootSystem H).root ⟨β, hβ⟩) x

Tactic:
;

Goal state after:
case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
x : ↥H
⊢ ((rootSystem H).root ⟨α, hα⟩) x = ((rootSystem H).root ⟨β, hβ⟩) x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
ι : Type u_3
V : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (V i)
inst✝ : (i : ι) → Module k (V i)
ρ : (i : ι) → Representation k G (V i)
x✝ : ⨁ (i : ι), V i
i✝ : ι
⊢ ((lmap fun x ↦ (ρ x) 1) x✝) i✝ = (1 x✝) i✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
ι : Type u_3
V : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (V i)
inst✝ : (i : ι) → Module k (V i)
ρ : (i : ι) → Representation k G (V i)
x✝ : ⨁ (i : ι), V i
i✝ : ι
⊢ ((lmap fun x ↦ (ρ x) 1) x✝) i✝ = (1 x✝) i✝
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
ι : Type u_3
V : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (V i)
inst✝ : (i : ι) → Module k (V i)
ρ : (i : ι) → Representation k G (V i)
g h : G
x✝ : ⨁ (i : ι), V i
i✝ : ι
⊢ ((lmap fun x ↦ (ρ x) (g * h)) x✝) i✝ = (((lmap fun x ↦ (ρ x) g) * lmap fun x ↦ (ρ x) h) x✝) i✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
ι : Type u_3
V : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (V i)
inst✝ : (i : ι) → Module k (V i)
ρ : (i : ι) → Representation k G (V i)
g h : G
x✝ : ⨁ (i : ι), V i
i✝ : ι
⊢ ((lmap fun x ↦ (ρ x) (g * h)) x✝) i✝ = (((lmap fun x ↦ (ρ x) g) * lmap fun x ↦ (ρ x) h) x✝) i✝