mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ weightEquiv P P (x.comp y) = weightEquiv P P y ≪≫ₗ weightEquiv P P 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
P : RootPairing ι R M N
x y : P.Equiv P
⊢ weightEquiv P P x * weightEquiv P P y = weightEquiv P P y ≪≫ₗ weightEquiv P P 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
P : RootPairing ι R M N
x y : P.Equiv P
⊢ coweightEquiv P P (x.comp y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y

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.Equiv P
⊢ coweightEquiv P P x * coweightEquiv P P y = coweightEquiv P P y ≪≫ₗ coweightEquiv P P 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
⊢ ∀ (i j : ↥LieSubalgebra.root),
    ¬LinearIndependent K ![(rootSystem H).root i, (rootSystem H).root j] →
      (rootSystem H).root i = (rootSystem H).root j ∨ (rootSystem H).root i = -(rootSystem H).root j

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
x : k[G]
⊢ (leftRegular k G).norm x = 0 ↔ (linearCombination k fun x ↦ 1) x.coeff = 0

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
⊢ ker (leftRegular k G).norm = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k)).ker

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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : ((leftRegular k G) g) x = x
γ : G
⊢ x.coeff γ = x.coeff g

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✝² : 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)
⊢ (lmap fun x ↦ (ρ x) 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
ι₂✝ : 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
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
⊢ (↑(weightEquiv P Q f).symm).dualMap ∘ₗ ↑P.flip.toPerfPair = ↑Q.flip.toPerfPair ∘ₗ ↑(coweightEquiv P Q f).symm

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✝² : 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
⊢ (lmap fun x ↦ (ρ x) (g * h)) = (lmap fun x ↦ (ρ x) g) * lmap fun x ↦ (ρ x) h

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

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
g h : G
⊢ (ρV (g * h)).prodMap (ρW (g * h)) = (ρV g).prodMap (ρW g) * (ρV h).prodMap (ρW h)

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
W : Type u_4
inst✝⁵ : CommSemiring 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
⊢ TensorProduct.map (ρV 1) (ρW 1) = 1

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
W : Type u_4
inst✝⁵ : CommSemiring 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
g h : G
⊢ TensorProduct.map (ρV (g * h)) (ρW (g * h)) = TensorProduct.map (ρV g) (ρW g) * TensorProduct.map (ρV h) (ρW h)

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
htQ : t ∈ Q
⊢ ∀ (k : ι), (P.coroot' k) t = 0

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
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
⊢ (r •
      have this := x ⊗ₜ[k] y;
      this) =
    (r •
        have this := x;
        this) ⊗ₜ[k]
      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 = span K (⇑P.root '' {i | P.root i ∈ ↑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
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : k[G]
x : V
y : W
⊢ (r •
      have this := x ⊗ₜ[k] y;
      this) =
    x ⊗ₜ[k]
      (r •
        have this := y;
        this)

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
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
f₁ f₂ : V →ₗ[k] W
⊢ ρW g ∘ₗ (f₁ + f₂) ∘ₗ ρV g⁻¹ = ρW g ∘ₗ f₁ ∘ₗ ρV g⁻¹ + ρW g ∘ₗ f₂ ∘ₗ ρV g⁻¹

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
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
⊢ ⇑↑(weightEquiv P Q f).symm ∘ ⇑Q.root = ⇑P.root ∘ ⇑(↑f).indexEquiv.symm

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
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 : V →ₗ[k] W
⊢ ρW g ∘ₗ (r • f) ∘ₗ ρV g⁻¹ = (RingHom.id k) r • ρW g ∘ₗ f ∘ₗ ρV g⁻¹

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
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 : V →ₗ[k] W
⊢ { toFun := fun f ↦ ρW 1 ∘ₗ f ∘ₗ ρV 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } x = 1 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
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 : V →ₗ[k] W
⊢ { toFun := fun f ↦ ρW (g * h) ∘ₗ f ∘ₗ ρV (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } x =
    ({ toFun := fun f ↦ ρW g ∘ₗ f ∘ₗ ρV g⁻¹, map_add' := ⋯, map_smul' := ⋯ } *
        { toFun := fun f ↦ ρW h ∘ₗ f ∘ₗ ρV h⁻¹, map_add' := ⋯, map_smul' := ⋯ })
      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₂✝
ι₂ : 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
i : ι
⊢ (⇑↑(coweightEquiv P Q f).symm ∘ ⇑P.coroot) i = (⇑Q.coroot ∘ ⇑(↑f).indexEquiv.symm.symm) i

Tactic:
simp only [LinearEquiv.coe_coe, comp_apply, Equiv.symm_symm]

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
ι₂✝ : 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
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
i : ι
⊢ (coweightEquiv P Q f).symm (P.coroot i) = Q.coroot ((↑f).indexEquiv i)
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
f₁ f₂ : Dual k V
⊢ (f₁ + f₂) ∘ₗ ρV g⁻¹ = f₁ ∘ₗ ρV g⁻¹ + f₂ ∘ₗ ρV g⁻¹

Tactic:
by

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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
this✝ : ∀ (g : ↥P.weylGroup), q ∈ invtSubmodule (P.weylGroupRootRep g)
q' : ↥P.weylGroupRootRep.invtSubmodule := ⟨q, ⋯⟩
this : q' = ⊤
⊢ 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
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
⊢ (r • f) ∘ₗ ρV g⁻¹ = (RingHom.id k) r • f ∘ₗ ρV g⁻¹

Tactic:
by

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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
this : ∀ (g : ↥P.weylGroup), q ∈ invtSubmodule (P.weylGroupRootRep g)
⊢ 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
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
⊢ { toFun := fun f ↦ f ∘ₗ ρV 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } = 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
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
⊢ ⇑↑(coweightEquiv P Q f).symm ∘ ⇑P.coroot = ⇑Q.coroot ∘ ⇑(↑f).indexEquiv.symm.symm

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
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
⊢ { toFun := fun f ↦ f ∘ₗ ρV (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f ↦ f ∘ₗ ρV g⁻¹, map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f ↦ f ∘ₗ ρV h⁻¹, map_add' := ⋯, map_smul' := ⋯ }

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
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
⊢ Bijective ⇑↑(weightEquiv P Q f).symm

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
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
⊢ Bijective ⇑↑(coweightEquiv P Q f).symm

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
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
⊢ dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W

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✝⁴ : 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:
by

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✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
this : ↑q = ⊤
⊢ q = ⊥ ∨ 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✝⁴ : 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:
by

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✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
⊢ ↑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✝² : Monoid G
α : Type u_3
A : Type u_4
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
ρ : Representation k G A
g : G
x : α
a : A
⊢ ((ρ.finsupp α) g) (Finsupp.single x a) = Finsupp.single x ((ρ g) a)

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₂
P : RootPairing ι R M N
e : P.Equiv P
⊢ symm P P e * e = 1

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

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✝ : Nontrivial M
⊢ IsSimpleModule R[↥P.weylGroup] P.weylGroupRootRep.asModule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤

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₂
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)
⊢ (↑f).dualMap ∘ₗ ↑Q.flip.toPerfPair =
    ↑P.flip.toPerfPair ∘ₗ ↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm))

Tactic:
by

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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule ↑(P.coreflection i)
⊢ Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator ∈ invtSubmodule ↑(P.reflection i)

Tactic:
rw [LinearEquiv.map_mem_invtSubmodule_iff, LinearEquiv.symm_symm, toPerfPair_conj_reflection,
    Module.End.mem_invtSubmodule, ← Submodule.map_le_iff_le_comap]

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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule ↑(P.coreflection i)
⊢ Submodule.map (↑(P.coreflection i)).dualMap q.dualAnnihilator ≤ q.dualAnnihilator
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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule ↑(P.coreflection i)
⊢ Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator ∈ invtSubmodule ↑(P.reflection i)

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₂
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)
⊢ ⇑↑f ∘ ⇑P.root = ⇑Q.root ∘ ⇑e

Tactic:
by

Goal state after: