-- 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
⊢ c.ι.app j ≫
      (fun (f : c'.pt ⟶ Y) ↦
          (hc.desc
              { pt := F.1 Y,
                ι :=
                  {
                    app := fun (j : J) ↦
                      ((F.partialLeftAdjointHomEquiv :
                            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
                              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
                          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
                        (c'.ι.app j ≫ f),
                    naturality := ⋯ } } :
            c.pt ⟶
              Cocone.pt.{v_1, v₁, u_1, u₁} (J := J) (F := R ⋙ F.leftAdjointObjIsDefined.ι)
                { pt := F.1 Y,
                  ι :=
                    {
                      app := fun (j : J) ↦
                        ((F.partialLeftAdjointHomEquiv :
                              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
                                ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
                            (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
                          (c'.ι.app j ≫ f),
                      naturality := ⋯ } }))
        ((fun (g : (F ⋙ obj coyoneda (op c.pt)).obj Y) ↦
            (hc'.desc
                { pt := Y,
                  ι :=
                    {
                      app := fun (j : 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),
                      naturality := ⋯ } } :
              c'.pt ⟶
                Cocone.pt.{v_1, v₂, u_1, u₂} (J := J) (F := R ⋙ F.partialLeftAdjoint)
                  { pt := Y,
                    ι :=
                      {
                        app := fun (j : 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),
                        naturality := ⋯ } }))
          g) =
    c.ι.app j ≫ g

Tactic:
simp