-- 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 ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hki).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
          e.val :
        (fun (X : Type v) ↦ X) (F.obj (op i))) =
    d.lift k hk
      (Subtype.mk (p :=
        fun
          (x :
            (j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
                  F)
                j) ↦
        Membership.mem (γ :=
          Set
            ((j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
                  F)
                j))
          (sections
            (Functor.op
                (Monotone.functor (f :=
                  (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
              F))
          x)
        (fun (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) ↦
          match (motive :=
            (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k_1, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k_1)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
                    (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
                  e.val :
                (fun (X : Type v) ↦ X) (F.obj (op i))))
        ⋯)
have rw : d.lift k hk
    (Subtype.mk (p :=
      fun
        (x :
          (j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              j) ↦
      Membership.mem (γ :=
        Set
          ((j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              j))
        (sections
          (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
            F))
        x)
      (fun (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) ↦
        match (motive :=
          (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              x)
          x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op k_1)))
            e.val)
      sorry) =
  d.lift k hk
    (Subtype.mk (p :=
      fun
        (x :
          (j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              j) ↦
      Membership.mem (γ :=
        Set
          ((j : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              j))
        (sections
          (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
            F))
        x)
      (fun (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) ↦
        match (motive :=
          (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) sorry) ⋙
                F)
              x)
          x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
                  (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
                e.val :
              (fun (X : Type v) ↦ X) (F.obj (op i))))
      sorry)
Tactic: rw [← comp_apply, ← map_comp, ← op_comp, homOfLE_comp,
      e.map_limit k hk (hki.trans hij)]