case neg
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ eraseP p (xs ++ l₂) = eraseP p xs ++ l₂
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
⊢ eraseP p (x :: xs ++ l₂) = eraseP p (x :: xs) ++ l₂
by_cases h' : p x <;> simp [h']
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ a = x → p x = true
case neg
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ eraseP p (xs ++ l₂) = eraseP p xs ++ l₂
rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
no goals
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ a = x → p x = true
intro | rfl => exact pa
no goals
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
x✝ : a = x
h : a ∈ a :: xs
h' : ¬p a = true
⊢ p a = true
exact pa