-- 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)
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)
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)
⊢ 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 ∘ₗ 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)
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]