rev

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

sum

@[simp]

theorem Fin.sum_zero {α : Type u_1} [Zero α] [Add α] (x : Fin 0 → α) : Fin.sum x = 0

theorem Fin.sum_succ {α : Type u_1} {n : Nat} [Zero α] [Add α] (x : Fin (n + 1) → α) : Fin.sum x = x 0 + Fin.sum fun (x_1 : Fin n) => x x_1.succ

@[simp]

theorem Fin.sum_eq_sum_map_finRange {α : Type u_1} {n : Nat} [Zero α] [Add α] (x : Fin n → α) : Fin.sum x = (List.map x (List.finRange n)).sum

prod

@[simp]

theorem Fin.prod_zero {α : Type u_1} [One α] [Mul α] (x : Fin 0 → α) : Fin.prod x = 1

theorem Fin.prod_succ {α : Type u_1} {n : Nat} [One α] [Mul α] (x : Fin (n + 1) → α) : Fin.prod x = x 0 * Fin.prod fun (x_1 : Fin n) => x x_1.succ

@[simp]

theorem Fin.prod_eq_prod_map_finRange {α : Type u_1} {n : Nat} [One α] [Mul α] (x : Fin n → α) : Fin.prod x = (List.map x (List.finRange n)).prod

countP

@[simp]

theorem Fin.countP_zero (p : Fin 0 → Bool) : Fin.countP p = 0

@[simp]

theorem Fin.countP_one (p : Fin 1 → Bool) : Fin.countP p = (p 0).toNat

theorem Fin.countP_succ {n : Nat} (p : Fin (n + 1) → Bool) : Fin.countP p = (p 0).toNat + Fin.countP fun (x : Fin n) => p x.succ

@[simp]

theorem Fin.countP_eq_countP_map_finRange {n : Nat} (x : Fin n → Bool) : Fin.countP x = List.countP x (List.finRange n)

theorem Fin.countP_le {n : Nat} (p : Fin n → Bool) : Fin.countP p ≤ n

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).or (findSome? fun (x : Fin n) => f x.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 (x : Fin n) => f x.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 (x : Fin n) => f x.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.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

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

findSomeRev?

@[simp]

theorem Fin.findSome?_rev {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? fun (x : Fin n) => f x.rev) = findSomeRev? f

@[simp]

theorem Fin.findSomeRev?_rev {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSomeRev? fun (x : Fin n) => f x.rev) = findSome? f

@[simp]

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

@[simp]

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

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)

@[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

@[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

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

@[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

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

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

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

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

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

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

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)

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

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?

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

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 (x : Fin n) => p x.succ)

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.

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.bind_find?_isSome {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (find? fun (i : Fin n) => (f i).isSome).bind f = findSome? f

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

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

theorem Fin.find?_rev {n : Nat} {p : Fin n → Bool} : (find? fun (x : Fin n) => p x.rev) = Option.map rev (findRev? p)

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?

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Fin.findRev?_rev {n : Nat} {p : Fin n → Bool} : (findRev? fun (x : Fin n) => p x.rev) = Option.map rev (find? p)

theorem Fin.map_rev_find? {n : Nat} {p : Fin n → Bool} : Option.map rev (find? fun (x : Fin n) => p x.rev) = findRev? p

theorem Fin.find?_le_findRev? {n : Nat} {p : Fin n → Bool} : find? p ≤ findRev? p

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

@[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