-- 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)
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)
⊢ 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_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)
  (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]