α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ∃ x y,
    get? l ↑i = some x ∧
      get? l' ↑i = some y ∧
        f x y =
          f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get (zipWith f l l') i =
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
rw [← Option.some_inj, ← get?_eq_get, get?_zip_with_eq_some]
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ∃ x y,
    get? l ↑i = some x ∧
      get? l' ↑i = some y ∧
        f x y =
          f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
exact
  ⟨l.get ⟨i, lt_length_left_of_zipWith i.isLt⟩, l'.get ⟨i, lt_length_right_of_zipWith i.isLt⟩,
    by rw [get?_eq_get], by rw [get?_eq_get]; exact ⟨rfl, rfl⟩⟩
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get? l ↑i = some (get l { val := ↑i, isLt := (_ : ↑i < length l) })
rw [get?_eq_get]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ some (get l' { val := ↑i, isLt := ?m.160309 }) = some (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) ∧
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) =
      f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })

α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ↑i < length l'
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get? l' ↑i = some (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) ∧
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) =
      f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
rw [get?_eq_get]
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ some (get l' { val := ↑i, isLt := ?m.160309 }) = some (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) ∧
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) =
      f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })

α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.159788
ε : Type ?u.159791
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ↑i < length l'
exact ⟨rfl, rfl⟩