case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ List.erase l a = eraseTR l a
⊢ @List.erase = @eraseTR
funext α _ l a
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ List.erase l a = eraseTR.go l a l #[]
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ List.erase l a = eraseTR l a
simp [eraseTR]
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ List.erase l a = eraseTR.go l a l #[]
suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
  (this l #[] (by simp)).symm
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
xs : List α
⊢ ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
case h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
a : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
intro xs
no goals
α : Type u_1
x✝ : BEq α
l : List α
a : α
this : ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
⊢ l = #[].data ++ l
simp
no goals
case h.h.h.h.nil
α : Type u_1
x✝ : BEq α
l : List α
a : α
acc : Array α
h : l = acc.data ++ []
⊢ eraseTR.go l a [] acc = acc.data ++ List.erase [] a
simp [List.erase, eraseTR.go, h]
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ (bif x == a then acc.data ++ xs else eraseTR.go l a xs (Array.push acc x)) =
    acc.data ++
      match x == a with
      | true => xs
      | false => x :: List.erase xs a
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ eraseTR.go l a (x :: xs) acc = acc.data ++ List.erase (x :: xs) a
simp [List.erase, eraseTR.go]
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ eraseTR.go l a xs (Array.push acc x) = acc.data ++ x :: List.erase xs a
case h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ (bif x == a then acc.data ++ xs else eraseTR.go l a xs (Array.push acc x)) =
    acc.data ++
      match x == a with
      | true => xs
      | false => x :: List.erase xs a
cases x == a <;> simp
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ List.erase xs a = acc.data ++ x :: List.erase xs a

case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ eraseTR.go l a xs (Array.push acc x) = acc.data ++ x :: List.erase xs a
rw [IH]
case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.h.cons.false
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ List.erase xs a = acc.data ++ x :: List.erase xs a

case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
no goals
case h.h.h.h.cons.false.a
α : Type u_1
x✝ : BEq α
l : List α
a x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ List.erase xs a
acc : Array α
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
exact h