mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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✝ : ↥P.invtRootSubmodule
p : Submodule R M
hp : p ∈ P.invtRootSubmodule
⊢ ⟨⊥, ⋯⟩ ≤ ⟨p, hp⟩

Tactic:
simp

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
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W
x✝ : V
⊢ (W.mapQ W (ρ 1) ⋯ ∘ₗ W.mkQ) x✝ = (1 ∘ₗ W.mkQ) x✝

Tactic:
simp

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
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:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : N
⊢ f.coweightMap x = g.coweightMap x

Tactic:
dsimp [coweightHom] at hfg
    simp_all

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

Tactic:
simp

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

Tactic:
simp

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

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✝ 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:
simp

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})
this : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = univ
⊢ span K (range ⇑P.root) = ⊤

Tactic:
simp

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:
simp

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:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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
x : M
⊢ (↑(f.comp (id P))).weightMap x = (↑f).weightMap x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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
x : N₂
⊢ (↑(f.comp (id P))).coweightMap x = (↑f).coweightMap x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
x : ι
⊢ (↑(f.comp (id P))).indexEquiv x = (↑f).indexEquiv x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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
x : M
⊢ (↑((id Q).comp f)).weightMap x = (↑f).weightMap x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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
x : N₂
⊢ (↑((id Q).comp f)).coweightMap x = (↑f).coweightMap x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
x : ι
⊢ (↑((id Q).comp f)).indexEquiv x = (↑f).indexEquiv x

Tactic:
simp

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
h₁ h₂ : H
⊢ (fun x ↦ g • x) h₁ = (fun x ↦ g • x) h₂ → h₁ = h₂

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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₁
x✝ : M
⊢ (↑((h.comp g).comp f)).weightMap x✝ = (↑(h.comp (g.comp f))).weightMap x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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₁
x✝ : N₃
⊢ (↑((h.comp g).comp f)).coweightMap x✝ = (↑(h.comp (g.comp f))).coweightMap x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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₁
x✝ : ι
⊢ (↑((h.comp g).comp f)).indexEquiv x✝ = (↑(h.comp (g.comp f))).indexEquiv x✝

Tactic:
simp

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:
simp

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:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
⊢ (ρV 1).prodMap (ρW 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : Dual k V
x✝ : V
⊢ ((r • f) ∘ₗ ρV g⁻¹) x✝ = ((RingHom.id k) r • f ∘ₗ ρV g⁻¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
x✝¹ : Dual k V
x✝ : V
⊢ ({ toFun := fun f ↦ f ∘ₗ ρV 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ = (1 x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x✝¹ : Dual k V
x✝ : V
⊢ ({ toFun := fun f ↦ f ∘ₗ ρV (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (({ toFun := fun f ↦ f ∘ₗ ρV g⁻¹, map_add' := ⋯, map_smul' := ⋯ } *
          { toFun := fun f ↦ f ∘ₗ ρV h⁻¹, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
x✝¹ : α
x✝ : A
⊢ ((Finsupp.lsum k) fun i ↦ Finsupp.lsingle i ∘ₗ ρ 1) (Finsupp.single x✝¹ x✝) = 1 (Finsupp.single x✝¹ x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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₂
P : RootPairing ι R M N
e : P.Equiv P
m : M
⊢ (weightEquiv P P (symm P P e * e)) m = (↑1).weightMap m

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
x✝³ x✝² : G
x✝¹ : α
x✝ : A
⊢ ((Finsupp.lsum k) fun i ↦ Finsupp.lsingle i ∘ₗ ρ (x✝³ * x✝²)) (Finsupp.single x✝¹ x✝) =
    (((Finsupp.lsum k) fun i ↦ Finsupp.lsingle i ∘ₗ ρ x✝³) * (Finsupp.lsum k) fun i ↦ Finsupp.lsingle i ∘ₗ ρ x✝²)
      (Finsupp.single x✝¹ x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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₂
P : RootPairing ι R M N
e : P.Equiv P
m : N
⊢ (coweightEquiv P P (symm P P e * e)) m = (↑1).coweightMap m

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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₂
P : RootPairing ι R M N
e : P.Equiv P
m : ι
⊢ (↑(symm P P e * e)).indexEquiv m = (↑1).indexEquiv m

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Monoid G
α : Type u_3
g h : G
i : α
r : k
⊢ ((free k G α) g) (Finsupp.single i (MonoidAlgebra.single h r)) = Finsupp.single i (MonoidAlgebra.single (g * h) r)

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
y : α →₀ k[G]
⊢ 0 • y = ((free k G α).asAlgebraHom 0) y

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.zero
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
⊢ MonoidAlgebra.single g a • 0 = ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) 0

Tactic:
simp

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₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
x✝¹ : N₂
x✝ : M
⊢ (((↑f).dualMap ∘ₗ ↑Q.flip.toPerfPair) x✝¹) x✝ =
    ((↑P.flip.toPerfPair ∘ₗ ↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm))) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.single.zero
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
h : α
⊢ MonoidAlgebra.single g a • Finsupp.single h 0 =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.single.single
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
h : α
i : G
b : k
⊢ MonoidAlgebra.single g a • Finsupp.single h (MonoidAlgebra.single i b) =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h (MonoidAlgebra.single i b))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: ⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: ⊢ ¬(∅.Nonempty ∧ BddBelow ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s ∈ s

Tactic:
by
  convert! (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
  exact dif_pos ⟨h1, h2⟩

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
⊢ ∀ i ∈ {i | ¬Disjoint q (R ∙ P.root i)}, ¬Disjoint q (R ∙ P.root i)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
i : ι
hi : Disjoint q (R ∙ P.root i)
⊢ (P.coroot' i) (P.root i) = 2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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₂
P : RootPairing ι R M N
f : P.Aut
x✝ : M
⊢ (↑f * ↑(symm P P f)).weightMap x✝ = (Hom.weightMap 1) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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₂
P : RootPairing ι R M N
f : P.Aut
x✝ : N
⊢ (↑f * ↑(symm P P f)).coweightMap x✝ = (Hom.coweightMap 1) x✝

Tactic:
simp

Goal state after: