Merge branch 'wojciech/hashmap_beq2' into wojciech/hashmap_deceq

Author: wkrozowski

src/Init/Data/List/Perm.lean

@@ -602,13 +602,10 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | 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)
+  rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
+
+theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.any f = l₂.any f := by
+  rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum

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

@@ -498,6 +498,7 @@ def beq [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] (m₁ m₂ : R
 @[inline] def diff [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β :=
   if m₁.1.size ≤ m₂.1.size then m₁.filter (fun k _ => !m₂.contains k) else (eraseManyEntries m₁ m₂.1).1
 
+
 section
 
 variable {β : Type v}

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

@@ -159,9 +159,9 @@ theorem beq_eq [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] {m₁ m
   simp [Raw.beq, h₁.size_buckets_pos, h₂.size_buckets_pos]
 
 theorem Const.beq_eq {β : Type v} [BEq α] [Hashable α] [BEq β] {m₁ m₂ : Raw α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) :
-     Raw.Const.beq m₁ m₂ = Raw₀.Const.beq ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by
+    Raw.Const.beq m₁ m₂ = Raw₀.Const.beq ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by
   simp [Raw.Const.beq, h₁.size_buckets_pos, h₂.size_buckets_pos]
-  
+
 theorem diff_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) :
     m₁.diff m₂ = Raw₀.diff ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by
   simp [Raw.diff, h₁.size_buckets_pos, h₂.size_buckets_pos]

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

@@ -2613,6 +2613,7 @@ theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.v
 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
 
 section Union

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

@@ -7695,29 +7695,16 @@ theorem beqModel_congr [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] {l₁ l₂ l
     (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by
   simp only [beqModel, ne_eq, ite_not, Bool.if_false_right, Perm.length_eq p₁, Perm.length_eq p₂]
   suffices h : (l₁.all fun x => getValueCast? x.fst l₂ == some x.snd) = (l₃.all fun x => getValueCast? x.fst l₄ == some x.snd) by simp [h]
-  conv =>
-    lhs
-    rhs
-    ext x
-    rw [getValueCast?_of_perm hl p₂]
-  apply List.Perm.all_eq p₁
+  simp [getValueCast?_of_perm hl p₂, List.Perm.all_eq p₁]
 
 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
   simp only [beqModel, ne_eq, ite_not, Bool.if_false_right, Perm.length_eq p₁, Perm.length_eq p₂]
   suffices h : (l₁.all fun x => getValue? x.fst l₂ == some x.snd) = (l₃.all fun x => getValue? x.fst l₄ == some x.snd) by simp [h]
-  conv =>
-    lhs
-    rhs
-    ext x
-    rw [getValue?_of_perm hl p₂]
-  apply List.Perm.all_eq p₁
+  simp [getValue?_of_perm hl p₂, 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]
-  congr
-  ext x
-  rw [getValue?_eq_getValueCast?]
+  simp [beqModel, Const.beqModel, getValue?_eq_getValueCast?]
 
 theorem Const.perm_of_beqModel {β : Type v} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {l₁ l₂ : List ((_ : α) × β)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) :
     beqModel l₁ l₂ → l₁.Perm l₂ := by