-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_eq_iff {p} {l : List α} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
a' : α
l₁' l₂' : List α
h₁' : ∀ (b : α), b ∈ l₁' → ¬p b = true
h₂' : p a' = true
h : l₁ ++ a :: l₂ = l₁' ++ a' :: l₂'
q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂)
q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂')
⊢ l₁ = l₁'

Tactic:
simp [h] at q

Result:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
a' : α
l₁' l₂' : List α
h₁' : ∀ (b : α), b ∈ l₁' → ¬p b = true
h₂' : p a' = true
h : l₁ ++ a :: l₂ = l₁' ++ a' :: l₂'
q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂')
q : l₁ = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂')
⊢ l₁ = l₁'

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mpr.inr
α : Type u_1
l' : List α
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
h :
  ∃ a_1 l₁_1 l₂_1,
    (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_1 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ l' = l₁_1 ++ l₂_1
⊢ l₁ ++ l₂ = l'

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

Result:
case inr.intro.intro.intro.intro.intro.intro.mpr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
a' : α
l₁' l₂' : List α
h₁' : ∀ (b : α), b ∈ l₁' → ¬p b = true
h₂' : p a' = true
h : l₁ ++ a :: l₂ = l₁' ++ a' :: l₂'
⊢ l₁ ++ l₂ = l₁' ++ l₂'

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
a' : α
l₁' l₂' : List α
h₁' : ∀ (b : α), b ∈ l₁' → ¬p b = true
h₂' : p a' = true
h : l₁ ++ a :: l₂ = l₁' ++ a' :: l₂'
q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂)
⊢ ∀ (a : α), a ∈ l₁' → (!p a) = true

Tactic:
simpa using h₁'

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
p : α → Bool
l : List α
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₁ : l = l₁ ++ a :: l₂
w₂ : eraseP p l = l₁ ++ l₂
⊢ l₁ ++ l₂ = l' ↔
    (∀ (a : α), a ∈ l → ¬p a = true) ∧ l = l' ∨
      ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Tactic:
subst w₁

Result:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ l₁ ++ l₂ = l' ↔
    (∀ (a_1 : α), a_1 ∈ l₁ ++ a :: l₂ → ¬p a_1 = true) ∧ l₁ ++ a :: l₂ = l' ∨
      ∃ a_1 l₁_1 l₂_1,
        (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_1 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ l' = l₁_1 ++ l₂_1

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mp.h
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l₁ ++ a :: l₂ = l₁ ++ a :: l₂ ∧ l₁ ++ l₂ = l₁ ++ l₂

Tactic:
simp_all

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mpr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
a' : α
l₂' : List α
h₂' : p a' = true
h₁' : ∀ (b : α), b ∈ l₁ → ¬p b = true
h : l₁ ++ a :: l₂ = l₁ ++ a' :: l₂'
⊢ l₁ ++ l₂ = l₁ ++ l₂'

Tactic:
simp_all

Result:
no goals

Proof state:
case inl.mp
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p l = l
h' : eraseP p l = l'
⊢ (∀ (a : α), a ∈ l → ¬p a = true) ∧ l = l' ∨
    ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Tactic:
left

Result:
case inl.mp.h
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p l = l
h' : eraseP p l = l'
⊢ (∀ (a : α), a ∈ l → ¬p a = true) ∧ l = l'

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mp
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ (∀ (a_1 : α), a_1 ∈ l₁ ++ a :: l₂ → ¬p a_1 = true) ∧ l₁ ++ a :: l₂ = l₁ ++ l₂ ∨
    ∃ a_1 l₁_1 l₂_1,
      (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_1 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1

Tactic:
right

Result:
case inr.intro.intro.intro.intro.intro.intro.mp.h
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ ∃ a_1 l₁_1 l₂_1,
    (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_1 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1

Proof state:
case inl.mp.h
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p l = l
h' : eraseP p l = l'
⊢ (∀ (a : α), a ∈ l → ¬p a = true) ∧ l = l'

Tactic:
exact ⟨eraseP_eq_self_iff.1 h, by simp_all⟩

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mp.h
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ ∃ a_1 l₁_1 l₂_1,
    (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_1 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1

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

Result:
case inr.intro.intro.intro.intro.intro.intro.mp.h
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
w₂ : eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l₁ ++ a :: l₂ = l₁ ++ a :: l₂ ∧ l₁ ++ l₂ = l₁ ++ l₂