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

Tactic:
rw [← homOfLE_comp ((Order.lt_succ_iff_of_not_isMax hj).mp hi) (Order.le_succ j), op_comp,
        map_comp, comp_apply, d.map_succ, ← e.map_succ i hij,
        ← homOfLE_comp (Order.succ_le_of_lt hij) (Order.le_succ j), op_comp,
        map_comp, comp_apply, d.map_succ]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.WellOrderInductionData.map_succ, Order.succ_le_of_lt, CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ, CategoryTheory.comp_apply, CategoryTheory.homOfLE_comp, Iff.mp, Order.lt_succ_iff_of_not_isMax, CategoryTheory.Functor.map_comp, Order.le_succ