-- 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
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
rw :
  Eq (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (F.map f ≫
      ((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y')
              (F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y') → F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj)
        (F.partialRightAdjointMap g))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
              (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
        f ≫
      g.hom)
rw₁ :
  Eq (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (F.map f ≫
      ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y)
                (F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y) → F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj)
          (𝟙 (F.partialRightAdjointObj Y)) ≫
        g.hom)
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
              (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
        f ≫
      g.hom)
rw₂ :
  (F.map f ≫
        ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y)
                (F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y) → F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj)
          (𝟙 (F.partialRightAdjointObj Y))) ≫
      g.hom =
    ((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
              (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
        f ≫
      g.hom
rw₃ :
  Eq.{v₂ + 1} (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
                (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
          (f ≫ 𝟙 (F.partialRightAdjointObj Y)) ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
                (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
rw₄ rw₅ :
  Eq.{v₂ + 1} (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
                (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
                (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y')
              (F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))) :
          (a : X ⟶ F.partialRightAdjointObj Y') → F.obj X ⟶ Y'.obj)
        (f ≫ F.partialRightAdjointMap g) :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
                (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))

Tactic:
rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
    ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp, CategoryTheory.Functor.partialRightAdjointHomEquiv_map, CategoryTheory.Category.comp_id