-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : ModuleCat R
hf :
  SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.associator x x_1 x_2))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
          MonoidalCategoryStruct.associator (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x_1 x_2)))).hom
⊢ CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.associator x x_1 x_2)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
          MonoidalCategory.tensorIso
            (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1))))
            (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
        MonoidalCategoryStruct.associator (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
            (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
            (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x_1 x_2)))).hom

Tactic:
ext1