Lemmas on Fin and Fin-indexed tuples

We define operations on Fin and Fin-indexed tuples that are needed for Starlib.

theorem funext_heq_iff {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (x : α) → β x} {g : (x : α') → β' x} (ha : α = α') (hb : ∀ (x : α), β x = β' (cast ha x)) : f ≍ g ↔ ∀ (x : α), f x ≍ g (cast ha x)

Version of funext_iff for dependent functions f : (x : α) → β x and g : (x : α') → β' x.

theorem funext_heq {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (x : α) → β x} {g : (x : α') → β' x} (ha : α = α') (hb : ∀ (x : α), β x = β' (cast ha x)) : (∀ (x : α), f x ≍ g (cast ha x)) → f ≍ g

Alias of the reverse direction of funext_heq_iff.

---

Version of funext_iff for dependent functions f : (x : α) → β x and g : (x : α') → β' x.

theorem funext₂_iff {α : Sort u} {β : α → Sort v} {γ : (a : α) → β a → Sort w} {f g : (a : α) → (b : β a) → γ a b} : f = g ↔ ∀ (a : α) (b : β a), f a b = g a b

theorem funext₂_heq_iff {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {γ : (a : α) → β a → Sort w} {γ' : (a : α') → β' a → Sort w} {f : (a : α) → (b : β a) → γ a b} {g : (a : α') → (b : β' a) → γ' a b} (ha : α = α') (hb : ∀ (a : α), β a = β' (cast ha a)) (hc : ∀ (a : α) (b : β a), γ a b = γ' (cast ha a) (cast ⋯ b)) : f ≍ g ↔ ∀ (a : α) (b : β a), f a b ≍ g (cast ha a) (cast ⋯ b)

Version of funext₂_iff for heterogeneous equality.

theorem funext₂_heq {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {γ : (a : α) → β a → Sort w} {γ' : (a : α') → β' a → Sort w} {f : (a : α) → (b : β a) → γ a b} {g : (a : α') → (b : β' a) → γ' a b} (ha : α = α') (hb : ∀ (a : α), β a = β' (cast ha a)) (hc : ∀ (a : α) (b : β a), γ a b = γ' (cast ha a) (cast ⋯ b)) : (∀ (a : α) (b : β a), f a b ≍ g (cast ha a) (cast ⋯ b)) → f ≍ g

Alias of the reverse direction of funext₂_heq_iff.

---

Version of funext₂_iff for heterogeneous equality.

theorem Fin.heq_fun_iff' {k l : ℕ} {α : Fin k → Sort u} {β : Fin l → Sort u} (h : k = l) (h' : ∀ (i : Fin k), α i = β (Fin.cast h i)) {f : (i : Fin k) → α i} {g : (j : Fin l) → β j} : f ≍ g ↔ ∀ (i : Fin k), f i ≍ g (Fin.cast h i)

Version of Fin.heq_fun_iff for dependent functions f : (i : Fin k) → α i.

@[simp]

theorem Fin.cast_val {m n : ℕ} (h : m = n) (a : Fin m) : ↑(Fin.cast h a) = ↑a

Casting a Fin doesn't change its value.

@[simp]

theorem Fin.induction_one {motive : Fin 2 → Sort u_1} {zero : motive 0} {succ : (i : Fin 1) → motive i.castSucc → motive i.succ} : induction zero succ (last 1) = succ 0 zero

@[simp]

theorem Fin.induction_one' {motive : Fin 2 → Sort u_1} {zero : motive 0} {succ : (i : Fin 1) → motive i.castSucc → motive i.succ} : induction zero succ 1 = succ 0 zero

Alternate version of Fin.induction_one that uses 1 : Fin 2 instead of last 1.

@[simp]

theorem Fin.induction_two {motive : Fin 3 → Sort u_1} {zero : motive 0} {succ : (i : Fin 2) → motive i.castSucc → motive i.succ} : induction zero succ (last 2) = succ 1 (succ 0 zero)

@[simp]

theorem Fin.induction_two' {motive : Fin 3 → Sort u_1} {zero : motive 0} {succ : (i : Fin 2) → motive i.castSucc → motive i.succ} : induction zero succ 2 = succ 1 (succ 0 zero)

Alternate version of Fin.induction_two that uses 2 : Fin 3 instead of last 2.

theorem Fin.induction_heq {n n' : ℕ} {motive : Fin (n + 1) → Sort u} {motive' : Fin (n' + 1) → Sort u} {zero : motive 0} {zero' : motive' 0} {succ : (i : Fin n) → motive i.castSucc → motive i.succ} {succ' : (i : Fin n') → motive' i.castSucc → motive' i.succ} {i : Fin (n + 1)} {i' : Fin (n' + 1)} (hn : n = n') (hmotive : motive ≍ motive') (hzero : zero ≍ zero') (hsucc : succ ≍ succ') (hi : i ≍ i') : induction zero succ i ≍ induction zero' succ' i'

Heterogeneous equality on Fin.induction

theorem Fin.induction_init {n : ℕ} {motive : Fin (n + 2) → Sort u_1} {zero : motive 0} {succ : (i : Fin (n + 1)) → motive i.castSucc → motive i.succ} {i : Fin (n + 1)} : induction zero succ i.castSucc = induction zero (fun (j : Fin n) (x : init motive j.castSucc) => succ j.castSucc x) i

theorem Fin.induction_tail {n : ℕ} {motive : Fin (n + 2) → Sort u_1} {zero : motive 0} {succ : (i : Fin (n + 1)) → motive i.castSucc → motive i.succ} {i : Fin (n + 1)} : induction zero succ i.succ = induction (succ 0 zero) (fun (j : Fin n) (x : tail motive j.castSucc) => succ j.succ x) i

theorem Fin.induction_append_left {m n : ℕ} {motive : Fin (m + n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin (m + n)) → motive i.castSucc → motive i.succ} {i : Fin (m + 1)} : induction zero succ ⟨↑i, ⋯⟩ = induction zero (fun (j : Fin m) (x : (fun (j : Fin (m + 1)) => motive ⟨↑j, ⋯⟩) j.castSucc) => succ ⟨↑j, ⋯⟩ x) i

Fin.induction on m + n for i ≤ m steps is equivalent to Fin.induction on m for i steps.

theorem Fin.induction_append_right {m n : ℕ} {motive : Fin (m + n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin (m + n)) → motive i.castSucc → motive i.succ} {i : Fin (n + 1)} : induction zero succ (natAdd m i) = induction (induction zero (fun (j : Fin m) (x : (fun (j : Fin (m + 1)) => motive (Fin.cast ⋯ (castAdd n j))) j.castSucc) => succ (castAdd n j) x) (last m)) (fun (i : Fin n) (x : (fun (i : Fin (n + 1)) => motive (natAdd m i)) i.castSucc) => succ (natAdd m i) x) i

Fin.induction on m + n for m + i steps is equivalent to Fin.induction on n on i steps on the result of Fin.induction on m.

theorem Fin.insertNth_zero_eq_cases {n : ℕ} {α : Fin (n + 1) → Sort u} : insertNth 0 = cases

Fin.insertNth 0 is equivalent to Fin.cases.

@[simp]

theorem Fin.append_zero_of_succ_left {m n : ℕ} {α : Sort u_1} {u : Fin (m + 1) → α} {v : Fin n → α} : append u v 0 = u 0

@[simp]

theorem Fin.append_last_of_succ_right {m n : ℕ} {α : Sort u_1} {u : Fin m → α} {v : Fin (n + 1) → α} : append u v (last (m + n)) = v (last n)

theorem Fin.append_comp {m n : ℕ} {α : Sort u_1} {β : Sort u_2} {a : Fin m → α} {b : Fin n → α} (f : α → β) : append (f ∘ a) (f ∘ b) = f ∘ append a b

theorem Fin.append_comp' {m n : ℕ} {α : Sort u_1} {β : Sort u_2} {a : Fin m → α} {b : Fin n → α} (f : α → β) (i : Fin (m + n)) : append (f ∘ a) (f ∘ b) i = f (append a b i)

theorem Fin.addCases_left' {m n : ℕ} {motive : Fin (m + n) → Sort u_3} {left : (i : Fin m) → motive (castAdd n i)} {right : (j : Fin n) → motive (natAdd m j)} {i : Fin m} (j : Fin (m + n)) (h : j = castAdd n i) : addCases left right j = ⋯ ▸ left i

theorem Fin.addCases_right' {m n : ℕ} {motive : Fin (m + n) → Sort u_3} {left : (i : Fin m) → motive (castAdd n i)} {right : (j : Fin n) → motive (natAdd m j)} {i : Fin n} (j : Fin (m + n)) (h : j = natAdd m i) : addCases left right j = ⋯ ▸ right i

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

theorem Fin.append_left_of_lt {m n : ℕ} {α : Sort u_1} {u : Fin m → α} {v : Fin n → α} (j : ℕ) (h : j < m + n) (hlt : j < m) : append u v ⟨j, h⟩ = u ⟨j, hlt⟩

theorem Fin.append_right_of_not_lt {m n : ℕ} {α : Sort u_1} {u : Fin m → α} {v : Fin n → α} (j : ℕ) (h : j < m + n) (hge : ¬j < m) : append u v ⟨j, h⟩ = v ⟨j - m, ⋯⟩

theorem Fin.append_left_injective {m n : ℕ} {α : Sort u_1} (b : Fin n → α) : Function.Injective fun (x : Fin m → α) => append x b

theorem Fin.append_right_injective {m n : ℕ} {α : Sort u_1} (a : Fin m → α) : Function.Injective (append a)

def Fin.addCases' {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (left : (i : Fin m) → α i) (right : (j : Fin n) → β j) (i : Fin (m + n)) : append α β i

Version of Fin.addCases that splits the motive into two dependent vectors α and β, and the return type is Fin.append α β.

@[simp]

theorem Fin.addCases'_left {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (left : (i : Fin m) → α i) (right : (j : Fin n) → β j) (i : Fin m) : addCases' left right (castAdd n i) = ⋯ ▸ left i

@[simp]

theorem Fin.addCases'_right {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (left : (i : Fin m) → α i) (right : (j : Fin n) → β j) (i : Fin n) : addCases' left right (natAdd m i) = ⋯ ▸ right i

def Fin.castSum (l : List ℕ) {n : ℕ} (h : n ∈ l) : Fin n → Fin l.sum

theorem Fin.castSum_castLT {l' : List ℕ} {i : ℕ} (j : Fin i) : castSum (i :: l') ⋯ j = j.castLT ⋯

theorem Fin.castSum_castAdd {n m : ℕ} (i : Fin n) : castSum [n, m] ⋯ i = castAdd m i

def Fin.sumCases {l : List ℕ} {motive : Fin l.sum → Sort u_1} (cases : (n : ℕ) → (h : n ∈ l) → (i : Fin n) → motive (castSum l h i)) (i : Fin l.sum) : motive i

def Fin.finSuccEquivNth' {n : ℕ} (i : Fin n) : Fin n ≃ Option (Fin (n - 1))