-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
this : a ≠ c
al : a ∈ l₁ ∨ a ∈ l₂
⊢ a ∈ l₁ ++ l₂

Tactic:
simp [al]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
⊢ a ∈ eraseP p l

Tactic:
match exists_or_eq_self_of_eraseP p l with
| .inl h => rw [h]; assumption
| .inr ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ =>
  rw [h₄]; rw [h₃] at al
  have : a ≠ c := fun h => (h ▸ pa).elim h₂
  simp [this] at al; simp [al]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
al : a ∈ l₁ ++ c :: l₂
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ a ∈ l₁ ++ l₂

Tactic:
have : a ≠ c := fun h => (h ▸ pa).elim h₂

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
al : a ∈ l₁ ++ c :: l₂
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
this : a ≠ c
⊢ a ∈ l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ l

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
al : a ∈ l₁ ++ c :: l₂
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
this : a ≠ c
⊢ a ∈ l₁ ++ l₂

Tactic:
simp [this] at al

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
this : a ≠ c
al : a ∈ l₁ ∨ a ∈ l₂
⊢ a ∈ l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ a ∈ eraseP p l

Tactic:
rw [h₄]

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ a ∈ l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ a ∈ l₁ ++ l₂

Tactic:
rw [h₃] at al

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
c : α
l₁ l₂ : List α
al : a ∈ l₁ ++ c :: l₂
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ a ∈ l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ a ∈ eraseP p l ↔ a ∈ l

Tactic:
refine ⟨mem_of_mem_eraseP, fun al => ?_⟩

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
⊢ a ∈ eraseP p l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ eraseP p l

Tactic:
rw [h]

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ l