-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem Nodup.erase_eq_filter [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a)

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝ : α
l✝ : List α
m : ∀ (a' : α), a' ∈ l✝ → a✝ ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l✝
ih : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝ :: l✝).erase a = filter (fun x => x != a) (a✝ :: l✝)

Tactic:
rename_i b l

Result:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase a = filter (fun x => x != a) l
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)

Proof state:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true

Tactic:
simpa [@eq_comm α] using m

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l

Tactic:
apply Eq.symm

Result:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ ¬(b != b) = true

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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)]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l

Proof state:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l

Tactic:
rw [filter_eq_self]

Result:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) l
ih : l.erase b = filter (fun x => x != b) l
⊢ (b :: l).erase b = filter (fun x => x != b) (b :: l)

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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'
_n : Pairwise (fun x1 x2 => x1 ≠ x2) 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)