-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_eq_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x]

Proof state:
case cons.isTrue.mpr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ (∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []) → xs = []

Tactic:
rintro ⟨_, _, rfl, rfl⟩

Result:
case cons.isTrue.mpr.intro.intro.intro
α : Type u_1
p : α → Bool
x : α
h left✝ : p x = true
ih : eraseP p [] = [] ↔ [] = [] ∨ ∃ x, p x = true ∧ [] = [x]
⊢ [] = []

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Tactic:
simp only [reduceCtorEq, cons.injEq, false_or]

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] ↔ ∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []

Proof state:
case cons.isTrue.mp
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] → ∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []

Tactic:
rintro rfl

Result:
case cons.isTrue.mp
α : Type u_1
p : α → Bool
x : α
h : p x = true
ih : eraseP p [] = [] ↔ [] = [] ∨ ∃ x, p x = true ∧ [] = [x]
⊢ ∃ x_1, p x_1 = true ∧ x = x_1 ∧ [] = []

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
⊢ eraseP p (x :: xs) = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Tactic:
simp only [eraseP_cons, cond_eq_if]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
⊢ (if p x = true then xs else x :: eraseP p xs) = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
⊢ ∀ (x_1 : α), p x_1 = true → x = x_1 → ¬xs = []

Tactic:
rintro x h' rfl

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
h' : p x = true
⊢ ¬xs = []

Proof state:
case cons.isTrue.mp
α : Type u_1
p : α → Bool
x : α
h : p x = true
ih : eraseP p [] = [] ↔ [] = [] ∨ ∃ x, p x = true ∧ [] = [x]
⊢ ∃ x_1, p x_1 = true ∧ x = x_1 ∧ [] = []

Tactic:
simpa

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
⊢ (if p x = true then xs else x :: eraseP p xs) = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Tactic:
split <;> rename_i h

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
⊢ x :: eraseP p xs = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
⊢ x :: eraseP p xs = [] ↔ x :: xs = [] ∨ ∃ x_1, p x_1 = true ∧ x :: xs = [x_1]

Tactic:
simp only [reduceCtorEq, cons.injEq, false_or, false_iff, not_exists, not_and]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
⊢ ∀ (x_1 : α), p x_1 = true → x = x_1 → ¬xs = []

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : ¬p x = true
h' : p x = true
⊢ ¬xs = []

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ eraseP p [] = [] ↔ [] = [] ∨ ∃ x, p x = true ∧ [] = [x]

Tactic:
simp

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] ↔ ∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []

Tactic:
constructor

Result:
case cons.isTrue.mp
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ xs = [] → ∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []

case cons.isTrue.mpr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
h : p x = true
⊢ (∃ x_1, p x_1 = true ∧ x = x_1 ∧ xs = []) → xs = []

Proof state:
case cons.isTrue.mpr.intro.intro.intro
α : Type u_1
p : α → Bool
x : α
h left✝ : p x = true
ih : eraseP p [] = [] ↔ [] = [] ∨ ∃ x, p x = true ∧ [] = [x]
⊢ [] = []

Tactic:
rfl

Result:
no goals