case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l : List α
a : α
⊢ List.erase [] a = List.filter (fun x => decide (x ≠ a)) []

case cons
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l : List α
d : Nodup l
a : α
⊢ List.erase l a = List.filter (fun x => decide (x ≠ a)) l
induction' d with b l m _ IH
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)

case neg
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
case cons
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
by_cases h : b = a
no goals
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l : List α
a : α
⊢ List.erase [] a = List.filter (fun x => decide (x ≠ a)) []
rfl
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.erase (b :: l) b = List.filter (fun x => decide (x ≠ b)) (b :: l)
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
subst h
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ l = List.filter (fun x => decide (x ≠ b)) l
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.erase (b :: l) b = List.filter (fun x => decide (x ≠ b)) (b :: l)
rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.filter (fun x => decide (x ≠ b)) l = l
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ l = List.filter (fun x => decide (x ≠ b)) l
symm
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ ∀ (a : α), a ∈ l → decide (a ≠ b) = true
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.filter (fun x => decide (x ≠ b)) l = l
rw [filter_eq_self]
no goals
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ ∀ (a : α), a ∈ l → decide (a ≠ b) = true
simpa [@eq_comm α] using m
no goals
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ ¬decide (b ≠ b) = true
simp
case neg.pa
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ decide (b ≠ a) = true
case neg
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
rw [erase_cons_tail _ h, filter_cons_of_pos, IH]
no goals
case neg.pa
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ decide (b ≠ a) = true
simp [h]