α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ List.nthLe (List.zipWith f ↑x ↑y) ↑i (_ : ↑i < List.length (List.zipWith f ↑x ↑y)) =
    f
      (match x, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ get (zipWith f x y) i = f (get x i) (get y i)
dsimp only [Vector.zipWith, Vector.get]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
y : Vector β n
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y) ↑i
      (_ : ↑i < List.length (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y)) =
    f
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ List.nthLe (List.zipWith f ↑x ↑y) ↑i (_ : ↑i < List.length (List.zipWith f ↑x ↑y)) =
    f
      (match x, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
cases x
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin n
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List β
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ }) ↑i
      (_ :
        ↑i <
          List.length
            (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ })) =
    f
      (match { val := val✝¹, property := property✝¹ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
y : Vector β n
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y) ↑i
      (_ : ↑i < List.length (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y)) =
    f
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
cases y
no goals
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin n
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List β
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ }) ↑i
      (_ :
        ↑i <
          List.length
            (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ })) =
    f
      (match { val := val✝¹, property := property✝¹ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
simp only [List.nthLe_zipWith]