-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
simp :
  Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y)
                Z).toModuleCat :
          Type u))
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)).toModuleCat :
          Type u)))
    (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))
    ((𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u))
            (ModuleCat.of R (↑Z.toModuleCat : Type u))) ≫
        (𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u))) ⊗ₘ
          𝟙 (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≫
      Iso.hom
          (α_ (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u))
            (ModuleCat.of R (↑Z.toModuleCat : Type u))) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u))
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (ModuleCat.of R (↑Y.toModuleCat : Type u)) (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z).toModuleCat : Type u))))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y)
                Z).toModuleCat :
          Type u))
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)).toModuleCat :
          Type u)))
    (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))
    (Iso.hom
      ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u))
                (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≪≫
          (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                  (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u)))) ⊗ᵢ
            Iso.refl (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≪≫
        α_ (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u))
            (ModuleCat.of R (↑Z.toModuleCat : Type u)) ≪≫
          (Iso.refl (ModuleCat.of R (↑X.toModuleCat : Type u)) ⊗ᵢ
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                  (ModuleCat.of R (↑Y.toModuleCat : Type u)) (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (ModuleCat.of R (↑X.toModuleCat : Type u))
                (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z).toModuleCat : Type u)))))

Tactic:
simp only [Iso.refl_symm, Iso.trans_hom,
          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.id_tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.id_tensorHom_id, CategoryTheory.Iso.refl_symm, CategoryTheory.Iso.refl_hom