ι : Type ?u.341936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    a :: lookmap.go f l #[]
ι : Type ?u.341936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) = a :: lookmap f l
simp only [lookmap, lookmap.go, Array.toListAppend_eq, Array.data_toArray, nil_append]
ι : Type ?u.341936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => Array.toListAppend (Array.push #[] a) (lookmap f l)) =
    a :: lookmap.go f l #[]
ι : Type ?u.341936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    a :: lookmap.go f l #[]
rw [lookmap.go_append, h]
no goals
ι : Type ?u.341936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => Array.toListAppend (Array.push #[] a) (lookmap f l)) =
    a :: lookmap.go f l #[]
rfl