-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Rep k G
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : X₃ ⟶ Y₃
⊢ ofHom ((Hom.hom (ofHom ((Hom.hom x).tensor (Hom.hom x_1)))).tensor (Hom.hom x_2)) ≫
      (mkIso (assoc Y₁.ρ Y₂.ρ Y₃.ρ)).hom =
    (mkIso (assoc X₁.ρ X₂.ρ X₃.ρ)).hom ≫
      ofHom ((Hom.hom x).tensor (Hom.hom (ofHom ((Hom.hom x_1).tensor (Hom.hom x_2)))))
have hf : ∀ (x_3 : (↑X₁ : Type u)) (x_4 : (↑X₂ : Type u)) (x_5 : (↑X₃ : Type u)),
  Eq (α := (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (Hom.hom
                                (ofHom ((Hom.hom (ofHom ((Hom.hom x).tensor (Hom.hom x_1)))).tensor (Hom.hom x_2)) ≫
                                  (mkIso (assoc Y₁.ρ Y₂.ρ Y₃.ρ)).hom)).toLinearMap) :
                        (↑X₁ : Type u) →ₗ[k]
                          (↑X₂ : Type u) →ₗ[k]
                            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                      (a : (↑X₁ : Type u)) →
                        (↑X₂ : Type u) →ₗ[k]
                          (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
                    x_3 :
                  (↑X₂ : Type u) →ₗ[k] (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                (a : (↑X₂ : Type u)) → (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
              x_4 :
            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
          (a : (↑X₃ : Type u)) → (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
        x_5 :
      (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (Hom.hom
                                ((mkIso (assoc X₁.ρ X₂.ρ X₃.ρ)).hom ≫
                                  ofHom
                                    ((Hom.hom x).tensor
                                      (Hom.hom (ofHom ((Hom.hom x_1).tensor (Hom.hom x_2))))))).toLinearMap) :
                        (↑X₁ : Type u) →ₗ[k]
                          (↑X₂ : Type u) →ₗ[k]
                            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                      (a : (↑X₁ : Type u)) →
                        (↑X₂ : Type u) →ₗ[k]
                          (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
                    x_3 :
                  (↑X₂ : Type u) →ₗ[k] (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                (a : (↑X₂ : Type u)) → (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
              x_4 :
            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
          (a : (↑X₃ : Type u)) → (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
        x_5 :
      (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
Tactic: ext