-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
⊢ 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)))))
have 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))))
Tactic: simp only [Iso.refl_symm, Iso.trans_hom,
          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.id_tensorHom_id]