-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
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₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h_1 : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
erw :
  Eq.{v₃ + 1} (α := X ⟶ U'.obj (F.obj Y'))
    (((adj₂.homEquiv X (F.obj Y') : Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj X ⟶ F.obj Y') (X ⟶ U'.obj (F.obj Y'))) :
          (a : F.obj (L.obj X) ⟶ F.obj Y') → X ⟶ U'.obj (F.obj Y'))
        (F.map
            (L.map g ≫
              (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj Y) :
                      (a : L.obj Y ⟶ (Fork.ofι (adj₁.unit.app Y') ⋯).pt) →
                        { h : L.obj Y ⟶ U.obj (F.obj Y') //
                          h ≫ U.map (F.map (adj₁.unit.app Y')) = h ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                    h) :
                L.obj Y ⟶ U.obj (F.obj Y'))) ≫
          adj₁.counit.app (F.obj Y')) :
      X ⟶ U'.obj (F.obj Y'))
    (g ≫
        (↑((Fork.IsLimit.homIso
                  (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y :
                (a :
                    Y ⟶
                      (limit.cone (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))).pt) →
                  { h : Y ⟶ U'.obj (F.obj Y') //
                    h ≫ U'.map (F.map (adj₁.unit.app Y')) = h ≫ otherMap L U' adj₁ adj₂ Y' })
              ((Equiv.symm
                    (Fork.IsLimit.homIso
                      (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y')))
                      Y) :
                  (a :
                      { f : Y ⟶ U'.obj (F.obj Y') //
                        f ≫ U'.map (F.map (adj₁.unit.app Y')) = f ≫ otherMap L U' adj₁ adj₂ Y' }) →
                    Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
                (Subtype.mk (p := fun (b : Y ⟶ U'.obj (F.obj Y')) ↦
                    b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ Y')
                    (((adj₂.homEquiv Y (F.obj Y') :
                          Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj Y') (Y ⟶ U'.obj (F.obj Y'))) :
                        (a : F.obj (L.obj Y) ⟶ F.obj Y') → Y ⟶ U'.obj (F.obj Y'))
                      (F.map
                          (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj Y) :
                                  (a : L.obj Y ⟶ Y') →
                                    { z : L.obj Y ⟶ U.obj (F.obj Y') //
                                      z ≫ U.map (F.map (adj₁.unit.app Y')) = z ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                                h) :
                            L.obj Y ⟶ U.obj (F.obj Y')) ≫
                        adj₁.counit.app (F.obj Y')))
                    ⋯ :
                  { b : Y ⟶ U'.obj (F.obj Y') //
                    b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ Y' }))) :
          Y ⟶ U'.obj (F.obj Y')) :
      X ⟶ U'.obj (F.obj Y'))
⊢ Eq.{v₃ + 1} (α := X ⟶ U'.obj (F.obj Y'))
    (((adj₂.homEquiv X (F.obj Y') : Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj X ⟶ F.obj Y') (X ⟶ U'.obj (F.obj Y'))) :
          (a : F.obj (L.obj X) ⟶ F.obj Y') → X ⟶ U'.obj (F.obj Y'))
        (F.map
            (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj X) :
                    (a : L.obj X ⟶ Y') →
                      { z : L.obj X ⟶ U.obj (F.obj Y') //
                        z ≫ U.map (F.map (adj₁.unit.app Y')) = z ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                  (L.map g ≫ h)) :
              L.obj X ⟶ U.obj (F.obj Y')) ≫
          adj₁.counit.app (F.obj Y')) :
      X ⟶ U'.obj (F.obj Y'))
    ((↑((Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X :
              (a : X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y') →
                { f : X ⟶ U'.obj (F.obj Y') // f ≫ U'.map (F.map (adj₁.unit.app Y')) = f ≫ otherMap L U' adj₁ adj₂ Y' })
            (g ≫
              (Equiv.symm
                    (Fork.IsLimit.homIso
                      (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y')))
                      Y) :
                  (a :
                      { f : Y ⟶ U'.obj (F.obj Y') //
                        f ≫ U'.map (F.map (adj₁.unit.app Y')) = f ≫ otherMap L U' adj₁ adj₂ Y' }) →
                    Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
                (Subtype.mk (p := fun (b : Y ⟶ U'.obj (F.obj Y')) ↦
                    b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ Y')
                    (((adj₂.homEquiv Y (F.obj Y') :
                          Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj Y') (Y ⟶ U'.obj (F.obj Y'))) :
                        (a : F.obj (L.obj Y) ⟶ F.obj Y') → Y ⟶ U'.obj (F.obj Y'))
                      (F.map
                          (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj Y) :
                                  (a : L.obj Y ⟶ Y') →
                                    { z : L.obj Y ⟶ U.obj (F.obj Y') //
                                      z ≫ U.map (F.map (adj₁.unit.app Y')) = z ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                                h) :
                            L.obj Y ⟶ U.obj (F.obj Y')) ≫
                        adj₁.counit.app (F.obj Y')))
                    ⋯ :
                  { b : Y ⟶ U'.obj (F.obj Y') //
                    b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ Y' }))) :
        X ⟶ U'.obj (F.obj Y')) :
      X ⟶ U'.obj (F.obj Y'))

Tactic:
erw [Fork.IsLimit.homIso_natural, Fork.IsLimit.homIso_natural]

Premises used: CategoryTheory.Limits.Fork.IsLimit.homIso_natural