Remove unnecessary lemmas

Author: wkrozowski

src/Init/GetElem.lean

@@ -240,7 +240,7 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
   getElem?_eq_some_iff.mp h
 
-theorem of_getElem_eq  [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem of_getElem_eq [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     {c : cont} {i : idx} [Decidable (dom c i)] {h} (_ : c[i] = e) : dom c i := h
 
 @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -718,8 +718,6 @@ theorem getThenInsertIfNew?_snd [EquivBEq α] [LawfulHashable α] {k : α} {v :
     (getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
   ext (ExtDHashMap.Const.getThenInsertIfNew?_snd)
 
-theorem mem_of_get_eq [LawfulBEq α] (m : ExtHashMap α β) {k : α} {v : β} {w} (_ : m.get k w = v) : k ∈ m := w
-
 instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (ExtHashMap α β) α β (fun m a => a ∈ m) where
   getElem?_def m a _ := by
     split

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -751,8 +751,6 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] {k : α} {v : β} :
     (getThenInsertIfNew? t k v).2 = t.insertIfNew k v :=
   ext <| ExtDTreeMap.Const.getThenInsertIfNew?_snd
 
-theorem mem_of_get_eq [TransCmp cmp] {k : α} {v : β} {w} (_ : t.get k w = v) : k ∈ t := w
-
 instance [TransCmp cmp] : LawfulGetElem (ExtTreeMap α β cmp) α β (fun m a => a ∈ m) where
   getElem?_def m a _ := by
     split

src/Std/Data/HashMap/Lemmas.lean

@@ -810,8 +810,6 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
     (getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
   ext (DHashMap.Const.getThenInsertIfNew?_snd)
 
-theorem mem_of_get_eq {k : α} {v : β} {w} (_ : m.get k w = v) : k ∈ m := w
-
 instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β (fun m a => a ∈ m) where
   getElem?_def m a _ := by
     split

src/Std/Data/HashMap/RawLemmas.lean

@@ -828,8 +828,6 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
     (getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
-theorem mem_of_get_eq {k : α} {v : β} {w} (_ : m.get k w = v) : k ∈ m := w
-
 @[simp, grind =]
 theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size :=

src/Std/Data/TreeMap/Lemmas.lean

@@ -782,8 +782,6 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] {k : α} {v : β} :
     (getThenInsertIfNew? t k v).2 = t.insertIfNew k v :=
   ext <| DTreeMap.Const.getThenInsertIfNew?_snd
 
-theorem mem_of_get_eq  {k : α} {v : β} {w} (_ : t.get k w = v) : k ∈ t := w
-
 instance [TransCmp cmp] : LawfulGetElem (TreeMap α β cmp) α β (fun m a => a ∈ m) where
   getElem?_def m a _ := by
     split

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -789,8 +789,6 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (getThenInsertIfNew? t k v).2 = t.insertIfNew k v :=
   ext <| DTreeMap.Raw.Const.getThenInsertIfNew?_snd h
 
-theorem mem_of_get_eq  {k : α} {v : β} {w} (_ : t.get k w = v) : k ∈ t := w
-
 @[simp, grind =]
 theorem length_keys [TransCmp cmp] (h : t.WF) :
     t.keys.length = t.size :=