-- 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
⊢ Eq (α :=
    (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)
    (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 j))) → (fun (X : Type v) ↦ X) (F.obj (op k_1)))
          e.val)
    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 e_x : ∀ (l : J) (hl : l ∈ Set.Iio k),
  Eq.{v + 1} (α :=
    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)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl)))
    (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)
      op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl) 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)
    (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)
      op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl) 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))))
Tactic: ext ⟨l, hl⟩