-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬l.any p = true
⊢ l.length = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : l.any p = true
⊢ l.length - 1 = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
simp only [any_eq_true, length_eq_zero] at h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ l.length - 1 = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Proof state:
case isTrue.mp
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ l.length - 1 = l.length → ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
intro

Result:
case isTrue.mp
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
a✝ : l.length - 1 = l.length
⊢ ∀ (a : α), a ∈ l → ¬p a = true

Proof state:
case isTrue.mpr.intro.intro
α : Type u_1
p : α → Bool
l : List α
a✝ : ∀ (a : α), a ∈ l → ¬p a = true
x : α
m : x ∈ l
h : p x = true
⊢ l.length - 1 = l.length

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ l.length - 1 = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
constructor

Result:
case isTrue.mp
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ l.length - 1 = l.length → ∀ (a : α), a ∈ l → ¬p a = true

case isTrue.mpr
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ (∀ (a : α), a ∈ l → ¬p a = true) → l.length - 1 = l.length

Proof state:
case isTrue.mpr
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ (∀ (a : α), a ∈ l → ¬p a = true) → l.length - 1 = l.length

Tactic:
intro

Result:
case isTrue.mpr
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
a✝ : ∀ (a : α), a ∈ l → ¬p a = true
⊢ l.length - 1 = l.length

Proof state:
case isTrue.mp
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
a✝ : l.length - 1 = l.length
⊢ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
simp_all [Nat.sub_one_eq_self]

Result:
no goals

Proof state:
case isTrue.mpr
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
a✝ : ∀ (a : α), a ∈ l → ¬p a = true
⊢ l.length - 1 = l.length

Tactic:
obtain ⟨x, m, h⟩ := h

Result:
case isTrue.mpr.intro.intro
α : Type u_1
p : α → Bool
l : List α
a✝ : ∀ (a : α), a ∈ l → ¬p a = true
x : α
m : x ∈ l
h : p x = true
⊢ l.length - 1 = l.length

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (if l.any p = true then l.length - 1 else l.length) = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : l.any p = true
⊢ l.length - 1 = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬l.any p = true
⊢ l.length = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = l ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ (if l.any p = true then l.length - 1 else l.length) = l.length ↔ ∀ (a : α), a ∈ l → ¬p a = true