-- 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 Y' : D
g : Y ⟶ Y'
f : c'.pt ⟶ Y
j : J
dsimp :
  Eq (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (c.ι.app j ≫
        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 ≫ g),
                naturality := ⋯ } } :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (c.ι.app j ≫
        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 := ⋯ } } ≫
          F.map g :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
⊢ Eq (α := (R ⋙ F.leftAdjointObjIsDefined.ι).obj j ⟶ F.obj Y')
    (c.ι.app j ≫
      ({
            toFun := 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 := ⋯ } },
            invFun := 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 := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ } :
          (a : c'.pt ⟶ Y') → (F ⋙ coyoneda.obj (op c.pt)).obj Y')
        (f ≫ g))
    (c.ι.app j ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op c.pt)).map g) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op c.pt)).obj Y)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op c.pt)).obj Y'))
        (({
                toFun := 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 := ⋯ } },
                invFun := 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 := ⋯ } },
                left_inv := ⋯, right_inv := ⋯ } :
              (a : c'.pt ⟶ Y) → (F ⋙ coyoneda.obj (op c.pt)).obj Y)
            f :
          (F ⋙ obj coyoneda (op c.pt)).obj Y))

Tactic:
dsimp