-- 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
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
        ((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)))
            e.val :
          (fun (X : Type v) ↦ X) (F.obj (op i))))
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
        ((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)))
            e.val :
          (fun (X : Type v) ↦ X) (F.obj (op i))))
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE hij))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE hij))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯ ≫ homOfLE hij).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯ ≫ homOfLE hij).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₇ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
rw₈ rw₉ :
  d.succ k ⋯
      ((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)))
        e.val) =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
        e.val)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ k))))
      ((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)))
          e.val :
        (fun (X : Type v) ↦ X) (F.obj (op i))) =
    d.succ k ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
        ((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)))
            e.val :
          (fun (X : Type v) ↦ X) (F.obj (op i))))

Tactic:
rw [← comp_apply, ← map_comp, ← comp_apply, ← map_comp, ← op_comp, ← op_comp,
      homOfLE_comp, homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ, CategoryTheory.comp_apply, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp, lt_of_lt_of_le