Documentation

Mathlib.Data.Fin.Tuple.Basic

Operation on tuples #

We interpret maps ∀ i : Fin n, α i as n-tuples of elements of possibly varying type α i, (α 0, …, α (n-1)). A particular case is Fin n → α of elements with all the same type. In this case when α i is a constant map, then tuples are isomorphic (but not definitionally equal) to Vectors.

Main declarations #

There are three (main) ways to consider Fin n as a subtype of Fin (n + 1), hence three (main) ways to move between tuples of length n and of length n + 1 by adding/removing an entry.

Adding at the start #

Adding at the end #

Adding in the middle #

For a pivot p : Fin (n + 1),

p = 0 means we add at the start. p = last n means we add at the end.

Miscellaneous #

theorem Fin.tuple0_le {α : Fin 0Type u_1} [(i : Fin 0) → Preorder (α i)] (f : (i : Fin 0) → α i) (g : (i : Fin 0) → α i) :
f g
def Fin.tail {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) :
α i.succ

The tail of an n+1 tuple, i.e., its last n entries.

Equations
Instances For
    theorem Fin.tail_def {n : } {α : Fin (n + 1)Type u_1} {q : (i : Fin (n + 1)) → α i} :
    (Fin.tail fun (k : Fin (n + 1)) => q k) = fun (k : Fin n) => q k.succ
    def Fin.cons {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin (n + 1)) :
    α i

    Adding an element at the beginning of an n-tuple, to get an n+1-tuple.

    Equations
    Instances For
      @[simp]
      theorem Fin.tail_cons {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) :
      @[simp]
      theorem Fin.cons_succ {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) :
      Fin.cons x p i.succ = p i
      @[simp]
      theorem Fin.cons_zero {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) :
      Fin.cons x p 0 = x
      @[simp]
      theorem Fin.cons_one {n : } {α : Fin (n + 2)Type u_1} (x : α 0) (p : (i : Fin n.succ) → α i.succ) :
      Fin.cons x p 1 = p 0
      @[simp]
      theorem Fin.cons_update {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) (y : α i.succ) :

      Updating a tuple and adding an element at the beginning commute.

      theorem Fin.cons_injective2 {n : } {α : Fin (n + 1)Type u} :

      As a binary function, Fin.cons is injective.

      @[simp]
      theorem Fin.cons_eq_cons {n : } {α : Fin (n + 1)Type u} {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α i.succ} {y : (i : Fin n) → α i.succ} :
      Fin.cons x₀ x = Fin.cons y₀ y x₀ = y₀ x = y
      theorem Fin.cons_left_injective {n : } {α : Fin (n + 1)Type u} (x : (i : Fin n) → α i.succ) :
      Function.Injective fun (x₀ : α 0) => Fin.cons x₀ x
      theorem Fin.cons_right_injective {n : } {α : Fin (n + 1)Type u} (x₀ : α 0) :
      theorem Fin.update_cons_zero {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (z : α 0) :

      Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

      @[simp]
      theorem Fin.cons_self_tail {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) :
      Fin.cons (q 0) (Fin.tail q) = q

      Concatenating the first element of a tuple with its tail gives back the original tuple

      def Fin.consCases {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin n.succ) → α i)Sort v} (h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)) (x : (i : Fin n.succ) → α i) :
      P x

      Recurse on an n+1-tuple by splitting it into a single element and an n-tuple.

      Equations
      Instances For
        @[simp]
        theorem Fin.consCases_cons {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin n.succ) → α i)Sort v} (h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)) (x₀ : α 0) (x : (i : Fin n) → α i.succ) :
        Fin.consCases h (Fin.cons x₀ x) = h x₀ x
        def Fin.consInduction {α : Type u_1} {P : {n : } → (Fin nα)Sort v} (h0 : P Fin.elim0) (h : {n : } → (x₀ : α) → (x : Fin nα) → P xP (Fin.cons x₀ x)) {n : } (x : Fin nα) :
        P x

        Recurse on a tuple by splitting into Fin.elim0 and Fin.cons.

        Equations
        Instances For
          theorem Fin.cons_injective_of_injective {n : } {α : Type u_1} {x₀ : α} {x : Fin nα} (hx₀ : x₀Set.range x) (hx : Function.Injective x) :
          theorem Fin.cons_injective_iff {n : } {α : Type u_1} {x₀ : α} {x : Fin nα} :
          @[simp]
          theorem Fin.forall_fin_zero_pi {α : Fin 0Sort u_1} {P : ((i : Fin 0) → α i)Prop} :
          (∀ (x : (i : Fin 0) → α i), P x) P finZeroElim
          @[simp]
          theorem Fin.exists_fin_zero_pi {α : Fin 0Sort u_1} {P : ((i : Fin 0) → α i)Prop} :
          (∃ (x : (i : Fin 0) → α i), P x) P finZeroElim
          theorem Fin.forall_fin_succ_pi {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin (n + 1)) → α i)Prop} :
          (∀ (x : (i : Fin (n + 1)) → α i), P x) ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (Fin.cons a v)
          theorem Fin.exists_fin_succ_pi {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin (n + 1)) → α i)Prop} :
          (∃ (x : (i : Fin (n + 1)) → α i), P x) ∃ (a : α 0) (v : (i : Fin n) → α i.succ), P (Fin.cons a v)
          @[simp]
          theorem Fin.tail_update_zero {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (z : α 0) :

          Updating the first element of a tuple does not change the tail.

          @[simp]
          theorem Fin.tail_update_succ {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.succ) :

          Updating a nonzero element and taking the tail commute.

          theorem Fin.comp_cons {n : } {α : Type u_1} {β : Type u_2} (g : αβ) (y : α) (q : Fin nα) :
          g Fin.cons y q = Fin.cons (g y) (g q)
          theorem Fin.comp_tail {n : } {α : Type u_1} {β : Type u_2} (g : αβ) (q : Fin n.succα) :
          theorem Fin.le_cons {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {x : α 0} {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ} :
          q Fin.cons x p q 0 x Fin.tail q p
          theorem Fin.cons_le {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {x : α 0} {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ} :
          Fin.cons x p q x q 0 p Fin.tail q
          theorem Fin.cons_le_cons {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α i.succ} {y : (i : Fin n) → α i.succ} :
          Fin.cons x₀ x Fin.cons y₀ y x₀ y₀ x y
          theorem Fin.pi_lex_lt_cons_cons {n : } {α : Fin (n + 1)Type u} {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α i.succ} {y : (i : Fin n) → α i.succ} (s : {i : Fin n.succ} → α iα iProp) :
          Pi.Lex (fun (x x_1 : Fin n.succ) => x < x_1) s (Fin.cons x₀ x) (Fin.cons y₀ y) s x₀ y₀ x₀ = y₀ Pi.Lex (fun (x x_1 : Fin n) => x < x_1) (fun (i : Fin n) => s) x y
          theorem Fin.range_fin_succ {n : } {α : Type u_1} (f : Fin (n + 1)α) :
          @[simp]
          theorem Fin.range_cons {α : Type u_1} {n : } (x : α) (b : Fin nα) :
          def Fin.append {m : } {n : } {α : Type u_1} (a : Fin mα) (b : Fin nα) :
          Fin (m + n)α

          Append a tuple of length m to a tuple of length n to get a tuple of length m + n. This is a non-dependent version of Fin.add_cases.

          Equations
          Instances For
            @[simp]
            theorem Fin.append_left {m : } {n : } {α : Type u_1} (u : Fin mα) (v : Fin nα) (i : Fin m) :
            Fin.append u v (Fin.castAdd n i) = u i
            @[simp]
            theorem Fin.append_right {m : } {n : } {α : Type u_1} (u : Fin mα) (v : Fin nα) (i : Fin n) :
            Fin.append u v (Fin.natAdd m i) = v i
            theorem Fin.append_right_nil {m : } {n : } {α : Type u_1} (u : Fin mα) (v : Fin nα) (hv : n = 0) :
            @[simp]
            theorem Fin.append_elim0 {m : } {α : Type u_1} (u : Fin mα) :
            Fin.append u Fin.elim0 = u Fin.cast
            theorem Fin.append_left_nil {m : } {n : } {α : Type u_1} (u : Fin mα) (v : Fin nα) (hu : m = 0) :
            @[simp]
            theorem Fin.elim0_append {n : } {α : Type u_1} (v : Fin nα) :
            Fin.append Fin.elim0 v = v Fin.cast
            theorem Fin.append_assoc {m : } {n : } {p : } {α : Type u_1} (a : Fin mα) (b : Fin nα) (c : Fin pα) :
            theorem Fin.append_left_eq_cons {α : Type u_1} {n : } (x₀ : Fin 1α) (x : Fin nα) :
            Fin.append x₀ x = Fin.cons (x₀ 0) x Fin.cast

            Appending a one-tuple to the left is the same as Fin.cons.

            theorem Fin.cons_eq_append {n : } {α : Type u_1} (x : α) (xs : Fin nα) :
            Fin.cons x xs = Fin.append (Fin.cons x Fin.elim0) xs Fin.cast

            Fin.cons is the same as appending a one-tuple to the left.

            @[simp]
            theorem Fin.append_cast_left {n : } {m : } {α : Type u_1} (xs : Fin nα) (ys : Fin mα) (n' : ) (h : n' = n) :
            @[simp]
            theorem Fin.append_cast_right {n : } {m : } {α : Type u_1} (xs : Fin nα) (ys : Fin mα) (m' : ) (h : m' = m) :
            theorem Fin.append_rev {m : } {n : } {α : Type u_1} (xs : Fin mα) (ys : Fin nα) (i : Fin (m + n)) :
            Fin.append xs ys i.rev = Fin.append (ys Fin.rev) (xs Fin.rev) (Fin.cast i)
            theorem Fin.append_comp_rev {m : } {n : } {α : Type u_1} (xs : Fin mα) (ys : Fin nα) :
            Fin.append xs ys Fin.rev = Fin.append (ys Fin.rev) (xs Fin.rev) Fin.cast
            def Fin.repeat {n : } {α : Type u_1} (m : ) (a : Fin nα) :
            Fin (m * n)α

            Repeat a m times. For example Fin.repeat 2 ![0, 3, 7] = ![0, 3, 7, 0, 3, 7].

            Equations
            Instances For
              @[simp]
              theorem Fin.repeat_apply {m : } {n : } {α : Type u_1} (a : Fin nα) (i : Fin (m * n)) :
              Fin.repeat m a i = a i.modNat
              @[simp]
              theorem Fin.repeat_zero {n : } {α : Type u_1} (a : Fin nα) :
              Fin.repeat 0 a = Fin.elim0 Fin.cast
              @[simp]
              theorem Fin.repeat_one {n : } {α : Type u_1} (a : Fin nα) :
              theorem Fin.repeat_succ {n : } {α : Type u_1} (a : Fin nα) (m : ) :
              @[simp]
              theorem Fin.repeat_add {n : } {α : Type u_1} (a : Fin nα) (m₁ : ) (m₂ : ) :
              Fin.repeat (m₁ + m₂) a = Fin.append (Fin.repeat m₁ a) (Fin.repeat m₂ a) Fin.cast
              theorem Fin.repeat_rev {m : } {n : } {α : Type u_1} (a : Fin nα) (k : Fin (m * n)) :
              Fin.repeat m a k.rev = Fin.repeat m (a Fin.rev) k
              theorem Fin.repeat_comp_rev {m : } {n : } {α : Type u_1} (a : Fin nα) :
              Fin.repeat m a Fin.rev = Fin.repeat m (a Fin.rev)

              In the previous section, we have discussed inserting or removing elements on the left of a tuple. In this section, we do the same on the right. A difference is that Fin (n+1) is constructed inductively from Fin n starting from the left, not from the right. This implies that Lean needs more help to realize that elements belong to the right types, i.e., we need to insert casts at several places.

              def Fin.init {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) :
              α i.castSucc

              The beginning of an n+1 tuple, i.e., its first n entries

              Equations
              Instances For
                theorem Fin.init_def {n : } {α : Fin (n + 1)Type u_1} {q : (i : Fin (n + 1)) → α i} :
                (Fin.init fun (k : Fin (n + 1)) => q k) = fun (k : Fin n) => q k.castSucc
                def Fin.snoc {n : } {α : Fin (n + 1)Type u} (p : (i : Fin n) → α i.castSucc) (x : α (Fin.last n)) (i : Fin (n + 1)) :
                α i

                Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

                Equations
                Instances For
                  @[simp]
                  theorem Fin.init_snoc {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) :
                  @[simp]
                  theorem Fin.snoc_castSucc {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n) :
                  Fin.snoc p x i.castSucc = p i
                  @[simp]
                  theorem Fin.snoc_comp_castSucc {n : } {α : Type u_1} {a : α} {f : Fin nα} :
                  Fin.snoc f a Fin.castSucc = f
                  @[simp]
                  theorem Fin.snoc_last {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) :
                  Fin.snoc p x (Fin.last n) = x
                  theorem Fin.snoc_zero {α : Type u_1} (p : Fin 0α) (x : α) :
                  Fin.snoc p x = fun (x_1 : Fin (0 + 1)) => x
                  @[simp]
                  theorem Fin.snoc_comp_nat_add {n : } {m : } {α : Type u_1} (f : Fin (m + n)α) (a : α) :
                  @[simp]
                  theorem Fin.snoc_cast_add {m : } {n : } {α : Fin (n + m + 1)Type u_1} (f : (i : Fin (n + m)) → α i.castSucc) (a : α (Fin.last (n + m))) (i : Fin n) :
                  Fin.snoc f a (Fin.castAdd (m + 1) i) = f (Fin.castAdd m i)
                  @[simp]
                  theorem Fin.snoc_comp_cast_add {n : } {m : } {α : Type u_1} (f : Fin (n + m)α) (a : α) :
                  @[simp]
                  theorem Fin.snoc_update {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n) (y : α i.castSucc) :
                  Fin.snoc (Function.update p i y) x = Function.update (Fin.snoc p x) i.castSucc y

                  Updating a tuple and adding an element at the end commute.

                  theorem Fin.update_snoc_last {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (z : α (Fin.last n)) :

                  Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

                  @[simp]
                  theorem Fin.snoc_init_self {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) :
                  Fin.snoc (Fin.init q) (q (Fin.last n)) = q

                  Concatenating the first element of a tuple with its tail gives back the original tuple

                  @[simp]
                  theorem Fin.init_update_last {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (z : α (Fin.last n)) :

                  Updating the last element of a tuple does not change the beginning.

                  @[simp]
                  theorem Fin.init_update_castSucc {n : } {α : Fin (n + 1)Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.castSucc) :

                  Updating an element and taking the beginning commute.

                  theorem Fin.tail_init_eq_init_tail {n : } {β : Type u_1} (q : Fin (n + 2)β) :

                  tail and init commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

                  theorem Fin.cons_snoc_eq_snoc_cons {n : } {β : Type u_1} (a : β) (q : Fin nβ) (b : β) :

                  cons and snoc commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

                  theorem Fin.comp_snoc {n : } {α : Type u_1} {β : Type u_2} (g : αβ) (q : Fin nα) (y : α) :
                  g Fin.snoc q y = Fin.snoc (g q) (g y)
                  theorem Fin.append_right_eq_snoc {α : Type u_1} {n : } (x : Fin nα) (x₀ : Fin 1α) :
                  Fin.append x x₀ = Fin.snoc x (x₀ 0)

                  Appending a one-tuple to the right is the same as Fin.snoc.

                  theorem Fin.snoc_eq_append {n : } {α : Type u_1} (xs : Fin nα) (x : α) :
                  Fin.snoc xs x = Fin.append xs (Fin.cons x Fin.elim0)

                  Fin.snoc is the same as appending a one-tuple

                  theorem Fin.append_left_snoc {n : } {m : } {α : Type u_1} (xs : Fin nα) (x : α) (ys : Fin mα) :
                  theorem Fin.append_right_cons {n : } {m : } {α : Type u_1} (xs : Fin nα) (y : α) (ys : Fin mα) :
                  theorem Fin.append_cons {m : } {n : } {α : Type u_1} (a : α) (as : Fin nα) (bs : Fin mα) :
                  theorem Fin.append_snoc {m : } {n : } {α : Type u_1} (as : Fin nα) (bs : Fin mα) (b : α) :
                  theorem Fin.comp_init {n : } {α : Type u_1} {β : Type u_2} (g : αβ) (q : Fin n.succα) :
                  @[inline]
                  def Fin.snocCases {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin n.succ) → α i)Sort u_1} (h : (xs : (i : Fin n) → α i.castSucc) → (x : α (Fin.last n)) → P (Fin.snoc xs x)) (x : (i : Fin n.succ) → α i) :
                  P x

                  Recurse on an n+1-tuple by splitting it its initial n-tuple and its last element.

                  Equations
                  Instances For
                    @[simp]
                    theorem Fin.snocCases_snoc {n : } {α : Fin (n + 1)Type u} {P : ((i : Fin (n + 1)) → α i)Sort u_1} (h : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (Fin.last n)) → P (Fin.snoc x x₀)) (x : (i : Fin n) → Fin.init α i) (x₀ : α (Fin.last n)) :
                    Fin.snocCases h (Fin.snoc x x₀) = h x x₀
                    def Fin.snocInduction {α : Type u_1} {P : {n : } → (Fin nα)Sort u_2} (h0 : P Fin.elim0) (h : {n : } → (x : Fin nα) → (x₀ : α) → P xP (Fin.snoc x x₀)) {n : } (x : Fin nα) :
                    P x

                    Recurse on a tuple by splitting into Fin.elim0 and Fin.snoc.

                    Equations
                    Instances For
                      def Fin.succAboveCases {n : } {α : Fin (n + 1)Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) :
                      α j

                      Define a function on Fin (n + 1) from a value on i : Fin (n + 1) and values on each Fin.succAbove i j, j : Fin n. This version is elaborated as eliminator and works for propositions, see also Fin.insertNth for a version without an @[elab_as_elim] attribute.

                      Equations
                      • i.succAboveCases x p j = if hj : j = i then x else if hlt : j < i then Eq.recOn (p (j.castPred )) else Eq.recOn (p (j.pred ))
                      Instances For
                        theorem Fin.forall_iff_succAbove {n : } {p : Fin (n + 1)Prop} (i : Fin (n + 1)) :
                        (∀ (j : Fin (n + 1)), p j) p i ∀ (j : Fin n), p (i.succAbove j)
                        def Fin.insertNth {n : } {α : Fin (n + 1)Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) :
                        α j

                        Insert an element into a tuple at a given position. For i = 0 see Fin.cons, for i = Fin.last n see Fin.snoc. See also Fin.succAboveCases for a version elaborated as an eliminator.

                        Equations
                        • i.insertNth x p j = i.succAboveCases x p j
                        Instances For
                          @[simp]
                          theorem Fin.insertNth_apply_same {n : } {α : Fin (n + 1)Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth x p i = x
                          @[simp]
                          theorem Fin.insertNth_apply_succAbove {n : } {α : Fin (n + 1)Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin n) :
                          i.insertNth x p (i.succAbove j) = p j
                          @[simp]
                          theorem Fin.insertNth_comp_succAbove {n : } {β : Type v} (i : Fin (n + 1)) (x : β) (p : Fin nβ) :
                          i.insertNth x p i.succAbove = p
                          theorem Fin.insertNth_eq_iff {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} :
                          i.insertNth x p = q q i = x p = fun (j : Fin n) => q (i.succAbove j)
                          theorem Fin.eq_insertNth_iff {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} :
                          q = i.insertNth x p q i = x p = fun (j : Fin n) => q (i.succAbove j)
                          theorem Fin.insertNth_apply_below {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} {j : Fin (n + 1)} (h : j < i) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) :
                          i.insertNth x p j = Eq.recOn (p (j.castPred ))
                          theorem Fin.insertNth_apply_above {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} {j : Fin (n + 1)} (h : i < j) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) :
                          i.insertNth x p j = Eq.recOn (p (j.pred ))
                          theorem Fin.insertNth_zero {n : } {α : Fin (n + 1)Type u} (x : α 0) (p : (j : Fin n) → α (Fin.succAbove 0 j)) :
                          Fin.insertNth 0 x p = Fin.cons x fun (j : Fin n) => cast (p j)
                          @[simp]
                          theorem Fin.insertNth_zero' {n : } {β : Type v} (x : β) (p : Fin nβ) :
                          theorem Fin.insertNth_last {n : } {α : Fin (n + 1)Type u} (x : α (Fin.last n)) (p : (j : Fin n) → α ((Fin.last n).succAbove j)) :
                          (Fin.last n).insertNth x p = Fin.snoc (fun (j : Fin n) => cast (p j)) x
                          @[simp]
                          theorem Fin.insertNth_last' {n : } {β : Type v} (x : β) (p : Fin nβ) :
                          (Fin.last n).insertNth x p = Fin.snoc p x
                          @[simp]
                          theorem Fin.insertNth_zero_right {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → Zero (α j)] (i : Fin (n + 1)) (x : α i) :
                          i.insertNth x 0 = Pi.single i x
                          theorem Fin.insertNth_rev {n : } {α : Type u_1} (i : Fin (n + 1)) (a : α) (f : Fin nα) (j : Fin (n + 1)) :
                          i.insertNth a f j.rev = i.rev.insertNth a (f Fin.rev) j
                          theorem Fin.insertNth_comp_rev {n : } {α : Type u_1} (i : Fin (n + 1)) (x : α) (p : Fin nα) :
                          i.insertNth x p Fin.rev = i.rev.insertNth x (p Fin.rev)
                          theorem Fin.cons_rev {α : Type u_1} {n : } (a : α) (f : Fin nα) (i : Fin (n + 1)) :
                          Fin.cons a f i.rev = Fin.snoc (f Fin.rev) a i
                          theorem Fin.cons_comp_rev {α : Type u_1} {n : } (a : α) (f : Fin nα) :
                          Fin.cons a f Fin.rev = Fin.snoc (f Fin.rev) a
                          theorem Fin.snoc_rev {α : Type u_1} {n : } (a : α) (f : Fin nα) (i : Fin (n + 1)) :
                          Fin.snoc f a i.rev = Fin.cons a (f Fin.rev) i
                          theorem Fin.snoc_comp_rev {α : Type u_1} {n : } (a : α) (f : Fin nα) :
                          Fin.snoc f a Fin.rev = Fin.cons a (f Fin.rev)
                          theorem Fin.insertNth_binop {n : } {α : Fin (n + 1)Type u} (op : (j : Fin (n + 1)) → α jα jα j) (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
                          (i.insertNth (op i x y) fun (j : Fin n) => op (i.succAbove j) (p j) (q j)) = fun (j : Fin (n + 1)) => op j (i.insertNth x p j) (i.insertNth y q j)
                          @[simp]
                          theorem Fin.insertNth_mul {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
                          @[simp]
                          theorem Fin.insertNth_add {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q
                          @[simp]
                          theorem Fin.insertNth_div {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
                          @[simp]
                          theorem Fin.insertNth_sub {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q
                          @[simp]
                          theorem Fin.insertNth_sub_same {n : } {α : Fin (n + 1)Type u} [(j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) :
                          i.insertNth x p - i.insertNth y p = Pi.single i (x - y)
                          theorem Fin.insertNth_le_iff {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} :
                          i.insertNth x p q x q i p fun (j : Fin n) => q (i.succAbove j)
                          theorem Fin.le_insertNth_iff {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} :
                          q i.insertNth x p q i x (fun (j : Fin n) => q (i.succAbove j)) p
                          theorem Fin.insertNth_mem_Icc {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} :
                          i.insertNth x p Set.Icc q₁ q₂ x Set.Icc (q₁ i) (q₂ i) p Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)
                          theorem Fin.preimage_insertNth_Icc_of_mem {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : x Set.Icc (q₁ i) (q₂ i)) :
                          i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)
                          theorem Fin.preimage_insertNth_Icc_of_not_mem {n : } {α : Fin (n + 1)Type u} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : xSet.Icc (q₁ i) (q₂ i)) :
                          i.insertNth x ⁻¹' Set.Icc q₁ q₂ =
                          def Fin.extractNth {n : } {α : Fin (n + 1)Type u} (i : Fin (n + 1)) (f : (j : Fin (n + 1)) → α j) :
                          α i × ((j : Fin n) → α (i.succAbove j))

                          Separates an n+1-tuple, returning a selected index and then the rest of the tuple. Functional form of Equiv.piFinSuccAbove.

                          Equations
                          • i.extractNth f = (f i, fun (j : Fin n) => f (i.succAbove j))
                          Instances For
                            @[simp]
                            theorem Fin.extractNth_insertNth {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} (x : α i) (p : (j : Fin n) → α (i.succAbove j)) :
                            i.extractNth (i.insertNth x p) = (x, p)
                            @[simp]
                            theorem Fin.insertNth_extractNth {n : } {α : Fin (n + 1)Type u} {i : Fin (n + 1)} (f : (j : Fin (n + 1)) → α j) :
                            i.insertNth (i.extractNth f).1 (i.extractNth f).2 = f
                            def Fin.find {n : } (p : Fin nProp) [DecidablePred p] :

                            find p returns the first index n where p n is satisfied, and none if it is never satisfied.

                            Equations
                            Instances For
                              theorem Fin.find_spec {n : } (p : Fin nProp) [DecidablePred p] {i : Fin n} :
                              i Fin.find pp i

                              If find p = some i, then p i holds

                              theorem Fin.isSome_find_iff {n : } {p : Fin nProp} [DecidablePred p] :
                              (Fin.find p).isSome = true ∃ (i : Fin n), p i

                              find p does not return none if and only if p i holds at some index i.

                              theorem Fin.find_eq_none_iff {n : } {p : Fin nProp} [DecidablePred p] :
                              Fin.find p = none ∀ (i : Fin n), ¬p i

                              find p returns none if and only if p i never holds.

                              theorem Fin.find_min {n : } {p : Fin nProp} [DecidablePred p] {i : Fin n} :
                              i Fin.find p∀ {j : Fin n}, j < i¬p j

                              If find p returns some i, then p j does not hold for j < i, i.e., i is minimal among the indices where p holds.

                              theorem Fin.find_min' {n : } {p : Fin nProp} [DecidablePred p] {i : Fin n} (h : i Fin.find p) {j : Fin n} (hj : p j) :
                              i j
                              theorem Fin.nat_find_mem_find {n : } {p : Fin nProp} [DecidablePred p] (h : ∃ (i : ) (hin : i < n), p i, hin) :
                              Nat.find h, Fin.find p
                              theorem Fin.mem_find_iff {n : } {p : Fin nProp} [DecidablePred p] {i : Fin n} :
                              i Fin.find p p i ∀ (j : Fin n), p ji j
                              theorem Fin.find_eq_some_iff {n : } {p : Fin nProp} [DecidablePred p] {i : Fin n} :
                              Fin.find p = some i p i ∀ (j : Fin n), p ji j
                              theorem Fin.mem_find_of_unique {n : } {p : Fin nProp} [DecidablePred p] (h : ∀ (i j : Fin n), p ip ji = j) {i : Fin n} (hi : p i) :
                              def Fin.contractNth {n : } {α : Type u_1} (j : Fin (n + 1)) (op : ααα) (g : Fin (n + 1)α) (k : Fin n) :
                              α

                              Sends (g₀, ..., gₙ) to (g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ).

                              Equations
                              • j.contractNth op g k = if k < j then g k.castSucc else if k = j then op (g k.castSucc) (g k.succ) else g k.succ
                              Instances For
                                theorem Fin.contractNth_apply_of_lt {n : } {α : Type u_1} (j : Fin (n + 1)) (op : ααα) (g : Fin (n + 1)α) (k : Fin n) (h : k < j) :
                                j.contractNth op g k = g k.castSucc
                                theorem Fin.contractNth_apply_of_eq {n : } {α : Type u_1} (j : Fin (n + 1)) (op : ααα) (g : Fin (n + 1)α) (k : Fin n) (h : k = j) :
                                j.contractNth op g k = op (g k.castSucc) (g k.succ)
                                theorem Fin.contractNth_apply_of_gt {n : } {α : Type u_1} (j : Fin (n + 1)) (op : ααα) (g : Fin (n + 1)α) (k : Fin n) (h : j < k) :
                                j.contractNth op g k = g k.succ
                                theorem Fin.contractNth_apply_of_ne {n : } {α : Type u_1} (j : Fin (n + 1)) (op : ααα) (g : Fin (n + 1)α) (k : Fin n) (hjk : j k) :
                                j.contractNth op g k = g (j.succAbove k)
                                theorem Fin.sigma_eq_of_eq_comp_cast {α : Type u_1} {a : (ii : ) × (Fin iiα)} {b : (ii : ) × (Fin iiα)} (h : a.fst = b.fst) :
                                a.snd = b.snd Fin.cast ha = b

                                To show two sigma pairs of tuples agree, it to show the second elements are related via Fin.cast.

                                theorem Fin.sigma_eq_iff_eq_comp_cast {α : Type u_1} {a : (ii : ) × (Fin iiα)} {b : (ii : ) × (Fin iiα)} :
                                a = b ∃ (h : a.fst = b.fst), a.snd = b.snd Fin.cast h

                                Fin.sigma_eq_of_eq_comp_cast as an iff.