-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_iff [LawfulBEq α] {a : α} {l : Array α} :
    l.erase a = l' ↔
      (a ∉ l ∧ l = l') ∨
        ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁.push 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' : Array α
h : ¬a' ∈ l'
x : Array α
⊢ ¬a' ∈ l'.push a' ++ x ∧ l'.push a' ++ x = l' ++ x ∨
    ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l'.push a' ++ x = l₁.push 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' : Array α
h : ¬a' ∈ l'
x : Array α
⊢ ∃ l₁, ¬a' ∈ l₁ ∧ ∃ x_1, l'.push a' ++ x = l₁.push a' ++ x_1 ∧ l' ++ x = l₁ ++ x_1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : Array α
h : ¬a ∈ l₁
x : Array α
⊢ l₁.push a ++ x = l₁.push a ++ x ∧ l₁ ++ x = l₁ ++ x

Tactic:
simp

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
l' : Array α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁.push a ++ x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ a_2 l₁, ¬a ∈ l₁ ∧ a_2 = a ∧ ∃ x, l = l₁.push 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 : Array α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁.push a_1 ++ x ∧ l = l₁ ++ x

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

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

Tactic:
constructor

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

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

Proof state:
α : Type u_1
inst✝¹ : BEq α
l' : Array α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ ((∀ (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₁.push a_1 ++ l₂ ∧ l' = l₁ ++ l₂) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂

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

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

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

Tactic:
left

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

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
l' : Array α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (¬a ∈ l ∧ l = l' ∨ ∃ a_1 l₁, ¬a ∈ l₁ ∧ a_1 = a ∧ ∃ x, l = l₁.push a_1 ++ x ∧ l' = l₁ ++ x) →
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁.push 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 : Array α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l ∨ ∃ l₁, ¬a ∈ l₁ ∧ ∃ x, l = l₁.push a ++ x ∧ l = l₁ ++ x

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

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

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

Result:
no goals

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

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

Result:
no goals

Proof state:
case mpr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : Array α
h : ¬a ∈ l₁
x : Array α
⊢ ¬a ∈ l₁.push a ++ x ∧ l₁.push a ++ x = l₁ ++ x ∨
    ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁.push a ++ x = l₁_1.push 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₁ : Array α
h : ¬a ∈ l₁
x : Array α
⊢ ∃ a_1 l₁_1, ¬a ∈ l₁_1 ∧ a_1 = a ∧ ∃ x_1, l₁.push a ++ x = l₁_1.push a_1 ++ x_1 ∧ l₁ ++ x = l₁_1 ++ x_1

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

Tactic:
rw [erase_eq_eraseP', eraseP_eq_iff]

Result:
α : Type u_1
inst✝¹ : BEq α
l' : Array α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ ((∀ (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₁.push a_1 ++ l₂ ∧ l' = l₁ ++ l₂) ↔
    ¬a ∈ l ∧ l = l' ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
left

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