case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = enumFromTR n l
⊢ @enumFrom = @enumFromTR
funext α n l
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = enumFromTR n l
simp [enumFromTR, -Array.size_toArray]
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
  | [], n => rfl
  | a::as, n => by
    rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]; simp; rfl
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l).data).snd
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l)
        (Array.size (toArray l))).snd
rw [Array.foldr_eq_foldr_data]
no goals
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l =
    (foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + Array.size (toArray l), []) (toArray l).data).snd
simp [go]
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ f a (Nat.succ n, enumFrom (Nat.succ n) as) = (n, enumFrom n (a :: as))
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ foldr f (n + length (a :: as), []) (a :: as) = (n, enumFrom n (a :: as))
rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ Nat.succ n - 1 = n
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ f a (Nat.succ n, enumFrom (Nat.succ n) as) = (n, enumFrom n (a :: as))
simp
no goals
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ Nat.succ n - 1 = n
rfl