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

Tactic:
constructor

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

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'

Proof state:
case inl.mp
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p 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:
intro h'

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

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

Tactic:
simp_all

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₂
⊢ 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:
rw [w₂]

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

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₂'
⊢ l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂)

Tactic:
rw [takeWhile_append_of_pos (by simp_all),
  takeWhile_cons_of_neg (by simp [h₂]), append_nil]

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p l = l
h' : eraseP p l = l'
⊢ l = l'

Tactic:
simp_all

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₂')
q : l₁ = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂')
⊢ l₁ = l₁'

Tactic:
rw [q', q]

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

Tactic:
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]

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

Proof state:
case inl
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p 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:
constructor

Result:
case inl.mp
α : Type u_1
l' : List α
p : α → Bool
l : List α
h : eraseP p 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₂

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'

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₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂')

Tactic:
rw [takeWhile_append_of_pos (by simpa using h₁'),
  takeWhile_cons_of_neg (by simp [h₂']), append_nil]

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

Tactic:
subst p

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