-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : ModuleCat R
⊢ 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
have 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
Tactic: ext1