-- 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 ⊥)
inst_3 : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
h :
  Eq.{v + 1} (α := F.obj (op i))
    ((↑(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)
              ⋯) :
          (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ F).obj j_1)
        (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)) :
      obj (C := { x : J // x ∈ Set.Iio j }ᵒᵖ)
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          F)
        (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        (val (e (Order.succ i) ⋯)) :
      (fun (X : Type v) ↦ X) (F.obj (op i)))
⊢ Eq (α := F.obj (op i))
    ((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 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)
            ⋯)) :
      (fun (X : Type v) ↦ X) (F.obj (op i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        (val (e (Order.succ i) ⋯)) :
      (fun (X : Type v) ↦ X) (F.obj (op i)))

Tactic:
rw [d.map_lift _ _ _ _ hi]

Premises used: CategoryTheory.Functor.WellOrderInductionData.map_lift