-- 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₁} D C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
rw :
  Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X')
                (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X'))) :
            (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X') → X.obj ⟶ F.obj (F.partialLeftAdjointObj X'))
          (F.partialLeftAdjointMap f) ≫
        F.map g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (f.hom ≫
        ((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ Y)
                (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
            (a : F.partialLeftAdjointObj X' ⟶ Y) → X'.obj ⟶ F.obj Y)
          g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
rw₁ :
  (f.hom ≫
        ((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ F.partialLeftAdjointObj X')
                (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X'))) :
            (a : F.partialLeftAdjointObj X' ⟶ F.partialLeftAdjointObj X') → X'.obj ⟶ F.obj (F.partialLeftAdjointObj X'))
          (𝟙 (F.partialLeftAdjointObj X'))) ≫
      F.map g =
    f.hom ≫
      ((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ Y)
              (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj X' ⟶ Y) → X'.obj ⟶ F.obj Y)
        g
⊢ Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ Y) (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj X ⟶ Y) → X.obj ⟶ F.obj Y)
        (F.partialLeftAdjointMap f ≫ g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (f.hom ≫
        ((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ Y)
                (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
            (a : F.partialLeftAdjointObj X' ⟶ Y) → X'.obj ⟶ F.obj Y)
          g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
have rw₂ : Eq (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
  (f.hom ≫
    ((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ F.partialLeftAdjointObj X')
              (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X'))) :
          (a : F.partialLeftAdjointObj X' ⟶ F.partialLeftAdjointObj X') → X'.obj ⟶ F.obj (F.partialLeftAdjointObj X'))
        (𝟙 (F.partialLeftAdjointObj X')) ≫
      F.map g)
  (f.hom ≫
    ((F.partialLeftAdjointHomEquiv :
          Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X' ⟶ Y) (X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
        (a : F.partialLeftAdjointObj X' ⟶ Y) → X'.obj ⟶ F.obj Y)
      g)
Tactic: rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc,
    ← partialLeftAdjointHomEquiv_comp, id_comp]