-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_filter {o : Option α} {p : α → Bool} :
    (o.filter p).attach =
      o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none

Proof state:
case some
α : Type u_1
p : α → Bool
a : α
⊢ (if p a = true then some a else none).attach =
    (some ⟨a, ⋯⟩).bind fun x => if h : p x.val = true then some ⟨x.val, ⋯⟩ else none

Tactic:
ext

Result:
case some.a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ a✝ ∈ (if p a = true then some a else none).attach ↔
    a✝ ∈ (some ⟨a, ⋯⟩).bind fun x => if h : p x.val = true then some ⟨x.val, ⋯⟩ else none

Proof state:
case some
α : Type u_1
p : α → Bool
a : α
⊢ (Option.filter p (some a)).attach =
    (some a).attach.bind fun x =>
      match x with
      | ⟨x, h⟩ => if h' : p x = true then some ⟨x, ⋯⟩ else none

Tactic:
simp only [filter_some, attach_some]

Result:
case some
α : Type u_1
p : α → Bool
a : α
⊢ (if p a = true then some a else none).attach =
    (some ⟨a, ⋯⟩).bind fun x => if h : p x.val = true then some ⟨x.val, ⋯⟩ else none

Proof state:
case some.a.mp.intro
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
h : p a = true
w : a = a✝.val
⊢ ∃ h, ⟨a, ⋯⟩ = a✝

Tactic:
refine ⟨h, by ext; simpa using w⟩

Result:
no goals

Proof state:
case some.a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ p a = true ∧ a = a✝.val ↔ ∃ h, ⟨a, ⋯⟩ = a✝

Tactic:
constructor

Result:
case some.a.mp
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ p a = true ∧ a = a✝.val → ∃ h, ⟨a, ⋯⟩ = a✝

case some.a.mpr
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ (∃ h, ⟨a, ⋯⟩ = a✝) → p a = true ∧ a = a✝.val

Proof state:
case some.a.mp
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ p a = true ∧ a = a✝.val → ∃ h, ⟨a, ⋯⟩ = a✝

Tactic:
rintro ⟨h, w⟩

Result:
case some.a.mp.intro
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
h : p a = true
w : a = a✝.val
⊢ ∃ h, ⟨a, ⋯⟩ = a✝

Proof state:
case a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
h : p a = true
w : a = a✝.val
⊢ ⟨a, ⋯⟩.val = a✝.val

Tactic:
simpa using w

Result:
no goals

Proof state:
case none
α : Type u_1
p : α → Bool
⊢ (Option.filter p none).attach =
    none.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ => if h' : p x = true then some ⟨x, ⋯⟩ else none

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.13618
o : Option α
p : α → Bool
x✝ : { x // x ∈ o }
x : α
h : x ∈ o
h' : p x = true
⊢ x ∈ Option.filter p o

Tactic:
simp_all

Result:
no goals

Proof state:
case some.a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ a✝ ∈ (if p a = true then some a else none).attach ↔
    a✝ ∈ (some ⟨a, ⋯⟩).bind fun x => if h : p x.val = true then some ⟨x.val, ⋯⟩ else none

Tactic:
simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
  dite_none_right_eq_some]

Result:
case some.a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ p a = true ∧ a = a✝.val ↔ ∃ h, ⟨a, ⋯⟩ = a✝

Proof state:
case some.a.mpr
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
⊢ (∃ h, ⟨a, ⋯⟩ = a✝) → p a = true ∧ a = a✝.val

Tactic:
rintro ⟨h, rfl⟩

Result:
case some.a.mpr.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
⊢ p a = true ∧ a = ⟨a, ⋯⟩.val

Proof state:
case some.a.mpr.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
⊢ p a = true ∧ a = ⟨a, ⋯⟩.val

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
h : p a = true
w : a = a✝.val
⊢ ⟨a, ⋯⟩ = a✝

Tactic:
ext

Result:
case a
α : Type u_1
p : α → Bool
a : α
a✝ : { x // x ∈ if p a = true then some a else none }
h : p a = true
w : a = a✝.val
⊢ ⟨a, ⋯⟩.val = a✝.val