case pos
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : p a = true
⊢ List.eraseP p l₁ <+ l₂✝

case neg
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : ¬p a = true
⊢ List.eraseP p l₁ <+ a :: List.eraseP p l₂✝
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
⊢ List.eraseP p l₁ <+ List.eraseP p (a :: l₂✝)
by_cases h : p a <;> simp [h]
no goals
case pos
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : p a = true
⊢ List.eraseP p l₁ <+ l₂✝

case neg
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : ¬p a = true
⊢ List.eraseP p l₁ <+ a :: List.eraseP p l₂✝
exacts [s.eraseP.trans (eraseP_sublist _), s.eraseP.cons _]
case pos
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : p a = true
⊢ l₁✝ <+ l₂✝

case neg
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : ¬p a = true
⊢ a :: List.eraseP p l₁✝ <+ a :: List.eraseP p l₂✝
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
⊢ List.eraseP p (a :: l₁✝) <+ List.eraseP p (a :: l₂✝)
by_cases h : p a <;> simp [h]
no goals
case pos
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : p a = true
⊢ l₁✝ <+ l₂✝

case neg
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : ¬p a = true
⊢ a :: List.eraseP p l₁✝ <+ a :: List.eraseP p l₂✝
exacts [s, s.eraseP.cons₂ _]