Theorem: Option.filter_eq_some' (HMem/Trace/Sound.lean)

State before:
α : Type u_1
f : α → Bool
b✝ b : α
⊢ Option.filter f (some b) = some b✝ ↔ some b = some b✝ ∧ f b✝ = true
Tactic:
simpa [Option.filter, And.comm (a := Eq b _)] using λ heq ↦ heq ▸ ⟨id, id⟩
State after:
no goals