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

        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
          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
            instance Fin.instZeroOfNeZeroNat {n : } [NeZero n] :
            Zero (Fin n)
            Equations
            instance Fin.instOneOfNeZeroNat {n : } [NeZero n] :
            One (Fin n)
            Equations
            @[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.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)

              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
              theorem Fin.zero_add {n : } [NeZero n] (k : Fin n) :
              0 + k = k
              instance Fin.instOfNatOfNeZeroNat {n : } {a : } [NeZero n] :
              OfNat (Fin n) a
              Equations
              • Fin.instOfNatOfNeZeroNat = { ofNat := Fin.ofNat' a }
              instance Fin.inhabited (n : ) [NeZero n] :
              Equations
              instance Fin.inhabitedFinOneAdd (n : ) :
              Inhabited (Fin (1 + n))
              Equations
              @[simp]
              theorem Fin.default_eq_zero (n : ) [NeZero n] :
              default = 0
              @[simp]
              theorem Fin.ofNat'_zero {n : } {h : 0 < n} [NeZero n] :
              @[simp]
              theorem Fin.ofNat'_one {n : } {h : 0 < n} [NeZero n] :
              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
              @[simp]
              theorem Fin.ofNat''_eq_cast (n : ) [NeZero n] (a : ) :
              Fin.ofNat'' 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
              @[simp]
              theorem Fin.one_eq_zero_iff {n : } [NeZero n] :
              1 = 0 n = 1
              @[simp]
              theorem Fin.zero_eq_one_iff {n : } [NeZero n] :
              0 = 1 n = 1

              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.cast_refl {n : } (h : n = n) :
                Fin.cast h = id
                @[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_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_apply {n : } {m : } (eq : n = m) (i : Fin n) :
                  (finCongr eq) i = Fin.cast eq i
                  @[simp]
                  theorem finCongr_symm_apply {n : } {m : } (eq : n = m) (i : Fin m) :
                  (finCongr eq).symm i = Fin.cast 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
                        @[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
                                        @[simp]
                                        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_ofNat_eq_mod (m : ) (n : ) [NeZero m] :
                                        n = 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
                                        instance Fin.toExpr (n : ) :
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        • Fin.toExpr 0 = { toExpr := finZeroElim, toTypeExpr := q(Fin 0) }