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

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

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ (if h : n + 1 < size (cons a x) then
      let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z
    else z) =
    if h : n < size x then
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
    else z
Tactic:
refine dite_congr (propext ⟨Nat.lt_of_succ_lt_succ,Nat.succ_lt_succ⟩) ?_ (λ _ => rfl)
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ ∀ (h : n < size x),
    (let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z) =
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ ∀ (h : n < size x),
    (let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z) =
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
Tactic:
intros
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ (let a_1 := (cons a x)[n + 1];
    if h : n + 1 < size (cons b y) then
      let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
    else z) =
    let a := x[n];
    if h : n < size y then
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f a b))
    else z

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ (let a_1 := (cons a x)[n + 1];
    if h : n + 1 < size (cons b y) then
      let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
    else z) =
    let a := x[n];
    if h : n < size y then
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f a b))
    else z
Tactic:
refine dite_congr (propext ⟨Nat.lt_of_succ_lt_succ,Nat.succ_lt_succ⟩) ?_ (λ _ => rfl)
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ ∀ (h : n < size y),
    (let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f x[n] b))

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ ∀ (h : n < size y),
    (let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f x[n] b))
Tactic:
intros
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ (let b_1 := (cons b y)[n + 1];
    zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
    let b := y[n];
    zipWithAux f x y (n + 1) (push z (f x[n] b))

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ (let b_1 := (cons b y)[n + 1];
    zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
    let b := y[n];
    zipWithAux f x y (n + 1) (push z (f x[n] b))
Tactic:
dsimp
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f x[n] y[n])) =
    zipWithAux f x y (n + 1) (push z (f x[n] y[n]))

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f x[n] y[n])) =
    zipWithAux f x y (n + 1) (push z (f x[n] y[n]))
Tactic:
exact zipWithAux_cons_cons_succ f a x b y (n+1) _
State after:
no goals