-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : 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)) =
    ((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
have 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))))
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]