case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs
⊢ @zipWith = @zipWithTR
funext α β γ f as bs
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs
let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
  | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
  | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
no goals
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs
exact (go as bs #[]).symm
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
head✝ : α
tail✝ : List α
acc : Array γ
⊢ zipWithTR.go f (head✝ :: tail✝) [] acc = acc.data ++ zipWith f (head✝ :: tail✝) []
simp [zipWithTR.go, zipWith]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as✝ : List α
bs✝ : List β
a : α
as : List α
b : β
bs : List β
acc : Array γ
⊢ zipWithTR.go f (a :: as) (b :: bs) acc = acc.data ++ zipWith f (a :: as) (b :: bs)
simp [zipWithTR.go, zipWith, go as bs]