mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ext

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

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

Tactic:
ext

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

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

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

Tactic:
ext

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

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

Tactic:
rw [this, add_zero]; exact hs

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.comp y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : M
⊢ (weightEquiv P P (x.comp y)) x✝ = (weightEquiv P P y ≪≫ₗ weightEquiv P P x) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
⊢ coweightEquiv P P (x.comp y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : N
⊢ (coweightEquiv P P (x.comp y)) x✝ = (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) x✝
Module: Mathlib.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]
⊢ ((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
          (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
        x =
      0 ↔
    (linearCombination k fun x ↦ 1) x.coeff = 0

Tactic:
constructor

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

case mpr
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
⊢ (linearCombination k fun x ↦ 1) x.coeff = 0 →
    ((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
          (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
        x =
      0
Module: Mathlib.RepresentationTheory.Basic

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

Tactic:
ext

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
h : (linearCombination k fun x ↦ 1) x.coeff = 0
a✝ : G
⊢ (((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
            (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
          x).coeff
      a✝ =
    (coeff 0) a✝
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:
ext

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x✝ : k[G]
⊢ x✝ ∈ ker (leftRegular k G).norm ↔ x✝ ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k)).ker
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:
ext

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

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

Tactic:
ext

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

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

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

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

Goal state after:
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
x✝² : Dual k V
x✝¹ : W
x✝ : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g))) x✝²) x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((ρV.linHom ρW) g ∘ₗ dualTensorHom k V W)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : 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:
ext

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₂
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✝
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:
ext

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₂
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✝ : ι
⊢ (⇑↑f ∘ ⇑P.root) x✝ = (⇑Q.root ∘ ⇑e) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case he
ι : 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)
g : N ≃ₗ[R] N₂ := ⋯
⊢ Q.toLinearMap = (RootPairing.map e f g).toLinearMap

Tactic:
ext

Goal state after:
case he
ι : 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)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝¹ : M₂
x✝ : N₂
⊢ (Q.toLinearMap x✝¹) x✝ = ((RootPairing.map e f g).toLinearMap x✝¹) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case hr
ι : 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)
g : N ≃ₗ[R] N₂ := ⋯
⊢ Q.root = (RootPairing.map e f g).root

Tactic:
ext

Goal state after:
case hr
ι : 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)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : 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
⊢ ↑f * ↑(symm P P f) = 1

Tactic:
ext

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

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✝

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
f : P.Aut
x✝ : ι
⊢ (↑f * ↑(symm P P f)).indexEquiv x✝ = (Hom.indexEquiv 1) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : 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
⊢ ↑(symm P P f) * ↑f = 1

Tactic:
ext

Goal state after:
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
⊢ (↑(symm P P f) * ↑f).weightMap x✝ = (Hom.weightMap 1) x✝

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
⊢ (↑(symm P P f) * ↑f).coweightMap x✝ = (Hom.coweightMap 1) x✝

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
f : P.Aut
x✝ : ι
⊢ (↑(symm P P f) * ↑f).indexEquiv x✝ = (Hom.indexEquiv 1) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h
ι : 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.Endˣ
⊢ LeftInverse ⇑f.inv.weightMap ⇑(↑f).weightMap ∧ RightInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

Tactic:
constructor

Goal state after:
case h.left
ι : 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.Endˣ
⊢ LeftInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

case h.right
ι : 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.Endˣ
⊢ RightInverse ⇑f.inv.weightMap ⇑(↑f).weightMap