-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (e i hij').val =
    d.lift i hi
      (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
        Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
          (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
        (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            (e i hij').val)
        ⋯)
l : J
hl : l ∈ Set.Iio i
⊢ Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        (e i hij').val :
      F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
have inl : Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
      (e i hij').val :
    F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
  ((↑(Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) sorry) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry) :
        (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ F).obj j_1)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) l sorry)) :
    obj (C := { x : J // x ∈ Set.Iio j }ᵒᵖ)
      (Functor.op
          (Monotone.functor (f :=
            (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) sorry) ⋙
        F)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) l sorry)))
Tactic: rw [map_lift _ _ _ _ _ (hl.trans hij')]