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