-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
dsimp :
  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)))))
⊢ CategoryTheory.Functor.map
      (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
        fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (Iso.hom (α_ X Y Z)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (Functor.obj
                  (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                    fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y))
                (Functor.obj
                  (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                    fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  Z))) ≪≫
          (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                  (Functor.obj
                    (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                      fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    X)
                  (Functor.obj
                    (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                      fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    Y))) ⊗ᵢ
            Iso.refl
              (Functor.obj
                (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                  fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                Z))) ≪≫
        α_
            (Functor.obj
              (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              X)
            (Functor.obj
              (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              Y)
            (Functor.obj
              (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              Z) ≪≫
          (Iso.refl
                (Functor.obj
                  (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                    fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  X) ⊗ᵢ
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                  (Functor.obj
                    (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                      fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    Y)
                  (Functor.obj
                    (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                      fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    Z))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (Functor.obj
                  (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                    fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  X)
                (Functor.obj
                  (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
                    fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)))).hom

Tactic:
dsimp only [forget₂_obj, forget₂_map_associator_hom]

Premises used: QuadraticModuleCat.forget₂_map_associator_hom, QuadraticModuleCat.forget₂_obj