-- 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 (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (op (Order.succ i)))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
        (val (e (Order.succ i) ⋯)) :
      F.obj (op (Order.succ i)))
h₁ :
  Eq (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    (val (e (Order.succ i) ⋯) : F.obj (op (Order.succ i)))
h₂ h₃ :
  Eq.{v + 1} (α := F.obj (op (Order.succ i)))
    ((↑(Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯) :
        (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) (Order.succ i) ⋯)))
    (val (e (Order.succ i) ⋯))
⊢ Eq (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (op (Order.succ i)))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
        (val (e (Order.succ i) ⋯)) :
      F.obj (op (Order.succ i)))

Tactic:
rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]

Premises used: Iff.mpr, Order.IsSuccLimit.succ_lt_iff, CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.Functor.WellOrderInductionData.map_lift