ι : Type ?u.424384
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ length (eraseP p l) + 1 = length l
ι : Type ?u.424384
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ length (eraseP p l) + 1 = length l
let ⟨_, l₁, l₂, _, _, h₁, h₂⟩ := exists_of_eraseP al pa
ι : Type ?u.424384
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ length l₁ + length l₂ + 1 = length l₁ + length (w✝ :: l₂)
ι : Type ?u.424384
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ length (eraseP p l) + 1 = length l
rw [h₂, h₁, length_append, length_append]
no goals
ι : Type ?u.424384
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ length l₁ + length l₂ + 1 = length l₁ + length (w✝ :: l₂)
rfl