-- 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' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
a :
  Eq.{v₁ + 1} (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((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)
        (F.partialLeftAdjointMap (R.map φ) ≫
          ((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1} ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                  (F.partialLeftAdjointObj (R.obj j') ⟶ Y)) :
              (a : (R.obj j').obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j') ⟶ Y)
            (c.ι.app j' ≫ g)) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((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)
        (((Equiv.symm F.partialLeftAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                (F.partialLeftAdjointObj (R.obj j) ⟶ Y)) :
            (a : (R.obj j).obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j) ⟶ Y)
          (c.ι.app j ≫ g)) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
a₁ :
  ((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)
      (F.partialLeftAdjointMap (R.map φ) ≫
        ((Equiv.symm F.partialLeftAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                (F.partialLeftAdjointObj (R.obj j') ⟶ Y)) :
            (a : (R.obj j').obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j') ⟶ Y)
          (c.ι.app j' ≫ g)) =
    c.ι.app j ≫ g
a₂ :
  (R.map φ).hom ≫
      ((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)
        (((Equiv.symm F.partialLeftAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                (F.partialLeftAdjointObj (R.obj j') ⟶ Y)) :
            (a : (R.obj j').obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j') ⟶ Y)
          (c.ι.app j' ≫ g)) =
    c.ι.app j ≫ g
a₃ : (R.map φ).hom ≫ c.ι.app j' ≫ g = c.ι.app j ≫ g
a₄ a₅ : c.ι.app j ≫ g = c.ι.app j ≫ g
⊢ Eq.{v₁ + 1} (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((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)
        (F.partialLeftAdjointMap (R.map φ) ≫
          ((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1} ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                  (F.partialLeftAdjointObj (R.obj j') ⟶ Y)) :
              (a : (R.obj j').obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j') ⟶ Y)
            (c.ι.app j' ≫ g)) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((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)
        (((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1} ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                  (F.partialLeftAdjointObj (R.obj j) ⟶ Y)) :
              (a : (R.obj j).obj ⟶ F.obj Y) → F.partialLeftAdjointObj (R.obj j) ⟶ Y)
            (c.ι.app j ≫ g) ≫
          𝟙 Y) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)

Tactic:
rw [comp_id, Equiv.apply_symm_apply, partialLeftAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, reassoc_of% this]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Category.comp_id, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp