Theorem: Option.forall_mem_filter (HMem/Trace/Sound.lean)

State before:
α : Type u_1
f : α → Bool
o : Option α
p : α → Prop
⊢ (∀ y ∈ Option.filter f o, p y) ↔ ∀ x ∈ o, f x = true → p x
Tactic:
simp
State after:
no goals