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

State before:
n m : Nat
α : Type ?u.31992
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ i < Array.size as.val
Tactic:
simp [hi]
State after:
no goals

State before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ Array.size as.val[i] = m
Tactic:
have : i < as.val.size := by rwa [as.property.1]
State after:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
this : i < Array.size as.val
⊢ Array.size as.val[i] = m

State before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
this : i < Array.size as.val
⊢ Array.size as.val[i] = m
Tactic:
simp [as.property.2 i this]
State after:
no goals

State before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ i < Array.size as.val
Tactic:
rwa [as.property.1]
State after:
no goals