Resolve Markus' comments

Author: wkrozowski

src/Std/Data/DHashMap/DecidableEquiv.lean

@@ -18,6 +18,6 @@ open Std.DHashMap.Internal
 
 namespace Std.DHashMap
 
-instance {α : Type u} {β : α → Type v} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)] (m₁ m₂ : DHashMap α β) : Decidable (m₁ ~m m₂) := @decidable_of_iff _ _ ⟨fun h => ⟨h⟩, fun h => h.1⟩ <| Raw₀.decidable_equiv ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ m₁.2 m₂.2
+instance {α : Type u} {β : α → Type v} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)] (m₁ m₂ : DHashMap α β) : Decidable (m₁ ~m m₂) := @decidable_of_iff _ _ ⟨fun h => ⟨h⟩, fun h => h.1⟩ <| Raw₀.decidableEquiv ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ m₁.2 m₂.2
 
 end Std.DHashMap

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -5140,9 +5140,8 @@ end Raw₀
 namespace Raw₀
 
 /-- Internal implementation detail -/
-def decidable_equiv [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)]
+def decidableEquiv [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)]
     (m₁ m₂ : Raw₀ α β) (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : Decidable (m₁.1.Equiv m₂.1) := by
-  have decBEq : Decidable (Raw₀.beq m₁ m₂ = true) := inferInstance
   apply decidable_of_iff (Raw₀.beq m₁ m₂ = true)
   constructor
   · apply Raw₀.equiv_of_beq h₁ h₂

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -19,6 +19,6 @@ open Std.DHashMap.Internal
 namespace Std.DHashMap.Raw
 
 instance {α : Type u} {β : α → Type v} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁.Equiv m₂) :=
-  Raw₀.decidable_equiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
+  Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
 
 end Std.DHashMap.Raw