-- 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
f : Y ⟶ c'.pt
j : J
⊢ (fun (g : (F.op ⋙ obj yoneda c.pt).obj (op Y)) ↦
          (hc'.lift
              { pt := Y,
                π :=
                  {
                    app := fun (j : 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),
                    naturality := ⋯ } } :
            Cone.pt.{v_1, v₁, u_1, u₁} (J := J) (F := R ⋙ F.partialRightAdjoint)
                { pt := Y,
                  π :=
                    {
                      app := fun (j : 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),
                      naturality := ⋯ : NatTrans (obj (const J) Y) (R ⋙ F.partialRightAdjoint) } :
                  Cone (R ⋙ F.partialRightAdjoint) } ⟶
              c'.pt))
        ((fun (f : Y ⟶ c'.pt) ↦
            (hc.lift
                { pt := F.1 Y,
                  π :=
                    {
                      app := fun (j : J) ↦
                        ((F.partialRightAdjointHomEquiv :
                              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                                (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
                            (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
                          (f ≫ c'.π.app j),
                      naturality := ⋯ } } :
              Cone.pt.{v_1, v₂, u_1, u₂} (J := J) (F := R ⋙ F.rightAdjointObjIsDefined.ι)
                  { pt := F.1 Y,
                    π :=
                      {
                        app := fun (j : J) ↦
                          ((F.partialRightAdjointHomEquiv :
                                Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                                  (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
                              (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
                            (f ≫ c'.π.app j),
                        naturality := ⋯ } } ⟶
                c.pt))
          f) ≫
      c'.π.app j =
    f ≫ c'.π.app j

Tactic:
simp