α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
⊢ a ∈ eraseP p l
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ a ∈ eraseP p l ↔ a ∈ l
refine ⟨mem_of_mem_eraseP, fun al => ?_⟩
no goals
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
⊢ a ∈ eraseP p l
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]
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ l
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ eraseP p l
rw [h]
no goals
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
al : a ∈ l
h : eraseP p l = l
⊢ a ∈ l
assumption
α : 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₂
α : 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
rw [h₄]
α : 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₂
α : 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₂
rw [h₃] at al
α : 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₂
α : 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₂
have : a ≠ c := fun h => (h ▸ pa).elim h₂
α : 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₂
α : 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₂
simp [this] at al
no goals
α : 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₂
simp [al]