-- 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
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 ⟶ 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')
⊢ 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 : 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')
    ((↑((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')

Tactic:
erw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]

Premises used: CategoryTheory.Limits.Cofork.IsColimit.homIso_natural