-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
simp :
  Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).toModuleCat :
          Type u))
      (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (ModuleCat.ofHom (Isometry.toLinearMap (Hom.toIsometry (Iso.hom (ρ_ X)))))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑(toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) : Type u))) ≫
      ModuleCat.of R (↑X.toModuleCat : Type u) ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫
        Iso.hom (ρ_ (ModuleCat.of R (↑X.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)) =
    ((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))
                  ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))))) ≪≫
          (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.symm (Iso.refl ((𝟙_ (ModuleCat R)) (𝒞 := 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)).hom

Tactic:
simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
          Iso.refl_hom, MonoidalCategory.tensorIso_hom, MonoidalCategory.id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, QuadraticModuleCat.forget₂_map, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.trans_assoc, QuadraticModuleCat.forget₂_obj, CategoryTheory.Iso.trans_hom, CategoryTheory.Iso.refl_symm, CategoryTheory.Iso.refl_hom