case x
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ get (tail (zipWith f x y)) m✝ = get (zipWith f (tail x) (tail y)) m✝
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ tail (zipWith f x y) = zipWith f (tail x) (tail y)
ext
no goals
case x
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ get (tail (zipWith f x y)) m✝ = get (zipWith f (tail x) (tail y)) m✝
simp [get_tail]