Theorem: Array.ZipWithN.zipWithNSizeGo (Advent/Array.lean)

State before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size (go as bs f p arr i) = size as
Tactic:
unfold go
State after:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size
      (if q : i < size as then
        let a := as[i];
        let b := bs[i];
        go as bs f p (push arr (f a b)) (i + 1)
      else arr) =
    size as

State before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size
      (if q : i < size as then
        let a := as[i];
        let b := bs[i];
        go as bs f p (push arr (f a b)) (i + 1)
      else arr) =
    size as
Tactic:
split
State after:
case inl
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : i < size as
⊢ size
      (let a := as[i];
      let b := bs[i];
      go as bs f p (push arr (f a b)) (i + 1)) =
    size as

case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as

State before:
case inl
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : i < size as
⊢ size
      (let a := as[i];
      let b := bs[i];
      go as bs f p (push arr (f a b)) (i + 1)) =
    size as

case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Tactic:
. apply zipWithNSizeGo
  . apply Nat.succ_le_of_lt
    assumption
  . rw [Array.size_push]
    simp
    assumption
State after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as

State before:
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Tactic:
. rw [<-ap] 
  apply Nat.le_antisymm
  . assumption
  . apply Nat.le_of_not_lt
    assumption
State after:
no goals