case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ eraseIdx l n = eraseIdxTR l n
⊢ @eraseIdx = @eraseIdxTR
funext α l n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ eraseIdx l n = eraseIdxTR.go l l n #[]
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ eraseIdx l n = eraseIdxTR l n
simp [eraseIdxTR]
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ eraseIdx l n = eraseIdxTR.go l l n #[]
suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
  (this l #[] (by simp)).symm
case h.h.h
α : Type u_1
l : List α
n : Nat
xs : List α
⊢ ∀ (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
intro xs
no goals
case h.h.h
α : Type u_1
l : List α
n : Nat
xs : List α
⊢ ∀ (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
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 [eraseIdx, eraseIdxTR.go]
rw [IH]; simp; simp; exact h
no goals
α : Type u_1
l : List α
n : Nat
this : ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
⊢ l = #[].data ++ l
simp
no goals
case h.h.h.nil
α : Type u_1
l : List α
n : Nat
acc : Array α
h : l = acc.data ++ []
⊢ eraseIdxTR.go l [] n acc = acc.data ++ eraseIdx [] n
simp [eraseIdx, eraseIdxTR.go, h]
no goals
case h.h.h.cons
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
n : Nat
acc : Array α
h : l = acc.data ++ x :: xs
⊢ eraseIdxTR.go l (x :: xs) n acc = acc.data ++ eraseIdx (x :: xs) n
match n with
| 0 => simp [eraseIdx, eraseIdxTR.go]
| n+1 =>
  simp [eraseIdx, eraseIdxTR.go]
  rw [IH]; simp; simp; exact h
no goals
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
n : Nat
acc : Array α
h : l = acc.data ++ x :: xs
⊢ eraseIdxTR.go l (x :: xs) 0 acc = acc.data ++ eraseIdx (x :: xs) 0
simp [eraseIdx, eraseIdxTR.go]
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
n✝ : Nat
acc : Array α
h : l = acc.data ++ x :: xs
n : Nat
⊢ eraseIdxTR.go l xs n (Array.push acc x) = acc.data ++ x :: eraseIdx xs n
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
n✝ : Nat
acc : Array α
h : l = acc.data ++ x :: xs
n : Nat
⊢ eraseIdxTR.go l (x :: xs) (n + 1) acc = acc.data ++ eraseIdx (x :: xs) (n + 1)
simp [eraseIdx, eraseIdxTR.go]
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ eraseIdx xs n
n✝ : Nat
acc : Array α
h : l = acc.data ++ x :: xs
n : Nat
⊢ (Array.push acc x).data ++ eraseIdx xs n = acc.data ++ x :: eraseIdx xs n

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

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