-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_append_iff {f : α → Option β} :
    filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mp.cons.h_2.inl.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
l : List α
x✝ : Option β
b : β
w : f x = some b
ih :
  ∀ {L₁ : List β},
    filterMap f l = L₁ ++ b :: filterMap f l →
      ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = b :: filterMap f l
h : b :: filterMap f l = [] ++ b :: filterMap f l
⊢ x :: l = [] ++ x :: l ∧ filterMap f [] = [] ∧ filterMap f (x :: l) = b :: filterMap f l

Tactic:
simp [filterMap_cons, w]

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
L₁ : List β
⊢ filterMap f (x :: l) = L₁ ++ L₂ → ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
simp only [filterMap_cons]

Result:
case mp.cons
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
L₁ : List β
⊢ (match f x with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
      L₁ ++ L₂ →
    ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mp.cons.h_2
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
L₁ : List β
x✝ : Option β
b : β
w : f x = some b
h : b :: filterMap f l = L₁ ++ L₂
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rcases cons_eq_append_iff.mp h with (⟨rfl, rfl⟩ | ⟨L₁, ⟨rfl, h⟩⟩)

Result:
case mp.cons.h_2.inl.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
l : List α
x✝ : Option β
b : β
w : f x = some b
ih :
  ∀ {L₁ : List β},
    filterMap f l = L₁ ++ b :: filterMap f l →
      ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = b :: filterMap f l
h : b :: filterMap f l = [] ++ b :: filterMap f l
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = [] ∧ filterMap f l₂ = b :: filterMap f l

case mp.cons.h_2.inr.intro.intro
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
x✝ : Option β
b : β
w : f x = some b
L₁ : List β
h✝ : filterMap f l = L₁ ++ L₂
h : b :: filterMap f l = b :: L₁ ++ L₂
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = b :: L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mpr
α : Type u_1
β : Type u_2
l : List α
L₁ L₂ : List β
f : α → Option β
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂) → filterMap f l = L₁ ++ L₂

Tactic:
rintro ⟨l₁, l₂, rfl, rfl, rfl⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ filterMap f (l₁ ++ l₂) = filterMap f l₁ ++ filterMap f l₂

Proof state:
case mp.nil
α : Type u_1
β : Type u_2
f : α → Option β
⊢ ∃ l₁ l₂, (l₁ = [] ∧ l₂ = []) ∧ filterMap f l₁ = [] ∧ filterMap f l₂ = []

Tactic:
exact ⟨[], [], by simp⟩

Result:
no goals

Proof state:
case mp.cons.h_2.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
b : β
w : f x = some b
l₁ l₂ : List α
ih :
  ∀ {L₁ : List β},
    filterMap f (l₁ ++ l₂) = L₁ ++ filterMap f l₂ →
      ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = L₁ ∧ filterMap f l₂_1 = filterMap f l₂
h✝ : filterMap f (l₁ ++ l₂) = filterMap f l₁ ++ filterMap f l₂
h : b :: filterMap f (l₁ ++ l₂) = b :: filterMap f l₁ ++ filterMap f l₂
⊢ ∃ l₁_1 l₂_1,
    x :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = b :: filterMap f l₁ ∧ filterMap f l₂_1 = filterMap f l₂

Tactic:
refine ⟨x :: l₁, l₂, ?_⟩

Result:
case mp.cons.h_2.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
b : β
w : f x = some b
l₁ l₂ : List α
ih :
  ∀ {L₁ : List β},
    filterMap f (l₁ ++ l₂) = L₁ ++ filterMap f l₂ →
      ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = L₁ ∧ filterMap f l₂_1 = filterMap f l₂
h✝ : filterMap f (l₁ ++ l₂) = filterMap f l₁ ++ filterMap f l₂
h : b :: filterMap f (l₁ ++ l₂) = b :: filterMap f l₁ ++ filterMap f l₂
⊢ x :: (l₁ ++ l₂) = x :: l₁ ++ l₂ ∧ filterMap f (x :: l₁) = b :: filterMap f l₁ ∧ filterMap f l₂ = filterMap f l₂

Proof state:
case mp.cons.h_1
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
L₁ : List β
x✝ : Option β
heq✝ : f x = none
⊢ filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
intro h

Result:
case mp.cons.h_1
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
L₁ : List β
x✝ : Option β
heq✝ : f x = none
h : filterMap f l = L₁ ++ L₂
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mp.cons.h_2.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
b : β
w : f x = some b
l₁ l₂ : List α
ih :
  ∀ {L₁ : List β},
    filterMap f (l₁ ++ l₂) = L₁ ++ filterMap f l₂ →
      ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = L₁ ∧ filterMap f l₂_1 = filterMap f l₂
h✝ : filterMap f (l₁ ++ l₂) = filterMap f l₁ ++ filterMap f l₂
h : b :: filterMap f (l₁ ++ l₂) = b :: filterMap f l₁ ++ filterMap f l₂
⊢ x :: (l₁ ++ l₂) = x :: l₁ ++ l₂ ∧ filterMap f (x :: l₁) = b :: filterMap f l₁ ∧ filterMap f l₂ = filterMap f l₂

Tactic:
simp [filterMap_cons, w]

Result:
no goals

Proof state:
case mp.nil
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
L₁ : List β
⊢ filterMap f [] = L₁ ++ L₂ → ∃ l₁ l₂, [] = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
simp only [filterMap_nil, nil_eq_append_iff, and_imp]

Result:
case mp.nil
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
L₁ : List β
⊢ L₁ = [] → L₂ = [] → ∃ l₁ l₂, (l₁ = [] ∧ l₂ = []) ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mp.cons.h_2.inr.intro.intro
α : Type u_1
β : Type u_2
L₂ : List β
f : α → Option β
x : α
l : List α
ih : ∀ {L₁ : List β}, filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂
x✝ : Option β
b : β
w : f x = some b
L₁ : List β
h✝ : filterMap f l = L₁ ++ L₂
h : b :: filterMap f l = b :: L₁ ++ L₂
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = b :: L₁ ∧ filterMap f l₂ = L₂

Tactic:
obtain ⟨l₁, l₂, rfl, rfl, rfl⟩ := ih ‹_›

Result:
case mp.cons.h_2.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
b : β
w : f x = some b
l₁ l₂ : List α
ih :
  ∀ {L₁ : List β},
    filterMap f (l₁ ++ l₂) = L₁ ++ filterMap f l₂ →
      ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = L₁ ∧ filterMap f l₂_1 = filterMap f l₂
h✝ : filterMap f (l₁ ++ l₂) = filterMap f l₁ ++ filterMap f l₂
h : b :: filterMap f (l₁ ++ l₂) = b :: filterMap f l₁ ++ filterMap f l₂
⊢ ∃ l₁_1 l₂_1,
    x :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = b :: filterMap f l₁ ∧ filterMap f l₂_1 = filterMap f l₂