Theorem: Array.zipWithAux_nil_second (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 x then
      let a := x[n];
      if h : n < size #[] then
        let b := #[][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 x then
      let a := x[n];
      if h : n < size #[] then
        let b := #[][n];
        zipWithAux f x #[] (n + 1) (push z (f a b))
      else z
    else z) =
    z
Tactic:
dsimp [size]
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then if h_1 : n < 0 then zipWithAux f x #[] (n + 1) (push z (f x[n] #[][n])) else z
    else z) =
    z

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then if h_1 : n < 0 then zipWithAux f x #[] (n + 1) (push z (f x[n] #[][n])) else z
    else z) =
    z
Tactic:
simp only [dif_neg n.not_lt_zero]
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then z else z) = z

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then z else z) = z
Tactic:
apply dite (n < x.size) <;> (intro h; simp only [h, dif_neg, dif_pos])
State after:
no goals

State before:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ ¬n < size x → (if h : n < List.length x.data then z else z) = z
Tactic:
intro h
State after:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
h : ¬n < size x
⊢ (if h : n < List.length x.data then z else z) = z

State before:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
h : ¬n < size x
⊢ (if h : n < List.length x.data then z else z) = z
Tactic:
simp only [h, dif_neg, dif_pos]
State after:
no goals