Insertions and appends in tuples

The positions k.castSucc and k.succ of Fin (m + 1) are adjacent: each one skips the other to land on k (Fin.succAbove_castSucc_self, Fin.succAbove_succ_self). This file reads off the entry of an insertion at one of them in the other position, and compares updating the two insertions there. It also shows how Fin.snoc interacts with reindexing along a map extended to send the last position to the last position. The image of an initial segment under Fin.cons is obtained by inserting the first entry into the corresponding image for the tail. A tuple of length three is determined by its three entries. A tuple in a sum type that starts on the left, ends on the right and never steps from right to left steps from left to right exactly once.

Main results

• Fin.insertNth_castSucc_apply_succ and Fin.insertNth_succ_apply_castSucc: after inserting at one of two adjacent positions, the other position holds the k-th entry of the tuple.
• Fin.update_insertNth_castSucc: inserting at k.castSucc and updating k.succ is inserting at k.succ and updating k.castSucc.
• Fin.snoc_comp_snoc_castSucc_comp: reindexing along g and then appending agrees with appending and then reindexing along the extension of g that fixes the last position.
• Fin.tail_contractNth_succ, Fin.init_contractNth_castSucc: contracting two adjacent entries away from the first (last) one commutes with dropping the first (last) entry.
• Fin.snoc_comp_swap_castSucc: exchanging two entries other than the last one commutes with appending.
• Fin.tail_snoc: dropping the first entry commutes with appending a last one.
• Fin.snoc_tail_comp_rev: appending the first entry to the reversed tail reverses the tuple.
• Fin.forall_snoc_eq_iff_snoc_eq: appending one entry to each of two tuples gives the same equality pattern exactly when the old patterns agree and the new entries repeat the same positions.
• Fin.update_append_castAdd, Fin.update_append_natAdd: updating an entry of Fin.append u v updates the corresponding entry of u or of v.
• Fin.append_comp_swap_castAdd, Fin.append_comp_swap_natAdd: exchanging two entries of Fin.append u v exchanges the corresponding entries of u or of v.
• Fin.contractNth_zero_cons, Fin.contractNth_succ_cons: contracting entries of a tuple Fin.cons x a.
• Fin.contractNth_castSucc_castSucc_snoc, Fin.contractNth_castSucc_last_snoc: contracting entries of a tuple Fin.snoc a x.
• Fin.init_contractNth_castSucc_last: contracting the last two entries and dropping the last one drops the last two entries.
• Fin.contractNth_last: contracting at the last position drops the last entry.
• Fin.contractNth_castSucc_castSucc_apply_last and Fin.contractNth_castSucc_last_apply_last: the last entry of a contraction.
• Fin.contractNth_castSucc_eq_update_removeNth_succ: contracting the entries j and j + 1 is deleting entry j + 1 and then overwriting entry j by the contraction.
• Fin.update_removeNth_succ_eq_removeNth_castSucc: deleting entry j + 1 and then overwriting entry j by the deleted entry is deleting entry j.
• Fin.contractNth_castSucc_const: contracting two adjacent entries of a constant tuple.
• Fin.insertNth_apply_zero_of_ne_zero, Fin.insertNth_apply_last_of_ne_last: inserting away from the first (last) position keeps the first (last) entry.
• Fin.contractNth_castSucc_insertNth_succ_castSucc: contracting the two steps of a path that meet at an inserted vertex.
• Fin.removeNth_succ_cons: deleting an entry of Fin.cons x a other than the first deletes the corresponding entry of a.
• Fin.insertNth_one_ne_zero: inserting the entry 1 gives a nonzero tuple.
• Fin.injective_apply_zero_one_two: a tuple of length three is determined by its entries.
• Fin.injective_comp_succAbove_of_eq and Fin.range_comp_succAbove_of_eq: if b p = b q, deleting the entry at p or at q gives an injective tuple in the same cases, and does not change the set of entries.
• Fin.existsUnique_isLeft_castSucc_and_isRight_succ: a tuple in α ⊕ β from the left summand to the right one that never steps back steps from left to right exactly once.

@[simp]

theorem Fin.insertNth_castSucc_apply_succ {m : ℕ} {α : Sort u_1} (k : Fin m) (u : α) (y : Fin m → α) : k.castSucc.insertNth u y k.succ = y k

After inserting at k.castSucc, the next position k.succ holds the k-th entry.

@[simp]

theorem Fin.insertNth_succ_apply_castSucc {m : ℕ} {α : Sort u_1} (k : Fin m) (v : α) (y : Fin m → α) : k.succ.insertNth v y k.castSucc = y k

After inserting at k.succ, the previous position k.castSucc holds the k-th entry.

theorem Fin.update_insertNth_castSucc {m : ℕ} {α : Sort u_1} (k : Fin m) (y : Fin m → α) (u v : α) : Function.update (k.castSucc.insertNth u y) k.succ v = Function.update (k.succ.insertNth v y) k.castSucc u

Two insertions at adjacent positions agree away from those positions.

theorem Fin.snoc_comp_snoc_castSucc_comp {m : ℕ} {α : Sort u_1} {n : ℕ} (c : Fin n → α) (z : α) (g : Fin m → Fin n) : snoc c z ∘ snoc (castSucc ∘ g) (last n) = snoc (c ∘ g) z

Appending z to c and reindexing along the extension of g that sends the last position to the last position is the same as appending z to c ∘ g.

theorem Fin.snoc_comp_swap_castSucc {α : Sort u_1} {n : ℕ} (c : Fin n → α) (z : α) (j k : Fin n) : snoc c z ∘ ⇑(Equiv.swap j.castSucc k.castSucc) = snoc (c ∘ ⇑(Equiv.swap j k)) z

Exchanging the entries j and k of Fin.snoc c z is appending z to c with the entries j and k exchanged.

theorem Fin.tail_snoc {α : Sort u_1} {n : ℕ} (a : Fin (n + 1) → α) (x : α) : tail (snoc a x) = snoc (tail a) x

Dropping the first entry of Fin.snoc a x is appending x to the tail of a.

theorem Fin.snoc_tail_comp_rev {α : Type u_2} {n : ℕ} (a : Fin (n + 1) → α) : snoc (tail a ∘ rev) (a 0) = a ∘ rev

Appending the first entry of a to its reversed tail is reversing a.

theorem Fin.forall_snoc_eq_iff_snoc_eq {α : Sort u_1} {β : Sort u_2} {n : ℕ} {a : Fin n → α} {b : Fin n → β} {x : α} {y : β} : (∀ (i j : Fin (n + 1)), snoc a x i = snoc a x j ↔ snoc b y i = snoc b y j) ↔ (∀ (i j : Fin n), a i = a j ↔ b i = b j) ∧ ∀ (i : Fin n), a i = x ↔ b i = y

Appending one entry to each of two tuples gives the same equality pattern exactly when the old patterns agree and the new entries repeat the same positions.

@[simp]

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

Updating Fin.append u v at a position of u is appending the updated u to v.

@[simp]

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

Updating Fin.append u v at a position of v is appending u to the updated v.

theorem Fin.append_comp_swap_castAdd {m : ℕ} {α : Sort u_1} {n : ℕ} (u : Fin m → α) (v : Fin n → α) (j k : Fin m) : append u v ∘ ⇑(Equiv.swap (castAdd n j) (castAdd n k)) = append (u ∘ ⇑(Equiv.swap j k)) v

Exchanging two entries of Fin.append u v at positions of u is appending v to u with those entries exchanged.

theorem Fin.append_comp_swap_natAdd {m : ℕ} {α : Sort u_1} {n : ℕ} (u : Fin m → α) (v : Fin n → α) (j k : Fin n) : append u v ∘ ⇑(Equiv.swap (natAdd m j) (natAdd m k)) = append u (v ∘ ⇑(Equiv.swap j k))

Exchanging two entries of Fin.append u v at positions of v is prepending u to v with those entries exchanged.

theorem Fin.tail_contractNth_succ {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin (n + 1)) (a : Fin (n + 2) → α) : tail (j.succ.contractNth op a) = j.contractNth op (tail a)

Contracting two adjacent entries after the first commutes with dropping the first entry.

theorem Fin.init_contractNth_castSucc {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin (n + 1)) (a : Fin (n + 2) → α) : init (j.castSucc.contractNth op a) = j.contractNth op (init a)

Contracting two adjacent entries before the last commutes with dropping the last entry.

theorem Fin.contractNth_zero_cons {α : Sort u_1} {n : ℕ} (op : α → α → α) (x : α) (a : Fin (n + 1) → α) : contractNth 0 op (cons x a) = cons (op x (a 0)) (tail a)

Contracting the first two entries of Fin.cons x a combines x with the first entry of a under op.

theorem Fin.contractNth_succ_cons {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin (n + 1)) (x : α) (a : Fin (n + 1) → α) : j.succ.contractNth op (cons x a) = cons x (j.contractNth op a)

Contracting two entries of Fin.cons x a other than the first contracts a.

theorem Fin.init_contractNth_castSucc_last {α : Sort u_1} {n : ℕ} (op : α → α → α) (a : Fin (n + 2) → α) : init ((last n).castSucc.contractNth op a) = init (init a)

Contracting the last two entries and dropping the last one drops the last two entries.

@[simp]

theorem Fin.contractNth_last {α : Sort u_1} {n : ℕ} (op : α → α → α) (a : Fin (n + 1) → α) : (last n).contractNth op a = init a

Contracting at the last position, which has no successor, drops the last entry.

@[simp]

theorem Fin.contractNth_castSucc_castSucc_apply_last {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin n) (a : Fin (n + 2) → α) : j.castSucc.castSucc.contractNth op a (last n) = a (last (n + 1))

A contraction not involving the last entry keeps the last entry.

@[simp]

theorem Fin.contractNth_castSucc_last_apply_last {α : Sort u_1} {n : ℕ} (op : α → α → α) (a : Fin (n + 2) → α) : (last n).castSucc.contractNth op a (last n) = op (a (last n).castSucc) (a (last (n + 1)))

Contracting the last two entries makes their product the last entry.

theorem Fin.contractNth_castSucc_castSucc_snoc {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin n) (a : Fin (n + 1) → α) (x : α) : j.castSucc.castSucc.contractNth op (snoc a x) = snoc (j.castSucc.contractNth op a) x

Contracting two entries of Fin.snoc a x other than the last contracts a.

theorem Fin.contractNth_castSucc_last_snoc {α : Sort u_1} {n : ℕ} (op : α → α → α) (a : Fin (n + 1) → α) (x : α) : (last n).castSucc.contractNth op (snoc a x) = snoc (init a) (op (a (last n)) x)

Contracting the last two entries of Fin.snoc a x combines the last entry of a with x under op.

theorem Fin.contractNth_castSucc_eq_update_removeNth_succ {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin (n + 1)) (a : Fin (n + 2) → α) : j.castSucc.contractNth op a = Function.update (j.succ.removeNth a) j (op (a j.castSucc) (a j.succ))

Contracting the entries j and j + 1 is deleting entry j + 1 and then overwriting entry j by the contraction.

theorem Fin.contractNth_castSucc_const {α : Sort u_1} {n : ℕ} (op : α → α → α) (j : Fin n) (x : α) : (j.castSucc.contractNth op fun (x_1 : Fin (n + 1)) => x) = Function.update (fun (x_1 : Fin n) => x) j (op x x)

Contracting two adjacent entries of a constant tuple overwrites one entry of the shorter constant tuple by the contraction.

theorem Fin.update_removeNth_succ_eq_removeNth_castSucc {α : Sort u_1} {n : ℕ} (j : Fin (n + 1)) (a : Fin (n + 2) → α) : Function.update (j.succ.removeNth a) j (a j.succ) = j.castSucc.removeNth a

Deleting entry j + 1 and then overwriting entry j by the deleted entry is deleting entry j.

@[simp]

theorem Fin.insertNth_apply_zero_of_ne_zero {β : Type u_2} {n : ℕ} {p : Fin (n + 2)} (hp : p ≠ 0) (v : β) (x : Fin (n + 1) → β) : p.insertNth v x 0 = x 0

Inserting at a position other than the first keeps the first entry.

@[simp]

theorem Fin.insertNth_apply_last_of_ne_last {β : Type u_2} {n : ℕ} {p : Fin (n + 2)} (hp : p ≠ last (n + 1)) (v : β) (x : Fin (n + 1) → β) : p.insertNth v x (last (n + 1)) = x (last n)

Inserting at a position other than the last keeps the last entry.

theorem Fin.contractNth_castSucc_insertNth_succ_castSucc {β : Sort u_2} {γ : Sort u_3} {n : ℕ} (op : γ → γ → γ) (l : Fin n) (f : Fin (n + 1) → β → β → γ) (x : Fin (n + 1) → β) (v : β) : (l.castSucc.contractNth op fun (k : Fin (n + 1)) => f k (l.succ.castSucc.insertNth v x k.castSucc) (l.succ.castSucc.insertNth v x k.succ)) = Function.update (fun (k : Fin n) => f (l.succ.succAbove k) (x k.castSucc) (x k.succ)) l (op (f l.castSucc (x l.castSucc) v) (f l.succ v (x l.succ)))

Contracting along a path with an inserted vertex. Let f k be a function of the two endpoints of the k-th step of a path. Along the path obtained from x by inserting v after xₗ, contracting the steps l and l + 1 gives the entries f ((l + 1).succAbove k) read along x, except in position l, which holds op (f l xₗ v) (f (l + 1) v xₗ₊₁).

theorem Fin.removeNth_succ_cons {α : Sort u_1} {n : ℕ} (j : Fin (n + 1)) (x : α) (a : Fin (n + 1) → α) : j.succ.removeNth (cons x a) = cons x (j.removeNth a)

Deleting an entry of Fin.cons x a other than the first deletes the corresponding entry of a.

@[simp]

theorem Fin.image_cons_le_eq_insert {m : ℕ} {α : Type u_2} {n : ℕ} (x : α) (p : Fin m → α) : cons x p '' {index : Fin (m + 1) | ↑index ≤ n} = insert x (p '' {index : Fin m | ↑index < n})

The image of the first n + 1 entries of a prepended tuple consists of its first entry and the image of the first n entries of its tail.

theorem Fin.insertNth_one_ne_zero {α : Type u_2} [Zero α] [One α] [NeZero 1] {n : ℕ} (i : Fin (n + 1)) (z : Fin n → α) : i.insertNth 1 z ≠ 0

Inserting the entry 1 into a tuple gives a tuple that does not vanish.

theorem Fin.injective_apply_zero_one_two {α : Type u_2} : Function.Injective fun (x : Fin 3 → α) => (x 0, x 1, x 2)

A tuple of length three is determined by its three entries.

theorem Fin.eq_of_injective_comp_succAbove {α : Sort u_1} {n : ℕ} {b : Fin (n + 1) → α} {q : Fin (n + 1)} (hq : Function.Injective (b ∘ q.succAbove)) {i j : Fin (n + 1)} (hi : i ≠ q) (hj : j ≠ q) (h : b i = b j) : i = j

If deleting the entry at q leaves an injective tuple, two positions other than q holding the same entry are equal.

theorem Fin.injective_comp_succAbove_of_eq {α : Sort u_1} {n : ℕ} {b : Fin (n + 1) → α} {p q : Fin (n + 1)} (h : b p = b q) (hp : Function.Injective (b ∘ p.succAbove)) : Function.Injective (b ∘ q.succAbove)

If b p = b q, deleting the entry at p leaves an injective tuple exactly when deleting the entry at q does.

theorem Fin.range_comp_succAbove_of_eq {α : Type u_2} {n : ℕ} {b : Fin (n + 1) → α} {p q : Fin (n + 1)} (hpq : p ≠ q) (h : b p = b q) : Set.range (b ∘ p.succAbove) = Set.range b

If b p = b q for p ≠ q, deleting the entry at p does not change the set of entries.

theorem Fin.existsUnique_isLeft_castSucc_and_isRight_succ {α : Type u_2} {β : Type u_3} {n : ℕ} (x : Fin (n + 1) → α ⊕ β) (h0 : (x 0).isLeft = true) (hlast : (x (last n)).isRight = true) (hstep : ∀ (l : Fin n), (x l.castSucc).isRight = true → (x l.succ).isRight = true) : ∃! l : Fin n, (x l.castSucc).isLeft = true ∧ (x l.succ).isRight = true

A tuple in α ⊕ β that starts in α, ends in β and never steps from β back to α steps from α to β at exactly one position.