-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
    (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
      | some a, some b => some (f a b) | _, _ => none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
as : Vector α n✝
bs : Vector β n✝
f : α → β → γ
i : Nat
⊢ (zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
bs : Vector β n✝
f : α → β → γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } bs)[i]? =
    match { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (match toArray✝¹[i]?, toArray✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none) =
    match toArray✝¹[i]?, toArray✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    match { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]?,
      { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp [Array.getElem?_zipWith]

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (match toArray✝¹[i]?, toArray✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none) =
    match toArray✝¹[i]?, toArray✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
bs : Vector β n✝
f : α → β → γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } bs)[i]? =
    match { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    match { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]?,
      { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none