-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem reverse_zipWith (h : l.length = l'.length) :
    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Proof state:
case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹}, tl.length = l'.length → (zipWith f tl l').reverse = zipWith f tl.reverse l'.reverse
hd' : α✝¹
tl' : List α✝¹
h : tl.length = tl'.length
this : tl.reverse.length = tl'.reverse.length
⊢ (zipWith f (hd :: tl) (hd' :: tl')).reverse = zipWith f (hd :: tl).reverse (hd' :: tl').reverse

Tactic:
simp [hl h, zipWith_append _ _ _ _ _ this]

Result:
no goals

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : List α✝²
l' : List α✝¹
h : l.length = l'.length
⊢ (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Tactic:
induction l generalizing l' with
| nil => simp
| cons hd tl hl =>
  cases l' with
  | nil => simp
  | cons hd' tl' =>
    simp only [Nat.add_right_cancel_iff, length] at h
    have : tl.reverse.length = tl'.reverse.length := by simp [h]
    simp [hl h, zipWith_append _ _ _ _ _ this]

Result:
no goals

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

Tactic:
simp only [Nat.add_right_cancel_iff, length] at h

Result:
case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹}, tl.length = l'.length → (zipWith f tl l').reverse = zipWith f tl.reverse l'.reverse
hd' : α✝¹
tl' : List α✝¹
h : tl.length = tl'.length
⊢ (zipWith f (hd :: tl) (hd' :: tl')).reverse = zipWith f (hd :: tl).reverse (hd' :: tl').reverse

Proof state:
case nil
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : List α✝¹
h : [].length = l'.length
⊢ (zipWith f [] l').reverse = zipWith f [].reverse l'.reverse

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 α✝¹}, tl.length = l'.length → (zipWith f tl l').reverse = zipWith f tl.reverse l'.reverse
l' : List α✝¹
h : (hd :: tl).length = l'.length
⊢ (zipWith f (hd :: tl) l').reverse = zipWith f (hd :: tl).reverse l'.reverse

Tactic:
cases l' with
| nil => simp
| cons hd' tl' =>
  simp only [Nat.add_right_cancel_iff, length] at h
  have : tl.reverse.length = tl'.reverse.length := by simp [h]
  simp [hl h, zipWith_append _ _ _ _ _ this]

Result:
no goals

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

Tactic:
have : tl.reverse.length = tl'.reverse.length := by simp [h]

Result:
case cons.cons
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹}, tl.length = l'.length → (zipWith f tl l').reverse = zipWith f tl.reverse l'.reverse
hd' : α✝¹
tl' : List α✝¹
h : tl.length = tl'.length
this : tl.reverse.length = tl'.reverse.length
⊢ (zipWith f (hd :: tl) (hd' :: tl')).reverse = zipWith f (hd :: tl).reverse (hd' :: tl').reverse

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
hd : α✝²
tl : List α✝²
hl : ∀ {l' : List α✝¹}, tl.length = l'.length → (zipWith f tl l').reverse = zipWith f tl.reverse l'.reverse
hd' : α✝¹
tl' : List α✝¹
h : tl.length = tl'.length
⊢ tl.reverse.length = tl'.reverse.length

Tactic:
simp [h]

Result:
no goals

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

Tactic:
simp

Result:
no goals