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
P : RootPairing ι R M N
x y : P.End
H :
  ∀ (x_1 : ι),
    Eq (α := ι) (((x * y).indexEquiv : (a : ι) → ι) x_1 : ι) ((x.indexEquiv * y.indexEquiv : (a : ι) → ι) x_1 : ι)
⊢ (x * y).indexEquiv = x.indexEquiv * y.indexEquiv

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.End
x_1 : ι
⊢ Eq (α := ι) (((x * y).indexEquiv : (a : ι) → ι) x_1 : ι) ((x.indexEquiv * y.indexEquiv : (a : ι) → ι) x_1 : ι)

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₂
e : P.Equiv Q
m : M
⊢ Eq.{u_6 + 1} (α := M₂) ((weightEquiv P Q e : (a : M) → M₂) m : M₂) (((↑e : P.Hom Q).weightMap : (a : M) → M₂) m : M₂)

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
ι₂ : 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₂
e : P.Equiv Q
m : M
⊢ ((weightEquiv P Q e).symm : (a : M₂) → M) (((↑e : P.Hom Q).weightMap : (a : M) → M₂) m : M₂) = m

Tactic:
(LinearEquiv.symm_apply_eq (weightEquiv P Q e)).mpr rfl

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, RootPairing.Equiv.weightEquiv, 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
rw : (weightEquiv P Q e : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m
⊢ ((↑e : P.Hom Q).weightMap : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m

Tactic:
rw [← weightEquiv_apply]

Premises used: RootPairing.Equiv.weightEquiv_apply
-- 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₂
e : P.Equiv Q
m : M₂
⊢ (weightEquiv P Q e : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m

Tactic:
LinearEquiv.apply_symm_apply (weightEquiv P Q e) m

Premises used: RootPairing.Equiv.weightEquiv, LinearEquiv.apply_symm_apply
-- 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₂
e : P.Equiv Q
m : M₂
⊢ (weightEquiv P Q e : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m

Tactic:
exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m

Premises used: RootPairing.Equiv.weightEquiv, LinearEquiv.apply_symm_apply
-- 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₂
e : P.Equiv Q
n : N₂
⊢ Eq.{u_4 + 1} (α := N) ((coweightEquiv P Q e : (a : N₂) → N) n : N) (((↑e : P.Hom Q).coweightMap : (a : N₂) → N) n : N)

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
ι₂ : 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₂
e : P.Equiv Q
n : N₂
⊢ ((coweightEquiv P Q e).symm : (a : N) → N₂) (((↑e : P.Hom Q).coweightMap : (a : N₂) → N) n : N) = n

Tactic:
(LinearEquiv.symm_apply_eq (coweightEquiv P Q e)).mpr rfl

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, RootPairing.Equiv.coweightEquiv, 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
rw : (coweightEquiv P Q e : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n
⊢ ((↑e : P.Hom Q).coweightMap : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n

Tactic:
rw [← coweightEquiv_apply]

Premises used: RootPairing.Equiv.coweightEquiv_apply
-- 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₂
e : P.Equiv Q
n : N
⊢ (coweightEquiv P Q e : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n

Tactic:
LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n

Premises used: RootPairing.Equiv.coweightEquiv, LinearEquiv.apply_symm_apply
-- 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₂
e : P.Equiv Q
n : N
⊢ (coweightEquiv P Q e : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n

Tactic:
exact LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n

Premises used: RootPairing.Equiv.coweightEquiv, LinearEquiv.apply_symm_apply
-- 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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
simp :
  Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂)
    (Function.comp.{u_3 + 1, u_9 + 1, u_12 + 1} (β := M₁) (⇑(↑g : P₁.Hom P₂).weightMap : (a : M₁) → M₂)
      (⇑(↑f : P.Hom P₁).weightMap : (a : M) → M₁))
⊢ Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂) (⇑((↑g : P₁.Hom P₂).comp (↑f : P.Hom P₁)).weightMap : (a : M) → M₂)

Tactic:
simp only [Hom.comp, LinearMap.coe_comp]

Premises used: RootPairing.Hom.comp, 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
ι₂_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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂)
    (Function.comp.{u_3 + 1, u_9 + 1, u_12 + 1} (β := M₁) (⇑(↑g : P₁.Hom P₂).weightMap : (a : M₁) → M₂)
      (⇑(↑f : P.Hom P₁).weightMap : (a : M) → M₁))

Tactic:
Bijective.comp g.bijective_weightMap f.bijective_weightMap

Premises used: RootPairing.Equiv.bijective_weightMap, Function.Bijective.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
ι₂_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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂)
    (Function.comp.{u_3 + 1, u_9 + 1, u_12 + 1} (β := M₁) (⇑(↑g : P₁.Hom P₂).weightMap : (a : M₁) → M₂)
      (⇑(↑f : P.Hom P₁).weightMap : (a : M) → M₁))

Tactic:
exact Bijective.comp g.bijective_weightMap f.bijective_weightMap

Premises used: RootPairing.Equiv.bijective_weightMap, Function.Bijective.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
ι₂_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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
simp :
  Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N)
    (Function.comp.{u_13 + 1, u_10 + 1, u_4 + 1} (β := N₁) (⇑(↑f : P.Hom P₁).coweightMap : (a : N₁) → N)
      (⇑(↑g : P₁.Hom P₂).coweightMap : (a : N₂) → N₁))
⊢ Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N) (⇑((↑g : P₁.Hom P₂).comp (↑f : P.Hom P₁)).coweightMap : (a : N₂) → N)

Tactic:
simp only [Hom.comp, LinearMap.coe_comp]

Premises used: RootPairing.Hom.comp, 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
ι₂_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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N)
    (Function.comp.{u_13 + 1, u_10 + 1, u_4 + 1} (β := N₁) (⇑(↑f : P.Hom P₁).coweightMap : (a : N₁) → N)
      (⇑(↑g : P₁.Hom P₂).coweightMap : (a : N₂) → N₁))

Tactic:
Bijective.comp f.bijective_coweightMap g.bijective_coweightMap

Premises used: RootPairing.Equiv.bijective_coweightMap, Function.Bijective.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
ι₂_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 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N)
    (Function.comp.{u_13 + 1, u_10 + 1, u_4 + 1} (β := N₁) (⇑(↑f : P.Hom P₁).coweightMap : (a : N₁) → N)
      (⇑(↑g : P₁.Hom P₂).coweightMap : (a : N₂) → N₁))

Tactic:
exact Bijective.comp f.bijective_coweightMap g.bijective_coweightMap

Premises used: RootPairing.Equiv.bijective_coweightMap, Function.Bijective.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_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₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ (↑(g.comp f) : P.Hom P₂) = (↑g : P₁.Hom P₂).comp (↑f : P.Hom P₁)

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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑(f.comp (id P)) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((↑(f.comp (id P)) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
      (((↑f : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
indexEquiv :
  ∀ (x : ι),
    Eq.{u_8 + 1} (α := ι₂) (((↑(f.comp (id P)) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
      (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : M
⊢ Eq.{u_9 + 1} (α := M₂) (((↑(f.comp (id P)) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
    (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : N₂
⊢ Eq.{u_4 + 1} (α := N) (((↑(f.comp (id P)) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
    (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : ι
⊢ Eq.{u_8 + 1} (α := ι₂) (((↑(f.comp (id P)) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
    (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑((id Q).comp f) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((↑((id Q).comp f) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
      (((↑f : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
indexEquiv :
  ∀ (x : ι),
    Eq.{u_8 + 1} (α := ι₂) (((↑((id Q).comp f) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
      (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : M
⊢ Eq.{u_9 + 1} (α := M₂) (((↑((id Q).comp f) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
    (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : N₂
⊢ Eq.{u_4 + 1} (α := N) (((↑((id Q).comp f) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
    (((↑f : P.Hom Q).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_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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
x : ι
⊢ Eq.{u_8 + 1} (α := ι₂) (((↑((id Q).comp f) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
    (((↑f : P.Hom Q).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_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₁
weightMap :
  ∀ (x : M),
    Eq.{u_15 + 1} (α := M₃) (((↑((h.comp g).comp f) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
      (((↑(h.comp (g.comp f)) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
coweightMap :
  ∀ (x : N₃),
    Eq.{u_4 + 1} (α := N) (((↑((h.comp g).comp f) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
      (((↑(h.comp (g.comp f)) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
indexEquiv :
  ∀ (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 : ι₃)
⊢ (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_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 : M
⊢ Eq.{u_15 + 1} (α := M₃) (((↑((h.comp g).comp f) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).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_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 : N₃
⊢ Eq.{u_4 + 1} (α := N) (((↑((h.comp g).comp f) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)

Tactic:
simp