clamp

@[simp]

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

foldlM

theorem Fin.foldlM_loop_lt {m : Type u_1 → Type u_2} {α : Type u_1} {n i : Nat} [Monad m] (f : α → Fin n → m α) (x : α) (h : i < n) : Fin.foldlM.loop n f x i = do let x ← f x ⟨i, h⟩ Fin.foldlM.loop n f x (i + 1)

theorem Fin.foldlM_loop_eq {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin n → m α) (x : α) : Fin.foldlM.loop n f x n = pure x

@[irreducible]

theorem Fin.foldlM_loop {m : Type u_1 → Type u_2} {α : Type u_1} {n i : Nat} [Monad m] (f : α → Fin (n + 1) → m α) (x : α) (h : i < n + 1) : Fin.foldlM.loop (n + 1) f x i = do let x ← f x ⟨i, h⟩ Fin.foldlM.loop n (fun (x : α) (j : Fin n) => f x j.succ) x i

@[simp]

theorem Fin.foldlM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : α → Fin 0 → m α) (x : α) : Fin.foldlM 0 f x = pure x

theorem Fin.foldlM_succ {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin (n + 1) → m α) (x : α) : Fin.foldlM (n + 1) f x = f x 0 >>= Fin.foldlM n fun (x : α) (j : Fin n) => f x j.succ

foldrM

theorem Fin.foldrM_loop_zero {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] (f : Fin n → α → m α) (x : α) : Fin.foldrM.loop n f ⟨0, ⋯⟩ x = pure x

theorem Fin.foldrM_loop_succ {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} {i : Nat} [Monad m] (f : Fin n → α → m α) (x : α) (h : i < n) : Fin.foldrM.loop n f ⟨i + 1, h⟩ x = f ⟨i, h⟩ x >>= Fin.foldrM.loop n f ⟨i, ⋯⟩

theorem Fin.foldrM_loop {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} {i : Nat} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) (x : α) (h : i + 1 ≤ n + 1) : Fin.foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = Fin.foldrM.loop n (fun (j : Fin n) => f j.succ) ⟨i, ⋯⟩ x >>= f 0

@[simp]

theorem Fin.foldrM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : Fin 0 → α → m α) (x : α) : Fin.foldrM 0 f x = pure x

theorem Fin.foldrM_succ {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) (x : α) : Fin.foldrM (n + 1) f x = Fin.foldrM n (fun (i : Fin n) => f i.succ) x >>= f 0

foldl

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

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

@[irreducible]

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

@[simp]

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_succ_last {α : Sort u_1} {n : Nat} (f : α → Fin (n + 1) → α) (x : α) : Fin.foldl (n + 1) f x = f (Fin.foldl n (fun (x1 : α) (x2 : Fin n) => f x1 x2.castSucc) x) (Fin.last n)

theorem Fin.foldl_eq_foldlM {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldl n f x = Fin.foldlM n f x

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} {i : Nat} (f : Fin n → α → α) (x : α) (h : i < n) : Fin.foldr.loop n f ⟨i + 1, h⟩ x = Fin.foldr.loop n f ⟨i, ⋯⟩ (f ⟨i, h⟩ x)

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

@[simp]

theorem Fin.foldr_zero {α : Sort u_1} (f : Fin 0 → α → α) (x : α) : Fin.foldr 0 f x = 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_succ_last {n : Nat} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : Fin.foldr (n + 1) f x = Fin.foldr n (fun (x : Fin n) => f x.castSucc) (f (Fin.last n) x)

theorem Fin.foldr_eq_foldrM {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : Fin.foldr n f x = Fin.foldrM n f x

theorem Fin.foldl_rev {n : Nat} {α : Sort u_1} (f : Fin n → α → α) (x : α) : Fin.foldl n (fun (x : α) (i : Fin n) => f i.rev x) x = Fin.foldr n f x

theorem Fin.foldr_rev {α : Sort u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldr n (fun (i : Fin n) (x : α) => f x i.rev) x = Fin.foldl n f x