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✝⁵ : Semiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ ↑(y * MulOpposite.unop z) = ↑y

Tactic:
by

Goal state after:
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 = ⊥ ↔ ∀ (i : ι), P.root i ∉ ↑q

Tactic:
by

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
⊢ Function.Injective (coroot ∘ Subtype.val)

Tactic:
by

Goal state after:
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✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
h : q = ⊤
⊢ range ⇑P.root ⊆ ↑↑q

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
⊢ QuotientGroup.con S ≤ Con.ker ρ

Tactic:
by

Goal state after:
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✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
h : range ⇑P.root ⊆ ↑↑q
⊢ q = ⊤

Tactic:
by

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
x✝ : ↥LieSubalgebra.root
α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
⊢ α.IsNonZero

Tactic:
by

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
x✝ : ↥LieSubalgebra.root
α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
⊢ (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } ⟨α, hα⟩))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } ⟨α, hα⟩) =
    2

Tactic:
by

Goal state after:
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
⊢ (Fin.init fun j ↦ (ρ (g ^ ↑j)) x) = fun j ↦ (ρ (g ^ ↑j)) x

Tactic:
by

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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
⊢ β.IsNonZero

Tactic:
by

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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
⊢ (reflectRoot α β).IsNonZero

Tactic:
by

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
⊢ ∀ (i : ↥LieSubalgebra.root),
    Set.MapsTo
      (⇑(preReflection ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } i)
          (LinearMap.id.flip ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } i))))
      (Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ })
      (Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ })

Tactic:
by

Goal state after:
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
⊢ Injective ⇑(coweightHom P)

Tactic:
by

Goal state after:
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
⊢ indexEquiv 1 = 1

Tactic:
by

Goal state after:
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 * y).indexEquiv = x.indexEquiv * y.indexEquiv

Tactic:
by

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
⊢ Submodule.span K (Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ }) = ⊤

Tactic:
by

Goal state after:
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})
⊢ {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = univ

Tactic:
by

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
α β : ↥LieSubalgebra.root
⊢ ↑(↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) =
    (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } α))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } β)

Tactic:
by

Goal state after:
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
⊢ (↑e).weightMap ((weightEquiv P Q e).symm m) = m

Tactic:
by

Goal state after:
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
n : ℕ
g : G
x : V
⊢ (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x

Tactic:
by

Goal state after:
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
⊢ (↑e).coweightMap ((coweightEquiv P Q e).symm n) = n

Tactic:
by

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
⊢ (rootSystem H).CorootForm = (killingForm K L).restrict H.toSubmodule

Tactic:
by

Goal state after:
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
⊢ ↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ 1 • x) ∘ₗ ↑(coeffLinearEquiv k) = 1

Tactic:
by

Goal state after:
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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective ⇑((↑g).comp ↑f).weightMap

Tactic:
by

Goal state after:
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})
⊢ S ⊔ T = ⊤

Tactic:
by

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

Tactic:
by

Goal state after:
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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective ⇑((↑g).comp ↑f).coweightMap

Tactic:
by

Goal state after:
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
⊢ ↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ (x * y) • x_1) ∘ₗ ↑(coeffLinearEquiv k) =
    ↑(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)

Tactic:
by

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
this : ⨆ α, ⨆ (_ : α.IsNonZero), corootSpace ⇑α = ⊤
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSubmodule α ≤ H.toLieSubmodule

Tactic:
by

Goal state after:
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
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ ↑(g.comp f) = (↑g).comp ↑f

Tactic:
by

Goal state after:
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
g : G
x : H
r : k
⊢ ((ofMulAction k G H) g) (MonoidAlgebra.single x r) = MonoidAlgebra.single (g • x) r

Tactic:
by

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
this : ⨆ α, ⨆ (_ : α.IsNonZero), corootSpace ⇑α = ⊤
⊢ H.toLieSubmodule ≤ ⨆ α, ⨆ (_ : α.IsNonZero), corootSubmodule α

Tactic:
by

Goal state after:
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
⊢ (let __src := (DistribMulAction.toAddMonoidEnd G A) 1;
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    1

Tactic:
by

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
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSubmodule α = H.toLieSubmodule

Tactic:
by

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

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
α β : ↥LieSubalgebra.root
⊢ (algebraMap ℤ K) (↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) = (rootSystem H).pairing α β

Tactic:
by

Goal state after:
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
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ f.comp (id P) = f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
A : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module k A
G : Type u_4
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
⊢ (ofDistribMulAction k G A).norm x = ∑ g, g • x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: G M : Type
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : Additive M
⊢ Additive.toMul ((ofMulDistribMulAction G M).norm x) = ∏ g, g • Additive.toMul x

Tactic:
by

Goal state after:
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
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ (id Q).comp f = f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective fun x ↦ g • x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
⊢ (((ofMulAction k G H) g) f).coeff h = f.coeff (g⁻¹ • h)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

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

Tactic:
by

Goal state after:
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 + t ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
⊢ ∀ (m : k[G]) (x : (ofMulAction k G G).asModule),
    (ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun (m • x) =
      (RingHom.id k[G]) m • (ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(ρ.asGroupHom g) = ρ g

Tactic:
by

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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
⊢ β.IsNonZero

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
i : G
⊢ ∀ (i_1 : G), i_1 ∈ Finset.univ ↔ i_1 * i ∈ Finset.univ

Tactic:
by

Goal state after:
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
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup N₁
inst✝⁸ : Module R N₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
i : G
⊢ ∀ i_1 ∈ Finset.univ, MonoidAlgebra.single (i_1 * i) 1 = MonoidAlgebra.single (i_1 * i) 1

Tactic:
by

Goal state after:
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
⊢ t ∈ Q

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
⊢ (leftRegular k G).norm =
    (lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
      (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k)

Tactic:
by

Goal state after: