Theorem: Array.zipWithAux_nil_first (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ zipWithAux f #[] x n z = z
Tactic:
unfold Array.zipWithAux
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ (if h : n < size #[] then
      let a := #[][n];
      if h : n < size x then
        let b := x[n];
        zipWithAux f #[] x (n + 1) (push z (f a b))
      else z
    else z) =
    z

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ (if h : n < size #[] then
      let a := #[][n];
      if h : n < size x then
        let b := x[n];
        zipWithAux f #[] x (n + 1) (push z (f a b))
      else z
    else z) =
    z
Tactic:
exact dif_neg n.not_lt_zero
State after:
no goals