-- 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
⊢ 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
have 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)))))
Tactic: dsimp only [forget₂_obj, forget₂_map_associator_hom]