-- 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} (α := X ⟶ R.obj Y')
    ((((fun (X : B) (Y : A) ↦
                (constructLeftAdjointEquiv R F' adj₁ adj₂ h_1 Y X :
                  Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
              X Y' :
            Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') (X ⟶ R.obj Y')) :
          (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') → X ⟶ R.obj Y')
        (h ≫ g) :
      X ⟶ R.obj Y')
    ((((fun (X : B) (Y : A) ↦
                  (constructLeftAdjointEquiv R F' adj₁ adj₂ h_1 Y X :
                    Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
                X Y :
              Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)) :
            (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) → X ⟶ R.obj Y)
          h ≫
        R.map g :
      X ⟶ R.obj Y')
have rw : Eq.{v₂ + 1} (α := F.obj (U.obj 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 ≫ g)) :
                F'.obj (U.obj X) ⟶ Y')))
          sorry) :
      F.obj (U.obj X) ⟶ R.obj Y') :
    F.obj (U.obj X) ⟶ R.obj Y')
  ((↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h_1 X) (R.obj Y') :
            (a : X ⟶ R.obj Y') →
              { 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 })
          ((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 }) ≫
            R.map g)) :
      F.obj (U.obj X) ⟶ R.obj Y') :
    F.obj (U.obj X) ⟶ R.obj Y')
Tactic: rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]