-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_filterMap (f : α → Option β) : ∀ (l : List α),
    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
  | [] => rfl
  | a::l => by
    rw [filterMap_cons, eraseP_cons]
    split <;> rename_i h
    · simp [h, eraseP_filterMap]
    · rename_i b
      rw [h, eraseP_cons]
      by_cases w : p b
      · simp [w]
      · simp only [w, cond_false]
        rw [filterMap_cons_some h, eraseP_filterMap]

Proof state:
case neg
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : ¬p b = true
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
simp only [w, cond_false]

Result:
case neg
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : ¬p b = true
⊢ b :: eraseP p (filterMap f l) =
    filterMap f
      (a ::
        eraseP
          (fun x =>
            match f x with
            | some y => p y
            | none => false)
          l)

Proof state:
case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
by_cases w : p b

Result:
case pos
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : p b = true
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

case neg
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : ¬p b = true
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Proof state:
case pos
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : p b = true
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
simp [w]

Result:
no goals

Proof state:
case h_1
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
h : f a = none
⊢ eraseP p (filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
simp [h, eraseP_filterMap]

Result:
no goals

Proof state:
case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b✝ : β
h : f a = some b✝
⊢ eraseP p (b✝ :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
rename_i b

Result:
case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
⊢ eraseP p (b :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Proof state:
case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
⊢ eraseP p (b :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
rw [h, eraseP_cons]

Result:
case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
⊢ (bif p b then filterMap f l else b :: eraseP p (filterMap f l)) =
    filterMap f
      (bif
          match some b with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
⊢ eraseP p
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Tactic:
split <;> rename_i h

Result:
case h_1
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
h : f a = none
⊢ eraseP p (filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

case h_2
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b✝ : β
h : f a = some b✝
⊢ eraseP p (b✝ :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)

Proof state:
case neg
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
x✝ : Option β
b : β
h : f a = some b
w : ¬p b = true
⊢ b :: eraseP p (filterMap f l) =
    filterMap f
      (a ::
        eraseP
          (fun x =>
            match f x with
            | some y => p y
            | none => false)
          l)

Tactic:
rw [filterMap_cons_some h, eraseP_filterMap]

Result:
no goals