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

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ size (zipWith x y f) = min (size x) (size y)
Tactic:
simp only [size, zipWith_data_eq_zipWith_data]
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.length (List.zipWith f x.data y.data) = min (List.length x.data) (List.length y.data)

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.length (List.zipWith f x.data y.data) = min (List.length x.data) (List.length y.data)
Tactic:
exact List.length_zipWith' f x.data y.data
State after:
no goals