-- 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:
case inl.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
h : eraseP p (l₁ ++ a :: l₂) = l₁ ++ a :: l₂
⊢ eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂

Tactic:
rw [eraseP_append_right _ h₁, eraseP_cons_of_pos h₂]

Result:
no goals

Proof state:
case inl.mpr.inl.intro
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ eraseP p l = l

Tactic:
assumption

Result:
no goals

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₂)
⊢ ¬(!p a') = true

Tactic:
simp [h₂']

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₁' l₂' : List α
h₁' : ∀ (b : α), b ∈ l₁' → ¬p b = true
h₂' : p a' = true
h : l₁ ++ a :: l₂ = l₁' ++ a' :: l₂'
⊢ l₁ ++ l₂ = l₁' ++ l₂'

Tactic:
have p : l₁ = l₁' := by
  have q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂) := by
    rw [takeWhile_append_of_pos (by simp_all),
      takeWhile_cons_of_neg (by simp [h₂]), append_nil]
  have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by
    rw [takeWhile_append_of_pos (by simpa using h₁'),
      takeWhile_cons_of_neg (by simp [h₂']), append_nil]
  simp [h] at q
  rw [q', q]

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₂'
p : l₁ = 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₂)
⊢ l₁ = l₁'

Tactic:
have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by
  rw [takeWhile_append_of_pos (by simpa using h₁'),
    takeWhile_cons_of_neg (by simp [h₂']), append_nil]

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.mp
α : 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_2 : α), a_2 ∈ l₁ ++ a :: l₂ → ¬p a_2 = true) ∧ l₁ ++ a :: l₂ = l' ∨
      ∃ a_2 l₁_1 l₂_1,
        (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧ p a_2 = true ∧ l₁ ++ a :: l₂ = l₁_1 ++ a_2 :: l₂_1 ∧ l' = l₁_1 ++ l₂_1

Tactic:
rintro rfl

Result:
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

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₂'
⊢ ¬(!p a) = true

Tactic:
simp [h₂]

Result:
no goals

Proof state:
case inl.mpr
α : Type u_1
l' : List α
p : α → Bool
l : List α
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₂) →
    eraseP p l = l'

Tactic:
rintro (⟨-, rfl⟩ | ⟨a, l₁, l₂, h₁, h₂, rfl, rfl⟩)

Result:
case inl.mpr.inl.intro
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ eraseP p l = l

case inl.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
h : eraseP p (l₁ ++ a :: l₂) = l₁ ++ a :: l₂
⊢ eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂

Proof state:
case inr.intro.intro.intro.intro.intro.intro.mpr
α : 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₂
⊢ ((∀ (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) →
    l₁ ++ l₂ = l'

Tactic:
rintro (h | h)

Result:
case inr.intro.intro.intro.intro.intro.intro.mpr.inl
α : 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 : α), a_1 ∈ l₁ ++ a :: l₂ → ¬p a_1 = true) ∧ l₁ ++ a :: l₂ = l'
⊢ l₁ ++ l₂ = l'

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'

Proof state:
case inr
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ eraseP p l = l₁ ++ l₂
⊢ 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:
obtain ⟨a, l₁, l₂, h₁, h₂, w₁, w₂⟩ := h

Result:
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₂
⊢ 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₂