refactor: rename congruence lemmas for union on DHashMap/HashMap/HashSet/DTreeMap/TreeMap/TreeSet (#11267)

This PR renames congruence lemmas for union on
`DHashMap`/`HashMap`/`HashSet`/`DTreeMap`/`TreeMap`/`TreeSet` to fit the
convention of being in the `Equiv` namespace.

Author: wkrozowski

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

@@ -2628,7 +2628,7 @@ theorem contains_of_contains_union_of_contains_eq_false_left [EquivBEq α]
   simp_to_model [union, contains] using List.contains_of_contains_insertList_of_contains_eq_false_left
 
 /- Equiv -/
-theorem union_equiv_congr_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α]
     (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₁.1.Equiv m₂.1) :
     (m₁.union m₃).1.Equiv (m₂.union m₃).1 := by
   revert equiv
@@ -2637,7 +2637,7 @@ theorem union_equiv_congr_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashab
   apply List.insertList_perm_of_perm_first equiv
   wf_trivial
 
-theorem union_equiv_congr_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α]
     (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₂.1.Equiv m₃.1) :
     (m₁.union m₂).1.Equiv (m₁.union m₃).1 := by
   revert equiv
@@ -2646,6 +2646,15 @@ theorem union_equiv_congr_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHasha
   apply @List.insertList_perm_of_perm_second _ _ _ _ (toListModel m₂.val.buckets) (toListModel m₃.val.buckets) (toListModel m₁.val.buckets) equiv
   all_goals wf_trivial
 
+theorem Equiv.union_congr {m₃ m₄ : Raw₀ α β} [EquivBEq α] [LawfulHashable α]
+    (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) (equiv₁ : m₁.1.Equiv m₃.1)  (equiv₂ : m₂.1.Equiv m₄.1) :
+    (m₁.union m₂).1.Equiv (m₃.union m₄).1 := by
+  revert equiv₁ equiv₂
+  simp_to_model [Equiv, union]
+  intro he₁ he₂
+  apply insertList_congr he₁ he₂
+  all_goals wf_trivial
+
 theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a}
     (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) :
     (m₁.union (m₂.insert p.fst p.snd)).1.Equiv ((m₁.union m₂).insert p.fst p.snd).1 := by

src/Std/Data/DHashMap/Lemmas.lean

@@ -1884,20 +1884,25 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α]
   exact @Raw₀.contains_of_contains_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k h₁ h₂
 
 /- Equiv -/
-theorem union_equiv_congr_left {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_left {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α]
     (equiv : m₁ ~m m₂) :
     (m₁ ∪ m₃) ~m (m₂ ∪ m₃) :=
-  ⟨@Raw₀.union_equiv_congr_left α β _ _ ⟨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 equiv.1⟩
+  ⟨@Raw₀.Equiv.union_left α β _ _ ⟨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 equiv.1⟩
 
-theorem union_equiv_congr_right {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_right {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α]
     (equiv : m₂ ~m m₃) :
     (m₁ ∪ m₂) ~m (m₁ ∪ m₃) :=
-  ⟨@Raw₀.union_equiv_congr_right α β _ _ ⟨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 equiv.1⟩
+  ⟨@Raw₀.Equiv.union_right α β _ _ ⟨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 equiv.1⟩
 
 theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} :
     (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) :=
   ⟨@Raw₀.union_insert_right_equiv_insert_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ p m₁.2 m₂.2⟩
 
+theorem Equiv.union_congr {m₃ m₄ : DHashMap α β} [EquivBEq α] [LawfulHashable α]
+    (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) :
+    (m₁ ∪ m₂) ~m (m₃ ∪ m₄) :=
+  ⟨@Raw₀.Equiv.union_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 equiv₁.1 equiv₂.1⟩
+
 @[deprecated union_insert_right_equiv_insert_union (since := "2025-11-03")]
 theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} :
     (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) :=

src/Std/Data/DHashMap/RawLemmas.lean

@@ -2041,26 +2041,36 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α]
   simp_to_raw using Raw₀.contains_of_contains_union_of_contains_eq_false_left
 
 /- Equiv -/
-theorem union_equiv_congr_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
+theorem Equiv.union_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
     (equiv : m₁ ~m m₂) :
     (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := by
   revert equiv
   simp only [Union.union]
   simp_to_raw
   intro hyp
-  apply Raw₀.union_equiv_congr_left
+  apply Raw₀.Equiv.union_left
   all_goals wf_trivial
 
-theorem union_equiv_congr_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
+theorem Equiv.union_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
     (equiv : m₂ ~m m₃) :
     (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := by
   revert equiv
   simp only [Union.union]
   simp_to_raw
   intro hyp
-  apply Raw₀.union_equiv_congr_right
+  apply Raw₀.Equiv.union_right
   all_goals wf_trivial
 
+theorem Equiv.union_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)
+    (equiv₁ : m₁ ~m m₃)
+    (equiv₂ : m₂ ~m m₄) :
+    (m₁ ∪ m₂) ~m (m₃ ∪ m₄) := by
+  simp only [Union.union]
+  revert equiv₁ equiv₂
+  simp_to_raw
+  intro equiv₁ equiv₂
+  apply Raw₀.Equiv.union_congr h₁ h₂ h₃ h₄ equiv₁ equiv₂
+
 theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a}
     (h₁ : m₁.WF) (h₂ : m₂.WF) :
     (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) := by

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -3389,7 +3389,7 @@ theorem union!_insert_right_equiv_insert_union! [TransOrd α] {p : (a : α) × 
   . wf_trivial
   . exact h₂.balanced
 
-theorem union_equiv_congr_left {m₃ : Impl α β} [TransOrd α]
+theorem Equiv.union_left {m₃ : Impl α β} [TransOrd α]
     (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) :
     (m₁.union m₃ h₁.balanced h₃.balanced).Equiv (m₂.union m₃ h₂.balanced h₃.balanced) := by
   revert equiv
@@ -3402,10 +3402,10 @@ theorem union!_equiv_congr_left {m₃ : Impl α β} [TransOrd α]
     (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) :
     (m₁.union! m₃).Equiv (m₂.union! m₃) := by
   rw [← union_eq_union!, ← union_eq_union!]
-  apply union_equiv_congr_left
+  apply Equiv.union_left
   all_goals wf_trivial
 
-theorem union_equiv_congr_right {m₃ : Impl α β} [TransOrd α]
+theorem Equiv.union_right {m₃ : Impl α β} [TransOrd α]
     (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) :
     (m₁.union m₂ h₁.balanced h₂.balanced).Equiv (m₁.union m₃ h₁.balanced h₃.balanced) := by
   revert equiv
@@ -3418,7 +3418,23 @@ theorem union!_equiv_congr_right {m₃ : Impl α β} [TransOrd α]
     (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) :
     (m₁.union! m₂).Equiv (m₁.union! m₃) := by
   rw [← union_eq_union!, ← union_eq_union!]
-  apply union_equiv_congr_right
+  apply Equiv.union_right
+  all_goals wf_trivial
+
+theorem Equiv.union_congr {m₃ m₄: Impl α β} [TransOrd α]
+    (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (equiv₁ : m₁.Equiv m₃)(equiv₂ : m₂.Equiv m₄) :
+    (m₁.union m₂ h₁.balanced h₂.balanced).Equiv (m₃.union m₄ h₃.balanced h₄.balanced) := by
+  revert equiv₁ equiv₂
+  simp_to_model [Equiv, union]
+  intro equiv₁ equiv₂
+  apply List.insertList_congr equiv₁ equiv₂
+  all_goals wf_trivial
+
+theorem union!_equiv_congr {m₃ m₄: Impl α β} [TransOrd α]
+    (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) :
+    (m₁.union! m₂).Equiv (m₃.union! m₄) := by
+  rw [← union_eq_union!, ← union_eq_union!]
+  apply Equiv.union_congr
   all_goals wf_trivial
 
 /- get? -/

src/Std/Data/DTreeMap/Lemmas.lean

@@ -2260,21 +2260,28 @@ theorem mem_of_mem_union_of_not_mem_left [TransCmp cmp]
 
 
 /- Equiv -/
-theorem union_equiv_congr_left {t₃ : DTreeMap α β cmp} [TransCmp cmp]
+theorem Equiv.union_left {t₃ : DTreeMap α β cmp} [TransCmp cmp]
     (equiv : t₁.Equiv t₂) :
     (t₁ ∪ t₃).Equiv (t₂ ∪ t₃) := by
   simp only [Union.union]
   constructor
   have ⟨equiv⟩ := equiv
-  apply Impl.union_equiv_congr_left t₁.wf t₂.wf t₃.wf equiv
+  apply Impl.Equiv.union_left t₁.wf t₂.wf t₃.wf equiv
 
-theorem union_equiv_congr_right {t₃ : DTreeMap α β cmp} [TransCmp cmp]
+theorem Equiv.union_right {t₃ : DTreeMap α β cmp} [TransCmp cmp]
     (equiv : t₂.Equiv t₃) :
     (t₁ ∪ t₂).Equiv (t₁ ∪ t₃) := by
   simp only [Union.union]
   constructor
   have ⟨equiv⟩ := equiv
-  apply Impl.union_equiv_congr_right t₁.wf t₂.wf t₃.wf equiv
+  apply Impl.Equiv.union_right t₁.wf t₂.wf t₃.wf equiv
+
+theorem Equiv.union_congr {t₃ t₄ : DTreeMap α β cmp} [TransCmp cmp]
+    (equiv₁ : t₁.Equiv t₃) (equiv₂ : t₂.Equiv t₄) :
+    (t₁ ∪ t₂).Equiv (t₃ ∪ t₄) := by
+  simp only [Union.union]
+  constructor
+  apply Impl.Equiv.union_congr t₁.wf t₂.wf t₃.wf t₄.wf equiv₁.1 equiv₂.1
 
 theorem union_insert_right_equiv_insert_union [TransCmp cmp] {p : (a : α) × β a} :
     (t₁ ∪ (t₂.insert p.fst p.snd)).Equiv ((t₁ ∪ t₂).insert p.fst p.snd) :=

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -2317,22 +2317,30 @@ theorem mem_of_mem_union_of_not_mem_left [TransCmp cmp]
   exact Impl.contains_of_contains_union!_of_contains_eq_false_left h₁ h₂
 
 /- Equiv -/
-theorem union_equiv_congr_left {t₃ : Raw α β cmp} [TransCmp cmp]
+theorem Equiv.union_left {t₃ : Raw α β cmp} [TransCmp cmp]
     (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁.Equiv t₂) :
     (t₁ ∪ t₃).Equiv (t₂ ∪ t₃) := by
   simp only [Union.union]
   constructor
   have ⟨equiv⟩ := equiv
   apply Impl.union!_equiv_congr_left h₁ h₂ h₃ equiv
 
-theorem union_equiv_congr_right {t₃ : Raw α β cmp} [TransCmp cmp]
+theorem Equiv.union_right {t₃ : Raw α β cmp} [TransCmp cmp]
     (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂.Equiv t₃) :
     (t₁ ∪ t₂).Equiv (t₁ ∪ t₃) := by
   simp only [Union.union]
   constructor
   have ⟨equiv⟩ := equiv
   apply Impl.union!_equiv_congr_right h₁ h₂ h₃ equiv
 
+theorem Equiv.union_congr {t₃ t₄ : Raw α β cmp} [TransCmp cmp]
+    (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF)
+    (equiv₁ : t₁.Equiv t₃) (equiv₂ : t₂.Equiv t₄) :
+    (t₁ ∪ t₂).Equiv (t₃ ∪ t₄) := by
+  simp only [Union.union]
+  constructor
+  apply Impl.union!_equiv_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1
+
 theorem union_insert_right_equiv_insert_union [TransCmp cmp] {p : (a : α) × β a}
     (h₁ : t₁.WF) (h₂ : t₂.WF) :
     (t₁ ∪ (t₂.insert p.fst p.snd)).Equiv ((t₁ ∪ t₂).insert p.fst p.snd) := by

src/Std/Data/ExtDHashMap/Basic.lean

@@ -351,15 +351,12 @@ def Const.insertManyIfNewUnit [EquivBEq α] [LawfulHashable α] {ρ : Type w}
     m := ⟨m.1.insertIfNew a (), fun _ init step => step (m.2 _ init step)⟩
   return m.1
 
-theorem union_congr [EquivBEq α] [LawfulHashable α] (a b c d : DHashMap α β) (h₁ : a ~m c) (h₂ : b ~m d) : a ∪ b ~m c ∪ d :=
-  DHashMap.Equiv.trans (DHashMap.union_equiv_congr_left h₁) (DHashMap.union_equiv_congr_right h₂)
-
 @[inline, inherit_doc DHashMap.union]
 def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : ExtDHashMap α β := lift₂ (fun x y : DHashMap α β => mk (x.union y))
   (fun a b c d equiv₁ equiv₂ => by
     simp only [DHashMap.union_eq, mk'.injEq]
     apply Quotient.sound
-    apply union_congr
+    apply DHashMap.Equiv.union_congr
     . exact equiv₁
     . exact equiv₂) m₁ m₂
 

src/Std/Data/ExtDTreeMap/Basic.lean

@@ -907,15 +907,12 @@ def insertManyIfNewUnit [TransCmp cmp] {ρ} [ForIn Id ρ α] (t : ExtDTreeMap α
 
 end Const
 
-theorem union_congr [TransCmp cmp] (a b c d : DTreeMap α β cmp) (h₁ : a ~m c) (h₂ : b ~m d) : a ∪ b ~m c ∪ d :=
-  DTreeMap.Equiv.trans (DTreeMap.union_equiv_congr_left h₁) (DTreeMap.union_equiv_congr_right h₂)
-
 @[inline, inherit_doc DTreeMap.union]
 def union [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β cmp := lift₂ (fun x y : DTreeMap α β cmp => mk (x.union y))
   (fun a b c d equiv₁ equiv₂ => by
     simp only [DTreeMap.union_eq, mk'.injEq]
     apply Quotient.sound
-    apply union_congr
+    apply DTreeMap.Equiv.union_congr
     . exact equiv₁
     . exact equiv₂) m₁ m₂
 

src/Std/Data/HashMap/Lemmas.lean

@@ -1389,15 +1389,20 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α]
   @DHashMap.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _  k
 
 /- Equiv -/
-theorem union_equiv_congr_left {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_left {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α]
     (equiv : m₁ ~m m₂) :
     (m₁ ∪ m₃) ~m (m₂ ∪ m₃) :=
-  ⟨DHashMap.union_equiv_congr_left equiv.1⟩
+  ⟨DHashMap.Equiv.union_left equiv.1⟩
 
-theorem union_equiv_congr_right {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α]
+theorem Equiv.union_right {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α]
     (equiv : m₂ ~m m₃) :
     (m₁ ∪ m₂) ~m (m₁ ∪ m₃) :=
-  ⟨DHashMap.union_equiv_congr_right equiv.1⟩
+  ⟨DHashMap.Equiv.union_right equiv.1⟩
+
+theorem Equiv.union_congr {m₃ m₄ : HashMap α β} [EquivBEq α] [LawfulHashable α]
+    (equiv₁ : m₁ ~m m₃)  (equiv₂ : m₂ ~m m₄) :
+    (m₁ ∪ m₂) ~m (m₃ ∪ m₄) :=
+  ⟨DHashMap.Equiv.union_congr equiv₁.1 equiv₂.1⟩
 
 theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : α × β} :
     (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) :=

src/Std/Data/HashMap/RawLemmas.lean

@@ -1353,15 +1353,20 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α]
   @DHashMap.Raw.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
 
 /- Equiv -/
-theorem union_equiv_congr_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
+theorem Equiv.union_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
     (equiv : m₁ ~m m₂) :
     (m₁ ∪ m₃) ~m (m₂ ∪ m₃) :=
-  ⟨@DHashMap.Raw.union_equiv_congr_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩
+  ⟨@DHashMap.Raw.Equiv.union_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩
 
-theorem union_equiv_congr_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
+theorem Equiv.union_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF)
     (equiv : m₂ ~m m₃) :
     (m₁ ∪ m₂) ~m (m₁ ∪ m₃) :=
-  ⟨@DHashMap.Raw.union_equiv_congr_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩
+  ⟨@DHashMap.Raw.Equiv.union_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩
+
+theorem Equiv.union_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)
+    (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) :
+    (m₁ ∪ m₂) ~m (m₃ ∪ m₄) :=
+  ⟨@DHashMap.Raw.Equiv.union_congr _ _ _ _ m₁.inner m₂.inner m₃.inner m₄.inner _ _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩
 
 theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : α × β}
     (h₁ : m₁.WF) (h₂ : m₂.WF) :