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

State before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ size (zipWithN as bs f p) = size as
Tactic:
apply zipWithNSizeGo
State after:
case ip
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 ≤ size as

case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]

State before:
case ip
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 ≤ size as

case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Tactic:
. apply Nat.zero_le
State after:
case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]

State before:
case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Tactic:
. simp [Array.size, List.length]
State after:
no goals