no goals
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l <+ l
match exists_or_eq_self_of_eraseP p l with
| .inl h => rw [h]; apply Sublist.refl
| .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ l <+ l
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ eraseP p l <+ l
rw [h]
no goals
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ l <+ l
apply Sublist.refl
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ l₁ ++ l₂ <+ l₁ ++ c :: l₂
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ eraseP p l <+ l
rw [h₄, h₃]
no goals
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ l₁ ++ l₂ <+ l₁ ++ c :: l₂
simp