∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1))
  (x_2 x_3 : ℕ),
  CategoryTheory.Functor.OfSequence.map x_1 x_2 x_3 =
    match (motive := (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → (x_5 x_6 : ℕ) → x_5 ≤ x_6 → (x x_5 ⟶ x x_6)) x, x_1,
      x_2, x_3 with
    | x, x_4, 0, 0 => fun x_5 => CategoryTheory.CategoryStruct.id (x 0)
    | x, f, 0, 1 => fun x => f 0
    | x, f, 0, l.succ => fun x_4 =>
      CategoryTheory.CategoryStruct.comp (f 0) (CategoryTheory.Functor.OfSequence.map (fun n => f (n + 1)) 0 l ⋯)
    | x, x_4, n.succ, 0 => fun a => nomatch a
    | x, f, k.succ, l.succ => fun x_4 => CategoryTheory.Functor.OfSequence.map (fun n => f (n + 1)) k l ⋯