-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (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₂} 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'
⊢ Eq.{v₃ + 1} (α := X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
    ((((fun (X : C) (Y : B) ↦
                (Equiv.symm (constructRightAdjointEquiv L U' adj₁ adj₂ h_1 X Y) :
                  Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y) (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)))
              X Y' :
            Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y') (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')) :
          (a : L.obj X ⟶ Y') → X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
        (L.map g ≫ h) :
      X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
    (g ≫
        (((fun (X : C) (Y : B) ↦
                  (Equiv.symm (constructRightAdjointEquiv L U' adj₁ adj₂ h_1 X Y) :
                    Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y) (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)))
                Y Y' :
              Equiv.{v₂ + 1, v₃ + 1} (L.obj Y ⟶ Y') (Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')) :
            (a : L.obj Y ⟶ Y') → Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
          h :
      X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y')
have rw : Eq.{v₃ + 1} (α := X ⟶ U'.obj (F.obj Y'))
  ((↑(Subtype.mk (p := fun (b : X ⟶ U'.obj (F.obj Y')) ↦
          b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ 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'))
            (((Equiv.symm (adj₁.homEquiv (L.obj X) (F.obj Y')) :
                  Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ U.obj (F.obj Y')) (F.obj (L.obj X) ⟶ F.obj Y')) :
                (a : L.obj X ⟶ U.obj (F.obj Y')) → F.obj (L.obj X) ⟶ F.obj Y')
              (↑((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'))))
          sorry) :
      X ⟶ U'.obj (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'))
                    (((Equiv.symm (adj₁.homEquiv (L.obj Y) (F.obj Y')) :
                          Equiv.{v₂ + 1, v₁ + 1} (L.obj Y ⟶ U.obj (F.obj Y')) (F.obj (L.obj Y) ⟶ F.obj Y')) :
                        (a : L.obj Y ⟶ U.obj (F.obj Y')) → F.obj (L.obj Y) ⟶ F.obj Y')
                      (↑((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'))))
                  sorry :
                { 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: rw [constructRightAdjointEquiv_symm_apply, constructRightAdjointEquiv_symm_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]