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

case cons
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.191507
ε : Type ?u.191510
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
l' : List β
n : ℕ
⊢ take n (zipWith f (hd :: tl) l') = zipWith f (take n (hd :: tl)) (take n l')
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.191507
ε : Type ?u.191510
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ take n (zipWith f l l') = zipWith f (take n l) (take 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.191507
ε : Type ?u.191510
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
l' : List β
n : ℕ
⊢ take n (zipWith f [] l') = zipWith f (take n []) (take n l')
simp
case cons.nil
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.191507
ε : Type ?u.191510
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : ℕ
⊢ take n (zipWith f (hd :: tl) []) = zipWith f (take n (hd :: tl)) (take n [])

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

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