case nil
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l'✝ l' : List δ
⊢ map f (zipWith g [] l') = zipWith (fun x y => f (g x y)) [] l'

case cons
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l'✝ : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
l' : List δ
⊢ map f (zipWith g (hd :: tl) l') = zipWith (fun x y => f (g x y)) (hd :: tl) l'
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l : List γ
l' : List δ
⊢ map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'
induction' l with hd tl hl generalizing l'
no goals
case nil
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l'✝ l' : List δ
⊢ map f (zipWith g [] l') = zipWith (fun x y => f (g x y)) [] l'
simp
case cons.nil
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
⊢ map f (zipWith g (hd :: tl) []) = zipWith (fun x y => f (g x y)) (hd :: tl) []

case cons.cons
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
head✝ : δ
tail✝ : List δ
⊢ map f (zipWith g (hd :: tl) (head✝ :: tail✝)) = zipWith (fun x y => f (g x y)) (hd :: tl) (head✝ :: tail✝)
case cons
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l'✝ : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
l' : List δ
⊢ map f (zipWith g (hd :: tl) l') = zipWith (fun x y => f (g x y)) (hd :: tl) l'
cases l'
no goals
case cons.nil
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
⊢ map f (zipWith g (hd :: tl) []) = zipWith (fun x y => f (g x y)) (hd :: tl) []
simp
no goals
case cons.cons
α : Type u
β : Type u_3
γ : Type u_2
δ✝ : Type ?u.62572
ε : Type ?u.62575
δ : Type u_1
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
head✝ : δ
tail✝ : List δ
⊢ map f (zipWith g (hd :: tl) (head✝ :: tail✝)) = zipWith (fun x y => f (g x y)) (hd :: tl) (head✝ :: tail✝)
simp [hl]