case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR p l
⊢ @replaceF = @replaceFTR
funext α p l
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR.go p l #[]
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR p l
simp [replaceFTR]
no goals
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR.go p l #[]
exact (go #[] _).symm
no goals
α : Type u_1
p : α → Option α
l : List α
acc : Array α
⊢ replaceFTR.go p [] acc = acc.data ++ replaceF p []
simp [replaceFTR.go, replaceF]
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (match p x with
    | none => replaceFTR.go p xs (Array.push acc x)
    | some a' => acc.data ++ a' :: xs) =
    acc.data ++
      match p x with
      | none => x :: replaceF p xs
      | some a => a :: xs
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p (x :: xs) acc = acc.data ++ replaceF p (x :: xs)
simp [replaceFTR.go, replaceF]
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p xs (Array.push acc x) = acc.data ++ x :: replaceF p xs
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (match p x with
    | none => replaceFTR.go p xs (Array.push acc x)
    | some a' => acc.data ++ a' :: xs) =
    acc.data ++
      match p x with
      | none => x :: replaceF p xs
      | some a => a :: xs
cases p x <;> simp
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (Array.push acc x).data ++ replaceF p xs = acc.data ++ x :: replaceF p xs
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p xs (Array.push acc x) = acc.data ++ x :: replaceF p xs
rw [go _ xs]
no goals
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (Array.push acc x).data ++ replaceF p xs = acc.data ++ x :: replaceF p xs
simp