Merge branch 'wojciech/hashmap_beq2' into wojciech/hashmap_deceq

Author: wkrozowski

src/Init/Data/List/Perm.lean

@@ -601,6 +601,15 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
+theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
+  rw [Bool.eq_iff_iff, Bool.eq_iff_iff, List.all_eq_true, List.all_eq_true]
+  simp only [iff_true]
+  constructor
+  · intro hyp e mem
+    exact hyp e (@Perm.mem_iff _ e l₁ l₂ hp |>.2 mem)
+  · intro hyp e mem
+    exact hyp e (@Perm.mem_iff _ e l₂ l₁ hp.symm |>.2 mem)
+
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 

src/Std/Data/DHashMap/RawLemmas.lean

@@ -9,6 +9,7 @@ prelude
 public import Std.Data.DHashMap.Internal.Raw
 public import Std.Data.DHashMap.Internal.RawLemmas
 import all Std.Data.DHashMap.Raw
+
 public section
 
 /-!

src/Std/Data/ExtDHashMap/Basic.lean

@@ -412,14 +412,14 @@ end Const
 namespace Const
 
 @[inline, inherit_doc DHashMap.beq]
-def beq_unit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) : Bool := lift₂ (fun x y : DHashMap α fun _ => Unit => DHashMap.Const.beq x y)
+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 beq_unit_of_eq [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : m₁ = m₂) : Const.beq_unit m₁ m₂ := by
+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_beq_unit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : Const.beq_unit m₁ m₂) : m₁ = m₂ := by
+theorem eq_of_beqUnit [LawfulBEq α] (m₁ m₂ : ExtDHashMap α fun _ => Unit) (h : Const.beqUnit m₁ m₂) : m₁ = m₂ := by
   apply eq_of_beq
   exact h
 

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_unit m₁.inner.inner m₂.inner.inner
+def beq [LawfulBEq α] (m₁ m₂ : ExtHashSet α) : Bool := ExtDHashMap.Const.beqUnit m₁.inner.inner m₂.inner.inner
 
 instance [LawfulBEq α] : BEq (ExtHashSet α) := ⟨beq⟩
 
@@ -214,15 +214,15 @@ instance [LawfulBEq α] : ReflBEq (ExtHashSet α) where
     intro a
     cases a
     case mk a =>
-      apply ExtDHashMap.Const.beq_unit_of_eq
+      apply ExtDHashMap.Const.beqUnit_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_beq_unit _ _ hyp
+    exact ExtDHashMap.Const.eq_of_beqUnit _ _ hyp
 
 instance {α : Type u} [DecidableEq α] [Hashable α] : DecidableEq (ExtHashSet α) :=
   fun m₁ m₂ => decidable_of_iff (m₁ == m₂) ⟨by simp, by simp⟩

src/Std/Data/HashMap/Raw.lean

@@ -256,7 +256,6 @@ def beq {β : Type v} [BEq α] [Hashable α] [BEq β] (m₁ m₂ : Raw α β) :
 
 instance [BEq α] [Hashable α] [BEq β] : BEq (Raw α β) := ⟨beq⟩
 
-
 section Unverified
 
 @[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ)

src/Std/Data/HashSet/Basic.lean

@@ -266,7 +266,6 @@ def beq [BEq α] (m₁ m₂ : HashSet α) : Bool :=
 
 instance [BEq α] : BEq (HashSet α) := ⟨beq⟩
 
-
 /--
 Computes the difference of the given hash sets.
 

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

@@ -3617,7 +3617,7 @@ theorem length_le_length_of_containsKey [BEq α] [EquivBEq α]
           simp [mem]
       · exact dl₂
 
-theorem containsKey_of_subset_of_length_eq [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) (hl : l₂.length = l₁.length) (hs : ∀ (a : α), containsKey a l₁ → containsKey a l₂)  : ∀ (a : α), containsKey a l₂ → containsKey a l₁ := by
+theorem containsKey_of_length_eq [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) (hl : l₂.length = l₁.length) (hs : ∀ (a : α), containsKey a l₁ → containsKey a l₂)  : ∀ (a : α), containsKey a l₂ → containsKey a l₁ := by
   intro a ha
   apply Classical.byContradiction
   intro hb
@@ -7692,7 +7692,7 @@ theorem perm_of_beqModel [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, Law
       by_cases hc₂ : containsKey a l₂
       case pos =>
         suffices (∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = true) by
-          rw [@containsKey_of_subset_of_length_eq α β _ _ l₁ l₂ hl₁ hl₂ he.symm this a hc₂] at hc₁
+          rw [@containsKey_of_length_eq α β _ _ l₁ l₂ hl₁ hl₂ he.symm this a hc₂] at hc₁
           contradiction
         intro k' mem
         have := eq_of_beq <| hyp2 k' mem
@@ -7703,15 +7703,6 @@ theorem perm_of_beqModel [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, Law
         rw [Bool.not_eq_true] at hc₂
         rw [getValueCast?_eq_none hc₁, getValueCast?_eq_none hc₂]
 
-theorem all_congr [BEq α] {l₁ l₂ : List ((a : α) × β a)} {f : (a : α) × β a → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
-  rw [Bool.eq_iff_iff, Bool.eq_iff_iff, List.all_eq_true, List.all_eq_true]
-  simp only [iff_true]
-  constructor
-  · intro hyp ⟨k,v⟩ mem
-    exact hyp ⟨k,v⟩ (@Perm.mem_iff _ ⟨k,v⟩ l₁ l₂ hp |>.2 mem)
-  · intro hyp ⟨k,v⟩ mem
-    exact hyp ⟨k,v⟩ (@Perm.mem_iff _ ⟨k,v⟩ l₂ l₁ hp.symm |>.2 mem)
-
 theorem beqModel_congr [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] {l₁ l₂ l₃ l₄ : List ((a : α) × β a)}
     (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by
   rw [beqModel]
@@ -7732,7 +7723,7 @@ theorem beqModel_congr [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] {l₁ l₂ l
       ext x
       rw [getValueCast?_of_perm hl p₂]
     rw [this]
-    apply all_congr p₁
+    apply List.Perm.all_eq p₁
 
 theorem Const.beqModel_congr {β : Type v} [BEq α] [LawfulBEq α] [BEq β] {l₁ l₂ l₃ l₄ : List ((_ : α) × β)}
     (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by
@@ -7754,7 +7745,7 @@ theorem Const.beqModel_congr {β : Type v} [BEq α] [LawfulBEq α] [BEq β] {l
       ext x
       rw [getValue?_of_perm hl p₂]
     rw [this]
-    apply all_congr p₁
+    apply List.Perm.all_eq p₁
 
 theorem beqModel_eq_constBeqModel {β : Type v} [BEq α] [LawfulBEq α] [BEq β] {l₁ l₂ : List ((_ : α) × β)} : beqModel l₁ l₂ = Const.beqModel l₁ l₂ := by
   rw [beqModel, Const.beqModel]