theorem Fin.le_antisymm_iff {n : Nat} {x : Fin n} {y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x

theorem Fin.le_antisymm {n : Nat} {x : Fin n} {y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x = y

clamp

@[simp]

theorem Fin.coe_clamp (n : Nat) (m : Nat) : ↑(Fin.clamp n m) = min n m

enum/list

@[simp]

theorem Fin.size_enum (n : Nat) : (Fin.enum n).size = n

@[simp]

theorem Fin.getElem_enum {n : Nat} (i : Nat) (h : i < (Fin.enum n).size) : (Fin.enum n)[i] = ⟨i, ⋯⟩

@[simp]

theorem Fin.length_list (n : Nat) : (Fin.list n).length = n

@[simp]

theorem Fin.get_list {n : Nat} (i : Fin (Fin.list n).length) : (Fin.list n).get i = Fin.cast ⋯ i

@[simp]

theorem Fin.list_zero : Fin.list 0 = []

theorem Fin.list_succ (n : Nat) : Fin.list (n + 1) = 0 :: List.map Fin.succ (Fin.list n)

foldl

theorem Fin.foldl_loop_lt {α : Sort u_1} {n : Nat} {m : Nat} (f : α → Fin n → α) (x : α) (h : m < n) : Fin.foldl.loop n f x m = Fin.foldl.loop n f (f x ⟨m, h⟩) (m + 1)

theorem Fin.foldl_loop_eq {α : Sort u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldl.loop n f x n = x

theorem Fin.foldl_loop {α : Sort u_1} {n : Nat} {m : Nat} (f : α → Fin (n + 1) → α) (x : α) (h : m < n + 1) : Fin.foldl.loop (n + 1) f x m = Fin.foldl.loop n (fun (x : α) (i : Fin n) => f x i.succ) (f x ⟨m, h⟩) m

theorem Fin.foldl_zero {α : Sort u_1} (f : α → Fin 0 → α) (x : α) : Fin.foldl 0 f x = x

theorem Fin.foldl_succ {α : Sort u_1} {n : Nat} (f : α → Fin (n + 1) → α) (x : α) : Fin.foldl (n + 1) f x = Fin.foldl n (fun (x : α) (i : Fin n) => f x i.succ) (f x 0)

theorem Fin.foldl_eq_foldl_list {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldl n f x = List.foldl f x (Fin.list n)

foldr

theorem Fin.foldr_loop_zero {n : Nat} {α : Sort u_1} (f : Fin n → α → α) (x : α) : Fin.foldr.loop n f ⟨0, ⋯⟩ x = x

theorem Fin.foldr_loop_succ {n : Nat} {α : Sort u_1} {m : Nat} (f : Fin n → α → α) (x : α) (h : m < n) : Fin.foldr.loop n f ⟨m + 1, h⟩ x = Fin.foldr.loop n f ⟨m, ⋯⟩ (f ⟨m, h⟩ x)

theorem Fin.foldr_loop {n : Nat} {α : Sort u_1} {m : Nat} (f : Fin (n + 1) → α → α) (x : α) (h : m + 1 ≤ n + 1) : Fin.foldr.loop (n + 1) f ⟨m + 1, h⟩ x = f 0 (Fin.foldr.loop n (fun (i : Fin n) => f i.succ) ⟨m, ⋯⟩ x)

theorem Fin.foldr_succ {n : Nat} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : Fin.foldr (n + 1) f x = f 0 (Fin.foldr n (fun (i : Fin n) => f i.succ) x)

theorem Fin.foldr_eq_foldr_list {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : Fin.foldr n f x = List.foldr f x (Fin.list n)