case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ removeNth l n = removeNthTR l n
⊢ @removeNth = @removeNthTR
funext α l n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ removeNth l n = removeNthTR.go l l n #[]
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ removeNth l n = removeNthTR l n
simp [removeNthTR]
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ removeNth l n = removeNthTR.go l l n #[]
suffices ∀ xs acc, l = acc.data ++ xs →
    removeNthTR.go l xs n acc = acc.data ++ xs.removeNth 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 → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
case h.h.h
α : Type u_1
l : List α
n : Nat
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
intro xs
no goals
α : Type u_1
l : List α
n : Nat
this : ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
⊢ l = #[].data ++ l
simp
no goals
case h.h.h.nil
α : Type u_1
l : List α
n : Nat
acc : Array α
⊢ l = acc.data ++ [] → removeNthTR.go l [] n acc = acc.data ++ removeNth [] n
simp [removeNth, removeNthTR.go]
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
acc : Array α
n✝ : Nat
⊢ l = acc.data ++ x :: xs → removeNthTR.go l xs n✝ (Array.push acc x) = acc.data ++ x :: removeNth xs n✝
case h.h.h.cons
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
n : Nat
acc : Array α
⊢ l = acc.data ++ x :: xs → removeNthTR.go l (x :: xs) n acc = acc.data ++ removeNth (x :: xs) n
cases n <;> simp [removeNth, removeNthTR.go, *]
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
acc : Array α
n✝ : Nat
h : l = acc.data ++ x :: xs
⊢ removeNthTR.go l xs n✝ (Array.push acc x) = acc.data ++ x :: removeNth xs n✝
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
acc : Array α
n✝ : Nat
⊢ l = acc.data ++ x :: xs → removeNthTR.go l xs n✝ (Array.push acc x) = acc.data ++ x :: removeNth xs n✝
intro h
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.data ++ xs → removeNthTR.go l xs n acc = acc.data ++ removeNth xs n
acc : Array α
n✝ : Nat
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ removeNth xs n✝ = acc.data ++ x :: removeNth xs n✝

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

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