-- 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 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
F : Functor.{v, w, u_1, w + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
a :
  Eq.{w + 1} (α :=
    ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
      (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))
    (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
            Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)) ⟶ X)
              (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))) :
          (a : X ⊗ 𝟙_ C ⟶ X) → ToType (F.obj (op (X ⊗ 𝟙_ C))))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X)
          (X ◁
            ((Equiv.symm
                    (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                      (↑x1 : Type w) →* (↑x2 : Type w))) :
                  Equiv.{w + 1, v + 1}
                    (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                      (F.obj (op (tensorUnit.{v, u_1} C (𝒞 := inst)))))
                    (tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ X)) :
                (a : ToType (F.obj (op (𝟙_ C)))) → 𝟙_ C ⟶ X)
              1)
          (((Equiv.symm
                  (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                    (↑x1 : Type w) →* (↑x2 : Type w))) :
                Equiv.{w + 1, v + 1}
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                  (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
              (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
            (HMul.hMul (α :=
              ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
              (β :=
              ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
              (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                        (↑x1 : Type w) →* (↑x2 : Type w)) :
                      Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)
                        (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                          MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))) :
                    (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
                  (fst X X) :
                ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
              (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                        (↑x1 : Type w) →* (↑x2 : Type w)) :
                      Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)
                        (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                          MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))) :
                    (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
                  (snd X X) :
                ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))))) :
      ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
        (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))
    (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
            Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)) ⟶ X)
              (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))) :
          (a : X ⊗ 𝟙_ C ⟶ X) → ToType (F.obj (op (X ⊗ 𝟙_ C))))
        (Iso.hom (ρ_ X)) :
      ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
        (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)) ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X)
      (X ◁
        ((Equiv.symm
                (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                  (↑x1 : Type w) →* (↑x2 : Type w))) :
              Equiv.{w + 1, v + 1}
                (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorUnit.{v, u_1} C (𝒞 := inst)))))
                (tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ X)) :
            (a : ToType (F.obj (op (𝟙_ C)))) → 𝟙_ C ⟶ X)
          1)
      (((Equiv.symm
              (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w))) :
            Equiv.{w + 1, v + 1}
              (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
              (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
          (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
        (HMul.hMul (α :=
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
          (β :=
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
          (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                  Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)
                    (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                      (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))) :
                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
              (fst X X) :
            ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
          (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                  Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)
                    (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                      (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))) :
                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
              (snd X X) :
            ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X)))))))
    (Iso.hom (ρ_ X))

Tactic:
apply α.homEquiv'.injective

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv', Equiv.injective