α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ List.erase l a = l₁ ++ l₂
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ List.erase l a = l₁ ++ l₂
let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ eraseP (fun b => decide (a = b)) l = l₁ ++ l₂
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ List.erase l a = l₁ ++ l₂
rw [erase_eq_eraseP]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ eraseP (fun b => decide (a = b)) l = l₁ ++ l₂
exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩