-- 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 e' : d.Extension val₀ j
h : e.val = e'.val
⊢ e = e'
have mk : ∀ (val : F.obj (op j))
  (map_zero :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
        val =
      val₀)
  (map_succ :
    ∀ (i : J) (hi : i < j),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
          val =
        d.succ i sorry
          ((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 i)))
            val))
  (map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (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)))
          val =
        d.lift i hi
          (Subtype.mk (p :=
            fun
              (x :
                (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J))
                          sorry) ⋙
                      F)
                    j) ↦
            Membership.mem (γ :=
              Set
                ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J))
                          sorry) ⋙
                      F)
                    j))
              (sections
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) sorry) ⋙
                  F))
              x)
            (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
              match (motive :=
                (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J))
                          sorry) ⋙
                      F)
                    x)
                x with
              | op ⟨k, 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)))
                  val)
            sorry))
  (h :
    { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j }.val =
      e'.val),
  { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j } = e'
Tactic: cases e
Cleared hypotheses: e, h