case nil
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
l' : List β
n : ℕ
⊢ drop n (zipWith f [] l') = zipWith f (drop n []) (drop n l')

case cons
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
l' : List β
n : ℕ
⊢ drop n (zipWith f (hd :: tl) l') = zipWith f (drop n (hd :: tl)) (drop n l')
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ drop n (zipWith f l l') = zipWith f (drop n l) (drop n l')
induction' l with hd tl hl generalizing l' n
no goals
case nil
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
l' : List β
n : ℕ
⊢ drop n (zipWith f [] l') = zipWith f (drop n []) (drop n l')
simp
case cons.nil
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
⊢ drop n (zipWith f (hd :: tl) []) = zipWith f (drop n (hd :: tl)) (drop n [])

case cons.cons
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
head✝ : β
tail✝ : List β
⊢ drop n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop n (hd :: tl)) (drop n (head✝ :: tail✝))
case cons
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
l' : List β
n : ℕ
⊢ drop n (zipWith f (hd :: tl) l') = zipWith f (drop n (hd :: tl)) (drop n l')
cases l'
no goals
case cons.nil
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
⊢ drop n (zipWith f (hd :: tl) []) = zipWith f (drop n (hd :: tl)) (drop n [])
simp
case cons.cons.zero
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
⊢ drop zero (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop zero (hd :: tl)) (drop zero (head✝ :: tail✝))

case cons.cons.succ
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ drop (succ n✝) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (drop (succ n✝) (hd :: tl)) (drop (succ n✝) (head✝ :: tail✝))
case cons.cons
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
head✝ : β
tail✝ : List β
⊢ drop n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop n (hd :: tl)) (drop n (head✝ :: tail✝))
cases n
no goals
case cons.cons.zero
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
⊢ drop zero (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop zero (hd :: tl)) (drop zero (head✝ :: tail✝))
simp
no goals
case cons.cons.succ
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.208573
ε : Type ?u.208576
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ drop (succ n✝) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (drop (succ n✝) (hd :: tl)) (drop (succ n✝) (head✝ :: tail✝))
simp [hl]