-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
    l.erase a = l' ↔
      (a ∉ l ∧ l = l') ∨
        ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Proof state:
case mp.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a' : α
l' : List α
h : ¬a' ∈ l'
x : List α
⊢ ¬a' ∈ l' ++ a' :: x ∧ l' ++ a' :: x = l' ++ x ∨
    ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l' ++ a' :: x = l₁ ++ a' :: x_1 ∧ l' ++ x = l₁ ++ x_1

Tactic:
right

Result:
case mp.inr.intro.intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a' : α
l' : List α
h : ¬a' ∈ l'
x : List α
⊢ ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l' ++ a' :: x = l₁ ++ a' :: x_1 ∧ l' ++ x = l₁ ++ x_1

Proof state:
case mpr.inl.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ l₁
x : List α
⊢ ¬a ∈ l₁ ++ a :: x ∧ l₁ ++ a :: x = l₁ ++ x ∨
    ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁ ++ a :: x = l₁_1 ++ a_1 :: x_1 ∧ l₁ ++ x = l₁_1 ++ x_1

Tactic:
right

Result:
case mpr.inr.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ l₁
x : List α
⊢ ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁ ++ a :: x = l₁_1 ++ a_1 :: x_1 ∧ l₁ ++ x = l₁_1 ++ x_1

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Tactic:
rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩)

Result:
case mp.inl.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l = l₁ ++ x

case mp.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a' : α
l' : List α
h : ¬a' ∈ l'
x : List α
⊢ ¬a' ∈ l' ++ a' :: x ∧ l' ++ a' :: x = l' ++ x ∨
    ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l' ++ a' :: x = l₁ ++ a' :: x_1 ∧ l' ++ x = l₁ ++ x_1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ l₁
x : List α
⊢ a = a ∧ ∃ x_1, l₁ ++ a :: x = l₁ ++ a :: x_1 ∧ l₁ ++ x = l₁ ++ x_1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l' = l₁ ++ x) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

case mpr
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ a_2 l₁, ¬a ∈ l₁ ∧ a_2 = a ∧ ∃ x, l = l₁ ++ a_2 :: x ∧ l' = l₁ ++ x

Proof state:
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ ((∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ∧ l = l' ∨
      ∃ a_1 l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬(b == a) = true) ∧ (a_1 == a) = true ∧ l = l₁ ++ a_1 :: l₂ ∧ l' = l₁ ++ l₂) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Tactic:
simp only [beq_iff_eq, forall_mem_ne', exists_and_left]

Result:
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l' = l₁ ++ x) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Proof state:
case mpr.inl.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l = l₁ ++ x

Tactic:
left

Result:
case mpr.inl.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l

Proof state:
case mp.inl.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a' : α
l' : List α
h : ¬a' ∈ l'
x : List α
⊢ l' ++ a' :: x = l' ++ a' :: x ∧ l' ++ x = l' ++ x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ l.erase a = l' ↔ ¬a ∈ l ∧ l = l' ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Tactic:
rw [erase_eq_eraseP', eraseP_eq_iff]

Result:
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ ((∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ∧ l = l' ∨
      ∃ a_1 l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬(b == a) = true) ∧ (a_1 == a) = true ∧ l = l₁ ++ a_1 :: l₂ ∧ l' = l₁ ++ l₂) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Proof state:
case mpr.inr.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ l₁
x : List α
⊢ ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁ ++ a :: x = l₁_1 ++ a_1 :: x_1 ∧ l₁ ++ x = l₁_1 ++ x_1

Tactic:
refine ⟨a, l₁, h, by simp⟩

Result:
no goals

Proof state:
case mp.inl.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l = l₁ ++ x

Tactic:
left

Result:
case mp.inl.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
l' : List α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ a_2 l₁, ¬a ∈ l₁ ∧ a_2 = a ∧ ∃ x, l = l₁ ++ a_2 :: x ∧ l' = l₁ ++ x

Tactic:
rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩)

Result:
case mpr.inl.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁ ++ a_1 :: x ∧ l = l₁ ++ x

case mpr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ l₁
x : List α
⊢ ¬a ∈ l₁ ++ a :: x ∧ l₁ ++ a :: x = l₁ ++ x ∨
    ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁ ++ a :: x = l₁_1 ++ a_1 :: x_1 ∧ l₁ ++ x = l₁_1 ++ x_1

Proof state:
case mp.inr.intro.intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a' : α
l' : List α
h : ¬a' ∈ l'
x : List α
⊢ ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l' ++ a' :: x = l₁ ++ a' :: x_1 ∧ l' ++ x = l₁ ++ x_1

Tactic:
refine ⟨l', h, x, by simp⟩

Result:
no goals