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_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
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₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
x : ι
⊢ Eq.{u_14 + 1} (α := ι₃) (((↑((h.comp g).comp f) : P.Hom P₃).indexEquiv : (a : ι) → ι₃) x : ι₃)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).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
⊢ (↑(weightEquiv P P 1) : M →ₗ[R] M) = 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
⊢ (↑(coweightEquiv P P 1) : N →ₗ[R] N) = 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 (α := P.Hom P) (↑1 : P.Hom P) 1

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.Equiv P
⊢ x * y = x.comp y

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.Equiv P
h :
  ∀ (x_1 : M),
    Eq (α := M) ((weightEquiv P P (x.comp y) : (a : M) → M) x_1 : M)
      ((weightEquiv P P y ≪≫ₗ weightEquiv P P x : (a : M) → M) x_1 : M)
⊢ weightEquiv P P (x.comp y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x

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 y : P.Equiv P
x_1 : M
⊢ Eq (α := M) ((weightEquiv P P (x.comp y) : (a : M) → M) x_1 : M)
    ((weightEquiv P P y ≪≫ₗ weightEquiv P P x : (a : M) → M) x_1 : 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
x y : P.Equiv P
⊢ weightEquiv P P x * weightEquiv P P y = weightEquiv P P y ≪≫ₗ weightEquiv P P x

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
P : RootPairing ι R M N
x y : P.Equiv P
h :
  ∀ (x_1 : N),
    Eq (α := N) ((coweightEquiv P P (x.comp y) : (a : N) → N) x_1 : N)
      ((coweightEquiv P P x ≪≫ₗ coweightEquiv P P y : (a : N) → N) x_1 : N)
⊢ coweightEquiv P P (x.comp y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y

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 y : P.Equiv P
x_1 : N
⊢ Eq (α := N) ((coweightEquiv P P (x.comp y) : (a : N) → N) x_1 : N)
    ((coweightEquiv P P x ≪≫ₗ coweightEquiv P P y : (a : N) → N) x_1 : 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
P : RootPairing ι R M N
x y : P.Equiv P
⊢ coweightEquiv P P x * coweightEquiv P P y = coweightEquiv P P y ≪≫ₗ coweightEquiv P P x

Tactic:
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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
h :
  ∀ (n : N) (m : M₂),
    Eq.{u_2 + 1} (α := R)
      (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                  (a : N) → Module.Dual R M₂)
                n :
              Module.Dual R M₂) :
            (a : M₂) → R)
          m :
        R)
      (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                  (a : N) → Module.Dual R M₂)
                n :
              Module.Dual R M₂) :
            (a : M₂) → R)
          m :
        R)
⊢ (↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂)

Tactic:
ext n m
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ m = (weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M)

Tactic:
(LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp rfl

Premises used: LinearEquiv.symm_apply_eq, RootPairing.Equiv.weightEquiv, Iff.mp, 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ m = (weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M)

Tactic:
exact (LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp rfl

Premises used: LinearEquiv.symm_apply_eq, RootPairing.Equiv.weightEquiv, Iff.mp, 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
h :
  Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)

Tactic:
nth_rw 2 [show m = (weightEquiv P Q f) ((weightEquiv P Q f).symm m) by
      exact (LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ n = (coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)

Tactic:
(LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp rfl

Premises used: LinearEquiv.symm_apply_eq, RootPairing.Equiv.coweightEquiv, Iff.mp, 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ n = (coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)

Tactic:
exact (LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp rfl

Premises used: LinearEquiv.symm_apply_eq, RootPairing.Equiv.coweightEquiv, Iff.mp, 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
h :
  Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)

Tactic:
nth_rw 1 [show n = (coweightEquiv P Q f) ((coweightEquiv P Q f).symm n) by
      exact (LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ (↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap

Tactic:
have := f.weight_coweight_transpose
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this :
  (↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap
⊢ ∀ (m : N₂) (n : M),
    Eq.{u_2 + 1} (α := R)
      (((((↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → M →ₗ[R] R)
                m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)
      (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap : (a : N₂) → M →ₗ[R] R) m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)

Tactic:
rw [LinearMap.ext_iff₂] at this

Premises used: LinearMap.ext_iff₂
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this :
  ∀ (m : N₂) (n : M),
    Eq.{u_2 + 1} (α := R)
      (((((↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → M →ₗ[R] R)
                m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)
      (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap : (a : N₂) → M →ₗ[R] R) m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)

Tactic:
Eq.symm (this ((coweightEquiv P Q f).symm n) ((weightEquiv P Q f).symm m))

Premises used: LinearEquiv.symm, RootPairing.Equiv.coweightEquiv, RootPairing.Equiv.weightEquiv, Eq.symm, DFunLike.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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this :
  ∀ (m : N₂) (n : M),
    Eq.{u_2 + 1} (α := R)
      (((((↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → M →ₗ[R] R)
                m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)
      (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap : (a : N₂) → M →ₗ[R] R) m :
              M →ₗ[R] R) :
            (a : M) → R)
          n :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)

Tactic:
exact Eq.symm (this ((coweightEquiv P Q f).symm n) ((weightEquiv P Q f).symm m))

Premises used: LinearEquiv.symm, RootPairing.Equiv.coweightEquiv, RootPairing.Equiv.weightEquiv, Eq.symm, DFunLike.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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
h :
  ∀ (i : ι₂),
    Eq.{u_3 + 1} (α := M)
      (Function.comp.{u_8 + 1, u_9 + 1, u_3 + 1} (β := M₂) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
        (⇑Q.root : (a : ι₂) → M₂) i)
      (Function.comp.{u_8 + 1, u_1 + 1, u_3 + 1} (β := ι) (⇑P.root : (a : ι) → M)
        (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i)
⊢ Eq (α := ι₂ → M)
    (Function.comp.{u_8 + 1, u_9 + 1, u_3 + 1} (β := M₂) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
      (⇑Q.root : (a : ι₂) → M₂))
    (Function.comp.{u_8 + 1, u_1 + 1, u_3 + 1} (β := ι) (⇑P.root : (a : ι) → M)
      (⇑(↑f : P.Hom Q).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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
i : ι₂
h :
  Eq.{u_3 + 1} (α := M) (((weightEquiv P Q f).symm : (a : M₂) → M) ((Q.root : (a : ι₂) → M₂) i : M₂) : M)
    ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M)
⊢ Eq.{u_3 + 1} (α := M)
    (Function.comp.{u_8 + 1, u_9 + 1, u_3 + 1} (β := M₂) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
      (⇑Q.root : (a : ι₂) → M₂) i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_3 + 1} (β := ι) (⇑P.root : (a : ι) → M)
      (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i)

Tactic:
simp only [LinearEquiv.coe_coe, comp_apply]

Premises used: 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
i : ι₂
⊢ Eq (α := ι → M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(↑f : P.Hom Q).weightMap : (a : M) → M₂)
      (⇑P.root : (a : ι) → M))
    (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂)
      (⇑(↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂))

Tactic:
have := f.root_weightMap