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

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

Tactic:
simp [hl]

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}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : α✝¹
tail✝ : List α✝¹
⊢ drop 0 (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop 0 (hd :: tl)) (drop 0 (head✝ :: tail✝))

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
case cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
l' : List α✝¹
n : Nat
⊢ drop n (zipWith f (hd :: tl) l') = zipWith f (drop n (hd :: tl)) (drop 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}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : Nat
⊢ drop n (zipWith f (hd :: tl) []) = zipWith f (drop n (hd :: tl)) (drop n [])

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

Proof state:
case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹} {n : Nat}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : Nat
head✝ : α✝¹
tail✝ : List α✝¹
⊢ drop n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop n (hd :: tl)) (drop 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}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : α✝¹
tail✝ : List α✝¹
⊢ drop 0 (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop 0 (hd :: tl)) (drop 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}, drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : α✝¹
tail✝ : List α✝¹
n✝ : Nat
⊢ drop (n✝ + 1) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (drop (n✝ + 1) (hd :: tl)) (drop (n✝ + 1) (head✝ :: tail✝))