-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_cons_iff {l} {b} {bs} :
    filterMap f l = b :: bs ↔
      ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ x, x ∈ l₁ → f x = none) ∧ f a = some b ∧
        filterMap f l₂ = bs

Proof state:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
h : f a = none
w : filterMap f l = b :: bs
ih : ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
⊢ ∃ l₁ a_1 l₂, a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = bs

Tactic:
obtain ⟨l₁, a', l₂, rfl, w₁, w₂, w₃⟩ := ih

Result:
case mp.cons.none.intro.intro.intro.intro.intro.intro
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
h : f a = none
l₁ : List α✝¹
a' : α✝¹
l₂ : List α✝¹
w : filterMap f (l₁ ++ a' :: l₂) = b :: bs
w₁ : ∀ (x : α✝¹), x ∈ l₁ → f x = none
w₂ : f a' = some b
w₃ : filterMap f l₂ = bs
⊢ ∃ l₁_1 a_1 l₂_1,
    a :: (l₁ ++ a' :: l₂) = l₁_1 ++ a_1 :: l₂_1 ∧
      (∀ (x : α✝¹), x ∈ l₁_1 → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂_1 = bs

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
h : f a = none
l₁ : List α✝¹
a' : α✝¹
l₂ : List α✝¹
w : filterMap f (l₁ ++ a' :: l₂) = b :: bs
w₁ : ∀ (x : α✝¹), x ∈ l₁ → f x = none
w₂ : f a' = some b
w₃ : filterMap f l₂ = bs
⊢ a :: (l₁ ++ a' :: l₂) = a :: l₁ ++ a' :: l₂ ∧
    (∀ (x : α✝¹), x ∈ a :: l₁ → f x = none) ∧ f a' = some b ∧ filterMap f l₂ = bs

Tactic:
simp_all

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
b : α✝
h : f a = some b
ih :
  filterMap f l = b :: filterMap f l →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = filterMap f l
⊢ a :: l = [] ++ a :: l ∧ (∀ (x : α✝¹), x ∈ [] → f x = none) ∧ f a = some b ∧ filterMap f l = filterMap f l

Tactic:
simp [h]

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
b : α✝
bs : List α✝
⊢ filterMap f l = b :: bs ↔
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs

Tactic:
constructor

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
b : α✝
bs : List α✝
⊢ filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs

case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
b : α✝
bs : List α✝
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs) →
    filterMap f l = b :: bs

Proof state:
case mp.nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
⊢ filterMap f [] = b :: bs →
    ∃ l₁ a l₂, [] = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
h : f a = none
⊢ filterMap f (a :: l) = b :: bs →
    ∃ l₁ a_2 l₂, a :: l = l₁ ++ a_2 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_2 = some b ∧ filterMap f l₂ = bs

Tactic:
simp only [filterMap_cons_none h]

Result:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
h : f a = none
⊢ filterMap f l = b :: bs →
    ∃ l₁ a_2 l₂, a :: l = l₁ ++ a_2 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_2 = some b ∧ filterMap f l₂ = bs

Proof state:
case mp.cons.some
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b✝ : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b✝ :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b✝ ∧ filterMap f l₂ = bs
b : α✝
h : f a = some b
⊢ b = b✝ →
    filterMap f l = bs →
      ∃ l₁ a_3 l₂, a :: l = l₁ ++ a_3 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_3 = some b✝ ∧ filterMap f l₂ = bs

Tactic:
rintro rfl rfl

Result:
case mp.cons.some
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
b : α✝
h : f a = some b
ih :
  filterMap f l = b :: filterMap f l →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = filterMap f l
⊢ ∃ l₁ a_1 l₂,
    a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = filterMap f l

Proof state:
case mp.cons.some
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b✝ : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b✝ :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b✝ ∧ filterMap f l₂ = bs
b : α✝
h : f a = some b
⊢ filterMap f (a :: l) = b✝ :: bs →
    ∃ l₁ a_2 l₂, a :: l = l₁ ++ a_2 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_2 = some b✝ ∧ filterMap f l₂ = bs

Tactic:
simp only [filterMap_cons_some h, cons.injEq, and_imp]

Result:
case mp.cons.some
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b✝ : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b✝ :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b✝ ∧ filterMap f l₂ = bs
b : α✝
h : f a = some b
⊢ b = b✝ →
    filterMap f l = bs →
      ∃ l₁ a_3 l₂, a :: l = l₁ ++ a_3 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_3 = some b✝ ∧ filterMap f l₂ = bs

Proof state:
case mp.cons.none.intro.intro.intro.intro.intro.intro
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
h : f a = none
l₁ : List α✝¹
a' : α✝¹
l₂ : List α✝¹
w : filterMap f (l₁ ++ a' :: l₂) = b :: bs
w₁ : ∀ (x : α✝¹), x ∈ l₁ → f x = none
w₂ : f a' = some b
w₃ : filterMap f l₂ = bs
⊢ ∃ l₁_1 a_1 l₂_1,
    a :: (l₁ ++ a' :: l₂) = l₁_1 ++ a_1 :: l₂_1 ∧
      (∀ (x : α✝¹), x ∈ l₁_1 → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂_1 = bs

Tactic:
exact ⟨a :: l₁, a', l₂, by simp_all⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
l₁ : List α✝¹
a : α✝¹
l₂ : List α✝¹
h₁ : ∀ (x : α✝¹), x ∈ l₁ → f x = none
h₂ : f a = some b
h₃ : filterMap f l₂ = bs
⊢ filterMap f (l₁ ++ a :: l₂) = b :: bs

Tactic:
simp_all [filterMap_eq_nil_iff.mpr h₁, filterMap_cons_some h₂]

Result:
no goals

Proof state:
case mp.cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
⊢ filterMap f (a :: l) = b :: bs →
    ∃ l₁ a_2 l₂, a :: l = l₁ ++ a_2 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_2 = some b ∧ filterMap f l₂ = bs

Tactic:
cases h : f a with
| none =>
  simp only [filterMap_cons_none h]
  intro w
  specialize ih w
  obtain ⟨l₁, a', l₂, rfl, w₁, w₂, w₃⟩ := ih
  exact ⟨a :: l₁, a', l₂, by simp_all⟩
| some b =>
  simp only [filterMap_cons_some h, cons.injEq, and_imp]
  rintro rfl rfl
  refine ⟨[], a, l, by simp [h]⟩

Result:
no goals

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
b : α✝
bs : List α✝
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs) →
    filterMap f l = b :: bs

Tactic:
rintro ⟨l₁, a, l₂, rfl, h₁, h₂, h₃⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
l₁ : List α✝¹
a : α✝¹
l₂ : List α✝¹
h₁ : ∀ (x : α✝¹), x ∈ l₁ → f x = none
h₂ : f a = some b
h₃ : filterMap f l₂ = bs
⊢ filterMap f (l₁ ++ a :: l₂) = b :: bs