case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l'✝ : List β
n : ℕ
h✝ : length l = length l'✝
l' : List β
h : length [] = length l'
⊢ reverse (zipWith f [] l') = zipWith f (reverse []) (reverse l')

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

case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length (hd :: tl) = length (hd' :: tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l'✝ : List β
n : ℕ
h✝ : length l = length l'✝
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
l' : List β
h : length (hd :: tl) = length l'
⊢ reverse (zipWith f (hd :: tl) l') = zipWith f (reverse (hd :: tl)) (reverse l')
cases' l' with hd' tl'
no goals
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
h : length (hd :: tl) = length []
⊢ reverse (zipWith f (hd :: tl) []) = zipWith f (reverse (hd :: tl)) (reverse [])
simp
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length (hd :: tl) = length (hd' :: tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
simp only [add_left_inj, length] at h
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
this : length (reverse tl) = length (reverse tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
have : tl.reverse.length = tl'.reverse.length := by simp [h]
no goals
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
this : length (reverse tl) = length (reverse tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
simp [hl _ h, zipWith_append _ _ _ _ _ this]
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.262855
ε : Type ?u.262858
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
⊢ length (reverse tl) = length (reverse tl')
simp [h]