Operation on tuples

We interpret maps ∀ i : Fin n, α i as n-tuples of elements of possibly varying type α i, (α 0, …, α (n-1)). A particular case is Fin n → α of elements with all the same type. In this case when α i is a constant map, then tuples are isomorphic (but not definitionally equal) to Vectors.

Main declarations

There are three (main) ways to consider Fin n as a subtype of Fin (n + 1), hence three (main) ways to move between tuples of length n and of length n + 1 by adding/removing an entry.

Adding at the start

• Fin.succ: Send i : Fin n to i + 1 : Fin (n + 1). This is defined in Core.
• Fin.cases: Induction/recursion principle for Fin: To prove a property/define a function for all Fin (n + 1), it is enough to prove/define it for 0 and for i.succ for all i : Fin n. This is defined in Core.
• Fin.cons: Turn a tuple f : Fin n → α and an entry a : α into a tuple Fin.cons a f : Fin (n + 1) → α by adding a at the start. In general, tuples can be dependent functions, in which case f : ∀ i : Fin n, α i.succ and a : α 0. This is a special case of Fin.cases.
• Fin.tail: Turn a tuple f : Fin (n + 1) → α into a tuple Fin.tail f : Fin n → α by forgetting the start. In general, tuples can be dependent functions, in which case Fin.tail f : ∀ i : Fin n, α i.succ.

Adding at the end

• Fin.castSucc: Send i : Fin n to i : Fin (n + 1). This is defined in Core.
• Fin.lastCases: Induction/recursion principle for Fin: To prove a property/define a function for all Fin (n + 1), it is enough to prove/define it for last n and for i.castSucc for all i : Fin n. This is defined in Core.
• Fin.snoc: Turn a tuple f : Fin n → α and an entry a : α into a tuple Fin.snoc f a : Fin (n + 1) → α by adding a at the end. In general, tuples can be dependent functions, in which case f : ∀ i : Fin n, α i.castSucc and a : α (last n). This is a special case of Fin.lastCases.
• Fin.init: Turn a tuple f : Fin (n + 1) → α into a tuple Fin.init f : Fin n → α by forgetting the end. In general, tuples can be dependent functions, in which case Fin.init f : ∀ i : Fin n, α i.castSucc.

Adding in the middle

For a pivot p : Fin (n + 1),

• Fin.succAbove: Send i : Fin n to
  • i : Fin (n + 1) if i < p,
  • i + 1 : Fin (n + 1) if p ≤ i.
• Fin.succAboveCases: Induction/recursion principle for Fin: To prove a property/define a function for all Fin (n + 1), it is enough to prove/define it for p and for p.succAbove i for all i : Fin n.
• Fin.insertNth: Turn a tuple f : Fin n → α and an entry a : α into a tuple Fin.insertNth f a : Fin (n + 1) → α by adding a in position p. In general, tuples can be dependent functions, in which case f : ∀ i : Fin n, α (p.succAbove i) and a : α p. This is a special case of Fin.succAboveCases.
• Fin.removeNth: Turn a tuple f : Fin (n + 1) → α into a tuple Fin.removeNth p f : Fin n → α by forgetting the p-th value. In general, tuples can be dependent functions, in which case Fin.removeNth f : ∀ i : Fin n, α (succAbove p i).

p = 0 means we add at the start. p = last n means we add at the end.

Miscellaneous

• Fin.find p h : returns the first index i : Fin n where p i is satisfied given the hypothesis that h : ∃ i, p i.
• Fin.append a b : append two tuples.
• Fin.repeat n a : repeat a tuple n times.

theorem Fin.tuple0_le {α : Fin 0 → Type u_1} [(i : Fin 0) → Preorder (α i)] (f g : (i : Fin 0) → α i) : f ≤ g

def Fin.tail {n : ℕ} {α : Fin (n + 1) → Sort 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.

theorem Fin.tail_def {n : ℕ} {α : Fin (n + 1) → Sort u_1} {q : (i : Fin (n + 1)) → α i} : (tail fun (k : Fin (n + 1)) => q k) = fun (k : Fin n) => q k.succ

def Fin.cons {n : ℕ} {α : Fin (n + 1) → Sort 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.

@[simp]

theorem Fin.tail_cons {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) : tail (cons x p) = p

@[simp]

theorem Fin.cons_succ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) : cons x p i.succ = p i

@[simp]

theorem Fin.cons_zero {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) : cons x p 0 = x

@[simp]

theorem Fin.cons_one {n : ℕ} {α : Fin (n + 2) → Sort u_1} (x : α 0) (p : (i : Fin n.succ) → α i.succ) : cons x p 1 = p 0

@[simp]

theorem Fin.cons_last {n : ℕ} {α : Fin (n + 2) → Sort u_1} (x : α 0) (p : (i : Fin n.succ) → α i.succ) : cons x p (last (n + 1)) = p (last n)

@[simp]

theorem Fin.cons_update {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) (y : α i.succ) : cons x (Function.update p i y) = Function.update (cons x p) i.succ y

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

theorem Fin.cons_injective2 {n : ℕ} {α : Fin (n + 1) → Sort u} : Function.Injective2 cons

As a binary function, Fin.cons is injective.

@[simp]

theorem Fin.cons_inj {n : ℕ} {α : Fin (n + 1) → Sort u} {x₀ y₀ : α 0} {x y : (i : Fin n) → α i.succ} : cons x₀ x = cons y₀ y ↔ x₀ = y₀ ∧ x = y

theorem Fin.cons_left_injective {n : ℕ} {α : Fin (n + 1) → Sort u} (x : (i : Fin n) → α i.succ) : Function.Injective fun (x₀ : α 0) => cons x₀ x

theorem Fin.cons_right_injective {n : ℕ} {α : Fin (n + 1) → Sort u} (x₀ : α 0) : Function.Injective (cons x₀)

@[simp]

theorem Fin.update_cons_zero {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (z : α 0) : Function.update (cons x p) 0 z = cons z p

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) → Sort u} (q : (i : Fin (n + 1)) → α i) : cons (q 0) (tail q) = q

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

def Fin.consEquiv {n : ℕ} (α : Fin (n + 1) → Type u_1) : α 0 × ((i : Fin n) → α i.succ) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the first element of the tuple.

This is Fin.cons as an Equiv.

@[simp]

theorem Fin.consEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : (i : Fin (n + 1)) → α i) : (consEquiv α).symm f = (f 0, tail f)

@[simp]

theorem Fin.consEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : α 0 × ((i : Fin n) → α i.succ)) (i : Fin (n + 1)) : (consEquiv α) f i = cons f.1 f.2 i

def Fin.consCases {n : ℕ} {α : Fin (n + 1) → Sort u} {motive : ((i : Fin n.succ) → α i) → Sort v} (cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (cons x₀ x)) (x : (i : Fin n.succ) → α i) : motive x

Recurse on an n+1-tuple by splitting it into a single element and an n-tuple.

@[simp]

theorem Fin.consCases_cons {n : ℕ} {α : Fin (n + 1) → Sort u} {motive : ((i : Fin n.succ) → α i) → Sort v} (cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (cons x₀ x)) (x₀ : α 0) (x : (i : Fin n) → α i.succ) : consCases cons (Fin.cons x₀ x) = cons x₀ x

def Fin.consInduction {α : Sort u_1} {motive : {n : ℕ} → (Fin n → α) → Sort v} (elim0 : motive elim0) (cons : {n : ℕ} → (x₀ : α) → (x : Fin n → α) → motive x → motive (cons x₀ x)) {n : ℕ} (x : Fin n → α) : motive x

Recurse on a tuple by splitting into Fin.elim0 and Fin.cons.

theorem Fin.cons_injective_of_injective {n : ℕ} {α : Type u_1} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x) (hx : Function.Injective x) : Function.Injective (cons x₀ x)

theorem Fin.cons_injective_iff {n : ℕ} {α : Type u_1} {x₀ : α} {x : Fin n → α} : Function.Injective (cons x₀ x) ↔ x₀ ∉ Set.range x ∧ Function.Injective x

theorem Fin.exists_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} (q : (i : Fin (n + 1)) → α i) : ∃ (x₀ : α 0) (x : (i : Fin n) → α i.succ), q = cons x₀ x

@[simp]

theorem Fin.forall_fin_zero_pi {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop} : (∀ (x : (i : Fin 0) → α i), P x) ↔ P finZeroElim

@[simp]

theorem Fin.exists_fin_zero_pi {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop} : (∃ (x : (i : Fin 0) → α i), P x) ↔ P finZeroElim

theorem Fin.forall_fin_succ_pi {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin (n + 1)) → α i) → Prop} : (∀ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (cons a v)

theorem Fin.exists_fin_succ_pi {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin (n + 1)) → α i) → Prop} : (∃ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∃ (a : α 0) (v : (i : Fin n) → α i.succ), P (cons a v)

@[simp]

theorem Fin.tail_update_zero {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i) (z : α 0) : tail (Function.update q 0 z) = tail q

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

@[simp]

theorem Fin.tail_update_succ {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.succ) : tail (Function.update q i.succ y) = Function.update (tail q) i y

Updating a nonzero element and taking the tail commute.

theorem Fin.comp_cons {n : ℕ} {α : Sort u_1} {β : Sort u_2} (g : α → β) (y : α) (q : Fin n → α) : g ∘ cons y q = cons (g y) (g ∘ q)

theorem Fin.comp_tail {n : ℕ} {α : Sort u_1} {β : Sort u_2} (g : α → β) (q : Fin n.succ → α) : g ∘ tail q = tail (g ∘ q)

theorem Fin.le_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {x : α 0} {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ} : q ≤ cons x p ↔ q 0 ≤ x ∧ tail q ≤ p

theorem Fin.cons_le {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {x : α 0} {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ} : cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ tail q

theorem Fin.cons_le_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {x₀ y₀ : α 0} {x y : (i : Fin n) → α i.succ} : cons x₀ x ≤ cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y

theorem Fin.range_fin_succ {n : ℕ} {α : Type u_1} (f : Fin (n + 1) → α) : Set.range f = insert (f 0) (Set.range (tail f))

@[simp]

theorem Fin.range_cons {α : Type u_1} {n : ℕ} (x : α) (b : Fin n → α) : Set.range (cons x b) = insert x (Set.range b)

def Fin.append {m n : ℕ} {α : Sort u_1} (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α

Append a tuple of length m to a tuple of length n to get a tuple of length m + n. This is a non-dependent version of Fin.add_cases.

@[simp]

theorem Fin.append_left {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m) : append u v (castAdd n i) = u i

@[simp]

theorem Fin.append_left' {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m) : append u v (castLE ⋯ i) = u i

Variant of append_left using Fin.castLE instead of Fin.castAdd.

@[simp]

theorem Fin.append_right {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin n) : append u v (natAdd m i) = v i

theorem Fin.append_right_nil {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hv : n = 0) : append u v = u ∘ Fin.cast ⋯

@[simp]

theorem Fin.append_elim0 {m : ℕ} {α : Sort u_1} (u : Fin m → α) : append u elim0 = u ∘ Fin.cast ⋯

theorem Fin.append_left_nil {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hu : m = 0) : append u v = v ∘ Fin.cast ⋯

@[simp]

theorem Fin.elim0_append {n : ℕ} {α : Sort u_1} (v : Fin n → α) : append elim0 v = v ∘ Fin.cast ⋯

theorem Fin.append_assoc {m n : ℕ} {α : Sort u_1} {p : ℕ} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) : append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

theorem Fin.append_left_eq_cons {α : Sort u_1} {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α) : append x₀ x = cons (x₀ 0) x ∘ Fin.cast ⋯

Appending a one-tuple to the left is the same as Fin.cons.

theorem Fin.cons_eq_append {n : ℕ} {α : Sort u_1} (x : α) (xs : Fin n → α) : cons x xs = append (cons x elim0) xs ∘ Fin.cast ⋯

Fin.cons is the same as appending a one-tuple to the left.

@[simp]

theorem Fin.append_cast_left {α : Sort u_1} {n m : ℕ} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ) (h : n' = n) : append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯

@[simp]

theorem Fin.append_cast_right {α : Sort u_1} {n m : ℕ} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ) (h : m' = m) : append xs (ys ∘ Fin.cast h) = append xs ys ∘ Fin.cast ⋯

theorem Fin.append_rev {α : Sort u_1} {m n : ℕ} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) : append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i)

theorem Fin.append_comp_rev {α : Sort u_1} {m n : ℕ} (xs : Fin m → α) (ys : Fin n → α) : append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast ⋯

theorem Fin.append_castAdd_natAdd {m n : ℕ} {α : Sort u_1} {f : Fin (m + n) → α} : (append (fun (i : Fin m) => f (castAdd n i)) fun (i : Fin n) => f (natAdd m i)) = f

theorem Fin.addCases_castAdd_natAdd {m n : ℕ} {γ : Fin (m + n) → Sort u_2} (v : (i : Fin (m + n)) → γ i) : (fun (i : Fin (m + n)) => addCases (fun (i : Fin m) => v (castAdd n i)) (fun (j : Fin n) => v (natAdd m j)) i) = v

Splitting a dependent finite sequence v into an initial part and a final part, and then concatenating these components, produces an identical sequence.

theorem Fin.append_comp_sumElim {m n : ℕ} {α : Sort u_1} {xs : Fin m → α} {ys : Fin n → α} : append xs ys ∘ Sum.elim (castAdd n) (natAdd m) = Sum.elim xs ys

theorem Fin.append_injective_iff {m n : ℕ} {α : Sort u_1} {xs : Fin m → α} {ys : Fin n → α} : Function.Injective (append xs ys) ↔ Function.Injective xs ∧ Function.Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j

def Fin.repeat {n : ℕ} {α : Sort u_1} (m : ℕ) (a : Fin n → α) : Fin (m * n) → α

Repeat a m times. For example Fin.repeat 2 ![0, 3, 7] = ![0, 3, 7, 0, 3, 7].

@[simp]

theorem Fin.repeat_apply {m n : ℕ} {α : Sort u_1} (a : Fin n → α) (i : Fin (m * n)) : «repeat» m a i = a i.modNat

@[simp]

theorem Fin.repeat_zero {n : ℕ} {α : Sort u_1} (a : Fin n → α) : «repeat» 0 a = elim0 ∘ Fin.cast ⋯

@[simp]

theorem Fin.repeat_one {n : ℕ} {α : Sort u_1} (a : Fin n → α) : «repeat» 1 a = a ∘ Fin.cast ⋯

theorem Fin.repeat_succ {n : ℕ} {α : Sort u_1} (a : Fin n → α) (m : ℕ) : «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯

@[simp]

theorem Fin.repeat_add {n : ℕ} {α : Sort u_1} (a : Fin n → α) (m₁ m₂ : ℕ) : «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast ⋯

theorem Fin.repeat_rev {m n : ℕ} {α : Sort u_1} (a : Fin n → α) (k : Fin (m * n)) : «repeat» m a k.rev = «repeat» m (a ∘ rev) k

theorem Fin.repeat_comp_rev {m n : ℕ} {α : Sort u_1} (a : Fin n → α) : «repeat» m a ∘ rev = «repeat» m (a ∘ rev)

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) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (i : Fin n) : α i.castSucc

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

theorem Fin.init_def {n : ℕ} {α : Fin (n + 1) → Sort u_1} {q : (i : Fin (n + 1)) → α i} : (init fun (k : Fin (n + 1)) => q k) = fun (k : Fin n) => q k.castSucc

def Fin.snoc {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : (i : Fin n) → α i.castSucc) (x : α (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.

@[simp]

theorem Fin.init_snoc {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) : init (snoc p x) = p

@[simp]

theorem Fin.snoc_castSucc {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n) : snoc p x i.castSucc = p i

@[simp]

theorem Fin.snoc_apply_zero {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) [NeZero n] : snoc p x 0 = p 0

@[simp]

theorem Fin.snoc_comp_castSucc {n : ℕ} {α : Sort u_2} {a : α} {f : Fin n → α} : snoc f a ∘ castSucc = f

@[simp]

theorem Fin.snoc_last {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) : snoc p x (last n) = x

theorem Fin.snoc_zero {α : Sort u_2} (p : Fin 0 → α) (x : α) : snoc p x = fun (x_1 : Fin (0 + 1)) => x

@[simp]

theorem Fin.snoc_comp_natAdd {n m : ℕ} {α : Sort u_2} (f : Fin (m + n) → α) (a : α) : snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a

@[simp]

theorem Fin.snoc_castAdd {m n : ℕ} {α : Fin (n + m + 1) → Sort u_2} (f : (i : Fin (n + m)) → α i.castSucc) (a : α (last (n + m))) (i : Fin n) : snoc f a (castAdd (m + 1) i) = f (castAdd m i)

@[simp]

theorem Fin.snoc_comp_castAdd {n m : ℕ} {α : Sort u_2} (f : Fin (n + m) → α) (a : α) : snoc f a ∘ castAdd (m + 1) = f ∘ castAdd m

@[simp]

theorem Fin.snoc_update {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n) (y : α i.castSucc) : snoc (Function.update p i y) x = Function.update (snoc p x) i.castSucc y

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

theorem Fin.update_snoc_last {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (i : Fin n) → α i.castSucc) (z : α (last n)) : Function.update (snoc p x) (last n) z = snoc p z

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

@[simp]

theorem Fin.range_snoc {n : ℕ} {α : Type u_2} (f : Fin n → α) (x : α) : Set.range (snoc f x) = insert x (Set.range f)

theorem Fin.snoc_injective2 {n : ℕ} {α : Fin (n + 1) → Sort u_1} : Function.Injective2 snoc

As a binary function, Fin.snoc is injective.

@[simp]

theorem Fin.snoc_inj {n : ℕ} {α : Fin (n + 1) → Sort u_1} {x y : (i : Fin n) → α i.castSucc} {xₙ yₙ : α (last n)} : snoc x xₙ = snoc y yₙ ↔ x = y ∧ xₙ = yₙ

theorem Fin.snoc_right_injective {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : (i : Fin n) → α i.castSucc) : Function.Injective (snoc x)

theorem Fin.snoc_left_injective {n : ℕ} {α : Fin (n + 1) → Sort u_1} (xₙ : α (last n)) : Function.Injective fun (x : (i : Fin n) → α i.castSucc) => snoc x xₙ

@[simp]

theorem Fin.snoc_init_self {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i) : snoc (init q) (q (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) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (z : α (last n)) : init (Function.update q (last n) z) = init q

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

@[simp]

theorem Fin.init_update_castSucc {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.castSucc) : init (Function.update q i.castSucc y) = Function.update (init q) i y

Updating an element and taking the beginning commute.

theorem Fin.tail_init_eq_init_tail {n : ℕ} {β : Sort u_2} (q : Fin (n + 2) → β) : tail (init q) = init (tail q)

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 : ℕ} {β : Sort u_2} (a : β) (q : Fin n → β) (b : β) : cons a (snoc q b) = snoc (cons a q) 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 : ℕ} {α : Sort u_2} {β : Sort u_3} (g : α → β) (q : Fin n → α) (y : α) : g ∘ snoc q y = snoc (g ∘ q) (g y)

theorem Fin.append_right_eq_snoc {α : Sort u_2} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α) : append x x₀ = snoc x (x₀ 0)

Appending a one-tuple to the right is the same as Fin.snoc.

theorem Fin.snoc_eq_append {n : ℕ} {α : Sort u_2} (xs : Fin n → α) (x : α) : snoc xs x = append xs (cons x elim0)

Fin.snoc is the same as appending a one-tuple

theorem Fin.append_left_snoc {n m : ℕ} {α : Sort u_2} (xs : Fin n → α) (x : α) (ys : Fin m → α) : append (snoc xs x) ys = append xs (cons x ys) ∘ Fin.cast ⋯

theorem Fin.append_right_cons {n m : ℕ} {α : Sort u_2} (xs : Fin n → α) (y : α) (ys : Fin m → α) : append xs (cons y ys) = append (snoc xs y) ys ∘ Fin.cast ⋯

theorem Fin.append_cons {m n : ℕ} {α : Sort u_2} (a : α) (as : Fin n → α) (bs : Fin m → α) : append (cons a as) bs = cons a (append as bs) ∘ Fin.cast ⋯

theorem Fin.append_snoc {m n : ℕ} {α : Sort u_2} (as : Fin n → α) (bs : Fin m → α) (b : α) : append as (snoc bs b) = snoc (append as bs) b

theorem Fin.comp_init {n : ℕ} {α : Sort u_2} {β : Sort u_3} (g : α → β) (q : Fin n.succ → α) : g ∘ init q = init (g ∘ q)

def Fin.snocEquiv {n : ℕ} (α : Fin (n + 1) → Type u_2) : α (last n) × ((i : Fin n) → α i.castSucc) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the last element of the tuple.

This is Fin.snoc as an Equiv.

@[simp]

theorem Fin.snocEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) (f : α (last n) × ((i : Fin n) → α i.castSucc)) (x✝ : Fin (n + 1)) : (snocEquiv α) f x✝ = snoc f.2 f.1 x✝

@[simp]

theorem Fin.snocEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) (f : (i : Fin (n + 1)) → α i) : (snocEquiv α).symm f = (f (last n), init f)

@[inline]

def Fin.snocCases {n : ℕ} {α : Fin (n + 1) → Sort u_1} {motive : ((i : Fin n.succ) → α i) → Sort u_2} (snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (snoc xs x)) (x : (i : Fin n.succ) → α i) : motive x

Recurse on an n+1-tuple by splitting it its initial n-tuple and its last element.

@[simp]

theorem Fin.snocCases_snoc {n : ℕ} {α : Fin (n + 1) → Sort u_1} {motive : ((i : Fin (n + 1)) → α i) → Sort u_2} (snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (snoc x x₀)) (x : (i : Fin n) → init α i) (x₀ : α (last n)) : snocCases snoc (Fin.snoc x x₀) = snoc x x₀

def Fin.snocInduction {α : Sort u_2} {motive : {n : ℕ} → (Fin n → α) → Sort u_3} (elim0 : motive elim0) (snoc : {n : ℕ} → (x : Fin n → α) → (x₀ : α) → motive x → motive (snoc x x₀)) {n : ℕ} (x : Fin n → α) : motive x

Recurse on a tuple by splitting into Fin.elim0 and Fin.snoc.

theorem Fin.snoc_injective_of_injective {n : ℕ} {α : Type u_2} {x₀ : α} {x : Fin n → α} (hx : Function.Injective x) (hx₀ : x₀ ∉ Set.range x) : Function.Injective (snoc x x₀)

theorem Fin.snoc_injective_iff {n : ℕ} {α : Type u_2} {x₀ : α} {x : Fin n → α} : Function.Injective (snoc x x₀) ↔ Function.Injective x ∧ x₀ ∉ Set.range x

def Fin.succAboveCases {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j

Define a function on Fin (n + 1) from a value on i : Fin (n + 1) and values on each Fin.succAbove i j, j : Fin n. This version is elaborated as eliminator and works for propositions, see also Fin.insertNth for a version without an @[elab_as_elim] attribute.

theorem Fin.forall_iff_succ {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ

Alias of Fin.forall_fin_succ.

theorem Fin.exists_iff_succ {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ (i : Fin (n + 1)), P i) ↔ P 0 ∨ ∃ (i : Fin n), P i.succ

Alias of Fin.exists_fin_succ.

theorem Fin.forall_iff_castSucc {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ P (last n) ∧ ∀ (i : Fin n), P i.castSucc

theorem Fin.forall_fin_add {m n : ℕ} (P : Fin (m + n) → Prop) : (∀ (i : Fin (m + n)), P i) ↔ (∀ (i : Fin m), P (castAdd n i)) ∧ ∀ (j : Fin n), P (natAdd m j)

A finite sequence of properties P holds for {0, ..., m + n - 1} iff it holds separately for both {0, ..., m - 1} and {m, ..., m + n - 1}.

theorem Fin.forall_fin_add_pi {m n : ℕ} {γ : Fin (m + n) → Sort u_3} {P : ((i : Fin (m + n)) → γ i) → Prop} : (∀ (v : (i : Fin (m + n)) → γ i), P v) ↔ ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)), P fun (i : Fin (m + n)) => addCases vₘ vₙ i

A property holds for all dependent finite sequence of length m + n iff it holds for the concatenation of all pairs of length m sequences and length n sequences.

theorem Fin.exists_iff_castSucc {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ (i : Fin (n + 1)), P i) ↔ P (last n) ∨ ∃ (i : Fin n), P i.castSucc

theorem Fin.forall_iff_succAbove {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∀ (i : Fin (n + 1)), P i) ↔ P p ∧ ∀ (i : Fin n), P (p.succAbove i)

theorem Fin.exists_iff_succAbove {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∃ (i : Fin (n + 1)), P i) ↔ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

theorem Fin.eq_self_or_eq_succAbove {n : ℕ} (p i : Fin (n + 1)) : i = p ∨ ∃ (j : Fin n), i = p.succAbove j

Analogue of Fin.eq_zero_or_eq_succ for succAbove.

def Fin.removeNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n) : α (p.succAbove i)

Remove the p-th entry of a tuple.

def Fin.insertNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j

Insert an element into a tuple at a given position. For i = 0 see Fin.cons, for i = Fin.last n see Fin.snoc. See also Fin.succAboveCases for a version elaborated as an eliminator.

@[simp]

theorem Fin.insertNth_apply_same {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p i = x

@[simp]

theorem Fin.insertNth_apply_succAbove {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin n) : i.insertNth x p (i.succAbove j) = p j

@[simp]

theorem Fin.succAbove_cases_eq_insertNth : @succAboveCases = @insertNth

theorem Fin.removeNth_apply {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n) : p.removeNth f i = f (p.succAbove i)

theorem Fin.removeNth_fun_const {α : Type u_3} {n : ℕ} (i : Fin (n + 1)) (a : α) : (i.removeNth fun (x : Fin (n + 1)) => a) = fun (x : Fin n) => a

@[simp]

theorem Fin.removeNth_insertNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (a : α p) (f : (i : Fin n) → α (p.succAbove i)) : p.removeNth (p.insertNth a f) = f

@[simp]

theorem Fin.removeNth_zero {n : ℕ} {α : Fin (n + 1) → Sort u_1} (f : (i : Fin (n + 1)) → α i) : removeNth 0 f = tail f

@[simp]

theorem Fin.removeNth_last {n : ℕ} {α : Type u_3} (f : Fin (n + 1) → α) : (last n).removeNth f = init f

@[simp]

theorem Fin.insertNth_comp_succAbove {n : ℕ} {β : Sort u_2} (i : Fin (n + 1)) (x : β) (p : Fin n → β) : i.insertNth x p ∘ i.succAbove = p

theorem Fin.insertNth_eq_iff {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)} {g : (j : Fin (n + 1)) → α j} : p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g

theorem Fin.eq_insertNth_iff {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)} {g : (j : Fin (n + 1)) → α j} : g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

theorem Fin.insertNth_injective2 {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} : Function.Injective2 p.insertNth

As a binary function, Fin.insertNth is injective.

@[simp]

theorem Fin.insertNth_inj {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {x y : (i : Fin n) → α (p.succAbove i)} {xₚ yₚ : α p} : p.insertNth xₚ x = p.insertNth yₚ y ↔ xₚ = yₚ ∧ x = y

theorem Fin.insertNth_left_injective {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : (i : Fin n) → α (p.succAbove i)) : Function.Injective fun (x_1 : α p) => p.insertNth x_1 x

theorem Fin.insertNth_right_injective {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : α p) : Function.Injective (p.insertNth x)

theorem Fin.insertNth_apply_below {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : j < i) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) : i.insertNth x p j = ⋯ ▸ p (j.castPred ⋯)

theorem Fin.insertNth_apply_above {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : i < j) (x : α i) (p : (k : Fin n) → α (i.succAbove k)) : i.insertNth x p j = ⋯ ▸ p (j.pred ⋯)

theorem Fin.insertNth_zero {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α 0) (p : (j : Fin n) → α (succAbove 0 j)) : insertNth 0 x p = cons x fun (j : Fin n) => cast ⋯ (p j)

@[simp]

theorem Fin.insertNth_zero' {n : ℕ} {β : Sort u_2} (x : β) (p : Fin n → β) : insertNth 0 x p = cons x p

theorem Fin.insertNth_last {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (last n)) (p : (j : Fin n) → α ((last n).succAbove j)) : (last n).insertNth x p = snoc (fun (j : Fin n) => cast ⋯ (p j)) x

@[simp]

theorem Fin.insertNth_last' {n : ℕ} {β : Sort u_2} (x : β) (p : Fin n → β) : (last n).insertNth x p = snoc p x

theorem Fin.insertNth_rev {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) : i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j

theorem Fin.insertNth_comp_rev {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (x : α) (p : Fin n → α) : i.insertNth x p ∘ rev = i.rev.insertNth x (p ∘ rev)

@[simp]

theorem Fin.insertNth_succ_cons {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (x a : α) (p : Fin n → α) : i.succ.insertNth x (cons a p) = cons a (i.insertNth x p)

theorem Fin.cons_rev {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) (i : Fin (n + 1)) : cons a f i.rev = snoc (f ∘ rev) a i

theorem Fin.cons_comp_rev {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) : cons a f ∘ rev = snoc (f ∘ rev) a

theorem Fin.snoc_rev {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) (i : Fin (n + 1)) : snoc f a i.rev = cons a (f ∘ rev) i

theorem Fin.snoc_comp_rev {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) : snoc f a ∘ rev = cons a (f ∘ rev)

theorem Fin.insertNth_binop {n : ℕ} {α : Fin (n + 1) → Sort u_1} (op : (j : Fin (n + 1)) → α j → α j → α j) (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : (i.insertNth (op i x y) fun (j : Fin n) => op (i.succAbove j) (p j) (q j)) = fun (j : Fin (n + 1)) => op j (i.insertNth x p j) (i.insertNth y q j)

theorem Fin.insertNth_le_iff {n : ℕ} {α : Fin (n + 1) → Type u_3} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} : i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun (j : Fin n) => q (i.succAbove j)

theorem Fin.le_insertNth_iff {n : ℕ} {α : Fin (n + 1) → Type u_3} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j} : q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun (j : Fin n) => q (i.succAbove j)) ≤ p

@[simp]

theorem Fin.removeNth_update {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (f : (j : Fin (n + 1)) → α j) : p.removeNth (Function.update f p x) = p.removeNth f

@[simp]

theorem Fin.removeNth_update_succAbove {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (i : Fin n) (x : α (p.succAbove i)) (f : (j : Fin (n + 1)) → α j) : p.removeNth (Function.update f (p.succAbove i) x) = Function.update (p.removeNth f) i x

@[simp]

theorem Fin.insertNth_removeNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (f : (j : Fin (n + 1)) → α j) : p.insertNth x (p.removeNth f) = Function.update f p x

theorem Fin.insertNth_self_removeNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (j : Fin (n + 1)) → α j) : p.insertNth (f p) (p.removeNth f) = f

@[simp]

theorem Fin.update_insertNth {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x y : α p) (f : (i : Fin n) → α (p.succAbove i)) : Function.update (p.insertNth x f) p y = p.insertNth y f

@[simp]

theorem Fin.insertNth_update {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (i : Fin n) (y : α (p.succAbove i)) (f : (j : Fin n) → α (p.succAbove j)) : p.insertNth x (Function.update f i y) = Function.update (p.insertNth x f) (p.succAbove i) y

def Fin.insertNthEquiv {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) : α p × ((i : Fin n) → α (p.succAbove i)) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple.

This is Fin.insertNth as an Equiv.

@[simp]

theorem Fin.insertNthEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) : (insertNthEquiv α p) f j = p.insertNth f.1 f.2 j

@[simp]

theorem Fin.insertNthEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) : (insertNthEquiv α p).symm f = (f p, p.removeNth f)

@[simp]

theorem Fin.insertNthEquiv_zero {n : ℕ} (α : Fin (n + 1) → Type u_3) : insertNthEquiv α 0 = consEquiv α

@[simp]

theorem Fin.insertNthEquiv_last (n : ℕ) (α : Type u_3) : insertNthEquiv (fun (x : Fin (n + 1)) => α) (last n) = snocEquiv fun (x : Fin (n + 1)) => α

Note this lemma can only be written about non-dependent tuples as insertNth (last n) = snoc is not a definitional equality.

theorem Fin.removeNth_removeNth_heq_swap {n : ℕ} {α : Fin (n + 2) → Sort u_3} (m : (i : Fin (n + 2)) → α i) (i : Fin (n + 1)) (j : Fin (n + 2)) : i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

A HEq version of Fin.removeNth_removeNth_eq_swap.

theorem Fin.removeNth_removeNth_eq_swap {n : ℕ} {α : Sort u_3} (m : Fin (n + 2) → α) (i : Fin (n + 1)) (j : Fin (n + 2)) : i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

Given an (n + 2)-tuple m and two indexes i : Fin (n + 1) and j : Fin (n + 2), one can remove jth element from m, then remove ith element from the result, or one can remove (j.succAbove i)th element from m, then remove (i.predAbove j)th element from the result.

These two operations correspond to removing the same two elements in a different order, so they result in the same n-tuple.

def Fin.find {n : ℕ} (p : Fin n → Prop) [DecidablePred p] (h : ∃ (k : Fin n), p k) : Fin n

Fin.find p h returns the smallest index k : Fin n where p k is satisfied, given that it is satisfied for some k.

theorem Fin.find_spec {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) : p (Fin.find p h)

Fin.find p h satisfies p.

theorem Fin.find_min {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) {j : Fin n} : j < Fin.find p h → ¬p j

For m : Fin n, if m < Fin.find p h then m does not satisfy p.

theorem Fin.find_le_of_pos {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) {j : Fin n} : p j → Fin.find p h ≤ j

For m : Fin n, if m satisfies p, then Fin.find p h ≤ m.

theorem Fin.find_eq_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (h : ∃ (k : Fin n), p k) : Fin.find p h = i ↔ p i ∧ ∀ j < i, ¬p j

@[simp]

theorem Fin.val_find {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) : ↑(Fin.find p h) = Nat.find ⋯

theorem Fin.find_nat_lt {n : ℕ} {p : ℕ → Prop} [DecidablePred p] (h : ∃ k < n, p k) : Nat.find ⋯ = ↑(Fin.find (fun (x : Fin n) => p ↑x) ⋯)

@[simp]

theorem Fin.find_lt_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) (i : Fin n) : Fin.find p h < i ↔ ∃ m < i, p m

@[simp]

theorem Fin.find_le_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) (i : Fin n) : Fin.find p h ≤ i ↔ ∃ m ≤ i, p m

@[simp]

theorem Fin.lt_find_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) (i : Fin n) : i < Fin.find p h ↔ ∀ m ≤ i, ¬p m

@[simp]

theorem Fin.le_find_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (k : Fin n), p k) (i : Fin n) : i ≤ Fin.find p h ↔ ∀ m < i, ¬p m

@[simp]

theorem Fin.find_eq_zero {n : ℕ} {p : Fin (n + 1) → Prop} [DecidablePred p] (h : ∃ (k : Fin (n + 1)), p k) : Fin.find p h = 0 ↔ p 0

theorem Fin.find_of_not_zero {n : ℕ} {p : Fin (n + 1) → Prop} [DecidablePred p] (h : ∃ (i : Fin (n + 1)), p i) (h0 : ¬p 0) : Fin.find p h = (Fin.find (fun (k : Fin n) => p k.succ) ⋯).succ

theorem Fin.find_eq_dite {n : ℕ} {p : Fin (n + 1) → Prop} [DecidablePred p] (h : ∃ (i : Fin (n + 1)), p i) : Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun (k : Fin n) => p k.succ) ⋯).succ

theorem Fin.find_mono_of_le {n : ℕ} {p q : Fin n → Prop} [DecidablePred p] [DecidablePred q] {i : Fin n} (hi : q i) (hpq : ∀ j ≤ i, q j → p j) : Fin.find p ⋯ ≤ Fin.find q ⋯

If a predicate q holds at some x and implies p up to that x, then the earliest xq such that q xq is at least the smallest xp where p xp. The stronger version of Fin.find_mono, since this one needs implication only up to Fin.find _ while the other requires q implying p everywhere.

theorem Fin.find_mono {n : ℕ} {p q : Fin n → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (i : Fin n), q i → p i) {hp : ∃ (i : Fin n), p i} {hq : ∃ (i : Fin n), q i} : Fin.find p hp ≤ Fin.find q hq

A weak version of Fin.find_mono_of_le, requiring q implies p everywhere.

theorem Fin.find_congr {n : ℕ} {p q : Fin n → Prop} [DecidablePred p] [DecidablePred q] {i : Fin n} (hi : p i) (hpq : ∀ j ≤ i, p j ↔ q j) : Fin.find p ⋯ = Fin.find q ⋯

If a predicate p holds at some x and agrees with q up to that x, then their Fin.find agree. The stronger version of Fin.find_congr', since this one needs agreement only up to Fin.find _ while the other requires p = q. Usage of this lemma will likely be via obtain ⟨x, hx⟩ := hp; apply Fin.find_congr hx to unify q, or provide it explicitly with rw [Fin.find_congr (q := q) hx].

theorem Fin.find_congr' {n : ℕ} {p q : Fin n → Prop} [DecidablePred p] [DecidablePred q] {hp : ∃ (i : Fin n), p i} {hq : ∃ (i : Fin n), q i} (hpq : ∀ {i : Fin n}, p i ↔ q i) : Fin.find p hp = Fin.find q hq

A weak version of Fin.find_congr, requiring p = q everywhere.

theorem Fin.find_le {n : ℕ} {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (hi : p i) : Fin.find p ⋯ ≤ i

theorem Fin.find_pos {n : ℕ} {p : Fin (n + 1) → Prop} [DecidablePred p] (h : ∃ (i : Fin (n + 1)), p i) : 0 < Fin.find p h ↔ ¬p 0

theorem Fin.find_of_find_le {m n : ℕ} {p : Fin (m + n) → Prop} [DecidablePred p] {hᵢ : ∃ (i : Fin (m + n)), p i} (hm : m ≤ ↑(Fin.find p hᵢ)) : Fin.find p hᵢ = natAdd m (Fin.find (fun (j : Fin n) => p (natAdd m j)) ⋯)

theorem Fin.find?_eq_dite {n : ℕ} {p : Fin n → Bool} : find? p = if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) => p x = true) h) else none

theorem Fin.find?_decide_eq_dite {n : ℕ} {p : Fin n → Prop} [DecidablePred p] : (find? fun (x : Fin n) => decide (p x)) = if h : ∃ (i : Fin n), p i then some (Fin.find p h) else none

theorem Fin.get_find?_eq_find_of_eq_true {n : ℕ} {i : Fin n} {p : Fin n → Bool} (h : p i = true) : (find? p).get ⋯ = Fin.find (fun (x : Fin n) => p x = true) ⋯

theorem Fin.find?_decide_get_eq_find {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (i : Fin n), p i) : (find? fun (x : Fin n) => decide (p x)).get ⋯ = Fin.find p h

theorem Fin.find_mem_find?_decide {n : ℕ} {p : Fin n → Prop} [DecidablePred p] (h : ∃ (i : Fin n), p i) : Fin.find p h ∈ find? fun (b : Fin n) => decide (p b)

theorem Fin.mem_find?_iff {n : ℕ} {p : Fin n → Bool} {i : Fin n} : i ∈ find? p ↔ p i = true ∧ ∀ j < i, ¬p j = true

theorem Fin.find?_eq_some_find_of_exists {n : ℕ} {p : Fin n → Bool} (h : ∃ (i : Fin n), p i = true) : find? p = some (Fin.find (fun (x : Fin n) => p x = true) h)

theorem Fin.find?_eq_some_find_of_isSome {n : ℕ} {p : Fin n → Bool} (h : (find? p).isSome = true) : find? p = some (Fin.find (fun (x : Fin n) => p x = true) ⋯)

def Fin.contractNth {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) : α

Sends (g₀, ..., gₙ) to (g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ).

theorem Fin.contractNth_apply_of_lt {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : ↑k < ↑j) : j.contractNth op g k = g k.castSucc

theorem Fin.contractNth_apply_of_eq {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : ↑k = ↑j) : j.contractNth op g k = op (g k.castSucc) (g k.succ)

theorem Fin.contractNth_apply_of_gt {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : ↑j < ↑k) : j.contractNth op g k = g k.succ

theorem Fin.contractNth_apply_of_ne {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (hjk : ↑j ≠ ↑k) : j.contractNth op g k = g (j.succAbove k)

theorem Fin.comp_contractNth {n : ℕ} {α : Sort u_1} {β : Sort u_2} (opα : α → α → α) (opβ : β → β → β) {f : α → β} (hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)) (j : Fin (n + 1)) (g : Fin (n + 1) → α) : f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

theorem Fin.sigma_eq_of_eq_comp_cast {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)} (h : a.fst = b.fst) : a.snd = b.snd ∘ Fin.cast h → a = b

To show two sigma pairs of tuples agree, it to show the second elements are related via Fin.cast.

theorem Fin.sigma_eq_iff_eq_comp_cast {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)} : a = b ↔ ∃ (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h

Fin.sigma_eq_of_eq_comp_cast as an iff.

def piFinTwoEquiv (α : Fin 2 → Type u) : ((i : Fin 2) → α i) ≃ α 0 × α 1

Π i : Fin 2, α i is equivalent to α 0 × α 1. See also finTwoArrowEquiv for a non-dependent version and prodEquivPiFinTwo for a version with inputs α β : Type u.

@[simp]

theorem piFinTwoEquiv_apply (α : Fin 2 → Type u) : ⇑(piFinTwoEquiv α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)

@[simp]

theorem piFinTwoEquiv_symm_apply (α : Fin 2 → Type u) : ⇑(piFinTwoEquiv α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)