-- 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
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
      (d.lift j hj
        (Subtype.mk (p :=
          fun
            (x :
              (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                        ⋯) ⋙
                    F)
                  j_1) ↦
          Membership.mem (γ :=
            Set
              ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                        ⋯) ⋙
                    F)
                  j_1))
            (sections
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
                F))
            x)
          (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦
            match (motive :=
              (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                        ⋯) ⋙
                    F)
                  x)
              x with
            | op ⟨i, hi⟩ => (e i hi).val)
          ⋯)) =
    val₀
have rw : (↑(Subtype.mk (p :=
          fun
            (x :
              (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (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)
                  j_1) ↦
          Membership.mem (γ :=
            Set
              ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (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)
                  j_1))
            (sections
              (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))
            x)
          (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦
            match (motive :=
              (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                obj
                  (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)
                  x)
              x with
            | op ⟨i, hi⟩ => (e i hi).val)
          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) ⊥ sorry)) =
  val₀
Tactic: rw [d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)]