Theorem: Misc.List.Nodup.erase_eq_filter (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
d : l.Nodup
a : α
⊢ l.erase a = filter (fun x => x != a) l
Tactic:
induction d
State after:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)

State before:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)
Tactic:
. rfl
State after:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)

State before:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
by_cases h : b = a
State after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : ¬b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)

State before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
subst h
State after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ (b :: l).erase b = filter (fun x => x != b) (b :: l)

State before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ (b :: l).erase b = filter (fun x => x != b) (b :: l)
Tactic:
rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
State after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l

State before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l
Tactic:
apply Eq.symm
State after:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l

State before:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l
Tactic:
rw [filter_eq_self]
State after:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true

State before:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true
Tactic:
simpa [@eq_comm α] using m
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ¬(b != b) = true
Tactic:
simp
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : ¬b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
simp [beq_false_of_ne h, IH, h]
State after:
no goals