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 : } :
      ∀ (a : Fin n), 0 < 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
      Instances For
        @[simp]
        theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
        equivSubtype a = a,
        @[simp]
        theorem Fin.equivSubtype_symm_apply {n : } (a : { i : // i < n }) :

        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α} :
        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'α} :
        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} :
        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.lt_or_ge {n : } (a b : Fin n) :
        a < b b a

        Fin.lt_or_ge is an alias of Fin.lt_or_le. It is preferred since it follows the mathlib naming convention.

        theorem Fin.le_or_gt {n : } (a b : Fin n) :
        a b b < a

        Fin.le_or_gt is an alias of Fin.le_or_lt. It is preferred since it follows the mathlib naming convention.

        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

        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.

        @[deprecated Fin.zero_le (since := "2025-05-13")]
        theorem Fin.zero_le' {n : } [NeZero n] (a : Fin n) :
        0 a
        @[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 #

          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 : } [NeZero n] :
          Nontrivial (Fin (n + 1))
          theorem Fin.exists_ne_and_ne_of_two_lt {n : } (i j : Fin n) (h : 2 < n) :
          ∃ (k : Fin n), k i k j

          If working with more than two elements, we can always pick a third distinct from two existing elements.

          @[simp]
          theorem Fin.default_eq_zero (n : ) [NeZero 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
          @[deprecated Fin.ofNat_eq_cast (since := "2025-05-30")]
          theorem Fin.ofNat'_eq_cast (n : ) [NeZero n] (a : ) :
          Fin.ofNat n a = a

          Alias of Fin.ofNat_eq_cast.

          @[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.natCast_eq_mk {m n : } (h : m < n) :
          have this := ; m = m, h
          theorem Fin.one_eq_mk_of_lt {n : } (h : 1 < n) :
          have this := ; 1 = 1, h
          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.castLE_natCast {m n : } [NeZero m] (h : m n) (a : ) :
          castLE h a = ↑(a % m)

          succ and casts into larger Fin types #

          @[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) :
          @[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_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
            @[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.

            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.

            @[deprecated Fin.castSucc_eq_zero_iff (since := "2025-05-13")]
            theorem Fin.castSucc_eq_zero_iff' {n : } [NeZero n] (a : Fin n) :
            a.castSucc = 0 a = 0
            @[deprecated Fin.castSucc_ne_zero_iff (since := "2025-05-13")]
            theorem Fin.castSucc_ne_zero_iff' {n : } [NeZero n] (a : Fin n) :
            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.castSucc_castAdd {n m : } (i : Fin n) :
            (castAdd m i).castSucc = castAdd (m + 1) i
            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) :
            (a.pred ha).castSucc = a.castSucc.pred
            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
              @[simp]
              theorem Fin.castPred_zero {n : } [NeZero n] :
              castPred 0 = 0
              @[deprecated Fin.castPred_zero (since := "2025-05-11")]
              theorem Fin.castPred_zero' {n : } [NeZero n] :
              castPred 0 = 0

              Alias of Fin.castPred_zero.

              @[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] :
              castPred 1 = 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) :
                p.succAbove (i.pred ) = 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) :
                p.succAbove (i.castPred ) = 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.

                @[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) :
                  p.predAbove i = i.castPred
                  theorem Fin.predAbove_of_lt_succ {n : } (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) :
                  p.predAbove i = i.castPred
                  theorem Fin.predAbove_of_castSucc_lt {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) :
                  p.predAbove i = i.pred
                  theorem Fin.predAbove_of_succ_le {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.succ i) :
                  p.predAbove i = i.pred
                  theorem Fin.predAbove_succ_of_lt {n : } (p i : Fin n) (h : i < p) :
                  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) :
                  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) :
                  (p.pred ).predAbove i = i.castPred
                  theorem Fin.predAbove_pred_of_le {n : } (p i : Fin (n + 1)) (h : p i) (hp : p 0) :
                  (p.pred hp).predAbove i = i.pred
                  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) :
                  (p.castPred ).predAbove i = i.pred
                  theorem Fin.predAbove_castPred_of_le {n : } (p i : Fin (n + 1)) (h : i p) (hp : p last n) :
                  (p.castPred hp).predAbove i = i.castPred
                  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.predAbove_zero_of_ne_zero {n : } [NeZero n] {i : Fin (n + 1)} (hi : i 0) :
                  predAbove 0 i = i.pred hi
                  theorem Fin.succ_predAbove_zero {n : } [NeZero n] {j : Fin (n + 1)} (h : j 0) :
                  (predAbove 0 j).succ = j
                  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.

                  theorem Fin.predAbove_predAbove_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
                  theorem Fin.succAbove_succAbove_predAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
                  theorem Fin.succAbove_succAbove_succAbove_predAbove {n : } (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n) :

                  Given i : Fin (n + 2) and j : Fin (n + 1), there are two ways to represent the order embedding Fin n → Fin (n + 2) leaving holes at i and i.succAbove j.

                  One is i.succAbove ∘ j.succAbove. It corresponds to embedding Fin n to Fin (n + 1) leaving a hole at j, then embedding the result to Fin (n + 2) leaving a hole at i. The other one is (i.succAbove j).succAbove ∘ (j.predAbove i).succAbove. It corresponds to swapping the roles of i and j.

                  This lemma says that these two ways are equal. It is used in Fin.removeNth_removeNth_eq_swap to show that two ways of removing 2 elements from a sequence give the same answer.

                  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)
                      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
                      @[simp]
                      theorem Fin.coe_ofNat_eq_mod (m n : ) [NeZero 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