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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
m : N
⊢ Eq (α := N) ((coweightEquiv P P (symm P P e * e) : (a : N) → N) m : N)
    ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P)
            (↑1 : P.Hom P) :
          (a : N) → N)
        m :
      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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
m : ι
⊢ Eq (α := ι) (((↑(symm P P e * e) : P.Hom P).indexEquiv : (a : ι) → ι) m : ι)
    ((Hom.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 : P.Hom P) :
          (a : ι) → ι)
        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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
h :
  ∀ (x : N₂) (x_1 : M),
    Eq.{u_2 + 1} (α := R)
      (((((↑f : M →ₗ[R] M₂).dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → Module.Dual R M)
                x :
              Module.Dual R M) :
            (a : M) → R)
          x_1 :
        R)
      (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ
                    (↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) :
                  (a : N₂) → Module.Dual R M)
                x :
              Module.Dual R M) :
            (a : M) → R)
          x_1 :
        R)
⊢ (↑f : M →ₗ[R] M₂).dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ
      (↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N)

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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
x : N₂
x_1 : M
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑f : M →ₗ[R] M₂).dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → Module.Dual R M) x :
            Module.Dual R M) :
          (a : M) → R)
        x_1 :
      R)
    (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ
                  (↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) :
                (a : N₂) → Module.Dual R M)
              x :
            Module.Dual R M) :
          (a : M) → R)
        x_1 :
      R)

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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
h :
  ∀ (x : ι),
    Eq.{u_6 + 1} (α := M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂) (⇑P.root : (a : ι) → M) x)
      (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂) (⇑e : (a : ι) → ι₂) x)
⊢ Eq (α := ι → M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂) (⇑P.root : (a : ι) → M))
    (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂) (⇑e : (a : ι) → ι₂))

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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
x : ι
⊢ Eq.{u_6 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂) (⇑P.root : (a : ι) → M) x)
    (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂) (⇑e : (a : ι) → ι₂) x)

Tactic:
simp [hf]
-- 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
h :
  ∀ (i : ι₂),
    Eq.{u_4 + 1} (α := N)
      (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
        (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
        (⇑Q.coroot : (a : ι₂) → N₂) i)
      (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i)
⊢ Eq (α := ι₂ → N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
h :
  Eq.{u_7 + 1} (α := N₂) ((Q.coroot : (a : ι₂) → N₂) i : N₂)
    ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
        (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
      N₂)
⊢ Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i)

Tactic:
rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply, Function.comp_apply, LinearEquiv.coe_coe
-- 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
rw : (((RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂) i : N₂)
| ((Q.coroot : (a : ι₂) → N₂) i : N₂)

Tactic:
rw [this]
-- 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
h :
  Eq.{u_7 + 1} (α := N₂) (((RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂) i : N₂)
    ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
        (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
      N₂)
⊢ Eq.{u_7 + 1} (α := N₂) ((Q.coroot : (a : ι₂) → N₂) i : N₂)
    ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
        (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
      N₂)

Tactic:
conv_lhs => rw [this]
-- 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
⊢ Eq.{u_7 + 1} (α := N₂) (((RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂) i : N₂)
    ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
        (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
      N₂)

Tactic:
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
ι₂ : 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
suffices : Q = RootPairing.map (P := P) e f g
⊢ Eq (α := ι₂ → N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι))

Tactic:
suffices Q = P.map e f g by
      ext i
      rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]
      conv_lhs => rw [this]
      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
ι₂ : 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
he : Q.toLinearMap = (RootPairing.map (P := P) e f g).toLinearMap
hr : Q.root = (RootPairing.map (P := P) e f g).root
⊢ Q = RootPairing.map (P := P) e f g

Tactic:
apply IsRootSystem.ext

Premises used: RootPairing.IsRootSystem.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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
he :
  ∀ (x : M₂) (x_1 : N₂),
    Eq.{u_2 + 1} (α := R) ((((Q.toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)
      (((((RootPairing.map (P := P) e f g).toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)
⊢ Q.toLinearMap = (RootPairing.map (P := P) e f g).toLinearMap

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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
hr :
  ∀ (x : ι₂),
    Eq.{u_6 + 1} (α := M₂) ((Q.root : (a : ι₂) → M₂) x : M₂)
      (((RootPairing.map (P := P) e f g).root : (a : ι₂) → M₂) x : M₂)
⊢ Q.root = (RootPairing.map (P := P) e f g).root

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
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x : M₂
x_1 : N₂
⊢ Eq.{u_2 + 1} (α := R) ((((Q.toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)
    (((((RootPairing.map (P := P) e f g).toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)

Tactic:
simp [RootPairing.map, RootPairing.map, g]

Premises used: RootPairing.map
-- 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_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x : ι₂
⊢ Eq.{u_6 + 1} (α := M₂) ((Q.root : (a : ι₂) → M₂) x : M₂)
    (((RootPairing.map (P := P) e f g).root : (a : ι₂) → M₂) x : M₂)

Tactic:
simp [hf, RootPairing.map, RootPairing.map]

Premises used: RootPairing.map
-- 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
weightMap :
  ∀ (x : M),
    Eq (α := M) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).weightMap : (a : M) → M) x : M)
      ((Hom.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)
coweightMap :
  ∀ (x : N),
    Eq (α := N) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).coweightMap : (a : N) → N) x : N)
      ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P) 1 :
            (a : N) → N)
          x :
        N)
indexEquiv :
  ∀ (x : ι),
    Eq (α := ι) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).indexEquiv : (a : ι) → ι) x : ι)
      ((Hom.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 :
            (a : ι) → ι)
          x :
        ι)
⊢ (↑f : P.Hom P) * (↑(symm P P f) : P.Hom P) = 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
ι₂ : 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
x : M
⊢ Eq (α := M) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).weightMap : (a : M) → M) x : M)
    ((Hom.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)

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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
x : N
⊢ Eq (α := N) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).coweightMap : (a : N) → N) x : N)
    ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P) 1 :
          (a : N) → N)
        x :
      N)

Tactic:
simp