-- 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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ obj yoneda c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
a :
  Eq.{v₂ + 1} (α :=
    F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j')) →
            F.obj (((const J).obj Y).obj j) ⟶ (R.obj j').obj)
        (map (obj (const J) Y) φ ≫
          ((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1}
                  (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j') ⟶
                    (R.obj j').obj (P := F.rightAdjointObjIsDefined))
                  (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j' ⟶ F.partialRightAdjointObj (R.obj j'))) :
              (a : F.obj (((const J).obj Y).obj j') ⟶ (R.obj j').obj) →
                ((const J).obj Y).obj j' ⟶ F.partialRightAdjointObj (R.obj j'))
            (g ≫ c.π.app j')) :
      F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j')) →
            F.obj (((const J).obj Y).obj j) ⟶ (R.obj j').obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1}
                  (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                  (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j))) :
              (a : F.obj (((const J).obj Y).obj j) ⟶ (R.obj j).obj) →
                ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j))
            (g ≫ c.π.app j) ≫
          (R ⋙ F.partialRightAdjoint).map φ) :
      F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
⊢ Eq.{v₁ + 1} (α := obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ (R ⋙ F.partialRightAdjoint).obj j')
    (map (obj (const J) Y) φ ≫
      ((Equiv.symm F.partialRightAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j') ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
              (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j' ⟶ F.partialRightAdjointObj (R.obj j'))) :
          (a : F.obj (((const J).obj Y).obj j') ⟶ (R.obj j').obj) →
            ((const J).obj Y).obj j' ⟶ F.partialRightAdjointObj (R.obj j'))
        (g ≫ c.π.app j'))
    (((Equiv.symm F.partialRightAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
              (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j))) :
          (a : F.obj (((const J).obj Y).obj j) ⟶ (R.obj j).obj) →
            ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j))
        (g ≫ c.π.app j) ≫
      (R ⋙ F.partialRightAdjoint).map φ)

Tactic:
apply F.partialRightAdjointHomEquiv.injective

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