-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : List α) :
    (filter f l).erase a = filter f (l.erase a)

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (if f x = true then x :: filter f xs else filter f xs).erase x = filter f xs

Tactic:
split

Result:
case pos.isTrue
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : f x = true
⊢ (x :: filter f xs).erase x = filter f xs

case pos.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : ¬f x = true
⊢ (filter f xs).erase x = filter f xs

Proof state:
case pos.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : ¬f x = true
⊢ ¬x ∈ filter f xs

Tactic:
simp_all [mem_filter]

Result:
no goals

Proof state:
case pos.isTrue
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : f x = true
⊢ (x :: filter f xs).erase x = filter f xs

Tactic:
rw [erase_cons_head]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
⊢ (if f x = true then x :: filter f xs else filter f xs).erase a =
    if f x = true then x :: filter f (xs.erase a) else filter f (xs.erase a)

Tactic:
split

Result:
case neg.isTrue
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
h✝ : f x = true
⊢ (x :: filter f xs).erase a = x :: filter f (xs.erase a)

case neg.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
h✝ : ¬f x = true
⊢ (filter f xs).erase a = filter f (xs.erase a)

Proof state:
case neg.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
h✝ : ¬f x = true
⊢ (filter f xs).erase a = filter f (xs.erase a)

Tactic:
rw [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
⊢ (filter f []).erase a = filter f ([].erase a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
⊢ ¬(x == a) = true

Tactic:
simpa using Ne.symm h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
h✝ : f x = true
⊢ ¬(x == a) = true

Tactic:
simpa using Ne.symm h

Result:
no goals

Proof state:
case pos.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : ¬f x = true
⊢ (filter f xs).erase x = filter f xs

Tactic:
rw [erase_of_not_mem]

Result:
case pos.isFalse
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
h✝ : ¬f x = true
⊢ ¬x ∈ filter f xs

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
⊢ (filter f (x :: xs)).erase a = filter f ((x :: xs).erase a)

Tactic:
by_cases h : a = x

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase a = filter f ((x :: xs).erase a)

case neg
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
⊢ (filter f (x :: xs)).erase a = filter f ((x :: xs).erase a)

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase a = filter f ((x :: xs).erase a)

Tactic:
rw [erase_cons]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase a = filter f (if (x == a) = true then xs else x :: xs.erase a)

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase x = filter f xs

Tactic:
rw [filter_cons]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (if f x = true then x :: filter f xs else filter f xs).erase x = filter f xs

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
⊢ (filter f (x :: xs)).erase a = filter f ((x :: xs).erase a)

Tactic:
rw [erase_cons_tail (by simpa using Ne.symm h), filter_cons, filter_cons]

Result:
case neg
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
⊢ (if f x = true then x :: filter f xs else filter f xs).erase a =
    if f x = true then x :: filter f (xs.erase a) else filter f (xs.erase a)

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase a = filter f (if (x == a) = true then xs else x :: xs.erase a)

Tactic:
simp only [h, beq_self_eq_true, ↓reduceIte]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : a = x
⊢ (filter f (x :: xs)).erase x = filter f xs

Proof state:
case neg.isTrue
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
x : α
xs : List α
ih : (filter f xs).erase a = filter f (xs.erase a)
h : ¬a = x
h✝ : f x = true
⊢ (x :: filter f xs).erase a = x :: filter f (xs.erase a)

Tactic:
rw [erase_cons_tail (by simpa using Ne.symm h), ih]

Result:
no goals