mathlib documentation

data.fin

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

Casts

Operation on tuples

We interpret maps Π i : fin n, α i as tuples (α 0, …, α (n-1)). If α i is a constant map, then tuples are isomorphic (but not definitionally equal) to vectors.

We define the following operations:

Misc definitions

def fin_zero_elim {α : fin 0Sort u} (x : fin 0) :
α x

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

Equations
@[instance]
theorem fact.succ.pos {n : } :
fact (0 < n.succ)

@[instance]
theorem fact.bit0.pos {n : } [h : fact (0 < n)] :
fact (0 < bit0 n)

@[instance]
theorem fact.bit1.pos {n : } :
fact (0 < bit1 n)

@[instance]
theorem fact.pow.pos {p n : } [h : fact (0 < p)] :
fact (0 < p ^ n)

@[instance]
def fin.fin_to_nat (n : ) :

Equations
theorem fin.is_lt {n : } (i : fin n) :
i < n

def fin.of_nat' {n : } [h : fact (0 < n)] :
fin n

convert a to fin n, provided n is positive

Equations
@[simp]
theorem fin.eta {n : } (a : fin n) (h : a < n) :
a, h⟩ = a

@[ext]
theorem fin.ext {n : } {a b : fin n} :
a = ba = b

theorem fin.ext_iff {n : } (a b : fin n) :
a = b a = b

theorem fin.eq_iff_veq {n : } (a b : fin n) :
a = b a.val = b.val

theorem fin.ne_iff_vne {n : } (a b : fin n) :
a b a.val b.val

@[simp]
theorem fin.mk_eq_subtype_mk {n : } (a : ) (h : a < n) :
fin.mk a h = a, h⟩

theorem fin.mk.inj_iff {n a b : } {ha : a < n} {hb : b < n} :
a, ha⟩ = b, hb⟩ a = b

theorem fin.mk_val {m n : } (h : m < n) :
m, h⟩.val = m

theorem fin.eq_mk_iff_coe_eq {n : } {a : fin n} {k : } {hk : k < n} :
a = k, hk⟩ a = k

@[simp]
theorem fin.coe_mk {m n : } (h : m < n) :
m, h⟩ = m

theorem fin.mk_coe {n : } (i : fin n) :
i, _⟩ = i

theorem fin.coe_eq_val {n : } (a : fin n) :
a = a.val

@[simp]
theorem fin.val_eq_coe {n : } (a : fin n) :
a.val = a

@[simp]
theorem fin.val_one {n : } :
1.val = 1

@[simp]
theorem fin.val_two {n : } :
2.val = 2

@[simp]
theorem fin.coe_zero {n : } :
0 = 0

@[simp]
theorem fin.coe_one {n : } :
1 = 1

@[simp]
theorem fin.coe_two {n : } :
2 = 2

@[simp]
theorem fin.coe_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.coe_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.val_add {n : } (a b : fin n) :
(a + b).val = (a.val + b.val) % n

theorem fin.coe_add {n : } (a b : fin n) :
(a + b) = (a + b) % n

theorem fin.val_mul {n : } (a b : fin n) :
(a * b).val = (a.val) * b.val % n

theorem fin.coe_mul {n : } (a b : fin n) :
a * b = (a) * b % n

theorem fin.one_val {n : } :
1.val = 1 % (n + 1)

theorem fin.coe_one' {n : } :
1 = 1 % (n + 1)

@[simp]
theorem fin.val_zero' (n : ) :
0.val = 0

@[simp]
theorem fin.mk_zero {n : } :
0, _⟩ = 0

@[simp]
theorem fin.mk_one {n : } :
1, _⟩ = 1

@[simp]
theorem fin.mk_bit0 {m n : } (h : bit0 m < n) :
bit0 m, h⟩ = bit0 m, _⟩

@[simp]
theorem fin.mk_bit1 {m n : } (h : bit1 m < n + 1) :
bit1 m, h⟩ = bit1 m, _⟩

@[simp]
theorem fin.of_nat_eq_coe (n a : ) :

theorem fin.coe_val_of_lt {n a : } :
a < n + 1a.val = a

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

theorem fin.coe_val_eq_self {n : } (a : fin (n + 1)) :
(a.val) = a

Converting the value of a fin (n + 1) to fin (n + 1) results in the same value.

theorem fin.coe_coe_of_lt {n a : } :
a < n + 1a = a

Coercing an in-range number to fin (n + 1), and converting back to , results in that number.

@[simp]
theorem fin.coe_coe_eq_self {n : } (a : fin (n + 1)) :

Converting a fin (n + 1) to and back results in the same value.

theorem fin.heq_fun_iff {α : Type 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_ext_iff {k l : } (h : k = l) {i : fin k} {j : fin l} :
i == j i = j

@[instance]
def fin.nontrivial {n : } :
nontrivial (fin (n + 2))

theorem fin.exists_iff {n : } {p : fin n → Prop} :
(∃ (i : fin n), p i) ∃ (i : ) (h : i < n), p i, h⟩

theorem fin.forall_iff {n : } {p : fin n → Prop} :
(∀ (i : fin n), p i) ∀ (i : ) (h : i < n), p i, h⟩

theorem fin.lt_iff_coe_lt_coe {n : } {a b : fin n} :
a < b a < b

theorem fin.le_iff_coe_le_coe {n : } {a b : fin n} :
a b a b

theorem fin.zero_le {n : } (a : fin (n + 1)) :
0 a

@[simp]
theorem fin.coe_succ {n : } (j : fin n) :
(j.succ) = j + 1

theorem fin.succ_pos {n : } (a : fin n) :
0 < a.succ

theorem fin.succ.inj {n : } {a b : fin n} :
a.succ = b.succa = b

@[simp]
theorem fin.succ_inj {n : } {a b : fin n} :
a.succ = b.succ a = b

@[simp]
theorem fin.succ_le_succ_iff {n : } {a b : fin n} :
a.succ b.succ a b

@[simp]
theorem fin.succ_lt_succ_iff {n : } {a b : fin n} :
a.succ < b.succ a < b

theorem fin.succ_ne_zero {n : } (k : fin n) :
k.succ 0

@[simp]
theorem fin.succ_zero_eq_one {n : } :
0.succ = 1

theorem fin.mk_succ_pos {n : } (i : ) (h : i < n) :
0 < i.succ, _⟩

theorem fin.one_lt_succ_succ {n : } (a : fin n) :
1 < a.succ.succ

theorem fin.succ_succ_ne_one {n : } (a : fin n) :

@[simp]
theorem fin.coe_pred {n : } (j : fin (n + 1)) (h : j 0) :
(j.pred h) = j - 1

@[simp]
theorem fin.succ_pred {n : } (i : fin (n + 1)) (h : i 0) :
(i.pred h).succ = i

@[simp]
theorem fin.pred_succ {n : } (i : fin n) {h : i.succ 0} :
i.succ.pred h = i

@[simp]
theorem fin.pred_mk_succ {n : } (i : ) (h : i < n + 1) :
fin.pred i + 1, _⟩ _ = i, h⟩

@[simp]
theorem fin.pred_inj {n : } {a b : fin (n + 1)} {ha : a 0} {hb : b 0} :
a.pred ha = b.pred hb a = b

def fin.last (n : ) :
fin (n + 1)

The greatest value of fin (n+1)

Equations
def fin.cast_lt {n m : } (i : fin m) :
i.val < nfin n

cast_lt i h embeds i into a fin where h proves it belongs into.

Equations
def fin.cast_le {n m : } :
n mfin nfin m

cast_le h i embeds i into a larger fin type.

Equations
def fin.cast {n m : } :
n = mfin nfin m

cast eq i embeds i into a equal fin type.

Equations
def fin.cast_add {n : } (m : ) :
fin nfin (n + m)

cast_add m i embeds i : fin n in fin (n+m).

Equations
def fin.cast_succ {n : } :
fin nfin (n + 1)

cast_succ i embeds i : fin n in fin (n+1).

Equations
def fin.succ_above {n : } :
fin (n + 1)fin nfin (n + 1)

succ_above p i embeds fin n into fin (n + 1) with a hole around p.

Equations
def fin.pred_above {n : } (p i : fin (n + 1)) :
i pfin n

pred_above p i h embeds i : fin (n+1) into fin n by ignoring p.

Equations
def fin.sub_nat {n : } (m : ) (i : fin (n + m)) :
m ifin n

sub_nat i h subtracts m from i, generalizes fin.pred.

Equations
def fin.add_nat {n : } (m : ) :
fin nfin (n + m)

add_nat i h adds m on i, generalizes fin.succ.

Equations
def fin.nat_add (n : ) {m : } :
fin mfin (n + m)

nat_add i h adds n on i

Equations
theorem fin.le_last {n : } (i : fin (n + 1)) :

@[simp]
theorem fin.coe_cast {n m : } (k : fin n) (h : n = m) :

@[simp]
theorem fin.coe_cast_succ {n : } (k : fin n) :

@[simp]
theorem fin.coe_cast_lt {n m : } (k : fin m) (h : k < n) :

@[simp]
theorem fin.coe_cast_le {n m : } (k : fin m) (h : m n) :

@[simp]
theorem fin.coe_cast_add {n m : } (k : fin m) :

theorem fin.last_val (n : ) :
(fin.last n).val = n

@[simp]
theorem fin.coe_last {n : } :

@[simp]
theorem fin.succ_last (n : ) :

@[simp]
theorem fin.cast_succ_cast_lt {n : } (i : fin (n + 1)) (h : i < n) :

@[simp]
theorem fin.cast_lt_cast_succ {n : } (a : fin n) (h : a < n) :

@[simp]
theorem fin.coe_sub_nat {n m : } (i : fin (n + m)) (h : m i) :
(fin.sub_nat m i h) = i - m

@[simp]
theorem fin.coe_add_nat {n m : } (i : fin (n + m)) :

@[simp]
theorem fin.cast_succ_inj {n : } {a b : fin n} :

theorem fin.cast_succ_lt_last {n : } (a : fin n) :

@[simp]
theorem fin.cast_succ_zero {n : } :

theorem fin.cast_succ_pos {n : } (i : fin (n + 1)) :
0 < i0 < i.cast_succ

cast_succ i is positive when i is positive

theorem fin.last_pos {n : } :
0 < fin.last (n + 1)

theorem fin.coe_nat_eq_last (n : ) :

theorem fin.le_coe_last {n : } (i : fin (n + 1)) :
i n

theorem fin.eq_last_of_not_lt {n : } {i : fin (n + 1)} :
¬i < ni = fin.last n

theorem fin.add_one_pos {n : } (i : fin (n + 1)) :
i < fin.last n0 < i + 1

theorem fin.one_pos {n : } :
0 < 1

theorem fin.zero_ne_one {n : } :
0 1

@[simp]
theorem fin.zero_eq_one_iff {n : } :
0 = 1 n = 0

@[simp]
theorem fin.one_eq_zero_iff {n : } :
1 = 0 n = 0

theorem fin.cast_succ_lt_succ {n : } (i : fin n) :

@[simp]
theorem fin.coe_eq_cast_succ {n : } {a : fin n} :

@[simp]
theorem fin.coe_succ_eq_succ {n : } {a : fin n} :

theorem fin.lt_succ {n : } {a : fin n} :

@[simp]
theorem fin.pred_one {n : } :
1.pred _ = 0

theorem fin.pred_add_one {n : } (i : fin (n + 2)) (h : i < n + 1) :
(i + 1).pred _ = i.cast_lt h

def fin.clamp (n m : ) :
fin (m + 1)

min n m as an element of fin (m + 1)

Equations
@[simp]
theorem fin.coe_clamp (n m : ) :
(fin.clamp n m) = min n m

theorem fin.cast_le_injective {n₁ n₂ : } (h : n₁ n₂) :

theorem fin.succ_above_below {n : } (p : fin (n + 1)) (i : fin n) :

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

@[simp]

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

@[simp]

Embedding fin n into fin (n + 1) with a whole around last n embeds by cast_succ

theorem fin.succ_above_above {n : } (p : fin (n + 1)) (i : fin n) :
p i.cast_succp.succ_above i = i.succ

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

theorem fin.succ_above_lt_ge {n : } (p : fin (n + 1)) (i : fin n) :

Embedding i : fin n into fin (n + 1) is always about some hole p

theorem fin.succ_above_lt_gt {n : } (p : fin (n + 1)) (i : fin n) :
i.cast_succ < p p < i.succ

Embedding i : fin n into fin (n + 1) is always about some hole p

@[simp]
theorem fin.succ_above_lt_iff {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.lt_succ_above_iff {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.succ_above_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

theorem fin.succ_above_pos {n : } (p : fin (n + 2)) (i : fin (n + 1)) :
0 < i0 < p.succ_above i

Embedding a positive fin n results in a positive fin (n + 1)`

theorem fin.succ_above_right_inj {n : } {a b : fin n} {x : fin (n + 1)} :

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

@[simp]
theorem fin.succ_above_descend {n : } (p i : fin (n + 1)) (h : i p) :
p.succ_above (p.pred_above i h) = i

Embedding a fin (n + 1) into fin n and embedding it back around the same hole gives the starting fin (n + 1)

@[simp]
theorem fin.pred_above_succ_above {n : } (p : fin (n + 1)) (i : fin n) :
p.pred_above (p.succ_above i) _ = i

Embedding a fin n into fin (n + 1) and embedding it back around the same hole gives the starting fin n

theorem fin.succ_above_left_inj {n : } {x y : fin (n + 1)} :

succ_above is injective at the pivot

succ_above is injective at the pivot

theorem fin.strict_mono_iff_lt_succ {n : } {α : Type u_1} [preorder α] {f : fin n → α} :
strict_mono f ∀ (i : ) (h : i + 1 < n), f i, _⟩ < f i + 1, h⟩

A function f on fin n is strictly monotone if and only if f i < f (i+1) for all i.

def fin.succ_rec {C : Π (n : ), fin nSort u_1} (H0 : Π (n : ), C n.succ 0) (Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ) {n : } (i : fin n) :
C n i

Define C n i by induction on i : fin n interpreted as (0 : fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

Equations
def fin.succ_rec_on {n : } (i : fin n) {C : Π (n : ), fin nSort u_1} :
(Π (n : ), C n.succ 0)(Π (n : ) (i : fin n), C n iC n.succ i.succ)C n i

Define C n i by induction on i : fin n interpreted as (0 : fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

A version of fin.succ_rec taking i : fin n as the first argument.

Equations
@[simp]
theorem fin.succ_rec_on_zero {C : Π (n : ), fin nSort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ} (n : ) :
0.succ_rec_on H0 Hs = H0 n

@[simp]
theorem fin.succ_rec_on_succ {C : Π (n : ), fin nSort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ} {n : } (i : fin n) :
i.succ.succ_rec_on H0 Hs = Hs n i (i.succ_rec_on H0 Hs)

def fin.induction {n : } {C : fin (n + 1)Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C i.cast_succC i.succ) (i : fin (n + 1)) :
C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

Equations
  • fin.induction h0 hs = λ (i : fin (n + 1)), subtype.cases_on i (λ (i : ) (hi : i < n + 1), nat.rec (λ (hi : 0 < n + 1), _.mpr h0) (λ (i : ) (IH : Π (hi : i < n + 1), C i, hi⟩) (hi : i.succ < n + 1), hs i, _⟩ (IH _)) i hi)
def fin.induction_on {n : } (i : fin (n + 1)) {C : fin (n + 1)Sort u_1} :
C 0(Π (i : fin n), C i.cast_succC i.succ)C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

A version of fin.induction taking i : fin (n + 1) as the first argument.

Equations
def fin.cases {n : } {C : fin n.succSort u_1} (H0 : C 0) (Hs : Π (i : fin n), C i.succ) (i : fin n.succ) :
C i

Define f : Π i : fin n.succ, C i by separately handling the cases i = 0 and i = j.succ, j : fin n.

Equations
@[simp]
theorem fin.cases_zero {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :
fin.cases H0 Hs 0 = H0

@[simp]
theorem fin.cases_succ {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} (i : fin n) :
fin.cases H0 Hs i.succ = Hs i

@[simp]
theorem fin.cases_succ' {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} {i : } (h : i + 1 < n + 1) :
fin.cases H0 Hs i.succ, h⟩ = Hs i, _⟩

theorem fin.forall_fin_succ {n : } {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 : } {P : fin (n + 1) → Prop} :
(∃ (i : fin (n + 1)), P i) P 0 ∃ (i : fin n), P i.succ

Tuples

We can think of the type Π(i : fin n), α i as n-tuples of elements of possibly varying type α i. A particular case is fin n → α of elements with all the same type. Here are some relevant operations, first about adding or removing elements at the beginning of a tuple.

@[instance]
def fin.tuple0_unique (α : fin 0Type u) :
unique (Π (i : fin 0), α i)

There is exactly one tuple of size zero.

Equations
def fin.tail {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :
α i.succ

The tail of an n+1 tuple, i.e., its last n entries

Equations
def fin.cons {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin (n + 1)) :
α i

Adding an element at the beginning of an n-tuple, to get an n+1-tuple

Equations
@[simp]
theorem fin.tail_cons {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :

@[simp]
theorem fin.cons_succ {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) :
fin.cons x p i.succ = p i

@[simp]
theorem fin.cons_zero {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :
fin.cons x p 0 = x

@[simp]
theorem fin.cons_update {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) (y : α i.succ) :

Updating a tuple and adding an element at the beginning commute.

theorem fin.update_cons_zero {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (z : α 0) :

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

@[simp]
theorem fin.cons_self_tail {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) :
fin.cons (q 0) (fin.tail q) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

@[simp]
theorem fin.tail_update_zero {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (z : α 0) :

Updating the first element of a tuple does not change the tail.

@[simp]
theorem fin.tail_update_succ {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α i.succ) :

Updating a nonzero element and taking the tail commute.

theorem fin.comp_cons {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (y : α) (q : fin n → α) :
g fin.cons y q = fin.cons (g y) (g q)

theorem fin.comp_tail {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :

def fin.append {n m : } {α : Type u_1} {o : } :
o = m + n(fin m → α)(fin n → α)fin o → α

fin.append ho u v appends two vectors of lengths m and n to produce one of length o = m + n. ho provides control of definitional equality for the vector length.

Equations

In the previous section, we have discussed inserting or removing elements on the left of a tuple. In this section, we do the same on the right. A difference is that fin (n+1) is constructed inductively from fin n starting from the left, not from the right. This implies that Lean needs more help to realize that elements belong to the right types, i.e., we need to insert casts at several places.

def fin.init {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :

The beginning of an n+1 tuple, i.e., its first n entries

Equations
def fin.snoc {n : } {α : fin (n + 1)Type u} (p : Π (i : fin n), α i.cast_succ) (x : α (fin.last n)) (i : fin (n + 1)) :
α i

Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

Equations
@[simp]
theorem fin.init_snoc {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) :

@[simp]
theorem fin.snoc_cast_succ {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) (i : fin n) :
fin.snoc p x i.cast_succ = p i

@[simp]
theorem fin.snoc_last {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) :
fin.snoc p x (fin.last n) = x

@[simp]
theorem fin.snoc_update {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) (i : fin n) (y : α i.cast_succ) :

Updating a tuple and adding an element at the end commute.

theorem fin.update_snoc_last {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) (z : α (fin.last n)) :

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

@[simp]
theorem fin.snoc_init_self {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) :
fin.snoc (fin.init q) (q (fin.last n)) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

@[simp]
theorem fin.init_update_last {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (z : α (fin.last n)) :

Updating the last element of a tuple does not change the beginning.

@[simp]
theorem fin.init_update_cast_succ {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α i.cast_succ) :

Updating an element and taking the beginning commute.

theorem fin.tail_init_eq_init_tail {n : } {β : Type u_1} (q : fin (n + 2) → β) :

tail and init commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

theorem fin.cons_snoc_eq_snoc_cons {n : } {β : Type u_1} (a : β) (q : fin n → β) (b : β) :

cons and snoc commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

theorem fin.comp_snoc {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n → α) (y : α) :
g fin.snoc q y = fin.snoc (g q) (g y)

theorem fin.comp_init {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :

def fin.find {n : } (p : fin n → Prop) [decidable_pred p] :

find p returns the first index n where p n is satisfied, and none if it is never satisfied.

Equations
theorem fin.find_spec {n : } (p : fin n → Prop) [decidable_pred p] {i : fin n} :
i fin.find pp i

If find p = some i, then p i holds

theorem fin.is_some_find_iff {n : } {p : fin n → Prop} [decidable_pred p] :
((fin.find p).is_some) ∃ (i : fin n), p i

find p does not return none if and only if p i holds at some index i.

theorem fin.find_eq_none_iff {n : } {p : fin n → Prop} [decidable_pred p] :
fin.find p = none ∀ (i : fin n), ¬p i

find p returns none if and only if p i never holds.

theorem fin.find_min {n : } {p : fin n → Prop} [decidable_pred p] {i : fin n} (hi : i fin.find p) {j : fin n} :
j < i¬p j

If find p returns some i, then p j does not hold for j < i, i.e., i is minimal among the indices where p holds.

theorem fin.find_min' {n : } {p : fin n → Prop} [decidable_pred p] {i : fin n} (h : i fin.find p) {j : fin n} :
p ji j

theorem fin.nat_find_mem_find {n : } {p : fin n → Prop} [decidable_pred p] (h : ∃ (i : ) (hin : i < n), p i, hin⟩) :

theorem fin.mem_find_iff {n : } {p : fin n → Prop} [decidable_pred p] {i : fin n} :
i fin.find p p i ∀ (j : fin n), p ji j

theorem fin.find_eq_some_iff {n : } {p : fin n → Prop} [decidable_pred p] {i : fin n} :
fin.find p = some i p i ∀ (j : fin n), p ji j

theorem fin.mem_find_of_unique {n : } {p : fin n → Prop} [decidable_pred p] (h : ∀ (i j : fin n), p ip ji = j) {i : fin n} :
p ii fin.find p

@[simp]
theorem fin.coe_of_nat_eq_mod (m n : ) :
n = n % m.succ

@[simp]
theorem fin.coe_of_nat_eq_mod' (m n : ) [I : fact (0 < m)] :