-- 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
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
inl :
  ∀ (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)))
        (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)
            ⋯)) =
      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 j))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
                (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)
                    ⋯)))
          ⋯)
⊢ (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)))
      (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)
          ⋯)) =
    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 j))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              (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)
                  ⋯)))
        ⋯)
have inr : ∀ (hj : Order.IsSuccLimit i) (e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1) (hij : i ≤ i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      (d.lift i hj
        (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 ⟨i_1, hi⟩ => (e i_1 hi).val)
          sorry)) =
    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 i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              (d.lift i hj
                (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 ⟨i_1, hi⟩ => (e i_1 hi).val)
                  sorry)))
        sorry)
Tactic: obtain hij' | rfl := hij.lt_or_eq
Cleared hypotheses: j, hj, e, hij