-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) :
    (l.erase a).erase b = (l.erase b).erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : a ∈ l
hb : b ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
match l, l.erase a, exists_erase_eq ha with
| _, _, ⟨l₁, l₂, ha', rfl, rfl⟩ =>
  if h₁ : b ∈ l₁ then
    rw [erase_append_left _ h₁, erase_append_left _ h₁,
        erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]
  else
    rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
        erase_cons_tail ab, erase_cons_head]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
l₁ l₂ : List α
ha' : ¬a ∈ l₁
ha : a ∈ l₁ ++ a :: l₂
hb : b ∈ l₁ ++ a :: l₂
h₁ : ¬b ∈ l₁
⊢ (l₁ ++ l₂).erase b = ((l₁ ++ a :: l₂).erase b).erase a

Tactic:
rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
    erase_cons_tail ab, erase_cons_head]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : a ∈ l
hb : ¬b ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
simp only [erase_of_not_mem hb, erase_of_not_mem (mt mem_of_mem_erase hb)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : (a == b) = true
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
rw [eq_of_beq ab]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
l₁ l₂ : List α
ha' : ¬a ∈ l₁
ha : a ∈ l₁ ++ a :: l₂
hb : b ∈ l₁ ++ a :: l₂
⊢ (l₁ ++ l₂).erase b = ((l₁ ++ a :: l₂).erase b).erase a

Tactic:
if h₁ : b ∈ l₁ then
  rw [erase_append_left _ h₁, erase_append_left _ h₁,
      erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]
else
  rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
      erase_cons_tail ab, erase_cons_head]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
if ha : a ∈ l then ?_ else
  simp only [erase_of_not_mem ha, erase_of_not_mem (mt mem_of_mem_erase ha)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : a ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : a ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
if hb : b ∈ l then ?_ else
  simp only [erase_of_not_mem hb, erase_of_not_mem (mt mem_of_mem_erase hb)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : a ∈ l
hb : b ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
l₁ l₂ : List α
ha' : ¬a ∈ l₁
ha : a ∈ l₁ ++ a :: l₂
hb : b ∈ l₁ ++ a :: l₂
h₁ : b ∈ l₁
⊢ (l₁ ++ l₂).erase b = ((l₁ ++ a :: l₂).erase b).erase a

Tactic:
rw [erase_append_left _ h₁, erase_append_left _ h₁,
    erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
ha : ¬a ∈ l
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
simp only [erase_of_not_mem ha, erase_of_not_mem (mt mem_of_mem_erase ha)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
if ab : a == b then rw [eq_of_beq ab] else ?_

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
ab : ¬(a == b) = true
⊢ (l.erase a).erase b = (l.erase b).erase a