foldl/foldr

theorem Fin.foldl_assoc {α : Sort u_1} {n : Nat} {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂ : α} : foldl n (fun (x : α) (i : Fin n) => op x (f i)) (op a₁ a₂) = op a₁ (foldl n (fun (x : α) (i : Fin n) => op x (f i)) a₂)

theorem Fin.foldr_assoc {α : Sort u_1} {n : Nat} {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂ : α} : foldr n (fun (i : Fin n) (x : α) => op (f i) x) (op a₁ a₂) = op (foldr n (fun (i : Fin n) (x : α) => op (f i) x) a₁) a₂

clamp

@[simp]

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

findSome?

@[simp]

theorem Fin.findSome?_zero {α : Type u_1} {f : Fin 0 → Option α} : findSome? f = none

@[simp]

theorem Fin.findSome?_one {α : Type u_1} {f : Fin 1 → Option α} : findSome? f = f 0

theorem Fin.findSome?_succ {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} : findSome? f = (f 0 <|> findSome? fun (i : Fin n) => f i.succ)

theorem Fin.findSome?_succ_of_some {n : Nat} {α : Type u_1} {x : α} {f : Fin (n + 1) → Option α} (h : f 0 = some x) : findSome? f = some x

theorem Fin.findSome?_succ_of_isSome {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} (h : (f 0).isSome = true) : findSome? f = f 0

theorem Fin.findSome?_succ_of_none {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} (h : f 0 = none) : findSome? f = findSome? fun (i : Fin n) => f i.succ

theorem Fin.findSome?_succ_of_isNone {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} (h : (f 0).isNone = true) : findSome? f = findSome? fun (i : Fin n) => f i.succ

@[simp]

theorem Fin.findSome?_eq_some_iff {n : Nat} {α : Type u_1} {a : α} {f : Fin n → Option α} : findSome? f = some a ↔ ∃ (i : Fin n), f i = some a ∧ ∀ (j : Fin n), j < i → f j = none

@[simp]

theorem Fin.findSome?_eq_none_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : findSome? f = none ↔ ∀ (i : Fin n), f i = none

theorem Fin.isNone_findSome?_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true

@[deprecated Fin.isNone_findSome?_iff (since := "2025-09-28")]

theorem Fin.findSome?_isNone_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true

Alias of Fin.isNone_findSome?_iff.

@[simp]

theorem Fin.isSome_findSome?_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? f).isSome = true ↔ ∃ (i : Fin n), (f i).isSome = true

@[deprecated Fin.isSome_findSome?_iff (since := "2025-09-28")]

theorem Fin.findSome?_isSome_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? f).isSome = true ↔ ∃ (i : Fin n), (f i).isSome = true

Alias of Fin.isSome_findSome?_iff.

theorem Fin.exists_minimal_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin n → Option α} (h : findSome? f = some x) : ∃ (i : Fin n), f i = some x ∧ ∀ (j : Fin n), j < i → f j = none

theorem Fin.exists_eq_some_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin n → Option α} (h : findSome? f = some x) : ∃ (i : Fin n), f i = some x

@[deprecated Fin.exists_eq_some_of_findSome?_eq_some (since := "2025-09-28")]

theorem Fin.exists_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin n → Option α} (h : findSome? f = some x) : ∃ (i : Fin n), f i = some x

Alias of Fin.exists_eq_some_of_findSome?_eq_some.

theorem Fin.eq_none_of_findSome?_eq_none {n : Nat} {α : Type u_1} {f : Fin n → Option α} (h : findSome? f = none) (i : Fin n) : f i = none

theorem Fin.exists_isSome_of_isSome_findSome? {n : Nat} {α : Type u_1} {f : Fin n → Option α} (h : (findSome? f).isSome = true) : ∃ (i : Fin n), (f i).isSome = true

theorem Fin.isNone_of_isNone_findSome? {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin n → Option α} (h : (findSome? f).isNone = true) : (f i).isNone = true

theorem Fin.isSome_findSome?_of_isSome {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin n → Option α} (h : (f i).isSome = true) : (findSome? f).isSome = true

theorem Fin.map_findSome? {n : Nat} {α : Type u_1} {β : Type u_2} (f : Fin n → Option α) (g : α → β) : Option.map g (findSome? f) = findSome? fun (x : Fin n) => Option.map g (f x)

theorem Fin.findSome?_guard {n : Nat} {p : Fin n → Bool} : findSome? (Option.guard p) = find? p

theorem Fin.findSome?_eq_findSome?_finRange {n : Nat} {α : Type u_1} (f : Fin n → Option α) : findSome? f = List.findSome? f (List.finRange n)

Fin.find?

@[simp]

theorem Fin.find?_zero {p : Fin 0 → Bool} : find? p = none

@[simp]

theorem Fin.find?_one {p : Fin 1 → Bool} : find? p = if p 0 = true then some 0 else none

theorem Fin.find?_succ {n : Nat} {p : Fin (n + 1) → Bool} : find? p = if p 0 = true then some 0 else Option.map succ (find? fun (i : Fin n) => p i.succ)

@[simp]

theorem Fin.find?_eq_some_iff {n : Nat} {i : Fin n} {p : Fin n → Bool} : find? p = some i ↔ p i = true ∧ ∀ (j : Fin n), j < i → p j = false

theorem Fin.isSome_find?_iff {n : Nat} {p : Fin n → Bool} : (find? p).isSome = true ↔ ∃ (i : Fin n), p i = true

@[deprecated Fin.isSome_find?_iff (since := "2025-09-28")]

theorem Fin.find?_isSome_iff {n : Nat} {p : Fin n → Bool} : (find? p).isSome = true ↔ ∃ (i : Fin n), p i = true

Alias of Fin.isSome_find?_iff.

@[simp]

theorem Fin.find?_eq_none_iff {n : Nat} {p : Fin n → Bool} : find? p = none ↔ ∀ (i : Fin n), p i = false

theorem Fin.isNone_find?_iff {n : Nat} {p : Fin n → Bool} : (find? p).isNone = true ↔ ∀ (i : Fin n), p i = false

@[deprecated Fin.isNone_find?_iff (since := "2025-09-28")]

theorem Fin.find?_isNone_iff {n : Nat} {p : Fin n → Bool} : (find? p).isNone = true ↔ ∀ (i : Fin n), p i = false

Alias of Fin.isNone_find?_iff.

theorem Fin.eq_true_of_find?_eq_some {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : find? p = some i) : p i = true

theorem Fin.eq_false_of_find?_eq_some_of_lt {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : find? p = some i) (j : Fin n) : j < i → p j = false

theorem Fin.eq_false_of_find?_eq_none {n : Nat} {p : Fin n → Bool} (h : find? p = none) (i : Fin n) : p i = false

theorem Fin.exists_eq_true_of_isSome_find? {n : Nat} {p : Fin n → Bool} (h : (find? p).isSome = true) : ∃ (i : Fin n), p i = true

theorem Fin.eq_false_of_isNone_find? {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : (find? p).isNone = true) : p i = false

theorem Fin.isSome_find?_of_eq_true {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : p i = true) : (find? p).isSome = true

theorem Fin.get_find?_eq_true {n : Nat} {p : Fin n → Bool} (h : (find? p).isSome = true) : p ((find? p).get h) = true

theorem Fin.get_find?_minimal {n : Nat} {p : Fin n → Bool} (h : (find? p).isSome = true) (j : Fin n) : j < (find? p).get h → p j = false

theorem Fin.find?_eq_find?_finRange {n : Nat} {p : Fin n → Bool} : find? p = List.find? p (List.finRange n)

exists

theorem Fin.exists_eq_true_iff_exists_minimal_eq_true {n : Nat} (p : Fin n → Bool) : (∃ (i : Fin n), p i = true) ↔ ∃ (i : Fin n), p i = true ∧ ∀ (j : Fin n), j < i → p j = false

theorem Fin.exists_iff_exists_minimal {n : Nat} (p : Fin n → Prop) [DecidablePred p] : (∃ (i : Fin n), p i) ↔ ∃ (i : Fin n), p i ∧ ∀ (j : Fin n), j < i → ¬p j

divNat / modNat / mkDivMod

@[simp]

theorem Fin.coe_divNat {m n : Nat} (i : Fin (m * n)) : ↑i.divNat = ↑i / n

@[simp]

theorem Fin.coe_modNat {m n : Nat} (i : Fin (m * n)) : ↑i.modNat = ↑i % n

@[simp]

theorem Fin.coe_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) : ↑(i.mkDivMod j) = n * ↑i + ↑j

@[simp]

theorem Fin.divNat_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) : (i.mkDivMod j).divNat = i

@[simp]

theorem Fin.modNat_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) : (i.mkDivMod j).modNat = j

@[simp]

theorem Fin.divNat_mkDivMod_modNat {m n : Nat} (k : Fin (m * n)) : k.divNat.mkDivMod k.modNat = k