Merge branch 'wojciech/hashmap_beq2' into wojciech/treemap_beq

Author: wkrozowski

src/Std/Data/ExtDHashMap/Basic.lean

@@ -406,22 +406,6 @@ theorem eq_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDHashMa
 
 end Const
 
-namespace Const
-
-@[inline, inherit_doc DHashMap.beq]
-def beqUnit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) : Bool := lift₂ (fun x y : DHashMap α fun _ => Unit => DHashMap.Const.beq x y)
-  (fun _ _ _ _ => DHashMap.Const.Equiv.beq_congr) m₁ m₂
-
-theorem beqUnit_of_eq [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : m₁ = m₂) : Const.beqUnit m₁ m₂ := by
-  apply beq_of_eq
-  exact h
-
-theorem eq_of_beqUnit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : Const.beqUnit m₁ m₂) : m₁ = m₂ := by
-  apply eq_of_beq
-  exact h
-
-end Const
-
 @[inline, inherit_doc DHashMap.inter]
 def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : ExtDHashMap α β := lift₂ (fun x y : DHashMap α β => mk (x.inter y))
   (fun a b c d equiv₁ equiv₂ => by

src/Std/Data/ExtHashSet/Basic.lean

@@ -205,24 +205,21 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : ExtHas
 instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashSet α) := ⟨union⟩
 
 @[inline, inherit_doc ExtHashMap.beq]
-def beq [LawfulBEq α] (m₁ m₂ : ExtHashSet α) : Bool := ExtDHashMap.Const.beqUnit m₁.inner.inner m₂.inner.inner
+def beq [LawfulBEq α] (m₁ m₂ : ExtHashSet α) : Bool := ExtDHashMap.Const.beq m₁.inner.inner m₂.inner.inner
 
 instance [LawfulBEq α] : BEq (ExtHashSet α) := ⟨beq⟩
 
 instance [LawfulBEq α] : ReflBEq (ExtHashSet α) where
-  rfl := by
-    intro a
-    cases a
-    case mk a =>
-      apply ExtDHashMap.Const.beqUnit_of_eq
-      rfl
+  rfl {a} := by
+    have ⟨a⟩ := a
+    exact ExtDHashMap.Const.beq_of_eq _ _ rfl
 
 instance [LawfulBEq α] : LawfulBEq (ExtHashSet α) where
   eq_of_beq {a} {b} hyp  := by
     have ⟨⟨a⟩⟩ := a
     have ⟨⟨b⟩⟩ := b
     simp only [mk.injEq, ExtHashMap.mk.injEq] at |- hyp
-    exact ExtDHashMap.Const.eq_of_beqUnit _ _ hyp
+    exact ExtDHashMap.Const.eq_of_beq _ _ hyp
 
 /--
 Computes the intersection of the given hash sets.