∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  (val : F.obj (Opposite.op j)) (map_zero : F.map (CategoryTheory.homOfLE ⋯).op val = val₀)
  (map_succ :
    ∀ (i : J) (hi : i < j),
      F.map (CategoryTheory.homOfLE ⋯).op val = d.succ i ⋯ (F.map (CategoryTheory.homOfLE ⋯).op val))
  (map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      F.map (CategoryTheory.homOfLE hij).op val =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => F.map (CategoryTheory.homOfLE ⋯).op val,
            ⋯⟩)
  (val_1 : F.obj (Opposite.op j)) (map_zero_1 : F.map (CategoryTheory.homOfLE ⋯).op val_1 = val₀)
  (map_succ_1 :
    ∀ (i : J) (hi : i < j),
      F.map (CategoryTheory.homOfLE ⋯).op val_1 = d.succ i ⋯ (F.map (CategoryTheory.homOfLE ⋯).op val_1))
  (map_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      F.map (CategoryTheory.homOfLE hij).op val_1 =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => F.map (CategoryTheory.homOfLE ⋯).op val_1,
            ⋯⟩),
  ({ val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit } =
      { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 }) =
    (val = val_1)