-- Module: Mathlib.RepresentationTheory.Rep.Basic
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₃
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))
⊢ 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)))))

Tactic:
ext