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

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

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

@[simp]

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

@[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.findSome?_isNone_iff {n : Nat} {α : Type u_1} {f : Fin n → Option α} : (findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true

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

theorem Fin.findSome?_guard {n : Nat} {p : Fin n → Bool} : findSome? (Option.guard fun (i : Fin n) => p i = true) = 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)

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_none {n : Nat} {p : Fin n → Bool} (h : find? p = none) (i : Fin n) : p i = false

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

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

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

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