-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_filterMap {l : List α} {f : α → Option β} :
    (l.filterMap f).attach = l.attach.filterMap
      fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩)

Proof state:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ (match f x with
    | none => filterMap f xs
    | some b => b :: filterMap f xs) =
    ?m.63176

Tactic:
simp only [h]

Result:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ a :: filterMap f xs = ?m.63176

Proof state:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ map (fun x_1 => ⟨x_1.val, ⋯⟩) (a :: filterMap f xs).attach =
    ⟨a, ⋯⟩ :: filterMap ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) xs.attach

Tactic:
rw [attach_cons, map_cons, map_map, ih, map_filterMap]

Result:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ ⟨⟨a, ⋯⟩.val, ⋯⟩ ::
      filterMap
        (fun x_1 =>
          Option.map
            ((fun x_2 => ⟨x_2.val, ⋯⟩) ∘ fun x =>
              match x with
              | ⟨y, h⟩ => ⟨y, ⋯⟩)
            (match x_1 with
            | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩))
        xs.attach =
    ⟨a, ⋯⟩ :: filterMap ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) xs.attach

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
h : f x = none
⊢ filterMap (fun x_1 => (f x_1.val).pbind fun a h_1 => some ⟨a, ⋯⟩) xs.attach =
    filterMap ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) xs.attach

Tactic:
rfl

Result:
no goals

Proof state:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
b✝ :
  { x_1 //
    x_1 ∈
      match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs }
a : β
h : a ∈ f x
w : ⟨a, ⋯⟩ = b✝
⊢ (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs).attach =
    b✝ :: filterMap ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) xs.attach

Tactic:
subst w

Result:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h : a ∈ f x
⊢ (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs).attach =
    ⟨a, ⋯⟩ :: filterMap ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) xs.attach

Proof state:
case cons.h_2.intro.intro.e_tail.e_f
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ (fun x_1 =>
      Option.map
        ((fun x_2 => ⟨x_2.val, ⋯⟩) ∘ fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        (match x_1 with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)) =
    (fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩

Tactic:
ext

Result:
case cons.h_2.intro.intro.e_tail.e_f.h.a
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝¹ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
x✝ : { x // x ∈ xs }
a✝ :
  { x_1 //
    x_1 ∈
      match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs }
⊢ a✝ ∈
      Option.map
        ((fun x_1 => ⟨x_1.val, ⋯⟩) ∘ fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        (match x✝ with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩) ↔
    a✝ ∈ ((fun x_1 => (f x_1.val).pbind fun a h => some ⟨a, ⋯⟩) ∘ fun x_1 => ⟨x_1.val, ⋯⟩) x✝

Proof state:
case cons.h_2.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
a : β
h✝ : a ∈ f x
h : f x = some a
⊢ a :: filterMap f xs = ?m.63176

Tactic:
rfl

Result:
no goals

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih :
  (filterMap f xs).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
x✝ :
  Option
    { x_1 //
      x_1 ∈
        match f x with
        | none => filterMap f xs
        | some b => b :: filterMap f xs }
h : f x = none
⊢ filterMap f xs = ?m.60801

Tactic:
rfl

Result:
no goals