Weaken the instances for the Const variant

Author: wkrozowski

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

@@ -2610,7 +2610,7 @@ theorem Const.Equiv.beq [LawfulHashable α] [EquivBEq α] [BEq β] [ReflBEq β]
 theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : beq m₁ m₂ = true → m₁.1.Equiv m₂.1 := by
   simp_to_model using List.Const.perm_of_beqModel
 
-theorem Const.Equiv.beq_congr [LawfulBEq α] {m₃ m₄ : Raw₀ α (fun _ => β)} [BEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) :
+theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw₀ α (fun _ => β)} [BEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) :
     m₁.1.Equiv m₃.1 → m₂.1.Equiv m₄.1 → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by
   simp_to_model using List.Const.beqModel_congr
 end

src/Std/Data/DHashMap/Lemmas.lean

@@ -1868,9 +1868,9 @@ theorem Const.equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : Const.beq m₁ m
   simp only at this
   exact this
 
-theorem Const.Equiv.beq_congr [LawfulBEq α] {m₃ m₄ : DHashMap α (fun _ => β)} : m₁ ~m m₃ → m₂ ~m m₄ → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by
+theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : DHashMap α (fun _ => β)} : m₁ ~m m₃ → m₂ ~m m₄ → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by
   intro h1 h2
-  exact @Raw₀.Const.Equiv.beq_congr α _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ ⟨m₃.1, m₃.2.size_buckets_pos⟩ ⟨m₄.1, m₄.2.size_buckets_pos⟩ _ m₁.2 m₂.2 m₃.2 m₄.2 h1.1 h2.1
+  exact @Raw₀.Const.Equiv.beq_congr α _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ ⟨m₃.1, m₃.2.size_buckets_pos⟩ ⟨m₄.1, m₄.2.size_buckets_pos⟩ _ m₁.2 m₂.2 m₃.2 m₄.2 h1.1 h2.1
 end
 
 section Union

src/Std/Data/DHashMap/RawLemmas.lean

@@ -3790,7 +3790,7 @@ theorem Const.Equiv.beq [LawfulHashable α] [EquivBEq α] [BEq β] [ReflBEq β]
 theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := by
   simp_to_raw using Raw₀.Const.equiv_of_beq
 
-theorem Const.Equiv.beq_congr [LawfulBEq α] [BEq β] {m₃ m₄ : Raw  α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
+theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw  α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
     m₁ ~m m₃ → m₂ ~m m₄ → Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ := by
   simp_to_raw
   intro w1 w2

src/Std/Data/ExtDHashMap/Basic.lean

@@ -387,7 +387,7 @@ namespace Const
 
 variable {β : Type v}
 @[inline, inherit_doc DHashMap.beq]
-def beq [LawfulBEq α] [BEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) : Bool := lift₂ (fun x y : DHashMap α fun _ => β => DHashMap.Const.beq x y)
+def beq [EquivBEq α] [LawfulHashable α] [BEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) : Bool := lift₂ (fun x y : DHashMap α fun _ => β => DHashMap.Const.beq x y)
   (fun _ _ _ _ => DHashMap.Const.Equiv.beq_congr) m₁ m₂
 
 theorem beq_of_eq [LawfulBEq α] [BEq β] [ReflBEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) (h : m₁ = m₂) : Const.beq m₁ m₂ := by

src/Std/Data/ExtHashMap/Basic.lean

@@ -250,7 +250,7 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : Ext
 instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashMap α β) := ⟨union⟩
 
 @[inline, inherit_doc ExtDHashMap.beq]
-def beq [LawfulBEq α] [BEq β] (m₁ m₂ : ExtHashMap α β) : Bool := ExtDHashMap.Const.beq m₁.inner m₂.inner
+def beq [EquivBEq α] [LawfulHashable α] [BEq β] (m₁ m₂ : ExtHashMap α β) : Bool := ExtDHashMap.Const.beq m₁.inner m₂.inner
 
 instance [LawfulBEq α] [BEq β] : BEq (ExtHashMap α β) := ⟨beq⟩
 

src/Std/Data/ExtHashSet/Basic.lean

@@ -205,7 +205,7 @@ 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.beq m₁.inner.inner m₂.inner.inner
+def beq [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : Bool := ExtDHashMap.Const.beq m₁.inner.inner m₂.inner.inner
 
 instance [LawfulBEq α] : BEq (ExtHashSet α) := ⟨beq⟩
 

src/Std/Data/HashMap/Lemmas.lean

@@ -1349,13 +1349,13 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α]
 section
 variable {β : Type v} {m₁ m₂ : HashMap α β} [BEq β]
 
-theorem Equiv.beq [LawfulHashable α] [EquivBEq α] [ReflBEq β] (h : m₁ ~m m₂) : m₁ == m₂ :=
+theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [ReflBEq β] (h : m₁ ~m m₂) : m₁ == m₂ :=
   DHashMap.Const.Equiv.beq h.1
 
 theorem equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : m₁ == m₂) : m₁ ~m m₂ :=
   ⟨DHashMap.Const.equiv_of_beq h⟩
 
-theorem Equiv.beq_congr [LawfulBEq α] {m₃ m₄ : HashMap α β} : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) := fun h1 h2 =>
+theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashMap α β} : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) := fun h1 h2 =>
   DHashMap.Const.Equiv.beq_congr h1.1 h2.1
 
 end

src/Std/Data/HashMap/RawLemmas.lean

@@ -1317,9 +1317,9 @@ theorem Equiv.beq [LawfulHashable α] [EquivBEq α] [BEq β] [ReflBEq β] (h₁
 theorem equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ == m₂ → m₁ ~m m₂ := fun hyp =>
   ⟨@DHashMap.Raw.Const.equiv_of_beq _ _ _ _ m₁.1 m₂.1 _ _ _ h₁.1 h₂.1 hyp⟩
 
-theorem Equiv.beq_congr [LawfulBEq α] [BEq β] {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
+theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
     m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) := fun hyp1 hyp2 =>
-  @DHashMap.Raw.Const.Equiv.beq_congr _ _ _ _ m₁.1 m₂.1 _ _ m₃.1 m₄.1 h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
+  @DHashMap.Raw.Const.Equiv.beq_congr _ _ _ _ m₁.1 m₂.1 _ _ _ m₃.1 m₄.1 h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
 
 end
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -823,9 +823,9 @@ theorem Equiv.beq [LawfulHashable α] [EquivBEq α] (h₁ : m₁.WF) (h₂ : m
 theorem equiv_of_beq [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ == m₂ → m₁ ~m m₂ := fun hyp =>
   ⟨@HashMap.Raw.equiv_of_beq _ _ _ _ m₁.1 m₂.1 _ _ _ h₁.1 h₂.1 hyp⟩
 
-theorem Equiv.beq_congr [LawfulBEq α] {m₃ m₄ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
+theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)  :
     m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) := fun hyp1 hyp2 =>
-  @HashMap.Raw.Equiv.beq_congr _ _ _ _ m₁.1 m₂.1 _ _ m₃.1 m₄.1 h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
+  @HashMap.Raw.Equiv.beq_congr _ _ _ _ m₁.1 m₂.1 _ _ _ m₃.1 m₄.1 h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
 
 end
 

src/Std/Data/Internal/List/Associative.lean

@@ -7725,7 +7725,7 @@ theorem beqModel_congr [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] {l₁ l₂ l
     rw [this]
     apply List.Perm.all_eq p₁
 
-theorem Const.beqModel_congr {β : Type v} [BEq α] [LawfulBEq α] [BEq β] {l₁ l₂ l₃ l₄ : List ((_ : α) × β)}
+theorem Const.beqModel_congr {β : Type v} [BEq α] [EquivBEq α] [BEq β] {l₁ l₂ l₃ l₄ : List ((_ : α) × β)}
     (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by
   rw [beqModel]
   split