-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_eq_cons_iff {l} {a} {as} :
    filter p l = a :: as ↔
      ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ x, x ∈ l₁ → ¬p x) ∧ p a ∧ filter p l₂ = as

Proof state:
case mp.cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
h : filter p (x :: l) = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
simp only [filter_cons] at h

Result:
case mp.cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
h : (if p x = true then x :: filter p l else filter p l) = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Proof state:
case mp.cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
⊢ filter p (x :: l) = a :: as →
    ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
intro h

Result:
case mp.cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
h : filter p (x :: l) = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Proof state:
case mp.cons.isFalse.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
w : ¬p x = true
l₁ l₂ : List α✝
h : filter p (l₁ ++ a :: l₂) = a :: as
w₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
w₂ : p a = true
w₃ : filter p l₂ = as
⊢ ∃ l₁_1 l₂_1,
    x :: (l₁ ++ a :: l₂) = l₁_1 ++ a :: l₂_1 ∧ (∀ (x : α✝), x ∈ l₁_1 → ¬p x = true) ∧ p a = true ∧ filter p l₂_1 = as

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

Result:
case mp.cons.isFalse.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
w : ¬p x = true
l₁ l₂ : List α✝
h : filter p (l₁ ++ a :: l₂) = a :: as
w₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
w₂ : p a = true
w₃ : filter p l₂ = as
⊢ x :: (l₁ ++ a :: l₂) = x :: l₁ ++ a :: l₂ ∧
    (∀ (x_1 : α✝), x_1 ∈ x :: l₁ → ¬p x_1 = true) ∧ p a = true ∧ filter p l₂ = as

Proof state:
case mp.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : ¬p x = true
h : filter p l = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
specialize ih h

Result:
case mp.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
w : ¬p x = true
h : filter p l = a :: as
ih : ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Proof state:
case mp.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
w : ¬p x = true
h : filter p l = a :: as
ih : ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

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

Result:
case mp.cons.isFalse.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
w : ¬p x = true
l₁ l₂ : List α✝
h : filter p (l₁ ++ a :: l₂) = a :: as
w₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
w₂ : p a = true
w₃ : filter p l₂ = as
⊢ ∃ l₁_1 l₂_1,
    x :: (l₁ ++ a :: l₂) = l₁_1 ++ a :: l₂_1 ∧ (∀ (x : α✝), x ∈ l₁_1 → ¬p x = true) ∧ p a = true ∧ filter p l₂_1 = as

Proof state:
case mp.nil
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
⊢ filter p [] = a :: as →
    ∃ l₁ l₂, [] = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : p x = true
h : x = a ∧ filter p l = as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
obtain ⟨rfl, rfl⟩ := h

Result:
case mp.cons.isTrue.intro
α✝ : Type u_1
p : α✝ → Bool
x : α✝
l : List α✝
w : p x = true
ih :
  filter p l = x :: filter p l →
    ∃ l₁ l₂, l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l
⊢ ∃ l₁ l₂, x :: l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l

Proof state:
case mp.cons.isFalse.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
w : ¬p x = true
l₁ l₂ : List α✝
h : filter p (l₁ ++ a :: l₂) = a :: as
w₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
w₂ : p a = true
w₃ : filter p l₂ = as
⊢ x :: (l₁ ++ a :: l₂) = x :: l₁ ++ a :: l₂ ∧
    (∀ (x_1 : α✝), x_1 ∈ x :: l₁ → ¬p x_1 = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
a : α✝
as : List α✝
⊢ (∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as) →
    filter p l = a :: as

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

Result:
case mpr.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as l₁ l₂ : List α✝
h₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
h : p a = true
h₂ : filter p l₂ = as
⊢ filter p (l₁ ++ a :: l₂) = a :: as

Proof state:
case mp.cons.isTrue.intro
α✝ : Type u_1
p : α✝ → Bool
x : α✝
l : List α✝
w : p x = true
ih :
  filter p l = x :: filter p l →
    ∃ l₁ l₂, l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l
⊢ x :: l = [] ++ x :: l ∧ (∀ (x : α✝), x ∈ [] → ¬p x = true) ∧ p x = true ∧ filter p l = filter p l

Tactic:
simp [w]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as l₁ l₂ : List α✝
h₁ : ∀ (x : α✝), x ∈ l₁ → ¬p x = true
h : p a = true
h₂ : filter p l₂ = as
⊢ filter p (l₁ ++ a :: l₂) = a :: as

Tactic:
simp [h₂, filter_cons, filter_eq_nil_iff.mpr h₁, h]

Result:
no goals

Proof state:
case mp.cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : p x = true
h : x :: filter p l = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
simp only [cons.injEq] at h

Result:
case mp.cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : p x = true
h : x = a ∧ filter p l = as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as