-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem erase_eq_eraseTR : @List.erase = @eraseTR

Proof state:
case h.h.h.h.cons.true
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif true then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match true with
      | true => xs
      | false => x :: xs.erase a

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif false then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match false with
      | true => xs
      | false => x :: xs.erase a

Tactic:
rw [IH] <;> simp_all

Result:
no goals

Proof state:
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif x == a then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match x == a with
      | true => xs
      | false => x :: xs.erase a

Tactic:
cases x == a

Result:
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif false then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match false with
      | true => xs
      | false => x :: xs.erase a

case h.h.h.h.cons.true
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif true then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match true with
      | true => xs
      | false => x :: xs.erase a

Proof state:
case h.h.h.h.nil
α : Type u_1
x✝ : BEq α
l : List α
a : α
acc : Array α
h : l = acc.toList ++ []
⊢ eraseTR.go l a [] acc = acc.toList ++ [].erase a

Tactic:
simp [List.erase, eraseTR.go, h]

Result:
no goals

Proof state:
α : Type u_1
x✝ : BEq α
l : List α
a : α
this : ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
⊢ l = #[].toList ++ l

Tactic:
simp

Result:
no goals

Proof state:
⊢ @List.erase = @eraseTR

Tactic:
funext α _ l a

Result:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ l.erase a = l.eraseTR a

Proof state:
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ eraseTR.go l a (x :: xs) acc = acc.toList ++ (x :: xs).erase a

Tactic:
simp only [eraseTR.go, Array.toListAppend_eq, List.erase]

Result:
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ (bif x == a then acc.toList ++ xs else eraseTR.go l a xs (acc.push x)) =
    acc.toList ++
      match x == a with
      | true => xs
      | false => x :: xs.erase a

Proof state:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ l.erase a = eraseTR.go l a l #[]

Tactic:
suffices ∀ xs acc, l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a from
  (this l #[] (by simp)).symm

Result:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a

Proof state:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a

Tactic:
intro xs

Result:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a

Proof state:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ l.erase a = l.eraseTR a

Tactic:
simp [eraseTR]

Result:
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ l.erase a = eraseTR.go l a l #[]