-- 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 ⊥)
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)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j_1 j' : { x : J // x ∈ Set.Iio i }ᵒᵖ
f : j_1 ⟶ j'
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (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'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (map
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) ⋯) ⋙
                F)
              f) :
          (a : (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ F).obj j_1)) →
            (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ F).obj j'))
        ((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 :
              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))
          j_1) :
      (fun (X : Type v) ↦ X)
        (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'))
    ((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 :
            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))
        j' :
      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')
have dsimp : Eq (α := F.obj (op (↑(unop j') : J)))
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (F.map
              (Quiver.Hom.op (map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) sorry) f.unop))) :
          TypeCat.Fun (F.obj (op (↑(unop j_1) : J))) (F.obj (op (↑(unop j') : J)))) :
        (a : F.obj (op (↑(unop j_1) : J))) → F.obj (op (↑(unop j') : J)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : F.obj (op j)) → F.obj (op (↑j_1.1 : J)))
          val :
        F.obj (op (↑j_1.1 : J))) :
    F.obj (op (↑(unop j') : J)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op j)) → F.obj (op (↑j'.1 : J)))
      val :
    F.obj (op (↑j'.1 : J)))
Tactic: dsimp