-- 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 ⊥)
j : J
val : F.obj (op j)
map_zero :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (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 ⋯))) :
          (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 ⋯
        ((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)))
          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))
                        ⋯) ⋙
                    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)))
                val)
          ⋯)
val_1 : F.obj (op j)
map_zero_1 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
      val_1 =
    val₀
map_succ_1 :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
        val_1 =
      d.succ 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)))
          val_1)
map_limit_1 :
  ∀ (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_1 =
      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)))
                val_1)
          ⋯)
h :
  { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j }.val =
    { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 : d.Extension val₀ j }.val
mk :
  ∀
    (map_zero_2 :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
          { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j }.val =
        val₀)
    (map_succ_2 :
      ∀ (i : J) (hi : i < j),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
            { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit :
                d.Extension val₀ j }.val =
          d.succ 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)))
              { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit :
                  d.Extension val₀ j }.val))
    (map_limit_2 :
      ∀ (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 := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit :
                d.Extension val₀ j }.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)))
                    { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit :
                        d.Extension val₀ j }.val)
              ⋯)),
    { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j } =
      {
        val :=
          { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j }.val,
        map_zero := map_zero_2, map_succ := map_succ_2, map_limit := map_limit_2 }
⊢ { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit : d.Extension val₀ j } =
    { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 }

Tactic:
subst h