-- 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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ obj yoneda c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
a :
  Eq.{v₂ + 1} (α := F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
                (Y ⟶ F.partialRightAdjointObj (R.obj j'))) :
            (a : F.obj Y ⟶ (R.obj j').obj) → Y ⟶ F.partialRightAdjointObj (R.obj j'))
          (g ≫ c.π.app j')) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                  (Y ⟶ F.partialRightAdjointObj (R.obj j))) :
              (a : F.obj Y ⟶ (R.obj j).obj) → Y ⟶ F.partialRightAdjointObj (R.obj j))
            (g ≫ c.π.app j) ≫
          F.partialRightAdjointMap (R.map φ)) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
a₁ :
  g ≫ c.π.app j' =
    ((F.partialRightAdjointHomEquiv :
          Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
            (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
        (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
      (((Equiv.symm F.partialRightAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                (Y ⟶ F.partialRightAdjointObj (R.obj j))) :
            (a : F.obj Y ⟶ (R.obj j).obj) → Y ⟶ F.partialRightAdjointObj (R.obj j))
          (g ≫ c.π.app j) ≫
        F.partialRightAdjointMap (R.map φ))
a₂ :
  g ≫ c.π.app j' =
    ((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
              (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                (Y ⟶ F.partialRightAdjointObj (R.obj j))) :
            (a : F.obj Y ⟶ (R.obj j).obj) → Y ⟶ F.partialRightAdjointObj (R.obj j))
          (g ≫ c.π.app j)) ≫
      (R.map φ).hom
a₃ : g ≫ c.π.app j' = (g ≫ c.π.app j) ≫ (R.map φ).hom
a₄ : g ≫ c.π.app j' = g ≫ c.π.app j ≫ (R.map φ).hom
⊢ Eq.{v₂ + 1} (α := F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        (𝟙 Y ≫
          ((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
                  (Y ⟶ F.partialRightAdjointObj (R.obj j'))) :
              (a : F.obj Y ⟶ (R.obj j').obj) → Y ⟶ F.partialRightAdjointObj (R.obj j'))
            (g ≫ c.π.app j')) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                  (Y ⟶ F.partialRightAdjointObj (R.obj j))) :
              (a : F.obj Y ⟶ (R.obj j).obj) → Y ⟶ F.partialRightAdjointObj (R.obj j))
            (g ≫ c.π.app j) ≫
          F.partialRightAdjointMap (R.map φ)) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
have a₅ : g ≫ c.π.app j' = g ≫ c.π.app j'
Tactic: rw [id_comp, Equiv.apply_symm_apply, partialRightAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, assoc, this]