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

State before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Fin (Array.size as.val)
⊢ Array.size as.val[i] = m
Tactic:
simp only [getElem_fin, as.property.2 i i.isLt]
State after:
no goals