-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ (acc.push x).toList ++ xs.eraseIdx n = acc.toList ++ x :: xs.eraseIdx n

case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = (acc.push x).toList ++ xs

Tactic:
simp

Result:
case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = (acc.push x).toList ++ xs

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ eraseIdxTR.go l xs n (acc.push x) = acc.toList ++ x :: xs.eraseIdx n

Tactic:
rw [IH]

Result:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ (acc.push x).toList ++ xs.eraseIdx n = acc.toList ++ x :: xs.eraseIdx n

case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = (acc.push x).toList ++ xs

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ eraseIdxTR.go l (x :: xs) 0 acc = acc.toList ++ (x :: xs).eraseIdx 0

Tactic:
simp [eraseIdx, eraseIdxTR.go]

Result:
no goals

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ eraseIdxTR.go l (x :: xs) (n + 1) acc = acc.toList ++ (x :: xs).eraseIdx (n + 1)

Tactic:
simp only [eraseIdxTR.go, eraseIdx]

Result:
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ eraseIdxTR.go l xs n (acc.push x) = acc.toList ++ x :: xs.eraseIdx n

Proof state:
case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = acc.toList ++ x :: xs

Tactic:
exact h

Result:
no goals

Proof state:
⊢ @eraseIdx = @eraseIdxTR

Tactic:
funext α l n

Result:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ l.eraseIdx n = l.eraseIdxTR n

Proof state:
case h.h.h
α : Type u_1
l : List α
n : Nat
xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n

Tactic:
induction xs generalizing n with intro acc h
| nil => simp [eraseIdx, eraseIdxTR.go, h]
| cons x xs IH =>
match n with
| 0 => simp [eraseIdx, eraseIdxTR.go]
| n+1 =>
simp only [eraseIdxTR.go, eraseIdx]
rw [IH]; simp; simp; exact h

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
this : ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
⊢ l = #[].toList ++ l

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ l.eraseIdx n = eraseIdxTR.go l l n #[]

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

Result:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n

Proof state:
case h.h.h.nil
α : Type u_1
l : List α
n : Nat
acc : Array α
h : l = acc.toList ++ []
⊢ eraseIdxTR.go l [] n acc = acc.toList ++ [].eraseIdx n

Tactic:
simp [eraseIdx, eraseIdxTR.go, h]

Result:
no goals

Proof state:
case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = (acc.push x).toList ++ xs

Tactic:
simp

Result:
case a
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n✝ : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
n : Nat
⊢ l = acc.toList ++ x :: xs

Proof state:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n

Tactic:
intro xs

Result:
case h.h.h
α : Type u_1
l : List α
n : Nat
xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n

Proof state:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ l.eraseIdx n = l.eraseIdxTR n

Tactic:
simp [eraseIdxTR]

Result:
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ l.eraseIdx n = eraseIdxTR.go l l n #[]

Proof state:
case h.h.h.cons
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n
n : Nat
acc : Array α
h : l = acc.toList ++ x :: xs
⊢ eraseIdxTR.go l (x :: xs) n acc = acc.toList ++ (x :: xs).eraseIdx n

Tactic:
match n with
| 0 => simp [eraseIdx, eraseIdxTR.go]
| n+1 =>
  simp only [eraseIdxTR.go, eraseIdx]
  rw [IH]; simp; simp; exact h

Result:
no goals