-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.toArray.size then
      let a := as.toArray[i + 1];
      if h : i + 1 < bs.toArray.size then
        let b := bs.toArray[i + 1];
        as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f a b))
      else cs
    else cs) =
    if h : i < as.tail.toArray.size then
      let a := as.tail.toArray[i];
      if h : i < bs.tail.toArray.size then
        let b := bs.tail.toArray[i];
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f a b))
      else cs
    else cs

Tactic:
simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.length then
      if h_1 : i + 1 < bs.length then as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Proof state:
case isTrue.isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : i + 1 < bs.length
⊢ as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1])) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Tactic:
rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : i + 1 < bs.length
⊢ i < bs.length - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.length then
      if h_1 : i + 1 < bs.length then as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Tactic:
split <;> rename_i h₁

Result:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
⊢ (if h : i + 1 < bs.length then as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1]))
    else cs) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : ¬i + 1 < as.length
⊢ cs =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : ¬i + 1 < as.length
⊢ ¬i < as.length - 1

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ cs =
    if h : i < bs.length - 1 then as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
    else cs

Tactic:
rw [dif_neg (by omega)]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
⊢ (if h : i + 1 < bs.length then as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1]))
    else cs) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Tactic:
split <;> rename_i h₂

Result:
case isTrue.isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : i + 1 < bs.length
⊢ as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f as[i + 1] bs[i + 1])) =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

case isTrue.isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ cs =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ as.toArray.zipWithAux bs.toArray f (i + 1) cs = as.tail.toArray.zipWithAux bs.tail.toArray f i cs

Tactic:
rw [zipWithAux]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.toArray.size then
      let a := as.toArray[i + 1];
      if h : i + 1 < bs.toArray.size then
        let b := bs.toArray[i + 1];
        as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f a b))
      else cs
    else cs) =
    as.tail.toArray.zipWithAux bs.tail.toArray f i cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ ¬i < bs.length - 1

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ cs =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Tactic:
rw [dif_pos (by omega)]

Result:
case isTrue.isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ cs =
    if h : i < bs.length - 1 then as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
    else cs

Proof state:
case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : ¬i + 1 < as.length
⊢ cs =
    if h : i < as.length - 1 then
      if h_1 : i < bs.length - 1 then
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f as[i + 1] bs[i + 1]))
      else cs
    else cs

Tactic:
rw [dif_neg (by omega)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : ¬i + 1 < bs.length
⊢ i < as.length - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
h₁ : i + 1 < as.length
h₂ : i + 1 < bs.length
⊢ i < as.length - 1

Tactic:
omega

Result:
no goals