-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
    (l : List α) (a : α) (i : Nat) (w : l.idxOf a = i) :
    l.erase a = l.eraseIdx i

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Tactic:
right

Result:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Proof state:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ idxOf a l

Tactic:
exact Nat.le_of_eq (idxOf_eq_length h).symm

Result:
no goals

Proof state:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l = l.eraseIdx (idxOf a l)

Tactic:
rw [eq_comm, eraseIdx_eq_self]

Result:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ idxOf a l

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Tactic:
left

Result:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l)

Proof state:
case pos.h.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as bs : List α
h' : ¬a ∈ as
h : a ∈ as ++ a :: bs
⊢ (as ++ a :: bs).eraseIdx (idxOf a (as ++ a :: bs)) = as ++ bs

Tactic:
rw [idxOf_append, if_neg h', idxOf_cons_self, eraseIdx_append_of_length_le] <;>
  simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Tactic:
by_cases h : a ∈ l

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Proof state:
case pos.h.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as bs : List α
h' : ¬a ∈ as
h : a ∈ as ++ a :: bs
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ as ++ a :: bs = l₁ ++ a :: l₂ ∧ (as ++ a :: bs).eraseIdx (idxOf a (as ++ a :: bs)) = l₁ ++ l₂

Tactic:
refine ⟨as, bs, h', by simp, ?_⟩

Result:
case pos.h.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as bs : List α
h' : ¬a ∈ as
h : a ∈ as ++ a :: bs
⊢ (as ++ a :: bs).eraseIdx (idxOf a (as ++ a :: bs)) = as ++ bs

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

Tactic:
rw [erase_eq_iff]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l) ∨ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Proof state:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.eraseIdx (idxOf a l) = l₁ ++ l₂

Tactic:
obtain ⟨as, bs, rfl, h'⟩ := eq_append_cons_of_mem h

Result:
case pos.h.intro.intro.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as bs : List α
h' : ¬a ∈ as
h : a ∈ as ++ a :: bs
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ as ++ a :: bs = l₁ ++ a :: l₂ ∧ (as ++ a :: bs).eraseIdx (idxOf a (as ++ a :: bs)) = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
w : idxOf a l = i
⊢ l.erase a = l.eraseIdx i

Tactic:
subst w

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ l.erase a = l.eraseIdx (idxOf a l)

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

Tactic:
simp

Result:
no goals

Proof state:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ ¬a ∈ l ∧ l = l.eraseIdx (idxOf a l)

Tactic:
refine ⟨h, ?_⟩

Result:
case neg.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l = l.eraseIdx (idxOf a l)