Finding subsingleton elements within multisets

This module provides Multiset.find? s p ⋯, which lifts List.find? to multisets.

def Multiset.find? {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : {x : α | x ∈ s ∧ p x}.Subsingleton → Option α

s.find? p ⋯ finds the subsingleton element of s satisfying the condition p, if one exists.

This is the multiset version of List.find?, and is like Multiset.choose, but Option-valued.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Multiset.find?_coe {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) (hp : {x : α | x ∈ ↑l ∧ p x}.Subsingleton) : find? p (↑l) hp = List.find? (fun (a : α) => decide (p a)) l

theorem Multiset.find?_some {α : Type u_1} (p : α → Prop) [DecidablePred p] {a : α} {s : Multiset α} {hp : {x : α | x ∈ s ∧ p x}.Subsingleton} : find? p s hp = some a → p a

@[simp]

theorem Multiset.find?_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : find? p 0 ⋯ = none

@[simp]

theorem Multiset.find?_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (s : Multiset α) (hp : {x : α | x ∈ a ::ₘ s ∧ p x}.Subsingleton) : find? p (a ::ₘ s) hp = if h : p a then some a else find? p s ⋯

@[simp]

theorem Multiset.find?_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (hp : {x : α | x ∈ {a} ∧ p x}.Subsingleton) : find? p {a} hp = if p a then some a else none

@[simp]

theorem Multiset.find?_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) (hp : {x : α | x ∈ s + t ∧ p x}.Subsingleton) : find? p (s + t) hp = (find? p s ⋯).or (find? p t ⋯)

@[simp]

theorem Multiset.find?_eq_some_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (hp : {x : α | x ∈ s ∧ p x}.Subsingleton) : find? p s hp = some a ↔ a ∈ s ∧ p a

@[simp]

theorem Multiset.find?_eq_none_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} (hp : {x : α | x ∈ s ∧ p x}.Subsingleton) : find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a

theorem Multiset.find?_congr {α : Type u_1} {p₁ p₂ : α → Prop} [DecidablePred p₁] [DecidablePred p₂] {s : Multiset α} (hp₁ : {x : α | x ∈ s ∧ p₁ x}.Subsingleton) (h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)) : find? p₁ s hp₁ = find? p₂ s ⋯

If two predicates agree on all the elements, so does find?.

theorem Multiset.find?_eq_choose {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} (hp : ∃! x : α, x ∈ s ∧ p x) : find? p s ⋯ = some (choose p s hp)