-- 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
α : 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✝ : β
heq✝ : f x = some b✝
⊢ b✝ :: filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rename_i b w

Result:
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
⊢ b :: filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

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

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
L₁ L₂ : List β
f : α → Option β
⊢ filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

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₂

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
⊢ ([] = [] ∧ [] = []) ∧ filterMap f [] = [] ∧ filterMap f [] = []

Tactic:
simp

Result:
no goals

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
h : filterMap f l = L₁ ++ L₂
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
obtain ⟨l₁, l₂, rfl, rfl, rfl⟩ := ih h

Result:
case mp.cons.h_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
heq✝ : f x = none
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₂
⊢ ∃ l₁_1 l₂_1, x :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = filterMap f l₁ ∧ filterMap f l₂_1 = filterMap f l₂

Proof state:
case mp.cons.h_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
heq✝ : f x = none
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₂
⊢ x :: (l₁ ++ l₂) = x :: l₁ ++ l₂ ∧ filterMap f (x :: l₁) = filterMap f l₁ ∧ filterMap f l₂ = filterMap f l₂

Tactic:
simp_all

Result:
no goals

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
⊢ ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = [] ∧ filterMap f l₂ = b :: filterMap f l

Tactic:
refine ⟨[], x :: l, ?_⟩

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
⊢ x :: l = [] ++ x :: l ∧ filterMap f [] = [] ∧ filterMap f (x :: l) = b :: filterMap f l

Proof state:
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₂

Tactic:
rintro rfl rfl

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

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 β
⊢ (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₂

Tactic:
split

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
⊢ filterMap f l = L₁ ++ L₂ → ∃ l₁ l₂, x :: l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

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✝ : β
heq✝ : f x = 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
⊢ b :: 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_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₂

Proof state:
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₂

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.h_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
heq✝ : f x = none
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₂
⊢ ∃ l₁_1 l₂_1, x :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = filterMap f l₁ ∧ filterMap f l₂_1 = filterMap f l₂

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

Result:
case mp.cons.h_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
x : α
x✝ : Option β
heq✝ : f x = none
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₂
⊢ x :: (l₁ ++ l₂) = x :: l₁ ++ l₂ ∧ filterMap f (x :: l₁) = filterMap f l₁ ∧ filterMap f l₂ = filterMap f l₂