case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l
⊢ @filterMap = @filterMapTR
funext α β f l
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l
let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
  | [], acc => by simp [filterMapTR.go, filterMap]
  | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
no goals
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l
exact (go l #[]).symm
no goals
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
acc : Array β
⊢ filterMapTR.go f [] acc = acc.data ++ filterMap f []
simp [filterMapTR.go, filterMap]
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ (match f a with
    | none => acc.data ++ filterMap f as
    | some b => acc.data ++ b :: filterMap f as) =
    acc.data ++
      match f a with
      | none => filterMap f as
      | some b => b :: filterMap f as
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ filterMapTR.go f (a :: as) acc = acc.data ++ filterMap f (a :: as)
simp [filterMapTR.go, filterMap, go as]
no goals
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ (match f a with
    | none => acc.data ++ filterMap f as
    | some b => acc.data ++ b :: filterMap f as) =
    acc.data ++
      match f a with
      | none => filterMap f as
      | some b => b :: filterMap f as
split <;> simp [*]