### rev #

### foldl/foldr #

source
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₂)
source
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 #

source
@[simp]
theorem Fin.coe_clamp (n m : Nat) :
↑(clamp n m) = min n m

### findSome? #

source
@[simp]
theorem Fin.findSome?_zero {α : Type u_1} {f : Fin 0 → Option α} :
findSome? f = none
source
@[simp]
theorem Fin.findSome?_one {α : Type u_1} {f : Fin 1 → Option α} :
findSome? f = f 0
source
theorem Fin.findSome?_succ {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} :
findSome? f = (f 0).or (findSome? fun (x : Fin n) => f x.succ)
source
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
source
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
source
theorem Fin.findSome?_succ_of_none {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} (h : f 0 = none) :
findSome? f = findSome? fun (x : Fin n) => f x.succ
source
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 (x : Fin n) => f x.succ
source
@[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
source
@[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
source
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
source
@[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`.

source
@[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
source
@[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`.

source
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
source
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
source
@[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`.

source
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
source
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
source
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
source
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
source
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)
source
theorem Fin.findSome?_guard {n : Nat} {p : Fin n → Bool} :
findSome? (Option.guard p) = find? p
source
theorem Fin.bind_findSome?_guard_isSome {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSome? (Option.guard fun (i : Fin n) => (f i).isSome)).bind f = findSome? f
source
theorem Fin.findSome?_eq_findSome?_finRange {n : Nat} {α : Type u_1} (f : Fin n → Option α) :
findSome? f = List.findSome? f (List.finRange n)

### findSomeRev? #

source
@[simp]
theorem Fin.findSome?_rev {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSome? fun (x : Fin n) => f x.rev) = findSomeRev? f
source
@[simp]
theorem Fin.findSomeRev?_rev {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSomeRev? fun (x : Fin n) => f x.rev) = findSome? f
source
@[simp]
theorem Fin.findSomeRev?_zero {α : Type u_1} {f : Fin 0 → Option α} :
findSomeRev? f = none
source
@[simp]
theorem Fin.findSomeRev?_one {α : Type u_1} {f : Fin 1 → Option α} :
findSomeRev? f = f 0
source
theorem Fin.findSomeRev?_succ {n : Nat} {α : Type u_1} {f : Fin (n + 1) → Option α} :
findSomeRev? f = (f (last n)).or (findSomeRev? fun (i : Fin n) => f i.castSucc)
source
@[simp]
theorem Fin.findSomeRev?_eq_some_iff {n : Nat} {α : Type u_1} {a : α} {f : Fin n → Option α} :
findSomeRev? f = some a ↔ ∃ (i : Fin n), f i = some a ∧ ∀ (j : Fin n), i < j → f j = none
source
@[simp]
theorem Fin.findSomeRev?_eq_none_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
findSomeRev? f = none ↔ ∀ (i : Fin n), f i = none
source
theorem Fin.isNone_findSomeRev?_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSomeRev? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true
source
@[simp]
theorem Fin.isSome_findSomeRev?_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSomeRev? f).isSome = true ↔ ∃ (i : Fin n), (f i).isSome = true
source
theorem Fin.exists_minimal_of_findSomeRev?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin n → Option α} (h : findSomeRev? f = some x) :
∃ (i : Fin n), f i = some x ∧ ∀ (j : Fin n), i < j → f j = none
source
theorem Fin.exists_eq_some_of_findSomeRev?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin n → Option α} (h : findSomeRev? f = some x) :
∃ (i : Fin n), f i = some x
source
theorem Fin.eq_none_of_findSomeRev?_eq_none {n : Nat} {α : Type u_1} {f : Fin n → Option α} (h : findSomeRev? f = none) (i : Fin n) :
f i = none
source
theorem Fin.exists_isSome_of_isSome_findSomeRev? {n : Nat} {α : Type u_1} {f : Fin n → Option α} (h : (findSomeRev? f).isSome = true) :
∃ (i : Fin n), (f i).isSome = true
source
theorem Fin.isNone_of_isNone_findSomeRev? {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin n → Option α} (h : (findSomeRev? f).isNone = true) :
(f i).isNone = true
source
theorem Fin.isSome_findSomeRev?_of_isSome {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin n → Option α} (h : (f i).isSome = true) :
(findSomeRev? f).isSome = true
source
theorem Fin.map_findSomeRev? {n : Nat} {α : Type u_1} {β : Type u_2} (f : Fin n → Option α) (g : α → β) :
Option.map g (findSomeRev? f) = findSomeRev? fun (x : Fin n) => Option.map g (f x)
source
theorem Fin.findSomeRev?_guard {n : Nat} {p : Fin n → Bool} :
findSomeRev? (Option.guard p) = findRev? p
source
theorem Fin.bind_findSomeRev?_guard_isSome {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findSomeRev? (Option.guard fun (i : Fin n) => (f i).isSome)).bind f = findSomeRev? f

### find? #

source
theorem Fin.find?_zero {p : Fin 0 → Bool} :
find? p = none
source
theorem Fin.find?_one {p : Fin 1 → Bool} :
find? p = if p 0 = true then some 0 else none
source
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 (x : Fin n) => p x.succ)
source
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
source
theorem Fin.isSome_find?_iff {n : Nat} {p : Fin n → Bool} :
(find? p).isSome = true ↔ ∃ (i : Fin n), p i = true
source
@[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`.

source
theorem Fin.find?_eq_none_iff {n : Nat} {p : Fin n → Bool} :
find? p = none ↔ ∀ (i : Fin n), p i = false
source
theorem Fin.isNone_find?_iff {n : Nat} {p : Fin n → Bool} :
(find? p).isNone = true ↔ ∀ (i : Fin n), p i = false
source
@[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`.

source
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
source
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
source
theorem Fin.eq_false_of_find?_eq_none {n : Nat} {p : Fin n → Bool} (h : find? p = none) (i : Fin n) :
p i = false
source
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
source
theorem Fin.eq_false_of_isNone_find? {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : (find? p).isNone = true) :
p i = false
source
theorem Fin.isSome_find?_of_eq_true {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : p i = true) :
(find? p).isSome = true
source
theorem Fin.get_find?_eq_true {n : Nat} {p : Fin n → Bool} (h : (find? p).isSome = true) :
p ((find? p).get h) = true
source
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
source
theorem Fin.bind_find?_isSome {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(find? fun (i : Fin n) => (f i).isSome).bind f = findSome? f
source
theorem Fin.find?_eq_find?_finRange {n : Nat} {p : Fin n → Bool} :
find? p = List.find? p (List.finRange n)
source
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
source
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
source
theorem Fin.find?_rev {n : Nat} {p : Fin n → Bool} :
(find? fun (x : Fin n) => p x.rev) = Option.map rev (findRev? p)
source
theorem Fin.map_rev_findRev? {n : Nat} {p : Fin n → Bool} :
Option.map rev (findRev? fun (x : Fin n) => p x.rev) = find? p

### findRev? #

source
theorem Fin.findRev?_zero {p : Fin 0 → Bool} :
findRev? p = none
source
theorem Fin.findRev?_succ {n : Nat} {p : Fin (n + 1) → Bool} :
findRev? p = if p (last n) = true then some (last n) else Option.map castSucc (findRev? fun (i : Fin n) => p i.castSucc)
source
theorem Fin.findRev?_one {p : Fin 1 → Bool} :
findRev? p = if p 0 = true then some 0 else none
source
theorem Fin.findRev?_eq_some_iff {n : Nat} {i : Fin n} {p : Fin n → Bool} :
findRev? p = some i ↔ p i = true ∧ ∀ (j : Fin n), i < j → p j = false
source
theorem Fin.findRev?_eq_none_iff {n : Nat} {p : Fin n → Bool} :
findRev? p = none ↔ ∀ (i : Fin n), p i = false
source
theorem Fin.isSome_findRev?_iff {n : Nat} {p : Fin n → Bool} :
(findRev? p).isSome = true ↔ ∃ (i : Fin n), p i = true
source
theorem Fin.isNone_findRev?_iff {n : Nat} {p : Fin n → Bool} :
(findRev? p).isNone = true ↔ ∀ (i : Fin n), p i = false
source
theorem Fin.eq_true_of_findRev?_eq_some {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : findRev? p = some i) :
p i = true
source
theorem Fin.eq_false_of_findRev?_eq_some_of_lt {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : findRev? p = some i) (j : Fin n) :
i < j → p j = false
source
theorem Fin.eq_false_of_findRev?_eq_none {n : Nat} {p : Fin n → Bool} (h : findRev? p = none) (i : Fin n) :
p i = false
source
theorem Fin.exists_eq_true_of_isSome_findRev? {n : Nat} {p : Fin n → Bool} (h : (findRev? p).isSome = true) :
∃ (i : Fin n), p i = true
source
theorem Fin.eq_false_of_isNone_findRev? {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : (findRev? p).isNone = true) :
p i = false
source
theorem Fin.isSome_findRev?_of_eq_true {n : Nat} {i : Fin n} {p : Fin n → Bool} (h : p i = true) :
(findRev? p).isSome = true
source
theorem Fin.get_findRev?_eq_true {n : Nat} {p : Fin n → Bool} (h : (findRev? p).isSome = true) :
p ((findRev? p).get h) = true
source
theorem Fin.get_findRev?_maximal {n : Nat} {p : Fin n → Bool} (h : (findRev? p).isSome = true) (j : Fin n) :
(findRev? p).get h < j → p j = false
source
theorem Fin.exists_eq_true_iff_exists_maximal_eq_true {n : Nat} (p : Fin n → Bool) :
(∃ (i : Fin n), p i = true) ↔ ∃ (i : Fin n), p i = true ∧ ∀ (j : Fin n), i < j → p j = false
source
theorem Fin.exists_iff_exists_maximal {n : Nat} (p : Fin n → Prop) [DecidablePred p] :
(∃ (i : Fin n), p i) ↔ ∃ (i : Fin n), p i ∧ ∀ (j : Fin n), i < j → ¬p j
source
theorem Fin.bind_findRev?_isSome {n : Nat} {α : Type u_1} {f : Fin n → Option α} :
(findRev? fun (i : Fin n) => (f i).isSome).bind f = findSomeRev? f
source
theorem Fin.findRev?_rev {n : Nat} {p : Fin n → Bool} :
(findRev? fun (x : Fin n) => p x.rev) = Option.map rev (find? p)
source
theorem Fin.map_rev_find? {n : Nat} {p : Fin n → Bool} :
Option.map rev (find? fun (x : Fin n) => p x.rev) = findRev? p
source
theorem Fin.find?_le_findRev? {n : Nat} {p : Fin n → Bool} :
find? p ≤ findRev? p
source
theorem Fin.find?_eq_findRev?_iff {n : Nat} {p : Fin n → Bool} :
find? p = findRev? p ↔ ∀ (i j : Fin n), p i = true → p j = true → i = j

### divNat / modNat / mkDivMod #

source
@[simp]
theorem Fin.coe_divNat {m n : Nat} (i : Fin (m * n)) :
↑i.divNat = ↑i / n
source
@[simp]
theorem Fin.coe_modNat {m n : Nat} (i : Fin (m * n)) :
↑i.modNat = ↑i % n
source
@[simp]
theorem Fin.coe_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) :
↑(i.mkDivMod j) = n * ↑i + ↑j
source
@[simp]
theorem Fin.divNat_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) :
(i.mkDivMod j).divNat = i
source
@[simp]
theorem Fin.modNat_mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) :
(i.mkDivMod j).modNat = j
source
@[simp]
theorem Fin.divNat_mkDivMod_modNat {m n : Nat} (k : Fin (m * n)) :
k.divNat.mkDivMod k.modNat = k