-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ Eq.{v₂ + 1} (α := unop (F.op.obj (op Y)) ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j)
    (({
              toFun := 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 := ⋯ } },
              invFun := 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 := ⋯ } },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Y ⟶ c'.pt) → (F.op ⋙ yoneda.obj c.pt).obj (op Y))
          (g ≫ f) ≫
        c.π.app j :
      unop (F.op.obj (op Y)) ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ obj yoneda c.pt).map g.op) :
            (a : (fun (X : Type v₂) ↦ X) ((F.op ⋙ yoneda.obj c.pt).obj (op Y'))) →
              (fun (X : Type v₂) ↦ X) ((F.op ⋙ yoneda.obj c.pt).obj (op Y)))
          (({
                  toFun := 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 := ⋯ } },
                  invFun := 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 := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : Y' ⟶ c'.pt) → (F.op ⋙ yoneda.obj c.pt).obj (op Y'))
              f :
            (F.op ⋙ obj yoneda c.pt).obj (op Y')) ≫
        c.π.app j :
      unop (F.op.obj (op Y)) ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j)
have dsimp : 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)
                ((g ≫ f) ≫ c'.π.app j),
            naturality := sorry } } ≫
    c.π.app j =
  (F.map g ≫
      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 := sorry : NatTrans (obj (const J) (F.1 Y')) (R ⋙ F.rightAdjointObjIsDefined.ι) } :
          Cone (R ⋙ F.rightAdjointObjIsDefined.ι) }) ≫
    c.π.app j
Tactic: dsimp