mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
m₁ : M₁ × M₂
⊢ Q₁ ((LinearMap.fst R M₁ M₂).toFun m₁) = (Q₁.prod 0) m₁

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R P
Q₂ : QuadraticMap R M₂ P
m₁ : M₁ × M₂
⊢ Q₂ ((LinearMap.snd R M₁ M₂).toFun m₁) = (prod 0 Q₂) m₁

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ polar (⇑(Q₁.prod Q₂)) x y = polar (⇑Q₁) x.1 y.1 + polar (⇑Q₂) x.2 y.2

Tactic:
dsimp [polar]

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ Q₁ (x.1 + y.1) + Q₂ (x.2 + y.2) - (Q₁ x.1 + Q₂ x.2) - (Q₁ y.1 + Q₂ y.2) =
    Q₁ (x.1 + y.1) - Q₁ x.1 - Q₁ y.1 + (Q₂ (x.2 + y.2) - Q₂ x.2 - Q₂ y.2)
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
⊢ ∀ x_1 ∈ Finset.univ, (Q x_1) (Pi.single i x x_1) = 0

Tactic:
intro j

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
⊢ j ∈ Finset.univ → (Q j) (Pi.single i x j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : M
⊢ ((Module.dualProdDualEquivDual R (Module.Dual R M) M).symm ((dualProd R M) x)).2 x✝ = x.1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : Module.Dual R M
⊢ ((Module.dualProdDualEquivDual R (Module.Dual R M) M).symm ((dualProd R M) x)).1 x✝ = x✝ x.2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ polar (⇑(pi Q)) x y = ∑ i, polar (⇑(Q i)) (x i) (y i)

Tactic:
dsimp [polar]

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ (pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ ∑ i, polar (⇑(Q i)) (x i) (y i) =
    ((∑ i, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i)) x) y

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
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥
W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, genWeightSpace_ne_bot' := h }
⊢ (↑2 * 2⁻¹) • ⇑α = ⇑α

Tactic:
simp

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

Goal state before:
pp: case refine_2.mul
ι : 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
w w₁ w₂ : P.Aut
hw₁ : w₁ ∈ Subgroup.closure (range (Equiv.reflection P))
hw₂ : w₂ ∈ Subgroup.closure (range (Equiv.reflection P))
h₁ : ((Equiv.weightHom P).domRestrict P.weylGroup) ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range P.reflection)
h₂ : ((Equiv.weightHom P).domRestrict P.weylGroup) ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range P.reflection)
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup) ⟨w₁ * w₂, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
| mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>

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

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 : ι
⊢ (Equiv.coweightHom P) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

Tactic:
simp

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

Goal state before:
pp: case refine_2.mul
ι : 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
w w₁ w₂ : P.Aut
hw₁ : w₁ ∈ Subgroup.closure (range (Equiv.reflection P))
hw₂ : w₂ ∈ Subgroup.closure (range (Equiv.reflection P))
h₁ :
  ((Equiv.coweightHom P).domRestrict P.weylGroup) ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
h₂ :
  ((Equiv.coweightHom P).domRestrict P.weylGroup) ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup) ⟨w₁ * w₂, ⋯⟩ ∈
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
| mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>

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

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 : ι
⊢ (Equiv.indexHom P) (Equiv.reflection P i) = P.reflectionPerm i

Tactic:
simp

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

Goal state before:
pp: case refine_2.mul
ι : 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
w w₁ w₂ : P.Aut
hw₁ : w₁ ∈ Subgroup.closure (range (Equiv.reflection P))
hw₂ : w₂ ∈ Subgroup.closure (range (Equiv.reflection P))
h₁ : P.weylGroupToPerm ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range P.reflectionPerm)
h₂ : P.weylGroupToPerm ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range P.reflectionPerm)
⊢ P.weylGroupToPerm ⟨w₁ * w₂, ⋯⟩ ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
| mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>

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

Goal state before:
pp: case mem
ι : 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
B : P.InvariantForm
g : P.Aut
i : ι
⊢ ∀ (x y : M), (B.form (⟨Equiv.reflection P i, ⋯⟩ • x)) (⟨Equiv.reflection P i, ⋯⟩ • y) = (B.form x) y

Tactic:
simp

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

Goal state before:
pp: case one
ι : 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
B : P.InvariantForm
g : P.Aut
⊢ ∀ (x y : M), (B.form (⟨1, ⋯⟩ • x)) (⟨1, ⋯⟩ • y) = (B.form x) y

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
⊢ LinearMap.id.dualMap ∘ₗ ↑P.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ LinearMap.id

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
⊢ ⇑LinearMap.id ∘ ⇑P.root = ⇑P.root ∘ ⇑(Equiv.refl ι)

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
⊢ ⇑LinearMap.id ∘ ⇑P.coroot = ⇑P.coroot ∘ ⇑(Equiv.refl ι).symm

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mp
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
g : G
x : V
⊢ x = (ρ g) ((ρ g⁻¹) x)

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mpr
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
g : G
y : V
⊢ (ρ g⁻¹) ((ρ g) y) = y

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✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ρ.asAlgebraHom (MonoidAlgebra.single g 1) = ρ g

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✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ r • x = ρ.asModuleEquiv ((algebraMap k k[G]) r • ρ.asModuleEquiv.symm 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✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g) x = ρ.asModuleEquiv ((of k G) g • ρ.asModuleEquiv.symm x)

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : ↥ρ.invtSubmodule
p : Submodule k V
hp : p ∈ ρ.invtSubmodule
⊢ ⟨p, hp⟩ ≤ ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : ↥ρ.invtSubmodule
p : Submodule k V
hp : p ∈ ρ.invtSubmodule
⊢ ⟨⊥, ⋯⟩ ≤ ⟨p, hp⟩

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
ι₂ : 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₁
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₁.Hom P₂
f : P.Hom P₁
i : ι₂
⊢ (⇑P.coroot ∘ ⇑f.indexEquiv.symm ∘ ⇑g.indexEquiv.symm) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i

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₂
f : P.Hom 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_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₂
f : P.Hom 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_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₂
f : P.Hom Q
x : ι
⊢ (f.comp (id P)).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
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : RestrictScalars k k[G] ρ.asModule
⊢ (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (MonoidAlgebra.single g 1 • (RestrictScalars.addEquiv k k[G] ρ.asModule) x) =
    (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k k[G] ρ.asModule) 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₂
f : P.Hom 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_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₂
f : P.Hom 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_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₂
f : P.Hom Q
x : ι
⊢ ((id Q).comp f).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_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : 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₂
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₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom 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_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : 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₂
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₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom 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_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : 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₂
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₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom 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: case of
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (m : G) (t : k), (t • (of k G) m) • v = t • (of k G) m • v

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

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
x✝ : V
⊢ x✝ ∈
      ↑((fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩)
          ((fun p ↦
              let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
            p)) ↔
    x✝ ∈ ↑p

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
g h : P.End
x✝ : M
⊢ (g * h).weightMap x✝ = (g.weightMap * h.weightMap) 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✝⁴ : Semiring k
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x✝ : V
⊢ ∀ (x : G), (ρ x) ((ρ g) x✝) = (ρ (x * 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
inst✝⁴ : Semiring k
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x✝ : V
⊢ ∀ (x : G), (ρ g) ((ρ x) x✝) = (ρ (g * 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
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W
x✝ : ↥W
⊢ ↑(((ρ 1).restrict ⋯) x✝) = ↑(1 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✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid 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✝ : ↥W
⊢ ↑(((ρ (x✝² * x✝¹)).restrict ⋯) x✝) = ↑(((ρ x✝²).restrict ⋯ * (ρ x✝¹).restrict ⋯) x✝)

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

Tactic:
simp

Goal state after: