Documentation

Mathlib.Data.Fin.Basic

The finite type with n elements #

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions #

Induction principles #

Embeddings and isomorphisms #

Other casts #

Misc definitions #

def finZeroElim {α : Fin 0Sort u_1} (x : Fin 0) :
α x

Elimination principle for the empty set Fin 0, dependent version.

Equations
Instances For
    @[deprecated Fin.eq_of_val_eq]
    theorem Fin.eq_of_veq {n : } {i : Fin n} {j : Fin n} :
    i = ji = j

    Alias of Fin.eq_of_val_eq.

    @[deprecated Fin.val_eq_of_eq]
    theorem Fin.veq_of_eq {n : } {i : Fin n} {j : Fin n} (h : i = j) :
    i = j

    Alias of Fin.val_eq_of_eq.

    @[deprecated Fin.ne_of_val_ne]
    theorem Fin.ne_of_vne {n : } {i : Fin n} {j : Fin n} (h : i j) :
    i j

    Alias of Fin.ne_of_val_ne.

    @[deprecated Fin.val_ne_of_ne]
    theorem Fin.vne_of_ne {n : } {i : Fin n} {j : Fin n} (h : i j) :
    i j

    Alias of Fin.val_ne_of_ne.

    instance Fin.instCanLiftNatValLt {n : } :
    CanLift (Fin n) Fin.val fun (x : ) => x < n
    Equations
    • =
    def Fin.rec0 {α : Fin 0Sort u_1} (i : Fin 0) :
    α i

    A dependent variant of Fin.elim0.

    Equations
    Instances For
      theorem Fin.size_positive {n : } :
      Fin n0 < n

      If you actually have an element of Fin n, then the n is always positive

      theorem Fin.size_positive' {n : } [Nonempty (Fin n)] :
      0 < n
      theorem Fin.prop {n : } (a : Fin n) :
      a < n
      theorem Fin.lt_of_le_of_lt {n : } {a : Fin n} {b : Fin n} {c : Fin n} :
      a bb < ca < c
      theorem Fin.lt_of_lt_of_le {n : } {a : Fin n} {b : Fin n} {c : Fin n} :
      a < bb ca < c
      theorem Fin.le_rfl {n : } {a : Fin n} :
      a a
      theorem Fin.lt_iff_le_and_ne {n : } {a : Fin n} {b : Fin n} :
      a < b a b a b
      theorem Fin.lt_or_lt_of_ne {n : } {a : Fin n} {b : Fin n} (h : a b) :
      a < b b < a
      theorem Fin.lt_or_le {n : } (a : Fin n) (b : Fin n) :
      a < b b a
      theorem Fin.le_or_lt {n : } (a : Fin n) (b : Fin n) :
      a b b < a
      theorem Fin.le_of_eq {n : } {a : Fin n} {b : Fin n} (hab : a = b) :
      a b
      theorem Fin.ge_of_eq {n : } {a : Fin n} {b : Fin n} (hab : a = b) :
      b a
      theorem Fin.eq_or_lt_of_le {n : } {a : Fin n} {b : Fin n} :
      a ba = b a < b
      theorem Fin.lt_or_eq_of_le {n : } {a : Fin n} {b : Fin n} :
      a ba < b a = b
      theorem Fin.lt_last_iff_ne_last {n : } {a : Fin (n + 1)} :
      theorem Fin.ne_zero_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (hab : a < b) :
      b 0
      theorem Fin.ne_last_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (hab : a < b) :
      @[simp]
      theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
      Fin.equivSubtype a = a,
      @[simp]
      theorem Fin.equivSubtype_symm_apply {n : } (a : { i : // i < n }) :
      Fin.equivSubtype.symm a = a,
      def Fin.equivSubtype {n : } :
      Fin n { i : // i < n }

      Equivalence between Fin n and { i // i < n }.

      Equations
      • Fin.equivSubtype = { toFun := fun (a : Fin n) => a, , invFun := fun (a : { i : // i < n }) => a, , left_inv := , right_inv := }
      Instances For

        coercions and constructions #

        theorem Fin.val_eq_val {n : } (a : Fin n) (b : Fin n) :
        a = b a = b
        @[deprecated Fin.ext_iff]
        theorem Fin.eq_iff_veq {n : } (a : Fin n) (b : Fin n) :
        a = b a = b
        theorem Fin.ne_iff_vne {n : } (a : Fin n) (b : Fin n) :
        a b a b
        @[simp]
        theorem Fin.mk_eq_mk {n : } {a : } {h : a < n} {a' : } {h' : a' < n} :
        a, h = a', h' a = a'
        theorem Fin.heq_fun_iff {α : Sort u_1} {k : } {l : } (h : k = l) {f : Fin kα} {g : Fin lα} :
        HEq f g ∀ (i : Fin k), f i = g i,

        Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

        theorem Fin.heq_fun₂_iff {α : Sort u_1} {k : } {l : } {k' : } {l' : } (h : k = l) (h' : k' = l') {f : Fin kFin k'α} {g : Fin lFin l'α} :
        HEq f g ∀ (i : Fin k) (j : Fin k'), f i j = g i, j,

        Assume k = l and k' = l'. If two functions Fin k → Fin k' → α and Fin l → Fin l' → α are equal on each pair, then they coincide (in the heq sense).

        theorem Fin.heq_ext_iff {k : } {l : } (h : k = l) {i : Fin k} {j : Fin l} :
        HEq i j i = j

        Two elements of Fin k and Fin l are heq iff their values in coincide. This requires k = l. For the left implication without this assumption, see val_eq_val_of_heq.

        order #

        theorem Fin.le_iff_val_le_val {n : } {a : Fin n} {b : Fin n} :
        a b a b
        @[simp]
        theorem Fin.val_fin_lt {n : } {a : Fin n} {b : Fin n} :
        a < b a < b

        a < b as natural numbers if and only if a < b in Fin n.

        @[simp]
        theorem Fin.val_fin_le {n : } {a : Fin n} {b : Fin n} :
        a b a b

        a ≤ b as natural numbers if and only if a ≤ b in Fin n.

        theorem Fin.min_val {n : } {a : Fin n} :
        min (↑a) n = a
        theorem Fin.max_val {n : } {a : Fin n} :
        max (↑a) n = n
        @[simp]
        theorem Fin.valEmbedding_apply {n : } (self : Fin n) :
        Fin.valEmbedding self = self

        The inclusion map Fin n → ℕ is an embedding.

        Equations
        • Fin.valEmbedding = { toFun := Fin.val, inj' := }
        Instances For
          @[simp]
          theorem Fin.equivSubtype_symm_trans_valEmbedding {n : } :
          Fin.equivSubtype.symm.toEmbedding.trans Fin.valEmbedding = Function.Embedding.subtype fun (x : ) => x < n

          Use the ordering on Fin n for checking recursive definitions.

          For example, the following definition is not accepted by the termination checker, unless we declare the WellFoundedRelation instance:

          def factorial {n : ℕ} : Fin n → ℕ
            | ⟨0, _⟩ := 1
            | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
          
          Equations
          • Fin.instWellFoundedRelation_mathlib = measure Fin.val
          @[deprecated Fin.ofNat']
          def Fin.ofNat'' {n : } [NeZero n] (i : ) :
          Fin n

          Given a positive n, Fin.ofNat' i is i % n as an element of Fin n.

          Equations
          Instances For
            @[simp]
            theorem Fin.val_zero' (n : ) [NeZero n] :
            0 = 0

            The Fin.val_zero in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

            @[simp]
            theorem Fin.zero_le' {n : } [NeZero n] (a : Fin n) :
            0 a

            The Fin.zero_le in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

            theorem Fin.pos_iff_ne_zero' {n : } [NeZero n] (a : Fin n) :
            0 < a a 0

            The Fin.pos_iff_ne_zero in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

            @[simp]
            theorem Fin.cast_eq_self {n : } (a : Fin n) :
            Fin.cast a = a
            @[simp]
            theorem Fin.cast_eq_zero {k : } {l : } [NeZero k] [NeZero l] (h : k = l) (x : Fin k) :
            Fin.cast h x = 0 x = 0
            theorem Fin.cast_injective {k : } {l : } (h : k = l) :
            @[simp]
            theorem Fin.revPerm_apply {n : } (i : Fin n) :
            Fin.revPerm i = i.rev
            @[simp]
            theorem Fin.revPerm_symm_apply {n : } (i : Fin n) :
            (Equiv.symm Fin.revPerm) i = i.rev
            def Fin.revPerm {n : } :

            Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by i ↦ n-(i+1).

            Equations
            Instances For
              @[simp]
              theorem Fin.revPerm_symm {n : } :
              Equiv.symm Fin.revPerm = Fin.revPerm
              theorem Fin.cast_rev {n : } {m : } (i : Fin n) (h : n = m) :
              Fin.cast h i.rev = (Fin.cast h i).rev
              theorem Fin.rev_eq_iff {n : } {i : Fin n} {j : Fin n} :
              i.rev = j i = j.rev
              theorem Fin.rev_ne_iff {n : } {i : Fin n} {j : Fin n} :
              i.rev j i j.rev
              theorem Fin.rev_lt_iff {n : } {i : Fin n} {j : Fin n} :
              i.rev < j j.rev < i
              theorem Fin.rev_le_iff {n : } {i : Fin n} {j : Fin n} :
              i.rev j j.rev i
              theorem Fin.lt_rev_iff {n : } {i : Fin n} {j : Fin n} :
              i < j.rev j < i.rev
              theorem Fin.le_rev_iff {n : } {i : Fin n} {j : Fin n} :
              i j.rev j i.rev
              @[simp]
              theorem Fin.val_rev_zero {n : } [NeZero n] :
              (Fin.rev 0) = n.pred
              theorem Fin.last_pos' {n : } [NeZero n] :
              theorem Fin.one_lt_last {n : } [NeZero n] :
              1 < Fin.last (n + 1)

              Coercions to and the fin_omega tactic. #

              theorem Fin.coe_int_sub_eq_ite {n : } (u : Fin n) (v : Fin n) :
              (u - v) = if v u then u - v else u - v + n
              theorem Fin.coe_int_sub_eq_mod {n : } (u : Fin n) (v : Fin n) :
              (u - v) = (u - v) % n
              theorem Fin.coe_int_add_eq_ite {n : } (u : Fin n) (v : Fin n) :
              (u + v) = if u + v < n then u + v else u + v - n
              theorem Fin.coe_int_add_eq_mod {n : } (u : Fin n) (v : Fin n) :
              (u + v) = (u + v) % n

              Preprocessor for omega to handle inequalities in Fin. Note that this involves a lot of case splitting, so may be slow.

              Equations
              Instances For

                addition, numerals, and coercion from Nat #

                @[simp]
                theorem Fin.val_one' (n : ) [NeZero n] :
                1 = 1 % n
                theorem Fin.val_one'' {n : } :
                1 = 1 % (n + 1)
                instance Fin.nontrivial {n : } :
                Nontrivial (Fin (n + 2))
                Equations
                • =
                theorem Fin.add_zero {n : } [NeZero n] (k : Fin n) :
                k + 0 = k
                instance Fin.inhabitedFinOneAdd (n : ) :
                Inhabited (Fin (1 + n))
                Equations
                @[simp]
                theorem Fin.default_eq_zero (n : ) [NeZero n] :
                default = 0
                instance Fin.instNatCast {n : } [NeZero n] :
                Equations
                theorem Fin.natCast_def {n : } [NeZero n] (a : ) :
                a = a % n,
                theorem Fin.val_add_eq_ite {n : } (a : Fin n) (b : Fin n) :
                (a + b) = if n a + b then a + b - n else a + b
                theorem Fin.intCast_val_sub_eq_sub_add_ite {n : } (a : Fin n) (b : Fin n) :
                (a - b) = a - b + (if b a then 0 else n)
                @[simp]
                theorem Fin.ofNat'_eq_cast (n : ) [NeZero n] (a : ) :
                Fin.ofNat' n a = a
                @[simp]
                theorem Fin.val_natCast (a : ) (n : ) [NeZero n] :
                a = a % n
                @[deprecated Fin.val_natCast]
                theorem Fin.val_nat_cast (a : ) (n : ) [NeZero n] :
                a = a % n

                Alias of Fin.val_natCast.

                theorem Fin.val_cast_of_lt {n : } [NeZero n] {a : } (h : a < n) :
                a = a

                Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

                @[simp]
                theorem Fin.cast_val_eq_self {n : } [NeZero n] (a : Fin n) :
                a = a

                If n is non-zero, converting the value of a Fin n to Fin n results in the same value.

                @[simp]
                theorem Fin.natCast_self (n : ) [NeZero n] :
                n = 0
                @[deprecated Fin.natCast_self]
                theorem Fin.nat_cast_self (n : ) [NeZero n] :
                n = 0

                Alias of Fin.natCast_self.

                @[simp]
                theorem Fin.natCast_eq_zero {a : } {n : } [NeZero n] :
                a = 0 n a
                @[deprecated Fin.natCast_eq_zero]
                theorem Fin.nat_cast_eq_zero {a : } {n : } [NeZero n] :
                a = 0 n a

                Alias of Fin.natCast_eq_zero.

                @[simp]
                theorem Fin.natCast_eq_last (n : ) :
                n = Fin.last n
                @[deprecated Fin.natCast_eq_last]
                theorem Fin.cast_nat_eq_last (n : ) :
                n = Fin.last n

                Alias of Fin.natCast_eq_last.

                theorem Fin.le_val_last {n : } (i : Fin (n + 1)) :
                i n
                theorem Fin.natCast_le_natCast {n : } {a : } {b : } (han : a n) (hbn : b n) :
                a b a b
                theorem Fin.natCast_lt_natCast {n : } {a : } {b : } (han : a n) (hbn : b n) :
                a < b a < b
                theorem Fin.natCast_mono {n : } {a : } {b : } (hbn : b n) (hab : a b) :
                a b
                theorem Fin.natCast_strictMono {n : } {a : } {b : } (hbn : b n) (hab : a < b) :
                a < b

                succ and casts into larger Fin types #

                def Fin.succEmb (n : ) :
                Fin n Fin (n + 1)

                Fin.succ as an Embedding

                Equations
                Instances For
                  @[simp]
                  theorem Fin.val_succEmb {n : } :
                  (Fin.succEmb n) = Fin.succ
                  @[simp]
                  theorem Fin.exists_succ_eq {n : } {x : Fin (n + 1)} :
                  (∃ (y : Fin n), y.succ = x) x 0
                  theorem Fin.exists_succ_eq_of_ne_zero {n : } {x : Fin (n + 1)} (h : x 0) :
                  ∃ (y : Fin n), y.succ = x
                  @[simp]
                  theorem Fin.succ_zero_eq_one' {n : } [NeZero n] :
                  theorem Fin.one_pos' {n : } [NeZero n] :
                  0 < 1
                  theorem Fin.zero_ne_one' {n : } [NeZero n] :
                  0 1
                  @[simp]
                  theorem Fin.succ_one_eq_two' {n : } [NeZero n] :

                  The Fin.succ_one_eq_two in Lean only applies in Fin (n+2). This one instead uses a NeZero n typeclass hypothesis.

                  @[simp]
                  theorem Fin.le_zero_iff' {n : } [NeZero n] {k : Fin n} :
                  k 0 k = 0

                  The Fin.le_zero_iff in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                  @[simp]
                  theorem Fin.castLE_inj {n : } {m : } {hmn : m n} {a : Fin m} {b : Fin m} :
                  Fin.castLE hmn a = Fin.castLE hmn b a = b
                  @[simp]
                  theorem Fin.castAdd_inj {n : } {m : } {a : Fin m} {b : Fin m} :
                  theorem Fin.castLE_injective {n : } {m : } (hmn : m n) :
                  @[simp]
                  theorem Fin.castLEEmb_apply {n : } {m : } (h : n m) (i : Fin n) :
                  def Fin.castLEEmb {n : } {m : } (h : n m) :
                  Fin n Fin m

                  Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

                  Equations
                  Instances For
                    @[simp]
                    theorem Fin.coe_castLEEmb {m : } {n : } (hmn : m n) :
                    theorem Fin.equiv_iff_eq {n : } {m : } :
                    Nonempty (Fin m Fin n) m = n
                    @[simp]
                    theorem Fin.castLE_castSucc {n : } {m : } (i : Fin n) (h : n + 1 m) :
                    Fin.castLE h i.castSucc = Fin.castLE i
                    @[simp]
                    theorem Fin.castLE_comp_castSucc {n : } {m : } (h : n + 1 m) :
                    Fin.castLE h Fin.castSucc = Fin.castLE
                    @[simp]
                    theorem Fin.castLE_rfl (n : ) :
                    Fin.castLE = id
                    @[simp]
                    theorem Fin.range_castLE {n : } {k : } (h : n k) :
                    Set.range (Fin.castLE h) = {i : Fin k | i < n}
                    @[simp]
                    theorem Fin.coe_of_injective_castLE_symm {n : } {k : } (h : n k) (i : Fin k) (hi : i Set.range (Fin.castLE h)) :
                    ((Equiv.ofInjective (Fin.castLE h) ).symm i, hi) = i
                    theorem Fin.leftInverse_cast {n : } {m : } (eq : n = m) :
                    theorem Fin.rightInverse_cast {n : } {m : } (eq : n = m) :
                    theorem Fin.cast_lt_cast {n : } {m : } (eq : n = m) {a : Fin n} {b : Fin n} :
                    Fin.cast eq a < Fin.cast eq b a < b
                    theorem Fin.cast_le_cast {n : } {m : } (eq : n = m) {a : Fin n} {b : Fin n} :
                    Fin.cast eq a Fin.cast eq b a b
                    @[simp]
                    theorem finCongr_symm_apply {n : } {m : } (eq : n = m) (i : Fin m) :
                    (finCongr eq).symm i = Fin.cast i
                    @[simp]
                    theorem finCongr_apply {n : } {m : } (eq : n = m) (i : Fin n) :
                    (finCongr eq) i = Fin.cast eq i
                    def finCongr {n : } {m : } (eq : n = m) :
                    Fin n Fin m

                    The 'identity' equivalence between Fin m and Fin n when m = n.

                    Equations
                    Instances For
                      @[simp]
                      theorem finCongr_apply_mk {n : } {m : } (h : m = n) (k : ) (hk : k < m) :
                      (finCongr h) k, hk = k,
                      @[simp]
                      theorem finCongr_refl {n : } (h : optParam (n = n) ) :
                      @[simp]
                      theorem finCongr_symm {n : } {m : } (h : m = n) :
                      (finCongr h).symm = finCongr
                      @[simp]
                      theorem finCongr_apply_coe {n : } {m : } (h : m = n) (k : Fin m) :
                      ((finCongr h) k) = k
                      theorem finCongr_symm_apply_coe {n : } {m : } (h : m = n) (k : Fin n) :
                      ((finCongr h).symm k) = k
                      theorem finCongr_eq_equivCast {n : } {m : } (h : n = m) :

                      While in many cases finCongr is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

                      @[simp]
                      theorem Fin.cast_zero {n : } {n' : } [NeZero n] {h : n = n'} :
                      Fin.cast h 0 = 0
                      theorem Fin.cast_eq_cast {n : } {m : } (h : n = m) :

                      While in many cases Fin.cast is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

                      @[simp]
                      theorem Fin.castAddEmb_apply {n : } (m : ) (i : Fin n) :
                      def Fin.castAddEmb {n : } (m : ) :
                      Fin n Fin (n + m)

                      Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

                      Equations
                      Instances For
                        @[simp]
                        theorem Fin.castSuccEmb_apply {n : } (i : Fin n) :
                        Fin.castSuccEmb i = Fin.castLE i
                        def Fin.castSuccEmb {n : } :
                        Fin n Fin (n + 1)

                        Fin.castSucc as an Embedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

                        Equations
                        Instances For
                          @[simp]
                          theorem Fin.coe_castSuccEmb {n : } :
                          Fin.castSuccEmb = Fin.castSucc
                          theorem Fin.castSucc_le_succ {n : } (i : Fin n) :
                          i.castSucc i.succ
                          @[simp]
                          theorem Fin.castSucc_le_castSucc_iff {n : } {a : Fin n} {b : Fin n} :
                          a.castSucc b.castSucc a b
                          @[simp]
                          theorem Fin.succ_le_castSucc_iff {n : } {a : Fin n} {b : Fin n} :
                          a.succ b.castSucc a < b
                          @[simp]
                          theorem Fin.castSucc_lt_succ_iff {n : } {a : Fin n} {b : Fin n} :
                          a.castSucc < b.succ a b
                          theorem Fin.le_of_castSucc_lt_of_succ_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} {i : Fin n} (hl : i.castSucc < a) (hu : b < i.succ) :
                          b < a
                          theorem Fin.castSucc_lt_or_lt_succ {n : } (p : Fin (n + 1)) (i : Fin n) :
                          i.castSucc < p p < i.succ
                          @[deprecated Fin.castSucc_lt_or_lt_succ]
                          theorem Fin.succAbove_lt_gt {n : } (p : Fin (n + 1)) (i : Fin n) :
                          i.castSucc < p p < i.succ

                          Alias of Fin.castSucc_lt_or_lt_succ.

                          theorem Fin.succ_le_or_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
                          i.succ p p i.castSucc
                          theorem Fin.exists_castSucc_eq_of_ne_last {n : } {x : Fin (n + 1)} (h : x Fin.last n) :
                          ∃ (y : Fin n), y.castSucc = x
                          theorem Fin.forall_fin_succ' {n : } {P : Fin (n + 1)Prop} :
                          (∀ (i : Fin (n + 1)), P i) (∀ (i : Fin n), P i.castSucc) P (Fin.last n)
                          theorem Fin.eq_castSucc_or_eq_last {n : } (i : Fin (n + 1)) :
                          (∃ (j : Fin n), i = j.castSucc) i = Fin.last n
                          theorem Fin.exists_fin_succ' {n : } {P : Fin (n + 1)Prop} :
                          (∃ (i : Fin (n + 1)), P i) (∃ (i : Fin n), P i.castSucc) P (Fin.last n)
                          @[simp]
                          theorem Fin.castSucc_zero' {n : } [NeZero n] :

                          The Fin.castSucc_zero in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                          theorem Fin.castSucc_pos' {n : } [NeZero n] {i : Fin n} (h : 0 < i) :
                          0 < i.castSucc

                          castSucc i is positive when i is positive.

                          The Fin.castSucc_pos in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                          @[simp]
                          theorem Fin.castSucc_eq_zero_iff' {n : } [NeZero n] (a : Fin n) :
                          a.castSucc = 0 a = 0

                          The Fin.castSucc_eq_zero_iff in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                          theorem Fin.castSucc_ne_zero_iff' {n : } [NeZero n] (a : Fin n) :
                          a.castSucc 0 a 0

                          The Fin.castSucc_ne_zero_iff in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

                          theorem Fin.castSucc_ne_zero_of_lt {n : } {p : Fin n} {i : Fin n} (h : p < i) :
                          i.castSucc 0
                          theorem Fin.succ_ne_last_iff {n : } (a : Fin (n + 1)) :
                          a.succ Fin.last (n + 1) a Fin.last n
                          theorem Fin.succ_ne_last_of_lt {n : } {p : Fin n} {i : Fin n} (h : i < p) :
                          i.succ Fin.last n
                          @[simp]
                          theorem Fin.coe_eq_castSucc {n : } {a : Fin n} :
                          a = a.castSucc
                          theorem Fin.coe_succ_lt_iff_lt {n : } {j : Fin n} {k : Fin n} :
                          j < k j < k
                          @[simp]
                          theorem Fin.range_castSucc {n : } :
                          Set.range Fin.castSucc = {i : Fin n.succ | i < n}
                          @[simp]
                          theorem Fin.coe_of_injective_castSucc_symm {n : } (i : Fin n.succ) (hi : i Set.range Fin.castSucc) :
                          ((Equiv.ofInjective Fin.castSucc ).symm i, hi) = i
                          @[simp]
                          theorem Fin.addNatEmb_apply {n : } (m : ) :
                          ∀ (x : Fin n), (Fin.addNatEmb m) x = x.addNat m
                          def Fin.addNatEmb {n : } (m : ) :
                          Fin n Fin (n + m)

                          Fin.addNat as an Embedding, addNatEmb m i adds m to i, generalizes Fin.succ.

                          Equations
                          Instances For
                            @[simp]
                            theorem Fin.natAddEmb_apply (n : ) {m : } (i : Fin m) :
                            def Fin.natAddEmb (n : ) {m : } :
                            Fin m Fin (n + m)

                            Fin.natAdd as an Embedding, natAddEmb n i adds n to i "on the left".

                            Equations
                            Instances For

                              pred #

                              theorem Fin.pred_one' {n : } [NeZero n] (h : optParam (1 0) ) :
                              Fin.pred 1 h = 0
                              theorem Fin.pred_last {n : } (h : optParam (¬Fin.last (n + 1) = 0) ) :
                              (Fin.last (n + 1)).pred h = Fin.last n
                              theorem Fin.pred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                              i.pred hi < j i < j.succ
                              theorem Fin.lt_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                              j < i.pred hi j.succ < i
                              theorem Fin.pred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                              i.pred hi j i j.succ
                              theorem Fin.le_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
                              j i.pred hi j.succ i
                              theorem Fin.castSucc_pred_eq_pred_castSucc {n : } {a : Fin (n + 1)} (ha : a 0) (ha' : optParam (a.castSucc 0) ) :
                              (a.pred ha).castSucc = a.castSucc.pred ha'
                              theorem Fin.castSucc_pred_add_one_eq {n : } {a : Fin (n + 1)} (ha : a 0) :
                              (a.pred ha).castSucc + 1 = a
                              theorem Fin.le_pred_castSucc_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.castSucc 0) :
                              b a.castSucc.pred ha b < a
                              theorem Fin.pred_castSucc_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.castSucc 0) :
                              a.castSucc.pred ha < b a b
                              theorem Fin.pred_castSucc_lt {n : } {a : Fin (n + 1)} (ha : a.castSucc 0) :
                              a.castSucc.pred ha < a
                              theorem Fin.le_castSucc_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
                              b (a.pred ha).castSucc b < a
                              theorem Fin.castSucc_pred_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
                              (a.pred ha).castSucc < b a b
                              theorem Fin.castSucc_pred_lt {n : } {a : Fin (n + 1)} (ha : a 0) :
                              (a.pred ha).castSucc < a
                              @[inline]
                              def Fin.castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                              Fin n

                              castPred i sends i : Fin (n + 1) to Fin n as long as i ≠ last n.

                              Equations
                              • i.castPred h = i.castLT
                              Instances For
                                @[simp]
                                theorem Fin.castLT_eq_castPred {n : } (i : Fin (n + 1)) (h : i < Fin.last n) (h' : optParam (¬i = Fin.last n) ) :
                                i.castLT h = i.castPred h'
                                @[simp]
                                theorem Fin.coe_castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                                (i.castPred h) = i
                                @[simp]
                                theorem Fin.castPred_castSucc {n : } {i : Fin n} (h' : optParam (¬i.castSucc = Fin.last n) ) :
                                i.castSucc.castPred h' = i
                                @[simp]
                                theorem Fin.castSucc_castPred {n : } (i : Fin (n + 1)) (h : i Fin.last n) :
                                (i.castPred h).castSucc = i
                                theorem Fin.castPred_eq_iff_eq_castSucc {n : } (i : Fin (n + 1)) (hi : i Fin.last n) (j : Fin n) :
                                i.castPred hi = j i = j.castSucc
                                @[simp]
                                theorem Fin.castPred_mk {n : } (i : ) (h₁ : i < n) (h₂ : optParam (i < n.succ) ) (h₃ : optParam (i, h₂ Fin.last n) ) :
                                i, h₂.castPred h₃ = i, h₁
                                theorem Fin.castPred_le_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                i.castPred hi j.castPred hj i j
                                theorem Fin.castPred_lt_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                i.castPred hi < j.castPred hj i < j
                                theorem Fin.castPred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                i.castPred hi < j i < j.castSucc
                                theorem Fin.lt_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                j < i.castPred hi j.castSucc < i
                                theorem Fin.castPred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                i.castPred hi j i j.castSucc
                                theorem Fin.le_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i Fin.last n) :
                                j i.castPred hi j.castSucc i
                                theorem Fin.castPred_inj {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i Fin.last n} {hj : j Fin.last n} :
                                i.castPred hi = j.castPred hj i = j
                                theorem Fin.castPred_zero' {n : } [NeZero n] (h : optParam (¬0 = Fin.last n) ) :
                                theorem Fin.castPred_zero {n : } (h : optParam (¬0 = Fin.last (n + 1)) ) :
                                @[simp]
                                theorem Fin.castPred_one {n : } [NeZero n] (h : optParam (¬1 = Fin.last (n + 1)) ) :
                                theorem Fin.rev_pred {n : } {i : Fin (n + 1)} (h : i 0) (h' : optParam (i.rev Fin.last n) ) :
                                (i.pred h).rev = i.rev.castPred h'
                                theorem Fin.rev_castPred {n : } {i : Fin (n + 1)} (h : i Fin.last n) (h' : optParam (i.rev 0) ) :
                                (i.castPred h).rev = i.rev.pred h'
                                theorem Fin.succ_castPred_eq_castPred_succ {n : } {a : Fin (n + 1)} (ha : a Fin.last n) (ha' : optParam (a.succ Fin.last (n + 1)) ) :
                                (a.castPred ha).succ = a.succ.castPred ha'
                                theorem Fin.succ_castPred_eq_add_one {n : } {a : Fin (n + 1)} (ha : a Fin.last n) :
                                (a.castPred ha).succ = a + 1
                                theorem Fin.castpred_succ_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
                                a.succ.castPred ha b a < b
                                theorem Fin.lt_castPred_succ_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
                                b < a.succ.castPred ha b a
                                theorem Fin.lt_castPred_succ {n : } {a : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
                                a < a.succ.castPred ha
                                theorem Fin.succ_castPred_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) :
                                (a.castPred ha).succ b a < b
                                theorem Fin.lt_succ_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) :
                                b < (a.castPred ha).succ b a
                                theorem Fin.lt_succ_castPred {n : } {a : Fin (n + 1)} (ha : a Fin.last n) :
                                a < (a.castPred ha).succ
                                theorem Fin.castPred_le_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a Fin.last n) (hb : b 0) :
                                a.castPred ha b.pred hb a < b
                                theorem Fin.pred_lt_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) (hb : b Fin.last n) :
                                a.pred ha < b.castPred hb a b
                                theorem Fin.pred_lt_castPred {n : } {a : Fin (n + 1)} (h₁ : a 0) (h₂ : a Fin.last n) :
                                a.pred h₁ < a.castPred h₂
                                def Fin.succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
                                Fin (n + 1)

                                succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.

                                Equations
                                • p.succAbove i = if i.castSucc < p then i.castSucc else i.succ
                                Instances For
                                  theorem Fin.succAbove_of_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) :
                                  p.succAbove i = i.castSucc

                                  Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by castSucc when the resulting i.castSucc < p.

                                  theorem Fin.succAbove_of_succ_le {n : } (p : Fin (n + 1)) (i : Fin n) (h : i.succ p) :
                                  p.succAbove i = i.castSucc
                                  theorem Fin.succAbove_of_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) (h : p i.castSucc) :
                                  p.succAbove i = i.succ

                                  Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by succ when the resulting p < i.succ.

                                  theorem Fin.succAbove_of_lt_succ {n : } (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) :
                                  p.succAbove i = i.succ
                                  theorem Fin.succAbove_succ_of_lt {n : } (p : Fin n) (i : Fin n) (h : p < i) :
                                  p.succ.succAbove i = i.succ
                                  theorem Fin.succAbove_succ_of_le {n : } (p : Fin n) (i : Fin n) (h : i p) :
                                  p.succ.succAbove i = i.castSucc
                                  @[simp]
                                  theorem Fin.succAbove_succ_self {n : } (j : Fin n) :
                                  j.succ.succAbove j = j.castSucc
                                  theorem Fin.succAbove_castSucc_of_lt {n : } (p : Fin n) (i : Fin n) (h : i < p) :
                                  p.castSucc.succAbove i = i.castSucc
                                  theorem Fin.succAbove_castSucc_of_le {n : } (p : Fin n) (i : Fin n) (h : p i) :
                                  p.castSucc.succAbove i = i.succ
                                  @[simp]
                                  theorem Fin.succAbove_castSucc_self {n : } (j : Fin n) :
                                  j.castSucc.succAbove j = j.succ
                                  theorem Fin.succAbove_pred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hi : optParam (i 0) ) :
                                  p.succAbove (i.pred hi) = i
                                  theorem Fin.succAbove_pred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i p) (hi : i 0) :
                                  p.succAbove (i.pred hi) = (i.pred hi).castSucc
                                  @[simp]
                                  theorem Fin.succAbove_pred_self {n : } (p : Fin (n + 1)) (h : p 0) :
                                  p.succAbove (p.pred h) = (p.pred h).castSucc
                                  theorem Fin.succAbove_castPred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hi : optParam (i Fin.last n) ) :
                                  p.succAbove (i.castPred hi) = i
                                  theorem Fin.succAbove_castPred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p i) (hi : i Fin.last n) :
                                  p.succAbove (i.castPred hi) = (i.castPred hi).succ
                                  theorem Fin.succAbove_castPred_self {n : } (p : Fin (n + 1)) (h : p Fin.last n) :
                                  p.succAbove (p.castPred h) = (p.castPred h).succ
                                  theorem Fin.succAbove_rev_left {n : } (p : Fin (n + 1)) (i : Fin n) :
                                  p.rev.succAbove i = (p.succAbove i.rev).rev
                                  theorem Fin.succAbove_rev_right {n : } (p : Fin (n + 1)) (i : Fin n) :
                                  p.succAbove i.rev = (p.rev.succAbove i).rev
                                  theorem Fin.succAbove_ne {n : } (p : Fin (n + 1)) (i : Fin n) :
                                  p.succAbove i p

                                  Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) never results in p itself

                                  theorem Fin.ne_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
                                  p p.succAbove i
                                  theorem Fin.succAbove_right_injective {n : } {p : Fin (n + 1)} :
                                  Function.Injective p.succAbove

                                  Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

                                  theorem Fin.succAbove_right_inj {n : } {p : Fin (n + 1)} {i : Fin n} {j : Fin n} :
                                  p.succAbove i = p.succAbove j i = j

                                  Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

                                  @[simp]
                                  theorem Fin.succAboveEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                                  p.succAboveEmb i = p.succAbove i
                                  def Fin.succAboveEmb {n : } (p : Fin (n + 1)) :
                                  Fin n Fin (n + 1)

                                  Fin.succAbove p as an Embedding.

                                  Equations
                                  • p.succAboveEmb = { toFun := p.succAbove, inj' := }
                                  Instances For
                                    @[simp]
                                    theorem Fin.coe_succAboveEmb {n : } (p : Fin (n + 1)) :
                                    p.succAboveEmb = p.succAbove
                                    @[simp]
                                    theorem Fin.succAbove_ne_zero_zero {n : } [NeZero n] {a : Fin (n + 1)} (ha : a 0) :
                                    a.succAbove 0 = 0
                                    theorem Fin.succAbove_eq_zero_iff {n : } [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) :
                                    a.succAbove b = 0 b = 0
                                    theorem Fin.succAbove_ne_zero {n : } [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) (hb : b 0) :
                                    a.succAbove b 0
                                    @[simp]
                                    theorem Fin.succAbove_zero {n : } :
                                    Fin.succAbove 0 = Fin.succ

                                    Embedding Fin n into Fin (n + 1) with a hole around zero embeds by succ.

                                    theorem Fin.succAbove_zero_apply {n : } (i : Fin n) :
                                    Fin.succAbove 0 i = i.succ
                                    @[simp]
                                    theorem Fin.succAbove_ne_last_last {n : } {a : Fin (n + 2)} (h : a Fin.last (n + 1)) :
                                    a.succAbove (Fin.last n) = Fin.last (n + 1)
                                    theorem Fin.succAbove_eq_last_iff {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) :
                                    a.succAbove b = Fin.last (n + 1) b = Fin.last n
                                    theorem Fin.succAbove_ne_last {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) (hb : b Fin.last n) :
                                    a.succAbove b Fin.last (n + 1)
                                    @[simp]
                                    theorem Fin.succAbove_last {n : } :
                                    (Fin.last n).succAbove = Fin.castSucc

                                    Embedding Fin n into Fin (n + 1) with a hole around last n embeds by castSucc.

                                    theorem Fin.succAbove_last_apply {n : } (i : Fin n) :
                                    (Fin.last n).succAbove i = i.castSucc
                                    @[deprecated]
                                    theorem Fin.succAbove_lt_ge {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    i.castSucc < p p i.castSucc
                                    theorem Fin.succAbove_lt_iff_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    p.succAbove i < p i.castSucc < p

                                    Embedding i : Fin n into Fin (n + 1) using a pivot p that is greater results in a value that is less than p.

                                    theorem Fin.succAbove_lt_iff_succ_le {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    p.succAbove i < p i.succ p
                                    theorem Fin.lt_succAbove_iff_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    p < p.succAbove i p i.castSucc

                                    Embedding i : Fin n into Fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

                                    theorem Fin.lt_succAbove_iff_lt_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    p < p.succAbove i p < i.succ
                                    theorem Fin.succAbove_pos {n : } [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) :
                                    0 < p.succAbove i

                                    Embedding a positive Fin n results in a positive Fin (n + 1)

                                    theorem Fin.castPred_succAbove {n : } (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : optParam (y.succAbove x Fin.last n) ) :
                                    (y.succAbove x).castPred h' = x
                                    theorem Fin.pred_succAbove {n : } (x : Fin n) (y : Fin (n + 1)) (h : y x.castSucc) (h' : optParam (y.succAbove x 0) ) :
                                    (y.succAbove x).pred h' = x
                                    theorem Fin.exists_succAbove_eq {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x y) :
                                    ∃ (z : Fin n), y.succAbove z = x
                                    @[simp]
                                    theorem Fin.exists_succAbove_eq_iff {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} :
                                    (∃ (z : Fin n), x.succAbove z = y) y x
                                    @[simp]
                                    theorem Fin.range_succAbove {n : } (p : Fin (n + 1)) :
                                    Set.range p.succAbove = {p}

                                    The range of p.succAbove is everything except p.

                                    @[simp]
                                    theorem Fin.range_succ (n : ) :
                                    Set.range Fin.succ = {0}

                                    succAbove is injective at the pivot

                                    @[simp]
                                    theorem Fin.succAbove_left_inj {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} :
                                    x.succAbove = y.succAbove x = y

                                    succAbove is injective at the pivot

                                    @[simp]
                                    theorem Fin.zero_succAbove {n : } (i : Fin n) :
                                    Fin.succAbove 0 i = i.succ
                                    @[simp]
                                    theorem Fin.succ_succAbove_zero {n : } [NeZero n] (i : Fin n) :
                                    i.succ.succAbove 0 = 0
                                    @[simp]
                                    theorem Fin.succ_succAbove_succ {n : } (i : Fin (n + 1)) (j : Fin n) :
                                    i.succ.succAbove j.succ = (i.succAbove j).succ

                                    succ commutes with succAbove.

                                    @[simp]
                                    theorem Fin.castSucc_succAbove_castSucc {n : } {i : Fin (n + 1)} {j : Fin n} :
                                    i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

                                    castSucc commutes with succAbove.

                                    theorem Fin.pred_succAbove_pred {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a 0) (hb : b 0) (hk : optParam (a.succAbove b 0) ) :
                                    (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

                                    pred commutes with succAbove.

                                    theorem Fin.castPred_succAbove_castPred {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) (hb : b Fin.last n) (hk : optParam (a.succAbove b Fin.last (n + 1)) ) :
                                    (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

                                    castPred commutes with succAbove.

                                    theorem Fin.rev_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
                                    (p.succAbove i).rev = p.rev.succAbove i.rev

                                    rev commutes with succAbove.

                                    @[simp]
                                    theorem Fin.succ_succAbove_one {n : } [NeZero n] (i : Fin (n + 1)) :
                                    i.succ.succAbove 1 = (i.succAbove 0).succ

                                    By moving succ to the outside of this expression, we create opportunities for further simplification using succAbove_zero or succ_succAbove_zero.

                                    @[simp]
                                    theorem Fin.one_succAbove_succ {n : } (j : Fin n) :
                                    Fin.succAbove 1 j.succ = j.succ.succ
                                    @[simp]
                                    def Fin.predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :
                                    Fin n

                                    predAbove p i surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

                                    Equations
                                    • p.predAbove i = if h : p.castSucc < i then i.pred else i.castPred
                                    Instances For
                                      theorem Fin.predAbove_of_le_castSucc {n : } (p : Fin n) (i : Fin (n + 1)) (h : i p.castSucc) (hi : optParam (i Fin.last n) ) :
                                      p.predAbove i = i.castPred hi
                                      theorem Fin.predAbove_of_lt_succ {n : } (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : optParam (i Fin.last n) ) :
                                      p.predAbove i = i.castPred hi
                                      theorem Fin.predAbove_of_castSucc_lt {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : optParam (i 0) ) :
                                      p.predAbove i = i.pred hi
                                      theorem Fin.predAbove_of_succ_le {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.succ i) (hi : optParam (i 0) ) :
                                      p.predAbove i = i.pred hi
                                      theorem Fin.predAbove_succ_of_lt {n : } (p : Fin n) (i : Fin n) (h : i < p) (hi : optParam (i.succ Fin.last n) ) :
                                      p.predAbove i.succ = i.succ.castPred hi
                                      theorem Fin.predAbove_succ_of_le {n : } (p : Fin n) (i : Fin n) (h : p i) :
                                      p.predAbove i.succ = i
                                      @[simp]
                                      theorem Fin.predAbove_succ_self {n : } (p : Fin n) :
                                      p.predAbove p.succ = p
                                      theorem Fin.predAbove_castSucc_of_lt {n : } (p : Fin n) (i : Fin n) (h : p < i) (hi : optParam (i.castSucc 0) ) :
                                      p.predAbove i.castSucc = i.castSucc.pred hi
                                      theorem Fin.predAbove_castSucc_of_le {n : } (p : Fin n) (i : Fin n) (h : i p) :
                                      p.predAbove i.castSucc = i
                                      @[simp]
                                      theorem Fin.predAbove_castSucc_self {n : } (p : Fin n) :
                                      p.predAbove p.castSucc = p
                                      theorem Fin.predAbove_pred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hp : optParam (p 0) ) (hi : optParam (i Fin.last n) ) :
                                      (p.pred hp).predAbove i = i.castPred hi
                                      theorem Fin.predAbove_pred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p i) (hp : p 0) (hi : optParam (i 0) ) :
                                      (p.pred hp).predAbove i = i.pred hi
                                      theorem Fin.predAbove_pred_self {n : } (p : Fin (n + 1)) (hp : p 0) :
                                      (p.pred hp).predAbove p = p.pred hp
                                      theorem Fin.predAbove_castPred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hp : optParam (p Fin.last n) ) (hi : optParam (i 0) ) :
                                      (p.castPred hp).predAbove i = i.pred hi
                                      theorem Fin.predAbove_castPred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i p) (hp : p Fin.last n) (hi : optParam (i Fin.last n) ) :
                                      (p.castPred hp).predAbove i = i.castPred hi
                                      theorem Fin.predAbove_castPred_self {n : } (p : Fin (n + 1)) (hp : p Fin.last n) :
                                      (p.castPred hp).predAbove p = p.castPred hp
                                      theorem Fin.predAbove_rev_left {n : } (p : Fin n) (i : Fin (n + 1)) :
                                      p.rev.predAbove i = (p.predAbove i.rev).rev
                                      theorem Fin.predAbove_rev_right {n : } (p : Fin n) (i : Fin (n + 1)) :
                                      p.predAbove i.rev = (p.rev.predAbove i).rev
                                      @[simp]
                                      theorem Fin.predAbove_right_zero {n : } [NeZero n] {i : Fin n} :
                                      i.predAbove 0 = 0
                                      @[simp]
                                      theorem Fin.predAbove_zero_succ {n : } [NeZero n] {i : Fin n} :
                                      Fin.predAbove 0 i.succ = i
                                      @[simp]
                                      theorem Fin.succ_predAbove_zero {n : } [NeZero n] {j : Fin (n + 1)} (h : j 0) :
                                      (Fin.predAbove 0 j).succ = j
                                      @[simp]
                                      theorem Fin.predAbove_zero_of_ne_zero {n : } [NeZero n] {i : Fin (n + 1)} (hi : i 0) :
                                      Fin.predAbove 0 i = i.pred hi
                                      theorem Fin.predAbove_zero {n : } [NeZero n] {i : Fin (n + 1)} :
                                      Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
                                      @[simp]
                                      theorem Fin.predAbove_right_last {n : } {i : Fin (n + 1)} :
                                      i.predAbove (Fin.last (n + 1)) = Fin.last n
                                      @[simp]
                                      theorem Fin.predAbove_last_castSucc {n : } {i : Fin (n + 1)} :
                                      (Fin.last n).predAbove i.castSucc = i
                                      @[simp]
                                      theorem Fin.predAbove_last_of_ne_last {n : } {i : Fin (n + 2)} (hi : i Fin.last (n + 1)) :
                                      (Fin.last n).predAbove i = i.castPred hi
                                      theorem Fin.predAbove_last_apply {n : } {i : Fin (n + 2)} :
                                      (Fin.last n).predAbove i = if hi : i = Fin.last (n + 1) then Fin.last n else i.castPred hi
                                      @[simp]
                                      theorem Fin.succAbove_predAbove {n : } {p : Fin n} {i : Fin (n + 1)} (h : i p.castSucc) :
                                      p.castSucc.succAbove (p.predAbove i) = i

                                      Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p is the identity away from p.

                                      @[simp]
                                      theorem Fin.predAbove_succAbove {n : } (p : Fin n) (i : Fin n) :
                                      p.predAbove (p.castSucc.succAbove i) = i

                                      Sending Fin n into Fin (n + 1) with a gap at p then back to Fin n by subtracting one from anything above p is the identity.

                                      @[simp]
                                      theorem Fin.succ_predAbove_succ {n : } (a : Fin n) (b : Fin (n + 1)) :
                                      a.succ.predAbove b.succ = (a.predAbove b).succ

                                      succ commutes with predAbove.

                                      @[simp]
                                      theorem Fin.castSucc_predAbove_castSucc {n : } (a : Fin n) (b : Fin (n + 1)) :
                                      a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

                                      castSucc commutes with predAbove.

                                      theorem Fin.rev_predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :
                                      (p.predAbove i).rev = p.rev.predAbove i.rev

                                      rev commutes with predAbove.

                                      def Fin.divNat {n : } {m : } (i : Fin (m * n)) :
                                      Fin m

                                      Compute i / n, where n is a Nat and inferred the type of i.

                                      Equations
                                      • i.divNat = i / n,
                                      Instances For
                                        @[simp]
                                        theorem Fin.coe_divNat {n : } {m : } (i : Fin (m * n)) :
                                        i.divNat = i / n
                                        def Fin.modNat {n : } {m : } (i : Fin (m * n)) :
                                        Fin n

                                        Compute i % n, where n is a Nat and inferred the type of i.

                                        Equations
                                        • i.modNat = i % n,
                                        Instances For
                                          @[simp]
                                          theorem Fin.coe_modNat {n : } {m : } (i : Fin (m * n)) :
                                          i.modNat = i % n
                                          theorem Fin.modNat_rev {n : } {m : } (i : Fin (m * n)) :
                                          i.rev.modNat = i.modNat.rev

                                          recursion and induction principles #

                                          theorem Fin.liftFun_iff_succ {n : } {α : Type u_1} (r : ααProp) [IsTrans α r] {f : Fin (n + 1)α} :
                                          ((fun (x1 x2 : Fin (n + 1)) => x1 < x2) r) f f ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
                                          instance Fin.neg (n : ) :
                                          Neg (Fin n)

                                          Negation on Fin n

                                          Equations
                                          • Fin.neg n = { neg := fun (a : Fin n) => (n - a) % n, }
                                          theorem Fin.neg_def {n : } (a : Fin n) :
                                          -a = (n - a) % n,
                                          theorem Fin.coe_neg {n : } (a : Fin n) :
                                          (-a) = (n - a) % n
                                          theorem Fin.eq_zero (n : Fin 1) :
                                          n = 0
                                          Equations
                                          @[deprecated Fin.val_eq_zero]
                                          theorem Fin.coe_fin_one (a : Fin 1) :
                                          a = 0
                                          theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i 0) :
                                          i = 1
                                          @[simp]
                                          theorem Fin.coe_neg_one {n : } :
                                          (-1) = n
                                          theorem Fin.last_sub {n : } (i : Fin (n + 1)) :
                                          Fin.last n - i = i.rev
                                          theorem Fin.add_one_le_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
                                          a + 1 b
                                          theorem Fin.exists_eq_add_of_le {n : } {a : Fin n} {b : Fin n} (h : a b) :
                                          kb, b = a + k
                                          theorem Fin.exists_eq_add_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
                                          k < b, k + 1 b b = a + k + 1
                                          theorem Fin.pos_of_ne_zero {n : } {a : Fin (n + 1)} (h : a 0) :
                                          0 < a
                                          theorem Fin.sub_succ_le_sub_of_le {n : } {u : Fin (n + 2)} {v : Fin (n + 2)} (h : u < v) :
                                          v - (u + 1) < v - u
                                          @[simp]
                                          theorem Fin.coe_natCast_eq_mod (m : ) (n : ) [NeZero m] :
                                          n = n % m
                                          @[simp]
                                          theorem Fin.coe_ofNat_eq_mod (m : ) (n : ) [NeZero m] :
                                          (OfNat.ofNat n) = OfNat.ofNat n % m

                                          mul #

                                          theorem Fin.mul_one' {n : } [NeZero n] (k : Fin n) :
                                          k * 1 = k
                                          theorem Fin.one_mul' {n : } [NeZero n] (k : Fin n) :
                                          1 * k = k
                                          theorem Fin.mul_zero' {n : } [NeZero n] (k : Fin n) :
                                          k * 0 = 0
                                          theorem Fin.zero_mul' {n : } [NeZero n] (k : Fin n) :
                                          0 * k = 0