case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR l n a
⊢ @set = @setTR
funext α l n a
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR.go l a l n #[]
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR l n a
simp [setTR]
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR.go l a l n #[]
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR.go l a l n #[]
let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
  setTR.go l a xs n acc = acc.data ++ xs.set n a
| [], _ => fun h => by simp [setTR.go, set, h]
| x::xs, 0 => by simp [setTR.go, set]
| x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
no goals
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ set l n a = setTR.go l a l n #[]
exact (go #[] _ _ rfl).symm
no goals
α : Type u_1
l : List α
n : Nat
a : α
acc : Array α
x✝ : Nat
h : l = acc.data ++ []
⊢ setTR.go l a [] x✝ acc = acc.data ++ set [] x✝ a
simp [setTR.go, set, h]
no goals
α : Type u_1
l : List α
n : Nat
a : α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs → setTR.go l a (x :: xs) 0 acc = acc.data ++ set (x :: xs) 0 a
simp [setTR.go, set]
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ setTR.go l a xs n (Array.push acc x) = acc.data ++ x :: set xs n a
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ setTR.go l a (x :: xs) (n + 1) acc = acc.data ++ set (x :: xs) (n + 1) a
simp [setTR.go, set]
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ set xs n a = acc.data ++ x :: set xs n a

case a
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ setTR.go l a xs n (Array.push acc x) = acc.data ++ x :: set xs n a
rw [go _ xs]
case a
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ set xs n a = acc.data ++ x :: set xs n a

case a
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
{simp}
no goals
case a
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp [h]