awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₁
φ : 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)
have h : Eq.{u_2 + 1} (α := R)
  (((((f.weightMap.dualMap ∘ₗ g.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)
Tactic: rw [← LinearMap.dualMap_comp_dualMap, ← LinearMap.comp_assoc _ f.coweightMap,
      ← f.weight_coweight_transpose, LinearMap.comp_assoc g.coweightMap,
      ← g.weight_coweight_transpose, ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₁
φ : N₂
x : M
h :
  Eq.{u_2 + 1} (α := R)
    (((((f.weightMap.dualMap ∘ₗ g.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)
⊢ 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)
have h₁ : Eq.{u_2 + 1} (α := R)
  (((((f.weightMap.dualMap ∘ₗ g.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)
Tactic: rw [← LinearMap.dualMap_comp_dualMap, ← LinearMap.comp_assoc _ f.coweightMap,
      ← f.weight_coweight_transpose, LinearMap.comp_assoc g.coweightMap,
      ← g.weight_coweight_transpose, ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₁
φ : N₂
x : M
h :
  Eq.{u_2 + 1} (α := R)
    (((((f.weightMap.dualMap ∘ₗ g.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)
h₁ :
  Eq.{u_2 + 1} (α := R)
    (((((f.weightMap.dualMap ∘ₗ g.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)
⊢ 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)
have h₂ : Eq.{u_2 + 1} (α := R)
  (((((f.weightMap.dualMap ∘ₗ g.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)
  (((((f.weightMap.dualMap ∘ₗ (↑P₁.flip.toPerfPair : N₁ →ₗ[R] Module.Dual R M₁)) ∘ₗ g.coweightMap :
              (a : N₂) → Module.Dual R M)
            φ :
          Module.Dual R M) :
        (a : M) → R)
      x :
    R)
Tactic: rw [← LinearMap.dualMap_comp_dualMap, ← LinearMap.comp_assoc _ f.coweightMap,
      ← f.weight_coweight_transpose, LinearMap.comp_assoc g.coweightMap,
      ← g.weight_coweight_transpose, ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₁
⊢ 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 : ι) → ι₂))
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_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)
have 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)
Tactic: simp only [LinearMap.coe_comp, Equiv.coe_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_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)
have h : Eq.{u_9 + 1} (α := M₂)
  (Function.comp.{u_1 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := 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)
Tactic: rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := 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)
      (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)
have h₁ : Eq.{u_9 + 1} (α := M₂)
  (Function.comp.{u_1 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
    (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₁) (⇑P₁.root : (a : ι₁) → M₁) (⇑f.indexEquiv : (a : ι) → ι₁)) 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)
Tactic: rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := 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)
h₁ :
  Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
      (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₁) (⇑P₁.root : (a : ι₁) → M₁) (⇑f.indexEquiv : (a : ι) → ι₁)) 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)
      (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)
have h₂ : Eq.{u_9 + 1} (α := M₂)
  (Function.comp.{u_1 + 1, u_5 + 1, u_9 + 1} (β := ι₁)
    (Function.comp.{u_5 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂) (⇑P₁.root : (a : ι₁) → M₁))
    (⇑f.indexEquiv : (a : ι) → ι₁) 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)
Tactic: rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := 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)
h₁ :
  Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂)
      (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₁) (⇑P₁.root : (a : ι₁) → M₁) (⇑f.indexEquiv : (a : ι) → ι₁)) 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)
h₂ :
  Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_5 + 1, u_9 + 1} (β := ι₁)
      (Function.comp.{u_5 + 1, u_6 + 1, u_9 + 1} (β := M₁) (⇑g.weightMap : (a : M₁) → M₂) (⇑P₁.root : (a : ι₁) → M₁))
      (⇑f.indexEquiv : (a : ι) → ι₁) 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)
      (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)
have h₃ : Eq.{u_9 + 1} (α := M₂)
  (Function.comp.{u_1 + 1, u_5 + 1, u_9 + 1} (β := ι₁)
    (Function.comp.{u_5 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑P₂.root : (a : ι₂) → M₂) (⇑g.indexEquiv : (a : ι₁) → ι₂))
    (⇑f.indexEquiv : (a : ι) → ι₁) 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)
Tactic: rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₁
⊢ 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 : ι₂) → ι))
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_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)
have 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)
Tactic: simp only [LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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_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)
have 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)
Tactic: rw [comp_assoc, g.coroot_coweightMap, ← comp_assoc, f.coroot_coweightMap, comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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
⊢ f.comp (id P) = f
have 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₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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₂)
⊢ f.comp (id P) = f
have 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)
Tactic: ext x