awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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₁
h :
  ∀ (φ : N₂) (x : M),
    Eq.{u_2 + 1} (α := R)
      (((((g.weightMap ∘ₗ f.weightMap).dualMap ∘ₗ (↑P₂.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) :
                  (a : N₂) → Module.Dual R M)
                φ :
              Module.Dual R M) :
            (a : M) → R)
          x :
        R)
      (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap ∘ₗ g.coweightMap : (a : N₂) → Module.Dual R M)
                φ :
              Module.Dual R M) :
            (a : M) → R)
          x :
        R)
⊢ (g.weightMap ∘ₗ f.weightMap).dualMap ∘ₗ (↑P₂.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap ∘ₗ g.coweightMap

Tactic:
ext φ x
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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₁
h :
  ∀ (i : ι),
    Eq.{u_9 + 1} (α := M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(g.weightMap ∘ₗ f.weightMap) : (a : M) → M₂)
        (⇑P.root : (a : ι) → M) i)
      (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑P₂.root : (a : ι₂) → M₂)
        (⇑(f.indexEquiv.trans g.indexEquiv) : (a : ι) → ι₂) i)
⊢ Eq (α := ι → M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(g.weightMap ∘ₗ f.weightMap) : (a : M) → M₂)
      (⇑P.root : (a : ι) → M))
    (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑P₂.root : (a : ι₂) → M₂)
      (⇑(f.indexEquiv.trans g.indexEquiv) : (a : ι) → ι₂))

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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 : ι
h :
  Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M)
      (Function.comp.{u_3 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂) (⇑f.weightMap : (a : M) → M₁))
      (⇑P.root : (a : ι) → M) i)
    (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑P₂.root : (a : ι₂) → M₂)
      (Function.comp.{u_1 + 1, u_5 + 1, u_8 + 1} (β := ι₁) (⇑g.indexEquiv : (a : ι₁) → ι₂)
        (⇑f.indexEquiv : (a : ι) → ι₁))
      i)
⊢ Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(g.weightMap ∘ₗ f.weightMap) : (a : M) → M₂)
      (⇑P.root : (a : ι) → M) i)
    (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑P₂.root : (a : ι₂) → M₂)
      (⇑(f.indexEquiv.trans g.indexEquiv) : (a : ι) → ι₂) i)

Tactic:
simp only [LinearMap.coe_comp, Equiv.coe_trans]

Premises used: LinearMap.coe_comp, Equiv.coe_trans
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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₁
h :
  ∀ (i : ι₂),
    Eq.{u_4 + 1} (α := N)
      (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(f.coweightMap ∘ₗ g.coweightMap) : (a : N₂) → N)
        (⇑P₂.coroot : (a : ι₂) → N₂) i)
      (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
        (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)
⊢ Eq (α := ι₂ → N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(f.coweightMap ∘ₗ g.coweightMap) : (a : N₂) → N)
      (⇑P₂.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι))

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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 : ι₂
h :
  Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂)
      (Function.comp.{u_10 + 1, u_7 + 1, u_4 + 1} (β := N₁) (⇑f.coweightMap : (a : N₁) → N)
        (⇑g.coweightMap : (a : N₂) → N₁))
      (⇑P₂.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)
⊢ Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(f.coweightMap ∘ₗ g.coweightMap) : (a : N₂) → N)
      (⇑P₂.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)

Tactic:
simp only [LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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 : ι₂
h :
  Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (Function.comp.{u_8 + 1, u_5 + 1, u_1 + 1} (β := ι₁) (⇑f.indexEquiv.symm : (a : ι₁) → ι)
        (⇑g.indexEquiv.symm : (a : ι₂) → ι₁))
      i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)
⊢ Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂)
      (Function.comp.{u_10 + 1, u_7 + 1, u_4 + 1} (β := N₁) (⇑f.coweightMap : (a : N₁) → N)
        (⇑g.coweightMap : (a : N₂) → N₁))
      (⇑P₂.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)

Tactic:
rw [comp_assoc, g.coroot_coweightMap, ← comp_assoc, f.coroot_coweightMap, comp_assoc]

Premises used: RootPairing.Hom.coroot_coweightMap, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : 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 : ι₂
⊢ Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (Function.comp.{u_8 + 1, u_5 + 1, u_1 + 1} (β := ι₁) (⇑f.indexEquiv.symm : (a : ι₁) → ι)
        (⇑g.indexEquiv.symm : (a : ι₂) → ι₁))
      i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(f.indexEquiv.trans g.indexEquiv).symm : (a : ι₂) → ι) i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
weightMap :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₂) (((f.comp (id P)).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((f.comp (id P)).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)
indexEquiv :
  ∀ (x : ι),
    Eq.{u_5 + 1} (α := ι₂) (((f.comp (id P)).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)
⊢ f.comp (id P) = f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : M
⊢ Eq.{u_6 + 1} (α := M₂) (((f.comp (id P)).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : N₂
⊢ Eq.{u_4 + 1} (α := N) (((f.comp (id P)).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : ι
⊢ Eq.{u_5 + 1} (α := ι₂) (((f.comp (id P)).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
weightMap :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₂) ((((id Q).comp f).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) ((((id Q).comp f).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)
indexEquiv :
  ∀ (x : ι),
    Eq.{u_5 + 1} (α := ι₂) ((((id Q).comp f).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)
⊢ (id Q).comp f = f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : M
⊢ Eq.{u_6 + 1} (α := M₂) ((((id Q).comp f).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : N₂
⊢ Eq.{u_4 + 1} (α := N) ((((id Q).comp f).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
x : ι
⊢ Eq.{u_5 + 1} (α := ι₂) ((((id Q).comp f).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : 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₁
weightMap :
  ∀ (x : M),
    Eq.{u_12 + 1} (α := M₃) ((((h.comp g).comp f).weightMap : (a : M) → M₃) x : M₃)
      (((h.comp (g.comp f)).weightMap : (a : M) → M₃) x : M₃)
coweightMap :
  ∀ (x : N₃),
    Eq.{u_4 + 1} (α := N) ((((h.comp g).comp f).coweightMap : (a : N₃) → N) x : N)
      (((h.comp (g.comp f)).coweightMap : (a : N₃) → N) x : N)
indexEquiv :
  ∀ (x : ι),
    Eq.{u_11 + 1} (α := ι₃) ((((h.comp g).comp f).indexEquiv : (a : ι) → ι₃) x : ι₃)
      (((h.comp (g.comp f)).indexEquiv : (a : ι) → ι₃) x : ι₃)
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : 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
⊢ Eq.{u_12 + 1} (α := M₃) ((((h.comp g).comp f).weightMap : (a : M) → M₃) x : M₃)
    (((h.comp (g.comp f)).weightMap : (a : M) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : 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₃
⊢ Eq.{u_4 + 1} (α := N) ((((h.comp g).comp f).coweightMap : (a : N₃) → N) x : N)
    (((h.comp (g.comp f)).coweightMap : (a : N₃) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : 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 : ι
⊢ Eq.{u_11 + 1} (α := ι₃) ((((h.comp g).comp f).indexEquiv : (a : ι) → ι₃) x : ι₃)
    (((h.comp (g.comp f)).indexEquiv : (a : ι) → ι₃) x : ι₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1)
    LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Eq.{u_4 + 1} (α := N →ₗ[R] N)
    (coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P) 1)
    LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ indexEquiv.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (R := R) (M := M) (N := N) (M₂ := M) (N₂ := N) (P := P) (Q := P) 1 =
    Equiv.refl ι

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
x y : P.Hom P
⊢ (x * y).weightMap = x.weightMap ∘ₗ y.weightMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
x y : P.Hom P
⊢ (x * y).coweightMap = y.coweightMap ∘ₗ x.coweightMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
x y : P.Hom P
⊢ Eq (α := (a : ι) → ι) (⇑(x * y).indexEquiv : (a : ι) → ι)
    (Function.comp (β := ι) (⇑x.indexEquiv : (a : ι) → ι) (⇑y.indexEquiv : (a : ι) → ι))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
h :
  ∀ (x : M),
    Eq (α := M)
      ((weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1 :
            (a : M) → M)
          x :
        M)
      ((1 : (a : M) → M) x : M)
⊢ Eq.{u_3 + 1} (α := Module.End R M)
    (weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1) 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
x : M
⊢ Eq (α := M)
    ((weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1 :
          (a : M) → M)
        x :
      M)
    ((1 : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g h : P.End
h₁ : ∀ (x : M), Eq (α := M) (((g * h).weightMap : (a : M) → M) x : M) ((g.weightMap * h.weightMap : (a : M) → M) x : M)
⊢ (g * h).weightMap = g.weightMap * h.weightMap

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g h : P.End
x : M
⊢ Eq (α := M) (((g * h).weightMap : (a : M) → M) x : M) ((g.weightMap * h.weightMap : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
weightMap : ∀ (x : M), Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
coweightMap : ∀ (x : N), Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)
indexEquiv : ∀ (x : ι), Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : M
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)

Tactic:
LinearMap.congr_fun hfg x

Premises used: LinearMap.congr_fun