-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ obj coyoneda (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
a :
  Eq.{v₁ + 1} (α :=
    (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j') →
            (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j'))
        ((R ⋙ F.partialLeftAdjoint).map φ ≫
          ((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1}
                  ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶
                    F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
                  (F.partialLeftAdjointObj (R.obj j') ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')) :
              (a : (R.obj j').obj ⟶ F.obj (((const J).obj Y).obj j')) →
                F.partialLeftAdjointObj (R.obj j') ⟶ ((const J).obj Y).obj j')
            (c.ι.app j' ≫ g)) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j') →
            (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j'))
        (((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1}
                  ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j))
                  (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j)) :
              (a : (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j)) →
                F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j)
            (c.ι.app j ≫ g) ≫
          map (obj (const J) Y) φ) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
⊢ Eq (α := (R ⋙ F.partialLeftAdjoint).obj j ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')
    ((R ⋙ F.partialLeftAdjoint).map φ ≫
      ((Equiv.symm F.partialLeftAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1}
              ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
              (F.partialLeftAdjointObj (R.obj j') ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')) :
          (a : (R.obj j').obj ⟶ F.obj (((const J).obj Y).obj j')) →
            F.partialLeftAdjointObj (R.obj j') ⟶ ((const J).obj Y).obj j')
        (c.ι.app j' ≫ g))
    (((Equiv.symm F.partialLeftAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1}
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j))
              (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j)) :
          (a : (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j)) →
            F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j)
        (c.ι.app j ≫ g) ≫
      map (obj (const J) Y) φ)

Tactic:
apply F.partialLeftAdjointHomEquiv.injective

Premises used: CategoryTheory.Functor.partialLeftAdjointHomEquiv, Equiv.injective