-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
rw :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
rw₁ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
rw₂ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)
rw₃ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
          Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)
rw₄ rw₅ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) Z.toModuleCat ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
    (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)) (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))
⊢ Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
            Z.toModuleCat) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
          𝟙 Z.toModuleCat)) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))

Tactic:
rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_tensorHom_id, CategoryTheory.Category.id_comp