feat: HashMap.empty_find? + helper lemmas (#544)

Co-authored-by: Joe Hendrix <jhendrix@whoisjoe.info>
Co-authored-by: Timo Carlin-Burns <timorcb@gmail.com>

Std/Data/Array/Lemmas.lean

@@ -31,6 +31,9 @@ theorem getElem?_neg [GetElem Cont Idx Elem Dom]
 
 @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
 
+@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
+    (mkArray n v)[i]'h = v := by simp [Array.getElem_eq_data_get]
+
 namespace Array
 
 attribute [simp] isEmpty uget

Std/Data/HashMap/Lemmas.lean

@@ -4,12 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Std.Data.HashMap.Basic
+import Std.Data.Array.Lemmas
 import Std.Util.ProofWanted
 
 namespace Std.HashMap
 
-@[simp] proof_wanted empty_find? [BEq α] [Hashable α] {a : α} :
-    (∅ : HashMap α β).find? a = none
+namespace Imp
+
+@[simp] theorem empty_buckets :
+    (empty : Imp α β).buckets = ⟨mkArray 8 AssocList.nil, by simp⟩ := rfl
+
+@[simp] theorem empty_val [BEq α] [Hashable α] : (∅ : HashMap α β).val = Imp.empty := rfl
+
+end Imp
+
+@[simp] theorem empty_find? [BEq α] [Hashable α] {a : α} :
+    (∅ : HashMap α β).find? a = none := by simp [find?, Imp.find?]
 
 proof_wanted insert_find? [BEq α] [Hashable α] (m : HashMap α β) (a a' : α) (b : β) :
     (m.insert a b).find? a' = if a' == a then some b else m.find? a'