Documentation

Mathlib.Data.Vector.Basic

Additional theorems and definitions about the Vector type #

This file introduces the infix notation ::ᵥ for Vector.cons.

If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

Equations
Instances For
    instance Vector.instInhabited {n : } {α : Type u_1} [Inhabited α] :
    Equations
    theorem Vector.toList_injective {n : } {α : Type u_1} :
    Function.Injective Vector.toList
    theorem Vector.ext {n : } {α : Type u_1} {v : Vector α n} {w : Vector α n} :
    (∀ (m : Fin n), v.get m = w.get m)v = w

    Two v w : Vector α n are equal iff they are equal at every single index.

    instance Vector.zero_subsingleton {α : Type u_1} :

    The empty Vector is a Subsingleton.

    Equations
    • =
    @[simp]
    theorem Vector.cons_val {n : } {α : Type u_1} (a : α) (v : Vector α n) :
    (a ::ᵥ v) = a :: v
    theorem Vector.eq_cons_iff {n : } {α : Type u_1} (a : α) (v : Vector α n.succ) (v' : Vector α n) :
    v = a ::ᵥ v' v.head = a v.tail = v'
    theorem Vector.ne_cons_iff {n : } {α : Type u_1} (a : α) (v : Vector α n.succ) (v' : Vector α n) :
    v a ::ᵥ v' v.head a v.tail v'
    theorem Vector.exists_eq_cons {n : } {α : Type u_1} (v : Vector α n.succ) :
    ∃ (a : α) (as : Vector α n), v = a ::ᵥ as
    @[simp]
    theorem Vector.toList_ofFn {α : Type u_1} {n : } (f : Fin nα) :
    (Vector.ofFn f).toList = List.ofFn f
    @[simp]
    theorem Vector.mk_toList {n : } {α : Type u_1} (v : Vector α n) (h : v.toList.length = n) :
    v.toList, h = v
    @[simp]
    theorem Vector.length_val {n : } {α : Type u_1} (v : Vector α n) :
    (v).length = n
    @[simp]
    theorem Vector.toList_map {n : } {α : Type u_1} {β : Type u_2} (v : Vector α n) (f : αβ) :
    (Vector.map f v).toList = List.map f v.toList
    @[simp]
    theorem Vector.head_map {n : } {α : Type u_1} {β : Type u_2} (v : Vector α (n + 1)) (f : αβ) :
    (Vector.map f v).head = f v.head
    @[simp]
    theorem Vector.tail_map {n : } {α : Type u_1} {β : Type u_2} (v : Vector α (n + 1)) (f : αβ) :
    (Vector.map f v).tail = Vector.map f v.tail
    theorem Vector.get_eq_get {n : } {α : Type u_1} (v : Vector α n) (i : Fin n) :
    v.get i = v.toList.get (Fin.cast i)
    @[simp]
    theorem Vector.get_replicate {n : } {α : Type u_1} (a : α) (i : Fin n) :
    (Vector.replicate n a).get i = a
    @[simp]
    theorem Vector.get_map {n : } {α : Type u_1} {β : Type u_2} (v : Vector α n) (f : αβ) (i : Fin n) :
    (Vector.map f v).get i = f (v.get i)
    @[simp]
    theorem Vector.map₂_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
    Vector.map₂ f Vector.nil Vector.nil = Vector.nil
    @[simp]
    theorem Vector.map₂_cons {n : } {α : Type u_1} {β : Type u_2} {γ : Type u_3} (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vector β n) (f : αβγ) :
    Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ Vector.map₂ f tl₁ tl₂
    @[simp]
    theorem Vector.get_ofFn {α : Type u_1} {n : } (f : Fin nα) (i : Fin n) :
    (Vector.ofFn f).get i = f i
    @[simp]
    theorem Vector.ofFn_get {n : } {α : Type u_1} (v : Vector α n) :
    Vector.ofFn v.get = v
    def Equiv.vectorEquivFin (α : Type u_2) (n : ) :
    Vector α n (Fin nα)

    The natural equivalence between length-n vectors and functions from Fin n.

    Equations
    • Equiv.vectorEquivFin α n = { toFun := Vector.get, invFun := Vector.ofFn, left_inv := , right_inv := }
    Instances For
      theorem Vector.get_tail {n : } {α : Type u_1} (x : Vector α n) (i : Fin (n - 1)) :
      x.tail.get i = x.get i + 1,
      @[simp]
      theorem Vector.get_tail_succ {n : } {α : Type u_1} (v : Vector α n.succ) (i : Fin n) :
      v.tail.get i = v.get i.succ
      @[simp]
      theorem Vector.tail_val {n : } {α : Type u_1} (v : Vector α n.succ) :
      v.tail = (v).tail
      @[simp]
      theorem Vector.tail_nil {α : Type u_1} :
      Vector.nil.tail = Vector.nil

      The tail of a nil vector is nil.

      @[simp]
      theorem Vector.singleton_tail {α : Type u_1} (v : Vector α 1) :
      v.tail = Vector.nil

      The tail of a vector made up of one element is nil.

      @[simp]
      theorem Vector.tail_ofFn {α : Type u_1} {n : } (f : Fin n.succα) :
      (Vector.ofFn f).tail = Vector.ofFn fun (i : Fin n) => f i.succ
      @[simp]
      theorem Vector.toList_empty {α : Type u_1} (v : Vector α 0) :
      v.toList = []
      @[simp]
      theorem Vector.toList_singleton {α : Type u_1} (v : Vector α 1) :
      v.toList = [v.head]

      The list that makes up a Vector made up of a single element, retrieved via toList, is equal to the list of that single element.

      @[simp]
      theorem Vector.empty_toList_eq_ff {n : } {α : Type u_1} (v : Vector α (n + 1)) :
      v.toList.isEmpty = false
      theorem Vector.not_empty_toList {n : } {α : Type u_1} (v : Vector α (n + 1)) :
      ¬v.toList.isEmpty = true
      @[simp]
      theorem Vector.map_id {α : Type u_1} {n : } (v : Vector α n) :
      Vector.map id v = v

      Mapping under id does not change a vector.

      theorem Vector.nodup_iff_injective_get {n : } {α : Type u_1} {v : Vector α n} :
      v.toList.Nodup Function.Injective v.get
      theorem Vector.head?_toList {n : } {α : Type u_1} (v : Vector α n.succ) :
      v.toList.head? = some v.head
      def Vector.reverse {n : } {α : Type u_1} (v : Vector α n) :
      Vector α n

      Reverse a vector.

      Equations
      • v.reverse = v.toList.reverse,
      Instances For
        theorem Vector.toList_reverse {n : } {α : Type u_1} {v : Vector α n} :
        v.reverse.toList = v.toList.reverse

        The List of a vector after a reverse, retrieved by toList is equal to the List.reverse after retrieving a vector's toList.

        @[simp]
        theorem Vector.reverse_reverse {n : } {α : Type u_1} {v : Vector α n} :
        v.reverse.reverse = v
        @[simp]
        theorem Vector.get_zero {n : } {α : Type u_1} (v : Vector α n.succ) :
        v.get 0 = v.head
        @[simp]
        theorem Vector.head_ofFn {α : Type u_1} {n : } (f : Fin n.succα) :
        (Vector.ofFn f).head = f 0
        theorem Vector.get_cons_zero {n : } {α : Type u_1} (a : α) (v : Vector α n) :
        (a ::ᵥ v).get 0 = a
        @[simp]
        theorem Vector.get_cons_nil {α : Type u_1} {ix : Fin 1} (x : α) :
        (x ::ᵥ Vector.nil).get ix = x

        Accessing the nth element of a vector made up of one element x : α is x itself.

        @[simp]
        theorem Vector.get_cons_succ {n : } {α : Type u_1} (a : α) (v : Vector α n) (i : Fin n) :
        (a ::ᵥ v).get i.succ = v.get i
        def Vector.last {n : } {α : Type u_1} (v : Vector α (n + 1)) :
        α

        The last element of a Vector, given that the vector is at least one element.

        Equations
        Instances For
          theorem Vector.last_def {n : } {α : Type u_1} {v : Vector α (n + 1)} :
          v.last = v.get (Fin.last n)

          The last element of a Vector, given that the vector is at least one element.

          theorem Vector.reverse_get_zero {n : } {α : Type u_1} {v : Vector α (n + 1)} :
          v.reverse.head = v.last

          The last element of a vector is the head of the reverse vector.

          def Vector.scanl {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α n) :
          Vector β (n + 1)

          Construct a Vector β (n + 1) from a Vector α n by scanning f : β → α → β from the "left", that is, from 0 to Fin.last n, using b : β as the starting value.

          Equations
          Instances For
            @[simp]
            theorem Vector.scanl_nil {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) :
            Vector.scanl f b Vector.nil = b ::ᵥ Vector.nil

            Providing an empty vector to scanl gives the starting value b : β.

            @[simp]
            theorem Vector.scanl_cons {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α n) (x : α) :
            Vector.scanl f b (x ::ᵥ v) = b ::ᵥ Vector.scanl f (f b x) v

            The recursive step of scanl splits a vector x ::ᵥ v : Vector α (n + 1) into the provided starting value b : β and the recursed scanl f b x : β as the starting value.

            This lemma is the cons version of scanl_get.

            @[simp]
            theorem Vector.scanl_val {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) {v : Vector α n} :
            (Vector.scanl f b v) = List.scanl f b v

            The underlying List of a Vector after a scanl is the List.scanl of the underlying List of the original Vector.

            @[simp]
            theorem Vector.toList_scanl {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α n) :
            (Vector.scanl f b v).toList = List.scanl f b v.toList

            The toList of a Vector after a scanl is the List.scanl of the toList of the original Vector.

            @[simp]
            theorem Vector.scanl_singleton {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α 1) :
            Vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ Vector.nil

            The recursive step of scanl splits a vector made up of a single element x ::ᵥ nil : Vector α 1 into a Vector of the provided starting value b : β and the mapped f b x : β as the last value.

            @[simp]
            theorem Vector.scanl_head {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α n) :
            (Vector.scanl f b v).head = b

            The first element of scanl of a vector v : Vector α n, retrieved via head, is the starting value b : β.

            @[simp]
            theorem Vector.scanl_get {n : } {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (v : Vector α n) (i : Fin n) :
            (Vector.scanl f b v).get i.succ = f ((Vector.scanl f b v).get i.castSucc) (v.get i)

            For an index i : Fin n, the nth element of scanl of a vector v : Vector α n at i.succ, is equal to the application function f : β → α → β of the castSucc i element of scanl f b v and get v i.

            This lemma is the get version of scanl_cons.

            def Vector.mOfFn {m : Type u → Type u_2} [Monad m] {α : Type u} {n : } :
            (Fin nm α)m (Vector α n)

            Monadic analog of Vector.ofFn. Given a monadic function on Fin n, return a Vector α n inside the monad.

            Equations
            Instances For
              theorem Vector.mOfFn_pure {m : Type u_2 → Type u_3} [Monad m] [LawfulMonad m] {α : Type u_2} {n : } (f : Fin nα) :
              (Vector.mOfFn fun (i : Fin n) => pure (f i)) = pure (Vector.ofFn f)
              def Vector.mmap {m : Type u → Type u_2} [Monad m] {α : Type u_3} {β : Type u} (f : αm β) {n : } :
              Vector α nm (Vector β n)

              Apply a monadic function to each component of a vector, returning a vector inside the monad.

              Equations
              Instances For
                @[simp]
                theorem Vector.mmap_nil {m : Type u_2 → Type u_3} [Monad m] {α : Type u_4} {β : Type u_2} (f : αm β) :
                Vector.mmap f Vector.nil = pure Vector.nil
                @[simp]
                theorem Vector.mmap_cons {m : Type u_2 → Type u_3} [Monad m] {α : Type u_4} {β : Type u_2} (f : αm β) (a : α) {n : } (v : Vector α n) :
                Vector.mmap f (a ::ᵥ v) = do let h'f a let t'Vector.mmap f v pure (h' ::ᵥ t')
                def Vector.inductionOn {α : Type u_1} {C : {n : } → Vector α nSort u_2} {n : } (v : Vector α n) (nil : C Vector.nil) (cons : {n : } → {x : α} → {w : Vector α n} → C wC (x ::ᵥ w)) :
                C v

                Define C v by induction on v : Vector α n.

                This function has two arguments: nil handles the base case on C nil, and cons defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w).

                It is used as the default induction principle for the induction tactic.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Vector.inductionOn_nil {α : Type u_1} {C : {n : } → Vector α nSort u_2} (nil : C Vector.nil) (cons : {n : } → {x : α} → {w : Vector α n} → C wC (x ::ᵥ w)) :
                  (Vector.nil.inductionOn nil fun {n : } {x : α} {w : Vector α n} => cons) = nil
                  @[simp]
                  theorem Vector.inductionOn_cons {α : Type u_1} {C : {n : } → Vector α nSort u_2} {n : } (x : α) (v : Vector α n) (nil : C Vector.nil) (cons : {n : } → {x : α} → {w : Vector α n} → C wC (x ::ᵥ w)) :
                  ((x ::ᵥ v).inductionOn nil fun {n : } {x : α} {w : Vector α n} => cons) = cons (v.inductionOn nil fun {n : } {x : α} {w : Vector α n} => cons)
                  def Vector.inductionOn₂ {n : } {α : Type u_1} {β : Type u_2} {C : {n : } → Vector α nVector β nSort u_4} (v : Vector α n) (w : Vector β n) (nil : C Vector.nil Vector.nil) (cons : {n : } → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x yC (a ::ᵥ x) (b ::ᵥ y)) :
                  C v w

                  Define C v w by induction on a pair of vectors v : Vector α n and w : Vector β n.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Vector.inductionOn₃ {n : } {α : Type u_1} {β : Type u_2} {γ : Type u_3} {C : {n : } → Vector α nVector β nVector γ nSort u_4} (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C Vector.nil Vector.nil Vector.nil) (cons : {n : } → {a : α} → {b : β} → {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y zC (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
                    C u v w

                    Define C u v w by induction on a triplet of vectors u : Vector α n, v : Vector β n, and w : Vector γ b.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Vector.casesOn {α : Type u_1} {m : } {motive : {n : } → Vector α nSort u_4} (v : Vector α m) (nil : motive Vector.nil) (cons : {n : } → (hd : α) → (tl : Vector α n) → motive (hd ::ᵥ tl)) :
                      motive v

                      Define motive v by case-analysis on v : Vector α n.

                      Equations
                      • Vector.casesOn v nil cons = v.inductionOn nil fun (x : ) (hd : α) (tl : Vector α x) (x_1 : motive tl) => cons hd tl
                      Instances For
                        def Vector.casesOn₂ {α : Type u_1} {β : Type u_2} {m : } {motive : {n : } → Vector α nVector β nSort u_4} (v₁ : Vector α m) (v₂ : Vector β m) (nil : motive Vector.nil Vector.nil) (cons : {n : } → (x : α) → (y : β) → (xs : Vector α n) → (ys : Vector β n) → motive (x ::ᵥ xs) (y ::ᵥ ys)) :
                        motive v₁ v₂

                        Define motive v₁ v₂ by case-analysis on v₁ : Vector α n and v₂ : Vector β n.

                        Equations
                        • Vector.casesOn₂ v₁ v₂ nil cons = v₁.inductionOn₂ v₂ nil fun (x : ) (x_1 : α) (y : β) (xs : Vector α x) (ys : Vector β x) (x_2 : motive xs ys) => cons x_1 y xs ys
                        Instances For
                          def Vector.casesOn₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {motive : {n : } → Vector α nVector β nVector γ nSort u_4} (v₁ : Vector α m) (v₂ : Vector β m) (v₃ : Vector γ m) (nil : motive Vector.nil Vector.nil Vector.nil) (cons : {n : } → (x : α) → (y : β) → (z : γ) → (xs : Vector α n) → (ys : Vector β n) → (zs : Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) :
                          motive v₁ v₂ v₃

                          Define motive v₁ v₂ v₃ by case-analysis on v₁ : Vector α n, v₂ : Vector β n, and v₃ : Vector γ n.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Vector.toArray {n : } {α : Type u_1} :
                            Vector α nArray α

                            Cast a vector to an array.

                            Equations
                            Instances For
                              def Vector.insertNth {n : } {α : Type u_1} (a : α) (i : Fin (n + 1)) (v : Vector α n) :
                              Vector α (n + 1)

                              v.insertNth a i inserts a into the vector v at position i (and shifting later components to the right).

                              Equations
                              Instances For
                                theorem Vector.insertNth_val {n : } {α : Type u_1} {a : α} {i : Fin (n + 1)} {v : Vector α n} :
                                (Vector.insertNth a i v) = List.insertNth (i) a v
                                @[simp]
                                theorem Vector.eraseIdx_val {n : } {α : Type u_1} {i : Fin n} {v : Vector α n} :
                                (Vector.eraseIdx i v) = (v).eraseIdx i
                                @[deprecated Vector.eraseIdx_val]
                                theorem Vector.removeNth_val {n : } {α : Type u_1} {i : Fin n} {v : Vector α n} :
                                (Vector.eraseIdx i v) = (v).eraseIdx i

                                Alias of Vector.eraseIdx_val.

                                theorem Vector.eraseIdx_insertNth {n : } {α : Type u_1} {a : α} {v : Vector α n} {i : Fin (n + 1)} :
                                @[deprecated Vector.eraseIdx_insertNth]
                                theorem Vector.removeNth_insertNth {n : } {α : Type u_1} {a : α} {v : Vector α n} {i : Fin (n + 1)} :

                                Alias of Vector.eraseIdx_insertNth.

                                theorem Vector.eraseIdx_insertNth' {n : } {α : Type u_1} {a : α} {v : Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} :
                                Vector.eraseIdx (j.succAbove i) (Vector.insertNth a j v) = Vector.insertNth a (i.predAbove j) (Vector.eraseIdx i v)
                                @[deprecated Vector.eraseIdx_insertNth']
                                theorem Vector.removeNth_insertNth' {n : } {α : Type u_1} {a : α} {v : Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} :
                                Vector.eraseIdx (j.succAbove i) (Vector.insertNth a j v) = Vector.insertNth a (i.predAbove j) (Vector.eraseIdx i v)

                                Alias of Vector.eraseIdx_insertNth'.

                                theorem Vector.insertNth_comm {n : } {α : Type u_1} (a : α) (b : α) (i : Fin (n + 1)) (j : Fin (n + 1)) (h : i j) (v : Vector α n) :
                                def Vector.set {n : } {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) :
                                Vector α n

                                set v n a replaces the nth element of v with a.

                                Equations
                                • v.set i a = (v).set (i) a,
                                Instances For
                                  @[simp]
                                  theorem Vector.toList_set {n : } {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).toList = v.toList.set (i) a
                                  @[simp]
                                  theorem Vector.get_set_same {n : } {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).get i = a
                                  theorem Vector.get_set_of_ne {n : } {α : Type u_1} {v : Vector α n} {i : Fin n} {j : Fin n} (h : i j) (a : α) :
                                  (v.set i a).get j = v.get j
                                  theorem Vector.get_set_eq_if {n : } {α : Type u_1} {v : Vector α n} {i : Fin n} {j : Fin n} (a : α) :
                                  (v.set i a).get j = if i = j then a else v.get j
                                  theorem Vector.sum_set {n : } {α : Type u_1} [AddMonoid α] (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).toList.sum = (Vector.take (i) v).toList.sum + a + (Vector.drop (i + 1) v).toList.sum
                                  theorem Vector.prod_set {n : } {α : Type u_1} [Monoid α] (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).toList.prod = (Vector.take (i) v).toList.prod * a * (Vector.drop (i + 1) v).toList.prod
                                  theorem Vector.sum_set' {n : } {α : Type u_1} [AddCommGroup α] (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).toList.sum = v.toList.sum + -v.get i + a
                                  theorem Vector.prod_set' {n : } {α : Type u_1} [CommGroup α] (v : Vector α n) (i : Fin n) (a : α) :
                                  (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a
                                  def Vector.traverse {n : } {F : Type u → Type u} [Applicative F] {α : Type u} {β : Type u} (f : αF β) :
                                  Vector α nF (Vector β n)

                                  Apply an applicative function to each component of a vector.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Vector.traverse_def {n : } {F : Type u → Type u} [Applicative F] {α : Type u} {β : Type u} (f : αF β) (x : α) (xs : Vector α n) :
                                    Vector.traverse f (x ::ᵥ xs) = Seq.seq (Vector.cons <$> f x) fun (x : Unit) => Vector.traverse f xs
                                    theorem Vector.id_traverse {n : } {α : Type u} (x : Vector α n) :
                                    theorem Vector.comp_traverse {n : } {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : Vector α n) :
                                    theorem Vector.traverse_eq_map_id {n : } {α : Type u_1} {β : Type u_1} (f : αβ) (x : Vector α n) :
                                    theorem Vector.naturality {n : } {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u} {β : Type u} (f : αF β) (x : Vector α n) :
                                    (fun {α : Type u} => η.app α) (Vector.traverse f x) = Vector.traverse ((fun {α : Type u} => η.app α) f) x
                                    Equations
                                    @[simp]
                                    theorem Vector.replicate_succ {α : Type u_1} {n : } (val : α) :
                                    @[simp]
                                    theorem Vector.get_append_cons_zero {α : Type u_1} {m : } {n : } (xs : Vector α n) (ys : Vector α m) {x : α} :
                                    ((x ::ᵥ xs).append ys).get 0, = x
                                    @[simp]
                                    theorem Vector.get_append_cons_succ {α : Type u_1} {m : } {n : } (xs : Vector α n) (ys : Vector α m) {x : α} {i : Fin (n + m)} {h : i + 1 < n.succ + m} :
                                    ((x ::ᵥ xs).append ys).get i + 1, h = (xs.append ys).get i
                                    @[simp]
                                    theorem Vector.append_nil {α : Type u_1} {n : } (xs : Vector α n) :
                                    xs.append Vector.nil = xs
                                    @[simp]
                                    theorem Vector.get_map₂ {α : Type u_2} {β : Type u_3} {n : } {γ : Type u_1} (v₁ : Vector α n) (v₂ : Vector β n) (f : αβγ) (i : Fin n) :
                                    (Vector.map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
                                    @[simp]
                                    theorem Vector.mapAccumr_cons {α : Type u_2} {n : } (xs : Vector α n) :
                                    ∀ {α_1 : Type} {β : Type u_1} {f : αα_1α_1 × β} {x : α} {s : α_1}, Vector.mapAccumr f (x ::ᵥ xs) s = let r := Vector.mapAccumr f xs s; let q := f x r.1; (q.1, q.2 ::ᵥ r.2)
                                    @[simp]
                                    theorem Vector.mapAccumr₂_cons {α : Type} {β : Type} {n : } (xs : Vector α n) (ys : Vector β n) :
                                    ∀ {α_1 β_1 : Type} {f : αβα_1α_1 × β_1} {x : α} {y : β} {s : α_1}, Vector.mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s = let r := Vector.mapAccumr₂ f xs ys s; let q := f x y r.1; (q.1, q.2 ::ᵥ r.2)