-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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
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')))
            ⋯) :
        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)))
                    ⋯ :
                  { 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')
⊢ 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')

Tactic:
rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]

Premises used: CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, Equiv.symm_apply_eq, Subtype.ext_iff