Theorem: LoVe.map_zip (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α α' β β' : Type
f : α → α'
g : β → β'
x : α
xs : List α
y : β
ys : List β
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip (x :: xs) (y :: ys)) = zip (map f (x :: xs)) (map g (y :: ys))
Tactic:
simp [zip, map, map_zip f g xs ys]
State after:
no goals

State before:
α α' β β' : Type
f : α → α'
g : β → β'
x✝ : List β
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip [] x✝) = zip (map f []) (map g x✝)
Tactic:
rfl
State after:
no goals

State before:
α α' β β' : Type
f : α → α'
g : β → β'
head✝ : α
tail✝ : List α
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip (head✝ :: tail✝) []) = zip (map f (head✝ :: tail✝)) (map g [])
Tactic:
rfl
State after:
no goals