Documentation

Init.Data.Fin.Lemmas

@[simp]
theorem Fin.ofNat_zero (n : Nat) [NeZero n] :
Fin.ofNat n 0 = 0
@[reducible, inline, deprecated Fin.ofNat_zero (since := "2025-05-28")]
abbrev Fin.ofNat'_zero (n : Nat) [NeZero n] :
Fin.ofNat n 0 = 0
Equations
    Instances For
      theorem Fin.mod_def {n : Nat} (a m : Fin n) :
      a % m = a % m,
      theorem Fin.mul_def {n : Nat} (a b : Fin n) :
      a * b = a * b % n,
      theorem Fin.sub_def {n : Nat} (a b : Fin n) :
      a - b = (n - b + a) % n,
      theorem Fin.pos' {n : Nat} [Nonempty (Fin n)] :
      0 < n
      @[simp]
      theorem Fin.is_lt {n : Nat} (a : Fin n) :
      a < n

      coercions and constructions #

      @[simp]
      theorem Fin.eta {n : Nat} (a : Fin n) (h : a < n) :
      a, h = a
      theorem Fin.ext {n : Nat} {a b : Fin n} (h : a = b) :
      a = b
      theorem Fin.ext_iff {n : Nat} {a b : Fin n} :
      a = b a = b
      theorem Fin.val_ne_iff {n : Nat} {a b : Fin n} :
      a b a b
      theorem Fin.forall_iff {n : Nat} {p : Fin nProp} :
      (∀ (i : Fin n), p i) ∀ (i : Nat) (h : i < n), p i, h
      theorem Fin.mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
      a, ha = b, hb a = b

      Restatement of Fin.mk.injEq as an iff.

      theorem Fin.val_mk {m n : Nat} (h : m < n) :
      m, h = m
      theorem Fin.eq_mk_iff_val_eq {n : Nat} {a : Fin n} {k : Nat} {hk : k < n} :
      a = k, hk a = k
      theorem Fin.mk_val {n : Nat} (i : Fin n) :
      i, = i
      @[simp]
      theorem Fin.mk_eq_zero {n a : Nat} {ha : a < n} [NeZero n] :
      a, ha = 0 a = 0
      @[simp]
      theorem Fin.zero_eq_mk {n a : Nat} {ha : a < n} [NeZero n] :
      0 = a, ha a = 0
      @[simp]
      theorem Fin.val_ofNat (n : Nat) [NeZero n] (a : Nat) :
      (Fin.ofNat n a) = a % n
      @[reducible, inline, deprecated Fin.val_ofNat (since := "2025-05-28")]
      abbrev Fin.val_ofNat' (n : Nat) [NeZero n] (a : Nat) :
      (Fin.ofNat n a) = a % n
      Equations
        Instances For
          @[simp]
          theorem Fin.ofNat_self {n : Nat} [NeZero n] :
          Fin.ofNat n n = 0
          @[reducible, inline, deprecated Fin.ofNat_self (since := "2025-05-28")]
          abbrev Fin.ofNat'_self {n : Nat} [NeZero n] :
          Fin.ofNat n n = 0
          Equations
            Instances For
              @[simp]
              theorem Fin.ofNat_val_eq_self {n : Nat} [NeZero n] (x : Fin n) :
              Fin.ofNat n x = x
              @[reducible, inline, deprecated Fin.ofNat_val_eq_self (since := "2025-05-28")]
              abbrev Fin.ofNat'_val_eq_self {n : Nat} [NeZero n] (x : Fin n) :
              Fin.ofNat n x = x
              Equations
                Instances For
                  @[simp]
                  theorem Fin.mod_val {n : Nat} (a b : Fin n) :
                  ↑(a % b) = a % b
                  @[simp]
                  theorem Fin.div_val {n : Nat} (a b : Fin n) :
                  ↑(a / b) = a / b
                  @[simp]
                  theorem Fin.modn_val {n : Nat} (a : Fin n) (b : Nat) :
                  (a.modn b) = a % b
                  @[simp]
                  theorem Fin.val_eq_zero (a : Fin 1) :
                  a = 0
                  theorem Fin.ite_val {n : Nat} {c : Prop} [Decidable c] {x : cFin n} (y : ¬cFin n) :
                  (if h : c then x h else y h) = if h : c then (x h) else (y h)
                  theorem Fin.dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
                  ↑(if c then x else y) = if c then x else y
                  Equations
                    def Fin.intCast {n : Nat} [NeZero n] (a : Int) :
                    Fin n
                    Equations
                      Instances For
                        Equations
                          theorem Fin.intCast_def {n : Nat} [NeZero n] (x : Int) :

                          order #

                          theorem Fin.le_def {n : Nat} {a b : Fin n} :
                          a b a b
                          theorem Fin.lt_def {n : Nat} {a b : Fin n} :
                          a < b a < b
                          theorem Fin.lt_iff_val_lt_val {n : Nat} {a b : Fin n} :
                          a < b a < b
                          @[simp]
                          theorem Fin.not_le {n : Nat} {a b : Fin n} :
                          ¬a b b < a
                          @[simp]
                          theorem Fin.not_lt {n : Nat} {a b : Fin n} :
                          ¬a < b b a
                          @[simp]
                          theorem Fin.le_refl {n : Nat} (a : Fin n) :
                          a a
                          @[simp]
                          theorem Fin.lt_irrefl {n : Nat} (a : Fin n) :
                          ¬a < a
                          theorem Fin.le_trans {n : Nat} {a b c : Fin n} :
                          a bb ca c
                          theorem Fin.lt_trans {n : Nat} {a b c : Fin n} :
                          a < bb < ca < c
                          theorem Fin.le_total {n : Nat} (a b : Fin n) :
                          a b b a
                          theorem Fin.lt_asymm {n : Nat} {a b : Fin n} (h : a < b) :
                          ¬b < a
                          theorem Fin.ne_of_lt {n : Nat} {a b : Fin n} (h : a < b) :
                          a b
                          theorem Fin.ne_of_gt {n : Nat} {a b : Fin n} (h : a < b) :
                          b a
                          theorem Fin.le_of_lt {n : Nat} {a b : Fin n} (h : a < b) :
                          a b
                          theorem Fin.lt_of_le_of_lt {n : Nat} {a b c : Fin n} :
                          a bb < ca < c
                          theorem Fin.lt_of_lt_of_le {n : Nat} {a b c : Fin n} :
                          a < bb ca < c
                          theorem Fin.le_rfl {n : Nat} {a : Fin n} :
                          a a
                          theorem Fin.lt_iff_le_and_ne {n : Nat} {a b : Fin n} :
                          a < b a b a b
                          theorem Fin.lt_or_lt_of_ne {n : Nat} {a b : Fin n} (h : a b) :
                          a < b b < a
                          theorem Fin.lt_or_le {n : Nat} (a b : Fin n) :
                          a < b b a
                          theorem Fin.le_or_lt {n : Nat} (a b : Fin n) :
                          a b b < a
                          theorem Fin.le_of_eq {n : Nat} {a b : Fin n} (hab : a = b) :
                          a b
                          theorem Fin.ge_of_eq {n : Nat} {a b : Fin n} (hab : a = b) :
                          b a
                          theorem Fin.eq_or_lt_of_le {n : Nat} {a b : Fin n} :
                          a ba = b a < b
                          theorem Fin.lt_or_eq_of_le {n : Nat} {a b : Fin n} :
                          a ba < b a = b
                          theorem Fin.is_le {n : Nat} (i : Fin (n + 1)) :
                          i n
                          @[simp]
                          theorem Fin.is_le' {n : Nat} {a : Fin n} :
                          a n
                          theorem Fin.mk_lt_of_lt_val {n : Nat} {b : Fin n} {a : Nat} (h : a < b) :
                          a, < b
                          theorem Fin.mk_le_of_le_val {n : Nat} {b : Fin n} {a : Nat} (h : a b) :
                          a, b
                          @[simp]
                          theorem Fin.mk_le_mk {n x y : Nat} {hx : x < n} {hy : y < n} :
                          x, hx y, hy x y
                          @[simp]
                          theorem Fin.mk_lt_mk {n x y : Nat} {hx : x < n} {hy : y < n} :
                          x, hx < y, hy x < y
                          @[simp]
                          theorem Fin.val_zero (n : Nat) [NeZero n] :
                          0 = 0
                          @[simp]
                          theorem Fin.mk_zero {n : Nat} :
                          0, = 0
                          @[simp]
                          theorem Fin.zero_le {n : Nat} [NeZero n] (a : Fin n) :
                          0 a
                          theorem Fin.zero_lt_one {n : Nat} :
                          0 < 1
                          @[simp]
                          theorem Fin.not_lt_zero {n : Nat} [NeZero n] (a : Fin n) :
                          ¬a < 0
                          theorem Fin.pos_iff_ne_zero {n : Nat} [NeZero n] {a : Fin n} :
                          0 < a a 0
                          theorem Fin.eq_zero_or_eq_succ {n : Nat} (i : Fin (n + 1)) :
                          i = 0 (j : Fin n), i = j.succ
                          theorem Fin.eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i 0) :
                          (j : Fin n), i = j.succ
                          theorem Fin.le_antisymm_iff {n : Nat} {x y : Fin n} :
                          x = y x y y x
                          theorem Fin.le_antisymm {n : Nat} {x y : Fin n} (h1 : x y) (h2 : y x) :
                          x = y
                          @[simp]
                          theorem Fin.val_rev {n : Nat} (i : Fin n) :
                          i.rev = n - (i + 1)
                          @[simp]
                          theorem Fin.rev_rev {n : Nat} (i : Fin n) :
                          i.rev.rev = i
                          @[simp]
                          theorem Fin.rev_le_rev {n : Nat} {i j : Fin n} :
                          i.rev j.rev j i
                          @[simp]
                          theorem Fin.rev_inj {n : Nat} {i j : Fin n} :
                          i.rev = j.rev i = j
                          theorem Fin.rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
                          i.rev = a,
                          @[simp]
                          theorem Fin.rev_lt_rev {n : Nat} {i j : Fin n} :
                          i.rev < j.rev j < i

                          last #

                          @[simp]
                          theorem Fin.val_last (n : Nat) :
                          (last n) = n
                          @[simp]
                          theorem Fin.last_zero :
                          last 0 = 0
                          @[simp]
                          theorem Fin.zero_eq_last_iff {n : Nat} :
                          0 = last n n = 0
                          @[simp]
                          theorem Fin.last_eq_zero_iff {n : Nat} :
                          last n = 0 n = 0
                          theorem Fin.le_last {n : Nat} (i : Fin (n + 1)) :
                          i last n
                          theorem Fin.last_pos {n : Nat} :
                          0 < last (n + 1)
                          theorem Fin.eq_last_of_not_lt {n : Nat} {i : Fin (n + 1)} (h : ¬i < n) :
                          i = last n
                          theorem Fin.val_lt_last {n : Nat} {i : Fin (n + 1)} :
                          i last ni < n
                          @[simp]
                          theorem Fin.rev_last (n : Nat) :
                          (last n).rev = 0
                          @[simp]
                          theorem Fin.rev_zero (n : Nat) :
                          rev 0 = last n

                          addition, numerals, and coercion from Nat #

                          @[simp]
                          theorem Fin.val_one (n : Nat) :
                          1 = 1
                          @[simp]
                          theorem Fin.mk_one {n : Nat} :
                          1, = 1
                          theorem Fin.fin_one_eq_zero (a : Fin 1) :
                          a = 0
                          @[simp]
                          theorem Fin.zero_eq_one_iff {n : Nat} [NeZero n] :
                          0 = 1 n = 1
                          @[simp]
                          theorem Fin.one_eq_zero_iff {n : Nat} [NeZero n] :
                          1 = 0 n = 1
                          theorem Fin.add_def {n : Nat} (a b : Fin n) :
                          a + b = (a + b) % n,
                          theorem Fin.val_add {n : Nat} (a b : Fin n) :
                          ↑(a + b) = (a + b) % n
                          @[simp]
                          theorem Fin.zero_add {n : Nat} [NeZero n] (k : Fin n) :
                          0 + k = k
                          @[simp]
                          theorem Fin.add_zero {n : Nat} [NeZero n] (k : Fin n) :
                          k + 0 = k
                          theorem Fin.val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last n) :
                          ↑(i + 1) = i + 1
                          @[simp]
                          theorem Fin.last_add_one (n : Nat) :
                          last n + 1 = 0
                          theorem Fin.val_add_one {n : Nat} (i : Fin (n + 1)) :
                          ↑(i + 1) = if i = last n then 0 else i + 1
                          @[simp]
                          theorem Fin.val_two {n : Nat} :
                          2 = 2
                          theorem Fin.add_one_pos {n : Nat} (i : Fin (n + 1)) (h : i < last n) :
                          0 < i + 1
                          theorem Fin.one_pos {n : Nat} :
                          0 < 1
                          theorem Fin.zero_ne_one {n : Nat} :
                          0 1

                          succ and casts into larger Fin types #

                          @[simp]
                          theorem Fin.val_succ {n : Nat} (j : Fin n) :
                          j.succ = j + 1
                          @[simp]
                          theorem Fin.succ_pos {n : Nat} (a : Fin n) :
                          0 < a.succ
                          @[simp]
                          theorem Fin.succ_le_succ_iff {n : Nat} {a b : Fin n} :
                          a.succ b.succ a b
                          @[simp]
                          theorem Fin.succ_lt_succ_iff {n : Nat} {a b : Fin n} :
                          a.succ < b.succ a < b
                          @[simp]
                          theorem Fin.succ_inj {n : Nat} {a b : Fin n} :
                          a.succ = b.succ a = b
                          theorem Fin.succ_ne_zero {n : Nat} (k : Fin n) :
                          k.succ 0
                          @[simp]
                          theorem Fin.succ_zero_eq_one {n : Nat} :
                          succ 0 = 1
                          @[simp]
                          theorem Fin.succ_one_eq_two {n : Nat} :
                          succ 1 = 2

                          Version of succ_one_eq_two to be used by dsimp

                          @[simp]
                          theorem Fin.succ_mk (n i : Nat) (h : i < n) :
                          i, h.succ = i + 1,
                          theorem Fin.mk_succ_pos {n : Nat} (i : Nat) (h : i < n) :
                          0 < i.succ,
                          theorem Fin.one_lt_succ_succ {n : Nat} (a : Fin n) :
                          1 < a.succ.succ
                          @[simp]
                          theorem Fin.add_one_lt_iff {n : Nat} {k : Fin (n + 2)} :
                          k + 1 < k k = last (n + 1)
                          @[simp]
                          theorem Fin.add_one_le_iff {n : Nat} {k : Fin (n + 1)} :
                          k + 1 k k = last n
                          @[simp]
                          theorem Fin.last_le_iff {n : Nat} {k : Fin (n + 1)} :
                          last n k k = last n
                          @[simp]
                          theorem Fin.lt_add_one_iff {n : Nat} {k : Fin (n + 1)} :
                          k < k + 1 k < last n
                          @[simp]
                          theorem Fin.le_zero_iff {n : Nat} {k : Fin (n + 1)} :
                          k 0 k = 0
                          theorem Fin.succ_succ_ne_one {n : Nat} (a : Fin n) :
                          @[simp]
                          theorem Fin.coe_castLT {m n : Nat} (i : Fin m) (h : i < n) :
                          (i.castLT h) = i
                          @[simp]
                          theorem Fin.castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) :
                          i, hn.castLT hm = i, hm
                          @[simp]
                          theorem Fin.coe_castLE {n m : Nat} (h : n m) (i : Fin n) :
                          (castLE h i) = i
                          @[simp]
                          theorem Fin.castLE_mk (i n m : Nat) (hn : i < n) (h : n m) :
                          castLE h i, hn = i,
                          @[simp]
                          theorem Fin.castLE_zero {n m : Nat} (h : n.succ m.succ) :
                          castLE h 0 = 0
                          @[simp]
                          theorem Fin.castLE_succ {m n : Nat} (h : m + 1 n + 1) (i : Fin m) :
                          castLE h i.succ = (castLE i).succ
                          @[simp]
                          theorem Fin.castLE_castLE {k m n : Nat} (km : k m) (mn : m n) (i : Fin k) :
                          castLE mn (castLE km i) = castLE i
                          @[simp]
                          theorem Fin.castLE_comp_castLE {k m n : Nat} (km : k m) (mn : m n) :
                          @[simp]
                          theorem Fin.coe_cast {n m : Nat} (h : n = m) (i : Fin n) :
                          (Fin.cast h i) = i
                          @[simp]
                          theorem Fin.cast_castLE {k m n : Nat} (km : k m) (mn : m = n) (i : Fin k) :
                          Fin.cast mn (castLE km i) = castLE i
                          @[simp]
                          theorem Fin.cast_castLT {k m n : Nat} (i : Fin k) (h : i < m) (mn : m = n) :
                          Fin.cast mn (i.castLT h) = i.castLT
                          @[simp]
                          theorem Fin.cast_zero {n m : Nat} [NeZero n] [NeZero m] (h : n = m) :
                          Fin.cast h 0 = 0
                          @[simp]
                          theorem Fin.cast_last {n n' : Nat} {h : n + 1 = n' + 1} :
                          Fin.cast h (last n) = last n'
                          @[simp]
                          theorem Fin.cast_mk {n m : Nat} (h : n = m) (i : Nat) (hn : i < n) :
                          Fin.cast h i, hn = i,
                          @[simp]
                          theorem Fin.cast_refl (n : Nat) (h : n = n) :
                          @[simp]
                          theorem Fin.cast_trans {n m k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
                          Fin.cast h' (Fin.cast h i) = Fin.cast i
                          theorem Fin.castLE_of_eq {m n : Nat} (h : m = n) {h' : m n} :
                          @[simp]
                          theorem Fin.coe_castAdd {n : Nat} (m : Nat) (i : Fin n) :
                          (castAdd m i) = i
                          @[simp]
                          theorem Fin.castAdd_zero {n : Nat} :
                          theorem Fin.castAdd_lt {m : Nat} (n : Nat) (i : Fin m) :
                          (castAdd n i) < m
                          @[simp]
                          theorem Fin.castAdd_mk {n : Nat} (m i : Nat) (h : i < n) :
                          castAdd m i, h = i,
                          @[simp]
                          theorem Fin.castAdd_castLT {n : Nat} (m : Nat) (i : Fin (n + m)) (hi : i < n) :
                          castAdd m (i.castLT hi) = i
                          @[simp]
                          theorem Fin.castLT_castAdd {n : Nat} (m : Nat) (i : Fin n) :
                          (castAdd m i).castLT = i
                          theorem Fin.castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
                          castAdd m (Fin.cast h i) = Fin.cast (castAdd m i)

                          For rewriting in the reverse direction, see Fin.cast_castAdd_left.

                          theorem Fin.cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
                          Fin.cast h (castAdd m i) = castAdd m (Fin.cast i)
                          @[simp]
                          theorem Fin.cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
                          Fin.cast h (castAdd m' i) = castAdd m i
                          theorem Fin.castAdd_castAdd {m n p : Nat} (i : Fin m) :
                          castAdd p (castAdd n i) = Fin.cast (castAdd (n + p) i)
                          @[simp]
                          theorem Fin.cast_succ_eq {n n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :

                          The cast of the successor is the successor of the cast. See Fin.succ_cast_eq for rewriting in the reverse direction.

                          theorem Fin.succ_cast_eq {n n' : Nat} (i : Fin n) (h : n = n') :
                          @[simp]
                          theorem Fin.coe_castSucc {n : Nat} (i : Fin n) :
                          i.castSucc = i
                          @[simp]
                          theorem Fin.castSucc_mk (n i : Nat) (h : i < n) :
                          @[simp]
                          theorem Fin.cast_castSucc {n n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
                          theorem Fin.castSucc_lt_succ {n : Nat} (i : Fin n) :
                          theorem Fin.le_castSucc_iff {n : Nat} {i : Fin (n + 1)} {j : Fin n} :
                          theorem Fin.castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
                          @[simp]
                          theorem Fin.succ_last (n : Nat) :
                          @[simp]
                          theorem Fin.succ_eq_last_succ {n : Nat} {i : Fin n.succ} :
                          i.succ = last (n + 1) i = last n
                          @[simp]
                          theorem Fin.castSucc_castLT {n : Nat} (i : Fin (n + 1)) (h : i < n) :
                          (i.castLT h).castSucc = i
                          @[simp]
                          theorem Fin.castLT_castSucc {n : Nat} (a : Fin n) (h : a < n) :
                          @[simp]
                          theorem Fin.castSucc_lt_castSucc_iff {n : Nat} {a b : Fin n} :
                          theorem Fin.castSucc_inj {n : Nat} {a b : Fin n} :
                          theorem Fin.castSucc_lt_last {n : Nat} (a : Fin n) :
                          @[simp]
                          theorem Fin.castSucc_zero {n : Nat} [NeZero n] :
                          @[simp]
                          theorem Fin.castSucc_one {n : Nat} :
                          theorem Fin.castSucc_pos {n : Nat} [NeZero n] {i : Fin n} (h : 0 < i) :

                          castSucc i is positive when i is positive

                          @[simp]
                          theorem Fin.castSucc_eq_zero_iff {n : Nat} [NeZero n] {a : Fin n} :
                          a.castSucc = 0 a = 0
                          theorem Fin.castSucc_ne_zero_iff {n : Nat} [NeZero n] {a : Fin n} :
                          @[simp]
                          theorem Fin.coeSucc_eq_succ {n : Nat} {a : Fin n} :
                          theorem Fin.lt_succ {n : Nat} {a : Fin n} :
                          theorem Fin.exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} :
                          ( (j : Fin n), j.castSucc = i) i last n
                          @[simp]
                          theorem Fin.coe_addNat {n : Nat} (m : Nat) (i : Fin n) :
                          (i.addNat m) = i + m
                          @[simp]
                          theorem Fin.addNat_zero (n : Nat) (i : Fin n) :
                          i.addNat 0 = i
                          @[simp]
                          theorem Fin.addNat_one {n : Nat} {i : Fin n} :
                          i.addNat 1 = i.succ
                          theorem Fin.le_coe_addNat {n : Nat} (m : Nat) (i : Fin n) :
                          m (i.addNat m)
                          @[simp]
                          theorem Fin.addNat_mk {m : Nat} (n i : Nat) (hi : i < m) :
                          i, hi.addNat n = i + n,
                          @[simp]
                          theorem Fin.cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
                          Fin.cast h (i.addNat 0) = Fin.cast i
                          theorem Fin.addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
                          (Fin.cast h i).addNat m = Fin.cast (i.addNat m)

                          For rewriting in the reverse direction, see Fin.cast_addNat_left.

                          theorem Fin.cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
                          Fin.cast h (i.addNat m) = (Fin.cast i).addNat m
                          @[simp]
                          theorem Fin.cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
                          Fin.cast h (i.addNat m') = i.addNat m
                          @[simp]
                          theorem Fin.coe_natAdd (n : Nat) {m : Nat} (i : Fin m) :
                          (natAdd n i) = n + i
                          @[simp]
                          theorem Fin.natAdd_mk {m : Nat} (n i : Nat) (hi : i < m) :
                          natAdd n i, hi = n + i,
                          theorem Fin.le_coe_natAdd {n : Nat} (m : Nat) (i : Fin n) :
                          m (natAdd m i)
                          @[simp]
                          theorem Fin.natAdd_zero {n : Nat} :
                          theorem Fin.natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
                          natAdd m (Fin.cast h i) = Fin.cast (natAdd m i)

                          For rewriting in the reverse direction, see Fin.cast_natAdd_right.

                          theorem Fin.cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
                          Fin.cast h (natAdd m i) = natAdd m (Fin.cast i)
                          @[simp]
                          theorem Fin.cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
                          Fin.cast h (natAdd m' i) = natAdd m i
                          theorem Fin.castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
                          castAdd p (natAdd m i) = Fin.cast (natAdd m (castAdd p i))
                          theorem Fin.natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
                          natAdd m (castAdd p i) = Fin.cast (castAdd p (natAdd m i))
                          theorem Fin.natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
                          natAdd m (natAdd n i) = Fin.cast (natAdd (m + n) i)
                          theorem Fin.cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
                          Fin.cast h (natAdd 0 i) = Fin.cast i
                          @[simp]
                          theorem Fin.cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
                          Fin.cast (natAdd n i) = i.addNat n
                          @[simp]
                          theorem Fin.cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
                          Fin.cast (i.addNat m) = natAdd m i
                          @[simp]
                          theorem Fin.natAdd_last {m n : Nat} :
                          natAdd n (last m) = last (n + m)
                          @[simp]
                          theorem Fin.addNat_last {m : Nat} (n : Nat) :
                          (last n).addNat m = Fin.cast (last (n + m))
                          theorem Fin.natAdd_castSucc {m n : Nat} {i : Fin m} :
                          @[simp]
                          theorem Fin.natAdd_eq_addNat (n : Nat) (i : Fin n) :
                          natAdd n i = i.addNat n
                          theorem Fin.rev_castAdd {n : Nat} (k : Fin n) (m : Nat) :
                          (castAdd m k).rev = k.rev.addNat m
                          theorem Fin.rev_addNat {n : Nat} (k : Fin n) (m : Nat) :
                          (k.addNat m).rev = castAdd m k.rev
                          theorem Fin.rev_castSucc {n : Nat} (k : Fin n) :
                          theorem Fin.rev_succ {n : Nat} (k : Fin n) :
                          @[simp]
                          theorem Fin.castSucc_succ {n : Nat} (i : Fin n) :
                          @[simp]
                          theorem Fin.castLE_refl {n : Nat} (h : n n) (i : Fin n) :
                          castLE h i = i
                          @[simp]
                          theorem Fin.castSucc_castLE {n m : Nat} (h : n m) (i : Fin n) :
                          (castLE h i).castSucc = castLE i
                          @[simp]
                          theorem Fin.castSucc_natAdd {k : Nat} (n : Nat) (i : Fin k) :

                          pred #

                          @[simp]
                          theorem Fin.coe_pred {n : Nat} (j : Fin (n + 1)) (h : j 0) :
                          (j.pred h) = j - 1
                          @[simp]
                          theorem Fin.succ_pred {n : Nat} (i : Fin (n + 1)) (h : i 0) :
                          (i.pred h).succ = i
                          @[simp]
                          theorem Fin.pred_succ {n : Nat} (i : Fin n) {h : i.succ 0} :
                          i.succ.pred h = i
                          theorem Fin.pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i 0) {j : Fin n} :
                          i.pred hi = j i = j.succ
                          theorem Fin.pred_mk_succ {n : Nat} (i : Nat) (h : i < n + 1) :
                          i + 1, .pred = i, h
                          @[simp]
                          theorem Fin.pred_mk_succ' {n : Nat} (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂ : i + 1, h₁ 0) :
                          i + 1, h₁.pred h₂ = i,
                          theorem Fin.pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w : i, h 0) :
                          i, h.pred w = i - 1,
                          @[simp]
                          theorem Fin.pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a 0} {hb : b 0} :
                          a.pred ha b.pred hb a b
                          @[simp]
                          theorem Fin.pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a 0} {hb : b 0} :
                          a.pred ha < b.pred hb a < b
                          @[simp]
                          theorem Fin.pred_inj {n : Nat} {a b : Fin (n + 1)} {ha : a 0} {hb : b 0} :
                          a.pred ha = b.pred hb a = b
                          @[simp]
                          theorem Fin.pred_one {n : Nat} :
                          pred 1 = 0
                          theorem Fin.pred_add_one {n : Nat} (i : Fin (n + 2)) (h : i < n + 1) :
                          (i + 1).pred = i.castLT h
                          @[simp]
                          theorem Fin.coe_subNat {n m : Nat} (i : Fin (n + m)) (h : m i) :
                          (subNat m i h) = i - m
                          @[simp]
                          theorem Fin.subNat_mk {n m i : Nat} (h₁ : i < n + m) (h₂ : m i) :
                          subNat m i, h₁ h₂ = i - m,
                          @[simp]
                          theorem Fin.subNat_zero {n : Nat} (i : Fin n) (h : 0 i) :
                          subNat 0 i h = i
                          @[simp]
                          theorem Fin.subNat_one_succ {n : Nat} (i : Fin (n + 1)) (h : 1 i) :
                          (subNat 1 i h).succ = i
                          @[simp]
                          theorem Fin.pred_castSucc_succ {n : Nat} (i : Fin n) :
                          @[simp]
                          theorem Fin.addNat_subNat {n m : Nat} {i : Fin (n + m)} (h : m i) :
                          (subNat m i h).addNat m = i
                          @[simp]
                          theorem Fin.subNat_addNat {n : Nat} (i : Fin n) (m : Nat) (h : m (i.addNat m) := ) :
                          subNat m (i.addNat m) h = i
                          @[simp]
                          theorem Fin.natAdd_subNat_cast {n m : Nat} {i : Fin (n + m)} (h : n i) :
                          natAdd n (subNat n (Fin.cast i) h) = i

                          Recursion and induction principles #

                          def Fin.succRec {motive : (n : Nat) → Fin nSort u_1} (zero : (n : Nat) → motive n.succ 0) (succ : (n : Nat) → (i : Fin n) → motive n imotive n.succ i.succ) {n : Nat} (i : Fin n) :
                          motive n i

                          An induction principle for Fin that considers a given i : Fin n as given by a sequence of i applications of Fin.succ.

                          The cases in the induction are:

                          • zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
                          • succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary bound n

                          Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive step. Fin.succRecOn is a version of this induction principle that takes the Fin argument first.

                          Equations
                            Instances For
                              def Fin.succRecOn {n : Nat} (i : Fin n) {motive : (n : Nat) → Fin nSort u_1} (zero : (n : Nat) → motive (n + 1) 0) (succ : (n : Nat) → (i : Fin n) → motive n imotive n.succ i.succ) :
                              motive n i

                              An induction principle for Fin that considers a given i : Fin n as given by a sequence of i applications of Fin.succ.

                              The cases in the induction are:

                              • zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
                              • succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary bound n

                              Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive step. Fin.succRec is a version of this induction principle that takes the Fin argument last.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Fin.succRecOn_zero {motive : (n : Nat) → Fin nSort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n imotive n.succ i.succ} (n : Nat) :
                                  succRecOn 0 zero succ = zero n
                                  @[simp]
                                  theorem Fin.succRecOn_succ {motive : (n : Nat) → Fin nSort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n imotive n.succ i.succ} {n : Nat} (i : Fin n) :
                                  i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)
                                  def Fin.induction {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSuccmotive i.succ) (i : Fin (n + 1)) :
                                  motive i

                                  Proves a statement by induction on the underlying Nat value in a Fin (n + 1).

                                  For the induction:

                                  • zero is the base case, demonstrating motive 0.
                                  • succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with Fin.castSucc) and demonstrating it for i.succ.

                                  Fin.inductionOn is a version of this induction principle that takes the Fin as its first parameter, Fin.cases is the corresponding case analysis operator, and Fin.reverseInduction is a version that starts at the greatest value instead of 0.

                                  Equations
                                    Instances For
                                      def Fin.induction.go {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSuccmotive i.succ) (i : Nat) (hi : i < n + 1) :
                                      motive i, hi
                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem Fin.induction_zero {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (hs : (i : Fin n) → motive i.castSuccmotive i.succ) :
                                          (fun (i : Fin (n + 1)) => induction zero hs i) 0 = zero
                                          @[simp]
                                          theorem Fin.induction_succ {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSuccmotive i.succ) (i : Fin n) :
                                          induction zero succ i.succ = succ i (induction zero succ i.castSucc)
                                          def Fin.inductionOn {n : Nat} (i : Fin (n + 1)) {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSuccmotive i.succ) :
                                          motive i

                                          Proves a statement by induction on the underlying Nat value in a Fin (n + 1).

                                          For the induction:

                                          • zero is the base case, demonstrating motive 0.
                                          • succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with Fin.castSucc) and demonstrating it for i.succ.

                                          Fin.induction is a version of this induction principle that takes the Fin as its last parameter.

                                          Equations
                                            Instances For
                                              def Fin.cases {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) :
                                              motive i

                                              Proves a statement by cases on the underlying Nat value in a Fin (n + 1).

                                              The two cases are:

                                              • zero, used when the value is of the form (0 : Fin (n + 1))
                                              • succ, used when the value is of the form (j : Fin n).succ

                                              The corresponding induction principle is Fin.induction.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Fin.cases_zero {n : Nat} {motive : Fin (n + 1)Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} :
                                                  cases zero succ 0 = zero
                                                  @[simp]
                                                  theorem Fin.cases_succ {n : Nat} {motive : Fin (n + 1)Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} (i : Fin n) :
                                                  cases zero succ i.succ = succ i
                                                  @[simp]
                                                  theorem Fin.cases_succ' {n : Nat} {motive : Fin (n + 1)Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} {i : Nat} (h : i + 1 < n + 1) :
                                                  cases zero succ i.succ, h = succ i,
                                                  theorem Fin.forall_fin_succ {n : Nat} {P : Fin (n + 1)Prop} :
                                                  (∀ (i : Fin (n + 1)), P i) P 0 ∀ (i : Fin n), P i.succ
                                                  theorem Fin.exists_fin_succ {n : Nat} {P : Fin (n + 1)Prop} :
                                                  ( (i : Fin (n + 1)), P i) P 0 (i : Fin n), P i.succ
                                                  theorem Fin.forall_fin_one {p : Fin 1Prop} :
                                                  (∀ (i : Fin 1), p i) p 0
                                                  theorem Fin.exists_fin_one {p : Fin 1Prop} :
                                                  ( (i : Fin 1), p i) p 0
                                                  theorem Fin.forall_fin_two {p : Fin 2Prop} :
                                                  (∀ (i : Fin 2), p i) p 0 p 1
                                                  theorem Fin.exists_fin_two {p : Fin 2Prop} :
                                                  ( (i : Fin 2), p i) p 0 p 1
                                                  theorem Fin.fin_two_eq_of_eq_zero_iff {a b : Fin 2} :
                                                  (a = 0 b = 0) → a = b
                                                  @[irreducible]
                                                  def Fin.reverseInduction {n : Nat} {motive : Fin (n + 1)Sort u_1} (last : motive (last n)) (cast : (i : Fin n) → motive i.succmotive i.castSucc) (i : Fin (n + 1)) :
                                                  motive i

                                                  Proves a statement by reverse induction on the underlying Nat value in a Fin (n + 1).

                                                  For the induction:

                                                  • last is the base case, demonstrating motive (Fin.last n).
                                                  • cast is the inductive step, assuming the motive for (j : Fin n).succ and demonstrating it for the predecessor j.castSucc.

                                                  Fin.induction is the non-reverse induction principle.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Fin.reverseInduction_last {n : Nat} {motive : Fin (n + 1)Sort u_1} {zero : motive (last n)} {succ : (i : Fin n) → motive i.succmotive i.castSucc} :
                                                      reverseInduction zero succ (last n) = zero
                                                      @[simp]
                                                      theorem Fin.reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1)Sort u_1} {zero : motive (last n)} {succ : (i : Fin n) → motive i.succmotive i.castSucc} (i : Fin n) :
                                                      reverseInduction zero succ i.castSucc = succ i (reverseInduction zero succ i.succ)
                                                      def Fin.lastCases {n : Nat} {motive : Fin (n + 1)Sort u_1} (last : motive (last n)) (cast : (i : Fin n) → motive i.castSucc) (i : Fin (n + 1)) :
                                                      motive i

                                                      Proves a statement by cases on the underlying Nat value in a Fin (n + 1), checking whether the value is the greatest representable or a predecessor of some other.

                                                      The two cases are:

                                                      • last, used when the value is Fin.last n
                                                      • cast, used when the value is of the form (j : Fin n).succ

                                                      The corresponding induction principle is Fin.reverseInduction.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Fin.lastCases_last {n : Nat} {motive : Fin (n + 1)Sort u_1} {last : motive (last n)} {cast : (i : Fin n) → motive i.castSucc} :
                                                          lastCases last cast (Fin.last n) = last
                                                          @[simp]
                                                          theorem Fin.lastCases_castSucc {n : Nat} {motive : Fin (n + 1)Sort u_1} {last : motive (last n)} {cast : (i : Fin n) → motive i.castSucc} (i : Fin n) :
                                                          lastCases last cast i.castSucc = cast i
                                                          def Fin.addCases {m n : Nat} {motive : Fin (m + n)Sort u} (left : (i : Fin m) → motive (castAdd n i)) (right : (i : Fin n) → motive (natAdd m i)) (i : Fin (m + n)) :
                                                          motive i

                                                          A case analysis operator for i : Fin (m + n) that separately handles the cases where i < m and where m ≤ i < m + n.

                                                          The first case, where i < m, is handled by left. In this case, i can be represented as Fin.castAdd n (j : Fin m).

                                                          The second case, where m ≤ i < m + n, is handled by right. In this case, i can be represented as Fin.natAdd m (j : Fin n).

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Fin.addCases_left {m n : Nat} {motive : Fin (m + n)Sort u_1} {left : (i : Fin m) → motive (castAdd n i)} {right : (i : Fin n) → motive (natAdd m i)} (i : Fin m) :
                                                              addCases left right (castAdd n i) = left i
                                                              @[simp]
                                                              theorem Fin.addCases_right {m n : Nat} {motive : Fin (m + n)Sort u_1} {left : (i : Fin m) → motive (castAdd n i)} {right : (i : Fin n) → motive (natAdd m i)} (i : Fin n) :
                                                              addCases left right (natAdd m i) = right i

                                                              zero #

                                                              @[simp]
                                                              theorem Fin.val_eq_zero_iff {n : Nat} [NeZero n] {a : Fin n} :
                                                              a = 0 a = 0
                                                              theorem Fin.val_ne_zero_iff {n : Nat} [NeZero n] {a : Fin n} :
                                                              a 0 a 0

                                                              add #

                                                              theorem Fin.ofNat_add {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                              Fin.ofNat n x + y = Fin.ofNat n (x + y)
                                                              @[reducible, inline, deprecated Fin.ofNat_add (since := "2025-05-28")]
                                                              abbrev Fin.ofNat_add' {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                              Fin.ofNat n x + y = Fin.ofNat n (x + y)
                                                              Equations
                                                                Instances For
                                                                  theorem Fin.add_ofNat {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                  x + Fin.ofNat n y = Fin.ofNat n (x + y)
                                                                  @[reducible, inline, deprecated Fin.add_ofNat (since := "2025-05-28")]
                                                                  abbrev Fin.add_ofNat' {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                  x + Fin.ofNat n y = Fin.ofNat n (x + y)
                                                                  Equations
                                                                    Instances For

                                                                      sub #

                                                                      theorem Fin.coe_sub {n : Nat} (a b : Fin n) :
                                                                      ↑(a - b) = (n - b + a) % n
                                                                      theorem Fin.ofNat_sub {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                                      Fin.ofNat n x - y = Fin.ofNat n (n - y + x)
                                                                      @[reducible, inline, deprecated Fin.ofNat_sub (since := "2025-05-28")]
                                                                      abbrev Fin.ofNat_sub' {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                                      Fin.ofNat n x - y = Fin.ofNat n (n - y + x)
                                                                      Equations
                                                                        Instances For
                                                                          theorem Fin.sub_ofNat {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                          x - Fin.ofNat n y = Fin.ofNat n (n - y % n + x)
                                                                          @[reducible, inline, deprecated Fin.sub_ofNat (since := "2025-05-28")]
                                                                          abbrev Fin.sub_ofNat' {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                          x - Fin.ofNat n y = Fin.ofNat n (n - y % n + x)
                                                                          Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Fin.sub_self {n : Nat} [NeZero n] {x : Fin n} :
                                                                              x - x = 0
                                                                              theorem Fin.coe_sub_iff_le {n : Nat} {a b : Fin n} :
                                                                              ↑(a - b) = a - b b a
                                                                              theorem Fin.sub_val_of_le {n : Nat} {a b : Fin n} :
                                                                              b a↑(a - b) = a - b
                                                                              theorem Fin.coe_sub_iff_lt {n : Nat} {a b : Fin n} :
                                                                              ↑(a - b) = n + a - b a < b

                                                                              neg #

                                                                              theorem Fin.val_neg {n : Nat} [NeZero n] (x : Fin n) :
                                                                              ↑(-x) = if x = 0 then 0 else n - x

                                                                              mul #

                                                                              theorem Fin.ofNat_mul {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                                              Fin.ofNat n x * y = Fin.ofNat n (x * y)
                                                                              @[reducible, inline, deprecated Fin.ofNat_mul (since := "2025-05-28")]
                                                                              abbrev Fin.ofNat_mul' {n : Nat} [NeZero n] (x : Nat) (y : Fin n) :
                                                                              Fin.ofNat n x * y = Fin.ofNat n (x * y)
                                                                              Equations
                                                                                Instances For
                                                                                  theorem Fin.mul_ofNat {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                                  x * Fin.ofNat n y = Fin.ofNat n (x * y)
                                                                                  @[reducible, inline, deprecated Fin.mul_ofNat (since := "2025-05-28")]
                                                                                  abbrev Fin.mul_ofNat' {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
                                                                                  x * Fin.ofNat n y = Fin.ofNat n (x * y)
                                                                                  Equations
                                                                                    Instances For
                                                                                      theorem Fin.val_mul {n : Nat} (a b : Fin n) :
                                                                                      ↑(a * b) = a * b % n
                                                                                      theorem Fin.coe_mul {n : Nat} (a b : Fin n) :
                                                                                      ↑(a * b) = a * b % n
                                                                                      theorem Fin.mul_one {n : Nat} [i : NeZero n] (k : Fin n) :
                                                                                      k * 1 = k
                                                                                      theorem Fin.mul_comm {n : Nat} (a b : Fin n) :
                                                                                      a * b = b * a
                                                                                      instance Fin.instCommutativeHMul {n : Nat} :
                                                                                      Std.Commutative fun (x1 x2 : Fin n) => x1 * x2
                                                                                      theorem Fin.mul_assoc {n : Nat} (a b c : Fin n) :
                                                                                      a * b * c = a * (b * c)
                                                                                      instance Fin.instAssociativeHMul {n : Nat} :
                                                                                      Std.Associative fun (x1 x2 : Fin n) => x1 * x2
                                                                                      theorem Fin.one_mul {n : Nat} [NeZero n] (k : Fin n) :
                                                                                      1 * k = k
                                                                                      instance Fin.instLawfulIdentityHMulOfNat {n : Nat} [NeZero n] :
                                                                                      Std.LawfulIdentity (fun (x1 x2 : Fin n) => x1 * x2) 1
                                                                                      theorem Fin.mul_zero {n : Nat} [NeZero n] (k : Fin n) :
                                                                                      k * 0 = 0
                                                                                      theorem Fin.zero_mul {n : Nat} [NeZero n] (k : Fin n) :
                                                                                      0 * k = 0