no goals
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = Array.toListAppend acc (lookmap f l)
cases l with
| nil => rfl
| cons hd tl =>
  rw [lookmap, go, go]
  cases f hd with
  | none => simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_data]; rfl
  | some a => rfl
no goals
case nil
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
⊢ go f [] acc = Array.toListAppend acc (lookmap f [])
rfl
case cons
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => Array.toListAppend acc (b :: tl)
    | none => go f tl (Array.push acc hd)) =
    Array.toListAppend acc
      (match f hd with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
case cons
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = Array.toListAppend acc (lookmap f (hd :: tl))
rw [lookmap, go, go]
no goals
case cons
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => Array.toListAppend acc (b :: tl)
    | none => go f tl (Array.push acc hd)) =
    Array.toListAppend acc
      (match f hd with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
cases f hd with
| none => simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_data]; rfl
| some a => rfl
case cons.none
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.data ++ ([hd] ++ lookmap f tl) = acc.data ++ (#[].data ++ ([hd] ++ lookmap f tl))
case cons.none
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match none with
    | some b => Array.toListAppend acc (b :: tl)
    | none => go f tl (Array.push acc hd)) =
    Array.toListAppend acc
      (match none with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_data]
no goals
case cons.none
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.data ++ ([hd] ++ lookmap f tl) = acc.data ++ (#[].data ++ ([hd] ++ lookmap f tl))
rfl
no goals
case cons.some
ι : Type ?u.340195
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
acc : Array α
hd : α
tl : List α
a : α
⊢ (match some a with
    | some b => Array.toListAppend acc (b :: tl)
    | none => go f tl (Array.push acc hd)) =
    Array.toListAppend acc
      (match some a with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
rfl