Theorem: Array.getElem_mkArray (Aoc2023/Utils.lean)

State before:
α : Type ?u.25800
n : Nat
a : α
i : Nat
hi : i < n
⊢ i < size (mkArray n a)
Tactic:
simp [size_mkArray, hi]
State after:
no goals

State before:
α : Type u_1
n : Nat
a : α
i : Nat
hi : i < n
⊢ let_fun this := (_ : i < size (mkArray n a));
  (mkArray n a)[i] = a
Tactic:
simp only [mkArray, Array.getElem_eq_data_get, List.get_replicate]
State after:
no goals