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 #

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

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

Equations
Instances For
    @[simp]
    theorem Fin.mk_eq_one {n a : } {ha : a < n + 2} :
    a, ha = 1 a = 1
    @[simp]
    theorem Fin.one_eq_mk {n a : } {ha : a < n + 2} :
    1 = a, ha a = 1
    instance Fin.instCanLiftNatValLt {n : } :
    CanLift (Fin n) val fun (x : ) => x < n
    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_last_iff_ne_last {n : } {a : Fin (n + 1)} :
      a < last n a last n
      theorem Fin.ne_zero_of_lt {n : } {a b : Fin (n + 1)} (hab : a < b) :
      b 0
      theorem Fin.ne_last_of_lt {n : } {a b : Fin (n + 1)} (hab : a < b) :
      a last n
      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
        @[simp]
        theorem Fin.equivSubtype_symm_apply {n : } (a : { i : // i < n }) :
        equivSubtype.symm a = a,
        @[simp]
        theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
        equivSubtype a = a,

        coercions and constructions #

        theorem Fin.val_eq_val {n : } (a b : Fin n) :
        a = b a = b
        theorem Fin.ne_iff_vne {n : } (a b : Fin n) :
        a b a b
        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 b : Fin n} :
        a b a b
        @[simp]
        theorem Fin.val_fin_lt {n : } {a 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 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

        The inclusion map Fin n → ℕ is an embedding.

        Equations
        Instances For

          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
          @[deprecated Fin.val_zero (since := "2025-02-24")]
          theorem Fin.val_zero' (n : ) [NeZero n] :
          0 = 0

          Alias of Fin.val_zero.

          @[simp]
          theorem Fin.mk_zero' (n : ) [NeZero n] :
          0, = 0

          Fin.mk_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.

          @[simp]
          theorem Fin.val_eq_zero_iff {n : } [NeZero n] {a : Fin n} :
          a = 0 a = 0
          theorem Fin.val_ne_zero_iff {n : } [NeZero n] {a : Fin n} :
          a 0 a 0
          @[simp]
          theorem Fin.val_pos_iff {n : } [NeZero n] {a : Fin n} :
          0 < a 0 < a
          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.last_pos' {n : } [NeZero n] :
          0 < last n
          theorem Fin.one_lt_last {n : } [NeZero n] :
          1 < last (n + 1)

          Coercions to and the fin_omega tactic. #

          theorem Fin.coe_int_sub_eq_ite {n : } (u v : Fin n) :
          ↑(u - v) = if v u then u - v else u - v + n
          theorem Fin.coe_int_sub_eq_mod {n : } (u v : Fin n) :
          ↑(u - v) = (u - v) % n
          theorem Fin.coe_int_add_eq_ite {n : } (u 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 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
            @[deprecated Fin.val_one' (since := "2025-03-10")]
            theorem Fin.val_one'' {n : } :
            1 = 1 % (n + 1)
            instance Fin.nontrivial {n : } :
            Nontrivial (Fin (n + 2))
            @[simp]
            theorem Fin.default_eq_zero (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 b : Fin n) :
            ↑(a + b) = if n a + b then a + b - n else a + b
            theorem Fin.val_add_eq_of_add_lt {n : } {a b : Fin n} (huv : a + b < n) :
            ↑(a + b) = a + b
            theorem Fin.intCast_val_sub_eq_sub_add_ite {n : } (a b : Fin n) :
            ↑(a - b) = a - b + ↑(if b a then 0 else n)
            theorem Fin.one_le_of_ne_zero {n : } [NeZero n] {k : Fin n} (hk : k 0) :
            1 k
            theorem Fin.val_sub_one_of_ne_zero {n : } [NeZero n] {i : Fin n} (hi : i 0) :
            ↑(i - 1) = i - 1
            @[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
            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
            @[simp]
            theorem Fin.natCast_eq_zero {a n : } [NeZero n] :
            a = 0 n a
            @[simp]
            theorem Fin.natCast_eq_last (n : ) :
            n = last n
            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.coe_succEmb {n : } :
              (succEmb n) = succ
              @[deprecated Fin.coe_succEmb (since := "2025-04-12")]
              theorem Fin.val_succEmb {n : } :
              (succEmb n) = succ

              Alias of Fin.coe_succEmb.

              @[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] :
              succ 0 = 1
              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] :
              succ 1 = 2

              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 b : Fin m} :
              castLE hmn a = castLE hmn b a = b
              @[simp]
              theorem Fin.castAdd_inj {n m : } {a b : Fin m} :
              castAdd n a = castAdd n b a = b
              theorem Fin.castLE_injective {n m : } (hmn : m 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.castLEEmb_apply {n m : } (h : n m) (i : Fin n) :
                (castLEEmb h) i = castLE h i
                @[simp]
                theorem Fin.coe_castLEEmb {m n : } (hmn : m n) :
                (castLEEmb hmn) = castLE hmn
                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) :
                @[simp]
                theorem Fin.castLE_comp_castSucc {n m : } (h : n + 1 m) :
                @[simp]
                theorem Fin.castLE_rfl (n : ) :
                castLE = id
                @[simp]
                theorem Fin.range_castLE {n k : } (h : n k) :
                Set.range (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 (castLE h)) :
                ((Equiv.ofInjective (castLE h) ).symm i, hi) = i
                theorem Fin.leftInverse_cast {n m : } (eq : n = m) :
                @[simp]
                theorem Fin.cast_inj {n m : } (eq : n = m) {a b : Fin n} :
                Fin.cast eq a = Fin.cast eq b a = b
                @[simp]
                theorem Fin.cast_lt_cast {n m : } (eq : n = m) {a b : Fin n} :
                Fin.cast eq a < Fin.cast eq b a < b
                @[simp]
                theorem Fin.cast_le_cast {n m : } (eq : n = m) {a b : Fin n} :
                Fin.cast eq a Fin.cast eq b a b
                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_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
                  @[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 : n = n := ) :
                  @[simp]
                  theorem finCongr_symm {n m : } (h : m = n) :
                  @[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.

                  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.

                  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.coe_castAddEmb {n : } (m : ) :
                    theorem Fin.castAddEmb_apply {n : } (m : ) (i : Fin n) :
                    (castAddEmb m) i = castAdd m 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
                      theorem Fin.castSucc_le_succ {n : } (i : Fin n) :
                      @[simp]
                      theorem Fin.castSucc_le_castSucc_iff {n : } {a b : Fin n} :
                      @[simp]
                      theorem Fin.succ_le_castSucc_iff {n : } {a b : Fin n} :
                      @[simp]
                      theorem Fin.castSucc_lt_succ_iff {n : } {a b : Fin n} :
                      theorem Fin.le_of_castSucc_lt_of_succ_lt {n : } {a 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
                      theorem Fin.succ_le_or_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
                      theorem Fin.eq_castSucc_of_ne_last {n : } {x : Fin (n + 1)} (h : x last n) :
                      ∃ (y : Fin n), y.castSucc = x
                      @[deprecated Fin.eq_castSucc_of_ne_last (since := "2025-02-06")]
                      theorem Fin.exists_castSucc_eq_of_ne_last {n : } {x : Fin (n + 1)} (h : x last n) :
                      ∃ (y : Fin n), y.castSucc = x

                      Alias of Fin.eq_castSucc_of_ne_last.

                      theorem Fin.forall_fin_succ' {n : } {P : Fin (n + 1)Prop} :
                      (∀ (i : Fin (n + 1)), P i) (∀ (i : Fin n), P i.castSucc) P (last n)
                      theorem Fin.eq_castSucc_or_eq_last {n : } (i : Fin (n + 1)) :
                      (∃ (j : Fin n), i = j.castSucc) i = last n
                      @[simp]
                      theorem Fin.castSucc_ne_last {n : } (i : Fin 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 (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.

                      @[simp]
                      theorem Fin.castSucc_pos_iff {n : } [NeZero n] {i : Fin n} :
                      0 < i.castSucc 0 < i
                      theorem Fin.castSucc_pos' {n : } [NeZero n] {i : Fin n} :
                      0 < i0 < 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) :

                      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 i : Fin n} (h : p < i) :
                      theorem Fin.succ_ne_last_iff {n : } (a : Fin (n + 1)) :
                      a.succ last (n + 1) a last n
                      theorem Fin.succ_ne_last_of_lt {n : } {p i : Fin n} (h : i < p) :
                      @[simp]
                      theorem Fin.coe_eq_castSucc {n : } {a : Fin n} :
                      a = a.castSucc
                      theorem Fin.coe_succ_lt_iff_lt {n : } {j k : Fin n} :
                      j < k j < k
                      @[simp]
                      theorem Fin.range_castSucc {n : } :
                      @[simp]
                      theorem Fin.coe_of_injective_castSucc_symm {n : } (i : Fin n.succ) (hi : i Set.range castSucc) :
                      ((Equiv.ofInjective castSucc ).symm i, hi) = i
                      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.addNatEmb_apply {n : } (m : ) (x✝ : Fin n) :
                        (addNatEmb m) x✝ = x✝.addNat 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
                          @[simp]
                          theorem Fin.natAddEmb_apply (n : ) {m : } (i : Fin m) :
                          (natAddEmb n) i = natAdd n i
                          theorem Fin.castSucc_castAdd {n m : } (i : Fin n) :
                          (castAdd m i).castSucc = castAdd (m + 1) i
                          theorem Fin.castSucc_natAdd {n m : } (i : Fin m) :
                          theorem Fin.succ_castAdd {n m : } (i : Fin n) :
                          (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) i + 1,
                          theorem Fin.succ_natAdd {n m : } (i : Fin m) :
                          (natAdd n i).succ = natAdd n i.succ

                          pred #

                          theorem Fin.pred_one' {n : } [NeZero n] (h : 1 0 := ) :
                          pred 1 h = 0
                          theorem Fin.pred_last {n : } (h : ¬last (n + 1) = 0 := ) :
                          (last (n + 1)).pred h = 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' : 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 b : Fin (n + 1)} (ha : a.castSucc 0) :
                          b a.castSucc.pred ha b < a
                          theorem Fin.pred_castSucc_lt_iff {n : } {a 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 b : Fin (n + 1)} (ha : a 0) :
                          b (a.pred ha).castSucc b < a
                          theorem Fin.castSucc_pred_lt_iff {n : } {a 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 last n) :
                          Fin n

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

                          Equations
                          Instances For
                            @[simp]
                            theorem Fin.castLT_eq_castPred {n : } (i : Fin (n + 1)) (h : i < last n) (h' : ¬i = last n := ) :
                            i.castLT h = i.castPred h'
                            @[simp]
                            theorem Fin.coe_castPred {n : } (i : Fin (n + 1)) (h : i last n) :
                            (i.castPred h) = i
                            @[simp]
                            theorem Fin.castPred_castSucc {n : } {i : Fin n} (h' : ¬i.castSucc = last n := ) :
                            @[simp]
                            theorem Fin.castSucc_castPred {n : } (i : Fin (n + 1)) (h : i last n) :
                            theorem Fin.castPred_eq_iff_eq_castSucc {n : } (i : Fin (n + 1)) (hi : i last n) (j : Fin n) :
                            i.castPred hi = j i = j.castSucc
                            @[simp]
                            theorem Fin.castPred_mk {n : } (i : ) (h₁ : i < n) (h₂ : i < n.succ := ) (h₃ : i, h₂ last n := ) :
                            i, h₂.castPred h₃ = i, h₁
                            @[simp]
                            theorem Fin.castPred_le_castPred_iff {n : } {i j : Fin (n + 1)} {hi : i last n} {hj : j last n} :
                            i.castPred hi j.castPred hj i j
                            theorem Fin.castPred_le_castPred {n : } {i j : Fin (n + 1)} (h : i j) (hj : j last n) :
                            i.castPred j.castPred hj

                            A version of the right-to-left implication of castPred_le_castPred_iff that deduces i ≠ last n from i ≤ j and j ≠ last n.

                            @[simp]
                            theorem Fin.castPred_lt_castPred_iff {n : } {i j : Fin (n + 1)} {hi : i last n} {hj : j last n} :
                            i.castPred hi < j.castPred hj i < j
                            theorem Fin.castPred_lt_castPred {n : } {i j : Fin (n + 1)} (h : i < j) (hj : j last n) :
                            i.castPred < j.castPred hj

                            A version of the right-to-left implication of castPred_lt_castPred_iff that deduces i ≠ last n from i < j.

                            theorem Fin.castPred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i last n) :
                            i.castPred hi < j i < j.castSucc
                            theorem Fin.lt_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i last n) :
                            j < i.castPred hi j.castSucc < i
                            theorem Fin.castPred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i last n) :
                            theorem Fin.le_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i last n) :
                            @[simp]
                            theorem Fin.castPred_inj {n : } {i j : Fin (n + 1)} {hi : i last n} {hj : j last n} :
                            i.castPred hi = j.castPred hj i = j
                            theorem Fin.castPred_zero' {n : } [NeZero n] (h : ¬0 = last n := ) :
                            castPred 0 h = 0
                            theorem Fin.castPred_zero {n : } (h : ¬0 = last (n + 1) := ) :
                            castPred 0 h = 0
                            @[simp]
                            theorem Fin.castPred_eq_zero {n : } [NeZero n] {i : Fin (n + 1)} (h : i last n) :
                            i.castPred h = 0 i = 0
                            @[simp]
                            theorem Fin.castPred_one {n : } [NeZero n] (h : ¬1 = last (n + 1) := ) :
                            castPred 1 h = 1
                            theorem Fin.succ_castPred_eq_castPred_succ {n : } {a : Fin (n + 1)} (ha : a last n) (ha' : a.succ 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 last n) :
                            (a.castPred ha).succ = a + 1
                            theorem Fin.castpred_succ_le_iff {n : } {a b : Fin (n + 1)} (ha : a.succ last (n + 1)) :
                            a.succ.castPred ha b a < b
                            theorem Fin.lt_castPred_succ_iff {n : } {a b : Fin (n + 1)} (ha : a.succ last (n + 1)) :
                            b < a.succ.castPred ha b a
                            theorem Fin.lt_castPred_succ {n : } {a : Fin (n + 1)} (ha : a.succ last (n + 1)) :
                            a < a.succ.castPred ha
                            theorem Fin.succ_castPred_le_iff {n : } {a b : Fin (n + 1)} (ha : a last n) :
                            (a.castPred ha).succ b a < b
                            theorem Fin.lt_succ_castPred_iff {n : } {a b : Fin (n + 1)} (ha : a last n) :
                            b < (a.castPred ha).succ b a
                            theorem Fin.lt_succ_castPred {n : } {a : Fin (n + 1)} (ha : a last n) :
                            a < (a.castPred ha).succ
                            theorem Fin.castPred_le_pred_iff {n : } {a b : Fin (n + 1)} (ha : a last n) (hb : b 0) :
                            a.castPred ha b.pred hb a < b
                            theorem Fin.pred_lt_castPred_iff {n : } {a b : Fin (n + 1)} (ha : a 0) (hb : b 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 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
                            Instances For
                              theorem Fin.succAbove_of_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) :

                              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) :
                              theorem Fin.succAbove_of_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) (h : p i.castSucc) :

                              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) :
                              theorem Fin.succAbove_succ_of_lt {n : } (p i : Fin n) (h : p < i) :
                              theorem Fin.succAbove_succ_of_le {n : } (p i : Fin n) (h : i p) :
                              @[simp]
                              theorem Fin.succAbove_succ_self {n : } (j : Fin n) :
                              theorem Fin.succAbove_castSucc_of_lt {n : } (p i : Fin n) (h : i < p) :
                              theorem Fin.succAbove_castSucc_of_le {n : } (p i : Fin n) (h : p i) :
                              @[simp]
                              theorem Fin.succAbove_pred_of_lt {n : } (p i : Fin (n + 1)) (h : p < i) (hi : i 0 := ) :
                              p.succAbove (i.pred hi) = i
                              theorem Fin.succAbove_pred_of_le {n : } (p 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 i : Fin (n + 1)) (h : i < p) (hi : i last n := ) :
                              p.succAbove (i.castPred hi) = i
                              theorem Fin.succAbove_castPred_of_le {n : } (p i : Fin (n + 1)) (h : p i) (hi : i last n) :
                              p.succAbove (i.castPred hi) = (i.castPred hi).succ
                              theorem Fin.succAbove_castPred_self {n : } (p : Fin (n + 1)) (h : p last n) :
                              @[simp]
                              theorem Fin.succAbove_ne {n : } (p : Fin (n + 1)) (i : Fin n) :

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

                              @[simp]
                              theorem Fin.ne_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :

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

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

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

                              def Fin.succAboveEmb {n : } (p : Fin (n + 1)) :
                              Fin n Fin (n + 1)

                              Fin.succAbove p as an Embedding.

                              Equations
                              Instances For
                                @[simp]
                                theorem Fin.succAboveEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                                @[simp]
                                theorem Fin.coe_succAboveEmb {n : } (p : Fin (n + 1)) :
                                @[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) :
                                @[simp]

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

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

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

                                theorem Fin.succAbove_lt_iff_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) :

                                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) :

                                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' : y.succAbove x 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' : y.succAbove x 0 := ) :
                                (y.succAbove x).pred h' = x
                                theorem Fin.exists_succAbove_eq {n : } {x y : Fin (n + 1)} (h : x y) :
                                ∃ (z : Fin n), y.succAbove z = x
                                @[simp]
                                theorem Fin.exists_succAbove_eq_iff {n : } {x y : Fin (n + 1)} :
                                (∃ (z : Fin n), x.succAbove z = y) y x
                                @[simp]
                                theorem Fin.range_succAbove {n : } (p : Fin (n + 1)) :

                                The range of p.succAbove is everything except p.

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

                                succAbove is injective at the pivot

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

                                succ commutes with succAbove.

                                @[simp]

                                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 : 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 last (n + 1)) (hb : b last n) (hk : a.succAbove b last (n + 1) := ) :

                                castPred commutes with succAbove.

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

                                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) :
                                @[simp]
                                theorem Fin.one_succAbove_one {n : } :
                                succAbove 1 1 = 2
                                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
                                Instances For
                                  theorem Fin.predAbove_of_le_castSucc {n : } (p : Fin n) (i : Fin (n + 1)) (h : i p.castSucc) (hi : i last n := ) :
                                  theorem Fin.predAbove_of_lt_succ {n : } (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : i last n := ) :
                                  theorem Fin.predAbove_of_castSucc_lt {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : 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 : i 0 := ) :
                                  p.predAbove i = i.pred hi
                                  theorem Fin.predAbove_succ_of_lt {n : } (p i : Fin n) (h : i < p) (hi : i.succ last n := ) :
                                  theorem Fin.predAbove_succ_of_le {n : } (p i : Fin n) (h : p i) :
                                  @[simp]
                                  theorem Fin.predAbove_succ_self {n : } (p : Fin n) :
                                  theorem Fin.predAbove_castSucc_of_lt {n : } (p i : Fin n) (h : p < i) (hi : i.castSucc 0 := ) :
                                  theorem Fin.predAbove_castSucc_of_le {n : } (p i : Fin n) (h : i p) :
                                  @[simp]
                                  theorem Fin.predAbove_castSucc_self {n : } (p : Fin n) :
                                  theorem Fin.predAbove_pred_of_lt {n : } (p i : Fin (n + 1)) (h : i < p) (hp : p 0 := ) (hi : i last n := ) :
                                  (p.pred hp).predAbove i = i.castPred hi
                                  theorem Fin.predAbove_pred_of_le {n : } (p i : Fin (n + 1)) (h : p i) (hp : p 0) (hi : 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 i : Fin (n + 1)) (h : p < i) (hp : p last n := ) (hi : i 0 := ) :
                                  (p.castPred hp).predAbove i = i.pred hi
                                  theorem Fin.predAbove_castPred_of_le {n : } (p i : Fin (n + 1)) (h : i p) (hp : p last n) (hi : i last n := ) :
                                  theorem Fin.predAbove_castPred_self {n : } (p : Fin (n + 1)) (hp : p last n) :
                                  @[simp]
                                  theorem Fin.predAbove_right_zero {n : } [NeZero n] {i : Fin n} :
                                  i.predAbove 0 = 0
                                  theorem Fin.predAbove_zero_succ {n : } [NeZero n] {i : Fin n} :
                                  @[simp]
                                  theorem Fin.succ_predAbove_zero {n : } [NeZero n] {j : Fin (n + 1)} (h : j 0) :
                                  (predAbove 0 j).succ = j
                                  @[simp]
                                  theorem Fin.predAbove_zero_of_ne_zero {n : } [NeZero n] {i : Fin (n + 1)} (hi : i 0) :
                                  predAbove 0 i = i.pred hi
                                  theorem Fin.predAbove_zero {n : } [NeZero n] {i : Fin (n + 1)} :
                                  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 (last (n + 1)) = last n
                                  theorem Fin.predAbove_last_castSucc {n : } {i : Fin (n + 1)} :
                                  @[simp]
                                  theorem Fin.predAbove_last_of_ne_last {n : } {i : Fin (n + 2)} (hi : i last (n + 1)) :
                                  theorem Fin.predAbove_last_apply {n : } {i : Fin (n + 2)} :
                                  (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi
                                  @[simp]
                                  theorem Fin.succAbove_predAbove {n : } {p : Fin n} {i : Fin (n + 1)} (h : i p.castSucc) :

                                  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.succ_succAbove_predAbove {n : } {p : Fin n} {i : Fin (n + 1)} (h : i p.succ) :

                                  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.succ is the identity away from p.succ.

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

                                  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)) :

                                  succ commutes with predAbove.

                                  @[simp]

                                  castSucc 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
                                  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
                                    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)) :

                                      recursion and induction principles #

                                      theorem Fin.liftFun_iff_succ {n : } {α : Type u_1} (r : ααProp) [IsTrans α r] {f : Fin (n + 1)α} :
                                      Relator.LiftFun (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
                                      theorem Fin.eq_one_of_ne_zero (i : Fin 2) (hi : i 0) :
                                      i = 1
                                      @[deprecated Fin.eq_one_of_ne_zero (since := "2025-04-27")]
                                      theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i 0) :
                                      i = 1

                                      Alias of Fin.eq_one_of_ne_zero.

                                      @[simp]
                                      theorem Fin.coe_neg_one {n : } :
                                      (-1) = n
                                      theorem Fin.last_sub {n : } (i : Fin (n + 1)) :
                                      last n - i = i.rev
                                      theorem Fin.add_one_le_of_lt {n : } {a b : Fin (n + 1)} (h : a < b) :
                                      a + 1 b
                                      theorem Fin.exists_eq_add_of_le {n : } {a b : Fin n} (h : a b) :
                                      kb, b = a + k
                                      theorem Fin.exists_eq_add_of_lt {n : } {a 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 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

                                      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