Operation on tuples

We interpret maps ∀ i : Fin n, α i∀ 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.

We define the following operations:

• Fin.tail : the tail of an n+1 tuple, i.e., its last n entries;
• Fin.cons : adding an element at the beginning of an n-tuple, to get an n+1-tuple;
• Fin.init : the beginning of an n+1 tuple, i.e., its first n entries;
• Fin.snoc : 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.
• Fin.insertNth : insert an element to a tuple at a given position.
• Fin.find p : returns the first index n where p n is satisfied, and none if it is never satisfied.
• Fin.append a b : append two tuples.
• Fin.repeat n a : repeat a tuple n times.

ink

@[simp]

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

ink

def Fin.tail {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) : α (Fin.succ i)

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

Equations

• Fin.tail q i = q (Fin.succ i)

ink

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

ink

def Fin.cons {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α (Fin.succ i)) (i : Fin (n + 1)) : α i

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

Equations

• Fin.cons x p j = Fin.cases x p j

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

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

ink

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

As a binary function, Fin.cons is injective.

ink

@[simp]

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

ink

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

ink

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

ink

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

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

ink

@[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

ink

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

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

Equations

• Fin.consCases h x = cast (_ : P (Fin.cons (x 0) (Fin.tail x)) = P x) (h (x 0) (Fin.tail x))

ink

@[simp]

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

ink

def Fin.consInduction {α : Type u_1} {P : {n : ℕ} → (Fin n → α) → Sort v} (h0 : P 0 Fin.elim0) (h : {n : ℕ} → (x₀ : α) → (x : Fin n → α) → P n x → P (n + 1) (Fin.cons x₀ x)) {n : ℕ} (x : Fin n → α) : P n x

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

Equations

• Fin.consInduction h0 h x_2 = Eq.mpr (_ : P 0 x_2 = P 0 Fin.elim0) h0
• Fin.consInduction h0 h x_2 = Fin.consCases (fun x₀ x => h n x₀ x (Fin.consInduction h0 (fun {n} => h n) x)) x_2

ink

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 (Fin.cons x₀ x)

ink

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

ink

@[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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

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

ink

@[simp]

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

Updating a nonzero element and taking the tail commute.

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

theorem Fin.pi_lex_lt_cons_cons {n : ℕ} {α : Fin (n + 1) → Type u} {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α (Fin.succ i)} {y : (i : Fin n) → α (Fin.succ i)} (s : {i : Fin (Nat.succ n)} → α i → α i → Prop) : Pi.Lex (fun x x_1 => x < x_1) s (Fin.cons x₀ x) (Fin.cons y₀ y) ↔ s 0 x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i => s (Fin.succ i)) x y

ink

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

ink

@[simp]

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

ink

def Fin.append {m : ℕ} {n : ℕ} {α : Type 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.

Equations

• Fin.append a b = Fin.addCases a b

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Fin.append_right_nil {m : ℕ} {n : ℕ} {α : Type u_1} (u : Fin m → α) (v : Fin n → α) (hv : n = 0) : Fin.append u v = u ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n = m))).toEmbedding

ink

@[simp]

theorem Fin.append_elim0' {m : ℕ} {α : Type u_1} (u : Fin m → α) : Fin.append u Fin.elim0' = u ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + 0 = m))).toEmbedding

ink

theorem Fin.append_left_nil {m : ℕ} {n : ℕ} {α : Type u_1} (u : Fin m → α) (v : Fin n → α) (hu : m = 0) : Fin.append u v = v ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n = n))).toEmbedding

ink

@[simp]

theorem Fin.elim0'_append {n : ℕ} {α : Type u_1} (v : Fin n → α) : Fin.append Fin.elim0' v = v ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : 0 + n = n))).toEmbedding

ink

theorem Fin.append_assoc {m : ℕ} {n : ℕ} {p : ℕ} {α : Type u_1} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) : Fin.append (Fin.append a b) c = Fin.append a (Fin.append b c) ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n + p = m + (n + p)))).toEmbedding

ink

def Fin.repeat {n : ℕ} {α : Type 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].

Equations

• Fin.repeat m a x = let i := x; a (Fin.modNat i)

ink

@[simp]

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

ink

@[simp]

theorem Fin.repeat_zero {n : ℕ} {α : Type u_1} (a : Fin n → α) : Fin.repeat 0 a = Fin.elim0' ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : 0 * n = 0))).toEmbedding

ink

@[simp]

theorem Fin.repeat_one {n : ℕ} {α : Type u_1} (a : Fin n → α) : Fin.repeat 1 a = a ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : 1 * n = n))).toEmbedding

ink

theorem Fin.repeat_succ {n : ℕ} {α : Type u_1} (a : Fin n → α) (m : ℕ) : Fin.repeat (Nat.succ m) a = Fin.append a (Fin.repeat m a) ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : Nat.succ m * n = n + m * n))).toEmbedding

ink

@[simp]

theorem Fin.repeat_add {n : ℕ} {α : Type u_1} (a : Fin n → α) (m₁ : ℕ) (m₂ : ℕ) : Fin.repeat (m₁ + m₂) a = Fin.append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ ↑(RelIso.toRelEmbedding (Fin.cast (_ : (m₁ + m₂) * n = m₁ * n + m₂ * n))).toEmbedding

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.

ink

def Fin.init {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) : α (↑Fin.castSucc.toEmbedding i)

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

Equations

• Fin.init q i = q (↑Fin.castSucc.toEmbedding i)

ink

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

ink

def Fin.snoc {n : ℕ} {α : Fin (n + 1) → Type u} (p : (i : Fin n) → α (↑Fin.castSucc.toEmbedding i)) (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

• Fin.snoc p x i = if h : ↑i < n then cast (_ : α (↑Fin.castSucc.toEmbedding (Fin.castLt i h)) = α i) (p (Fin.castLt i h)) else cast (_ : α (Fin.last n) = α i) x

ink

@[simp]

theorem Fin.init_snoc {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α (↑Fin.castSucc.toEmbedding i)) : Fin.init (Fin.snoc p x) = p

ink

@[simp]

theorem Fin.snoc_cast_succ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α (↑Fin.castSucc.toEmbedding i)) (i : Fin n) : Fin.snoc p x (↑Fin.castSucc.toEmbedding i) = p i

ink

@[simp]

theorem Fin.snoc_comp_cast_succ {n : ℕ} {α : Type u_1} {a : α} {f : Fin n → α} : Fin.snoc f a ∘ ↑Fin.castSucc.toEmbedding = f

ink

@[simp]

theorem Fin.snoc_last {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α (↑Fin.castSucc.toEmbedding i)) : Fin.snoc p x (Fin.last n) = x

ink

@[simp]

theorem Fin.snoc_comp_nat_add {n : ℕ} {m : ℕ} {α : Type u_1} (f : Fin (m + n) → α) (a : α) : Fin.snoc f a ∘ ↑(Fin.natAdd m).toEmbedding = Fin.snoc (f ∘ ↑(Fin.natAdd m).toEmbedding) a

ink

@[simp]

theorem Fin.snoc_cast_add {m : ℕ} {n : ℕ} {α : Fin (n + m + 1) → Type u_1} (f : (i : Fin (n + m)) → α (↑Fin.castSucc.toEmbedding i)) (a : α (Fin.last (n + m))) (i : Fin n) : Fin.snoc f a (↑(Fin.castAdd (m + 1)).toEmbedding i) = f (↑(Fin.castAdd m).toEmbedding i)

ink

@[simp]

theorem Fin.snoc_comp_cast_add {n : ℕ} {m : ℕ} {α : Type u_1} (f : Fin (n + m) → α) (a : α) : Fin.snoc f a ∘ ↑(Fin.castAdd (m + 1)).toEmbedding = f ∘ ↑(Fin.castAdd m).toEmbedding

ink

@[simp]

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

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

ink

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

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

ink

@[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

ink

@[simp]

theorem Fin.init_update_last {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (z : α (Fin.last n)) : Fin.init (Function.update q (Fin.last n) z) = Fin.init q

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

ink

@[simp]

theorem Fin.init_update_castSucc {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α (↑Fin.castSucc.toEmbedding i)) : Fin.init (Function.update q (↑Fin.castSucc.toEmbedding i) y) = Function.update (Fin.init q) i y

Updating an element and taking the beginning commute.

ink

theorem Fin.tail_init_eq_init_tail {n : ℕ} {β : Type u_1} (q : Fin (n + 2) → β) : Fin.tail (Fin.init q) = Fin.init (Fin.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.

ink

theorem Fin.cons_snoc_eq_snoc_cons {n : ℕ} {β : Type u_1} (a : β) (q : Fin n → β) (b : β) : Fin.cons a (Fin.snoc q b) = Fin.snoc (Fin.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.

ink

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)

ink

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

ink

def Fin.succAboveCases {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding 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.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Fin.forall_iff_succAbove {n : ℕ} {p : Fin (n + 1) → Prop} (i : Fin (n + 1)) : ((j : Fin (n + 1)) → p j) ↔ p i ∧ ((j : Fin n) → p (↑(Fin.succAbove i).toEmbedding j))

ink

def Fin.insertNth {n : ℕ} {α : Fin (n + 1) → Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding 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.

Equations

• Fin.insertNth i x p j = Fin.succAboveCases i x p j

ink

@[simp]

theorem Fin.insertNth_apply_same {n : ℕ} {α : Fin (n + 1) → Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i x p i = x

ink

@[simp]

theorem Fin.insertNth_apply_succAbove {n : ℕ} {α : Fin (n + 1) → Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) (j : Fin n) : Fin.insertNth i x p (↑(Fin.succAbove i).toEmbedding j) = p j

ink

@[simp]

theorem Fin.succAbove_cases_eq_insertNth : @Fin.succAboveCases = @Fin.insertNth

ink

@[simp]

theorem Fin.insertNth_comp_succAbove {n : ℕ} {β : Type v} (i : Fin (n + 1)) (x : β) (p : Fin n → β) : Fin.insertNth i x p ∘ ↑(Fin.succAbove i).toEmbedding = p

ink

theorem Fin.insertNth_eq_iff {n : ℕ} {α : Fin (n + 1) → Type u} {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)} {q : (j : Fin (n + 1)) → α j} : Fin.insertNth i x p = q ↔ q i = x ∧ p = fun j => q (↑(Fin.succAbove i).toEmbedding j)

ink

theorem Fin.eq_insertNth_iff {n : ℕ} {α : Fin (n + 1) → Type u} {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)} {q : (j : Fin (n + 1)) → α j} : q = Fin.insertNth i x p ↔ q i = x ∧ p = fun j => q (↑(Fin.succAbove i).toEmbedding j)

ink

theorem Fin.insertNth_apply_below {n : ℕ} {α : Fin (n + 1) → Type u} {i : Fin (n + 1)} {j : Fin (n + 1)} (h : j < i) (x : α i) (p : (k : Fin n) → α (↑(Fin.succAbove i).toEmbedding k)) : Fin.insertNth i x p j = Eq.recOn (_ : ↑(Fin.succAbove i).toEmbedding (Fin.castLt j (_ : ↑j < n)) = j) (p (Fin.castLt j (_ : ↑j < n)))

ink

theorem Fin.insertNth_apply_above {n : ℕ} {α : Fin (n + 1) → Type u} {i : Fin (n + 1)} {j : Fin (n + 1)} (h : i < j) (x : α i) (p : (k : Fin n) → α (↑(Fin.succAbove i).toEmbedding k)) : Fin.insertNth i x p j = Eq.recOn (_ : ↑(Fin.succAbove i).toEmbedding (Fin.pred j (_ : j ≠ 0)) = j) (p (Fin.pred j (_ : j ≠ 0)))

ink

theorem Fin.insertNth_zero {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (j : Fin n) → α (↑(Fin.succAbove 0).toEmbedding j)) : Fin.insertNth 0 x p = Fin.cons x fun j => cast (_ : α (↑(Fin.succAbove 0).toEmbedding j) = α (Fin.succ j)) (p j)

ink

@[simp]

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

ink

theorem Fin.insertNth_last {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (j : Fin n) → α (↑(Fin.succAbove (Fin.last n)).toEmbedding j)) : Fin.insertNth (Fin.last n) x p = Fin.snoc (fun j => cast (_ : α (↑(Fin.succAbove (Fin.last n)).toEmbedding j) = α (↑Fin.castSucc.toEmbedding j)) (p j)) x

ink

@[simp]

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

ink

@[simp]

theorem Fin.insertNth_zero_right {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → Zero (α j)] (i : Fin (n + 1)) (x : α i) : Fin.insertNth i x 0 = Pi.single i x

ink

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

ink

@[simp]

theorem Fin.insertNth_mul {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) (q : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i (x * y) (p * q) = Fin.insertNth i x p * Fin.insertNth i y q

ink

@[simp]

theorem Fin.insertNth_add {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) (q : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i (x + y) (p + q) = Fin.insertNth i x p + Fin.insertNth i y q

ink

@[simp]

theorem Fin.insertNth_div {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) (q : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i (x / y) (p / q) = Fin.insertNth i x p / Fin.insertNth i y q

ink

@[simp]

theorem Fin.insertNth_sub {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) (q : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i (x - y) (p - q) = Fin.insertNth i x p - Fin.insertNth i y q

ink

@[simp]

theorem Fin.insertNth_sub_same {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)) : Fin.insertNth i x p - Fin.insertNth i y p = Pi.single i (x - y)

ink

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

ink

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

ink

theorem Fin.insertNth_mem_Icc {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (↑(Fin.succAbove i).toEmbedding j)} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} : Fin.insertNth i x p ∈ Set.Icc q₁ q₂ ↔ x ∈ Set.Icc (q₁ i) (q₂ i) ∧ p ∈ Set.Icc (fun j => q₁ (↑(Fin.succAbove i).toEmbedding j)) fun j => q₂ (↑(Fin.succAbove i).toEmbedding j)

ink

theorem Fin.preimage_insertNth_Icc_of_mem {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : x ∈ Set.Icc (q₁ i) (q₂ i)) : Fin.insertNth i x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun j => q₁ (↑(Fin.succAbove i).toEmbedding j)) fun j => q₂ (↑(Fin.succAbove i).toEmbedding j)

ink

theorem Fin.preimage_insertNth_Icc_of_not_mem {n : ℕ} {α : Fin (n + 1) → Type u} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : ¬x ∈ Set.Icc (q₁ i) (q₂ i)) : Fin.insertNth i x ⁻¹' Set.Icc q₁ q₂ = ∅

ink

def Fin.find {n : ℕ} (p : Fin n → Prop) [inst : DecidablePred p] : Option (Fin n)

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

Equations

• One or more equations did not get rendered due to their size.
• Fin.find _p = none

ink

theorem Fin.find_spec {n : ℕ} (p : Fin n → Prop) [inst : DecidablePred p] {i : Fin n} : i ∈ Fin.find p → p i

If find p = some i, then p i holds

ink

theorem Fin.isSome_find_iff {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] : Option.isSome (Fin.find p) = true ↔ ∃ i, p i

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

ink

theorem Fin.find_eq_none_iff {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] : Fin.find p = none ↔ ∀ (i : Fin n), ¬p i

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

ink

theorem Fin.find_min {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} : 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.

ink

theorem Fin.find_min' {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} (h : i ∈ Fin.find p) {j : Fin n} (hj : p j) : i ≤ j

ink

theorem Fin.nat_find_mem_find {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ i hin, p { val := i, isLt := hin }) : { val := Nat.find h, isLt := (_ : Nat.find h < n) } ∈ Fin.find p

ink

theorem Fin.mem_find_iff {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} : i ∈ Fin.find p ↔ p i ∧ ∀ (j : Fin n), p j → i ≤ j

ink

theorem Fin.find_eq_some_iff {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} : Fin.find p = some i ↔ p i ∧ ∀ (j : Fin n), p j → i ≤ j

ink

theorem Fin.mem_find_of_unique {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∀ (i j : Fin n), p i → p j → i = j) {i : Fin n} (hi : p i) : i ∈ Fin.find p

ink

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

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

ink

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

Fin.sigma_eq_of_eq_comp_cast as an iff.