further renaming

Author: wkrozowski

src/Std/Data/ExtDHashMap/Basic.lean

@@ -397,7 +397,7 @@ theorem beq_of_eq [LawfulBEq α] [BEq β] [ReflBEq β] (m₁ m₂ : ExtDHashMap
     case mk b =>
       exact DHashMap.Const.Equiv.beq <| exact h
 
-theorem eq_of_beq_eq_true [LawfulBEq α] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) (h : Const.beq m₁ m₂) : m₁ = m₂ := by
+theorem eq_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) (h : Const.beq m₁ m₂) : m₁ = m₂ := by
   induction m₁
   case mk a =>
     induction m₂
@@ -416,8 +416,8 @@ theorem beq_unit_of_eq [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit)
   apply beq_of_eq
   exact h
 
-theorem eq_of_beq_unit_eq_true [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : Const.beq_unit m₁ m₂) : m₁ = m₂ := by
-  apply eq_of_beq_eq_true
+theorem eq_of_beq_unit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : Const.beq_unit m₁ m₂) : m₁ = m₂ := by
+  apply eq_of_beq
   exact h
 
 end Const

src/Std/Data/ExtHashMap/Basic.lean

@@ -262,7 +262,7 @@ instance [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (ExtHashMap α β) w
     have ⟨a⟩ := a
     have ⟨b⟩ := b
     simp only [mk.injEq] at |- hyp
-    exact ExtDHashMap.Const.eq_of_beq_eq_true _ _ hyp
+    exact ExtDHashMap.Const.eq_of_beq _ _ hyp
 
 @[inline, inherit_doc ExtDHashMap.inter]
 def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : ExtHashMap α β := ⟨ExtDHashMap.inter m₁.inner m₂.inner⟩

src/Std/Data/ExtHashSet/Basic.lean

@@ -222,7 +222,7 @@ instance [LawfulBEq α] : LawfulBEq (ExtHashSet α) where
     have ⟨⟨a⟩⟩ := a
     have ⟨⟨b⟩⟩ := b
     simp only [mk.injEq, ExtHashMap.mk.injEq] at |- hyp
-    exact ExtDHashMap.Const.eq_of_beq_unit_eq_true _ _ hyp
+    exact ExtDHashMap.Const.eq_of_beq_unit _ _ hyp
 
 /--
 Computes the intersection of the given hash sets.