Theorem: Vec₂.size_toArrayVec (Aoc2023/Utils.lean)

State before:
n m : Nat
α : Type u_1
grid : Vec₂ n m α
⊢ Array.size (toArrayVec grid) = n
Tactic:
rw [toArrayVec, Array.size_mapIdx, grid.property.1]
State after:
no goals