-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

Proof state:
case cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
l' : List α✝¹
n : Nat
⊢ take n (zipWith f (hd :: tl) l') = zipWith f (take n (hd :: tl)) (take n l')

Tactic:
cases l'

Result:
case cons.nil
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : Nat
⊢ take n (zipWith f (hd :: tl) []) = zipWith f (take n (hd :: tl)) (take n [])

case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : Nat
head✝ : α✝¹
tail✝ : List α✝¹
⊢ take n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take n (hd :: tl)) (take n (head✝ :: tail✝))

Proof state:
case cons.nil
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : Nat
⊢ take n (zipWith f (hd :: tl) []) = zipWith f (take n (hd :: tl)) (take n [])

Tactic:
simp

Result:
no goals

Proof state:
case nil
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : List α✝¹
n : Nat
⊢ take n (zipWith f [] l') = zipWith f (take n []) (take n l')

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons.zero
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : α✝¹
tail✝ : List α✝¹
⊢ take 0 (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take 0 (hd :: tl)) (take 0 (head✝ :: tail✝))

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons.succ
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : α✝¹
tail✝ : List α✝¹
n✝ : Nat
⊢ take (n✝ + 1) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (take (n✝ + 1) (hd :: tl)) (take (n✝ + 1) (head✝ :: tail✝))

Tactic:
simp [hl]

Result:
no goals

Proof state:
case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : Nat
head✝ : α✝¹
tail✝ : List α✝¹
⊢ take n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take n (hd :: tl)) (take n (head✝ :: tail✝))

Tactic:
cases n

Result:
case cons.cons.zero
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : α✝¹
tail✝ : List α✝¹
⊢ take 0 (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take 0 (hd :: tl)) (take 0 (head✝ :: tail✝))

case cons.cons.succ
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : α✝¹
tail✝ : List α✝¹
n✝ : Nat
⊢ take (n✝ + 1) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (take (n✝ + 1) (hd :: tl)) (take (n✝ + 1) (head✝ :: tail✝))