-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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 ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
obtain :
  ∀ (hi : Order.IsSuccLimit.{u} (α := J) ⊥) (hij : LE.le.{u} (α := J) ⊥ ⊥),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
        val₀ =
      d.lift ⊥ hi
        (Subtype.mk (p :=
          fun
            (x :
              (j : { x : J // Membership.mem (γ := Set J) (Set.Iio ⊥) x }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                          (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
                        ⋯) ⋙
                    F)
                  j) ↦
          Membership.mem (γ :=
            Set
              ((j : { x : J // Membership.mem (γ := Set J) (Set.Iio ⊥) x }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                          (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
                        ⋯) ⋙
                    F)
                  j))
            (sections
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                      (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
                    ⋯) ⋙
                F))
            x)
          (fun (x : { x : J // Membership.mem (γ := Set J) (Set.Iio ⊥) x }ᵒᵖ) ↦
            match (motive :=
              (x : { x : J // Membership.mem (γ := Set J) (Set.Iio ⊥) x }ᵒᵖ) →
                obj
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                          (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
                        ⋯) ⋙
                    F)
                  x)
              x with
            | op ⟨k, hk⟩ =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                  (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
                val₀)
          ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (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)) ⋯) ⋙
                  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)) ⋯) ⋙
                  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)) ⋯) ⋙
              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)) ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              val₀)
        ⋯)

Tactic:
obtain rfl : i = ⊥ := by simpa using hij

Premises used: rfl