-- 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
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)
⊢ 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))
have 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))
Tactic: rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]