case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR f as bs
⊢ @zipWithLeft' = @zipWithLeft'TR
funext α β γ f as bs
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR f as bs
simp [zipWithLeft'TR]
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]
let rec go (acc) : ∀ as bs, zipWithLeft'TR.go f as bs acc =
    let (l, r) := as.zipWithLeft' f bs; (acc.toList ++ l, r)
| [], bs => by simp [zipWithLeft'TR.go]
| _::_, [] => by simp [zipWithLeft'TR.go, Array.foldl_data_eq_map]
| a::as, b::bs => by simp [zipWithLeft'TR.go, go _ as bs]
no goals
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]
simp [zipWithLeft'TR, go]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs✝ : List β
acc : Array γ
bs : List β
⊢ zipWithLeft'TR.go f [] bs acc =
    match zipWithLeft' f [] bs with
    | (l, r) => (Array.toList acc ++ l, r)
simp [zipWithLeft'TR.go]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
acc : Array γ
head✝ : α
tail✝ : List α
⊢ zipWithLeft'TR.go f (head✝ :: tail✝) [] acc =
    match zipWithLeft' f (head✝ :: tail✝) [] with
    | (l, r) => (Array.toList acc ++ l, r)
simp [zipWithLeft'TR.go, Array.foldl_data_eq_map]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as✝ : List α
bs✝ : List β
acc : Array γ
a : α
as : List α
b : β
bs : List β
⊢ zipWithLeft'TR.go f (a :: as) (b :: bs) acc =
    match zipWithLeft' f (a :: as) (b :: bs) with
    | (l, r) => (Array.toList acc ++ l, r)
simp [zipWithLeft'TR.go, go _ as bs]