[GOAL]
α : Type u
l : Thunk (List α)
t : List α
⊢ (fun xs => Thunk.get l ++ xs) t = (fun xs => Thunk.get l ++ xs) [] ++ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
⊢ toList (ofList l) = l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
⊢ toList (ofList []) = []
case cons α : Type u head✝ : α tail✝ : List α ⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
simp only [DList.toList, DList.ofList, List.cons_append, List.append_nil]
[GOAL]
α : Type u
l : DList α
⊢ ofList (toList l) = l
[PROOFSTEP]
cases' l with app inv
[GOAL]
case mk
α : Type u
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ ofList (toList { apply := app, invariant := inv }) = { apply := app, invariant := inv }
[PROOFSTEP]
simp only [ofList, toList, mk.injEq]
[GOAL]
case mk
α : Type u
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ (fun x => app [] ++ x) = app
[PROOFSTEP]
funext x
[GOAL]
case mk.h
α : Type u
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
x : List α
⊢ app [] ++ x = app x
[PROOFSTEP]
rw [(inv x)]
[GOAL]
α : Type u
⊢ toList empty = []
[PROOFSTEP]
simp
[GOAL]
α : Type u
x : α
⊢ toList (singleton x) = [x]
[PROOFSTEP]
simp
[GOAL]
α : Type u
l₁ l₂ : DList α
⊢ toList (append l₁ l₂) = toList l₁ ++ toList l₂
[PROOFSTEP]
cases' l₁ with _ l₁_invariant
[GOAL]
case mk
α : Type u
l₂ : DList α
apply✝ : List α → List α
l₁_invariant : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ toList (append { apply := apply✝, invariant := l₁_invariant } l₂) =
    toList { apply := apply✝, invariant := l₁_invariant } ++ toList l₂
[PROOFSTEP]
cases' l₂
[GOAL]
case mk.mk
α : Type u
apply✝¹ : List α → List α
l₁_invariant : ∀ (l : List α), apply✝¹ l = apply✝¹ [] ++ l
apply✝ : List α → List α
invariant✝ : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ toList (append { apply := apply✝¹, invariant := l₁_invariant } { apply := apply✝, invariant := invariant✝ }) =
    toList { apply := apply✝¹, invariant := l₁_invariant } ++ toList { apply := apply✝, invariant := invariant✝ }
[PROOFSTEP]
simp
[GOAL]
case mk.mk
α : Type u
apply✝¹ : List α → List α
l₁_invariant : ∀ (l : List α), apply✝¹ l = apply✝¹ [] ++ l
apply✝ : List α → List α
invariant✝ : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ apply✝¹ (apply✝ []) = apply✝¹ [] ++ apply✝ []
[PROOFSTEP]
rw [l₁_invariant]
[GOAL]
α : Type u
x : α
l : DList α
⊢ toList (cons x l) = x :: toList l
[PROOFSTEP]
cases l
[GOAL]
case mk
α : Type u
x : α
apply✝ : List α → List α
invariant✝ : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ toList (cons x { apply := apply✝, invariant := invariant✝ }) =
    x :: toList { apply := apply✝, invariant := invariant✝ }
[PROOFSTEP]
simp
[GOAL]
α : Type u
x : α
l : DList α
⊢ toList (push l x) = toList l ++ [x]
[PROOFSTEP]
cases' l with _ l_invariant
[GOAL]
case mk
α : Type u
x : α
apply✝ : List α → List α
l_invariant : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ toList (push { apply := apply✝, invariant := l_invariant } x) =
    toList { apply := apply✝, invariant := l_invariant } ++ [x]
[PROOFSTEP]
simp
[GOAL]
case mk
α : Type u
x : α
apply✝ : List α → List α
l_invariant : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ apply✝ [x] = apply✝ [] ++ [x]
[PROOFSTEP]
rw [l_invariant]
