-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h_1 : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ Eq.{v₂ + 1} (α := F.obj (U.obj X) ⟶ R.obj Y')
    (((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y')) :
            Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y')) (F.obj (U.obj X) ⟶ R.obj Y')) :
          (a : U.obj X ⟶ U.obj (R.obj Y')) → F.obj (U.obj X) ⟶ R.obj Y')
        (((adj₂.homEquiv (U.obj X) Y' : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y') (U.obj X ⟶ (R ⋙ U).obj Y')) :
            (a : F'.obj (U.obj X) ⟶ Y') → U.obj X ⟶ U.obj (R.obj Y'))
          ((↑((Cofork.IsColimit.homIso
                      (colimit.isColimit
                        (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                      Y :
                    (a :
                        (colimit.cocone
                              (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))).pt ⟶
                          Y) →
                      { h : F'.obj (U.obj X) ⟶ Y //
                        F'.map (U.map (adj₁.counit.app X)) ≫ h = otherMap R F' adj₁ adj₂ X ≫ h })
                  h) :
              F'.obj (U.obj X) ⟶ Y) ≫
            g)) :
      F.obj (U.obj X) ⟶ R.obj Y')
    ((↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h_1 X) (R.obj Y) :
                (a : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ R.obj Y) →
                  { h : F.obj (U.obj X) ⟶ R.obj Y //
                    F.map (U.map (adj₁.counit.app X)) ≫ h = adj₁.counit.app (F.obj (U.obj X)) ≫ h })
              ((Equiv.symm (Cofork.IsColimit.homIso (counitCoequalises adj₁ h_1 X) (R.obj Y)) :
                  (a :
                      { z : F.obj (U.obj X) ⟶ R.obj Y //
                        F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app (F.obj (U.obj X)) ≫ z }) →
                    X ⟶ R.obj Y)
                (Subtype.mk (p := fun (b : F.obj (U.obj X) ⟶ R.obj Y) ↦
                    F.map (U.map (adj₁.counit.app X)) ≫ b = adj₁.counit.app (F.obj (U.obj X)) ≫ b)
                    (((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
                          Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
                        (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
                      (((adj₂.homEquiv (U.obj X) Y :
                            Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
                        (↑((Cofork.IsColimit.homIso
                                  (colimit.isColimit
                                    (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                                  Y :
                                (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) →
                                  { f : F'.obj (U.obj X) ⟶ Y //
                                    F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f })
                              h) :
                          F'.obj (U.obj X) ⟶ Y)))
                    ⋯ :
                  { b : F.obj (U.obj X) ⟶ R.obj Y //
                    F.map (U.map (adj₁.counit.app X)) ≫ b = adj₁.counit.app (F.obj (U.obj X)) ≫ b }))) :
          F.obj (U.obj X) ⟶ R.obj Y) ≫
        R.map g :
      F.obj (U.obj X) ⟶ R.obj Y')
have erw : Eq.{v₂ + 1} (α := F.obj (U.obj X) ⟶ R.obj Y')
  (((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y')) :
          Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y')) (F.obj (U.obj X) ⟶ R.obj Y')) :
        (a : U.obj X ⟶ U.obj (R.obj Y')) → F.obj (U.obj X) ⟶ R.obj Y')
      (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          (↑((Cofork.IsColimit.homIso
                    (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                    Y :
                  (a :
                      (colimit.cocone
                            (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))).pt ⟶
                        Y) →
                    { h : F'.obj (U.obj X) ⟶ Y //
                      F'.map (U.map (adj₁.counit.app X)) ≫ h = otherMap R F' adj₁ adj₂ X ≫ h })
                h) :
            F'.obj (U.obj X) ⟶ Y) ≫
        (R ⋙ U).map g) :
    F.obj (U.obj X) ⟶ R.obj Y')
  ((↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h_1 X) (R.obj Y) :
              (a : (Cofork.ofπ (adj₁.counit.app X) sorry).pt ⟶ R.obj Y) →
                { h : F.obj (U.obj X) ⟶ R.obj Y //
                  F.map (U.map (adj₁.counit.app X)) ≫ h = adj₁.counit.app (F.obj (U.obj X)) ≫ h })
            ((Equiv.symm (Cofork.IsColimit.homIso (counitCoequalises adj₁ h_1 X) (R.obj Y)) :
                (a :
                    { z : F.obj (U.obj X) ⟶ R.obj Y //
                      F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app (F.obj (U.obj X)) ≫ z }) →
                  X ⟶ R.obj Y)
              (Subtype.mk (p := fun (b : F.obj (U.obj X) ⟶ R.obj Y) ↦
                  F.map (U.map (adj₁.counit.app X)) ≫ b = adj₁.counit.app (F.obj (U.obj X)) ≫ b)
                  (((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
                        Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
                      (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
                    (((adj₂.homEquiv (U.obj X) Y :
                          Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                        (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
                      (↑((Cofork.IsColimit.homIso
                                (colimit.isColimit
                                  (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                                Y :
                              (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) →
                                { f : F'.obj (U.obj X) ⟶ Y //
                                  F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f })
                            h) :
                        F'.obj (U.obj X) ⟶ Y)))
                  sorry :
                { b : F.obj (U.obj X) ⟶ R.obj Y //
                  F.map (U.map (adj₁.counit.app X)) ≫ b = adj₁.counit.app (F.obj (U.obj X)) ≫ b }))) :
        F.obj (U.obj X) ⟶ R.obj Y) ≫
      R.map g :
    F.obj (U.obj X) ⟶ R.obj Y')
Tactic: erw [adj₂.homEquiv_naturality_right]