-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y_1 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
simp :
  HMul.hMul (α := (↑(F.obj (op (unop Y))) : Type v)) (β := (↑(F.obj (op (unop Y))) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (F.map (Quiver.Hom.op (lift f₁ f₂))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type v)) → (↑(F.obj (op (unop Y))) : Type v))
          ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
              (fst X X) :
            ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X)))) :
        (↑(F.obj (op (unop Y))) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (F.map (Quiver.Hom.op (lift f₁ f₂))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type v)) → (↑(F.obj (op (unop Y))) : Type v))
          ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
              (snd X X) :
            ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X)))) :
        (↑(F.obj (op (unop Y))) : Type v)) =
    HMul.hMul (α :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      (β :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₁ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₂ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))
⊢ (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
        (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X) (lift f₁ f₂)
        ((Equiv.symm
              (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))) :
            (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
          (HMul.hMul (α :=
            ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
            (β :=
            ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
            ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
                  (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
                (fst X X) :
              ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
            ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
                  (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
                (snd X X) :
              ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))))) =
    HMul.hMul (α :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      (β :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₁ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₂ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))

Tactic:
simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]

Premises used: Equiv.apply_symm_apply, map_mul, CategoryTheory.Functor.RepresentableBy.homEquiv'_comp