-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
    (l.eraseP p).eraseP q = (l.eraseP q).eraseP p

Proof state:
case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
by_cases h₂ : q a

Result:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
h₂ : q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
h₂ : ¬q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Proof state:
case cons
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
⊢ eraseP q (eraseP p (a :: l)) = eraseP p (eraseP q (a :: l))

Tactic:
simp only [eraseP_cons]

Result:
case cons
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Proof state:
case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
h₂ : ¬q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]

Result:
no goals

Proof state:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
by_cases h₂ : q a

Result:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
h₂ : q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
h₂ : ¬q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Proof state:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
h₂ : q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]

Result:
no goals

Proof state:
case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
h₂ : ¬q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]

Result:
no goals

Proof state:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
h₂ : q a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p q : α → Bool
h : ∀ (a : α), a ∈ [] → ¬p a = true ∨ ¬q a = true
⊢ eraseP q (eraseP p []) = eraseP p (eraseP q [])

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

Tactic:
by_cases h₁ : p a

Result:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : p a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)

case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true) → eraseP q (eraseP p l) = eraseP p (eraseP q l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬p a_1 = true ∨ ¬q a_1 = true
h₁ : ¬p a = true
⊢ eraseP q (bif p a then l else a :: eraseP p l) = eraseP p (bif q a then l else a :: eraseP q l)