chore: fix premises of size_union_of_not_mem

Author: wkrozowski

src/Std/Data/DHashMap/Lemmas.lean

@@ -1965,9 +1965,10 @@ theorem getKey!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] :
-    (∀ (a : α), m₁.contains a → m₂.contains a = false) →
-    (m₁ ∪ m₂).size = m₁.size + m₂.size :=
-  @Raw₀.size_union_of_not_mem _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2
+    (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
+    (m₁ ∪ m₂).size = m₁.size + m₂.size := by
+  simp only [← contains_eq_false_iff_not_mem]
+  exact @Raw₀.size_union_of_not_mem _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2
 
 theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size :=
   @Raw₀.size_left_le_size_union α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2

src/Std/Data/DHashMap/RawLemmas.lean

@@ -2149,8 +2149,15 @@ theorem getKey!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF)
-    (h₂ : m₂.WF) : (∀ (a : α), m₁.contains a → m₂.contains a = false) →
+    (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
     (m₁ ∪ m₂).size = m₁.size + m₂.size := by
+  intro hyp
+  conv at hyp =>
+    ext
+    lhs
+    rw [mem_iff_contains]
+  simp only [← contains_eq_false_iff_not_mem] at hyp
+  revert hyp
   simp only [Union.union]
   simp_to_raw using Raw₀.size_union_of_not_mem
 

src/Std/Data/HashMap/Lemmas.lean

@@ -1482,7 +1482,7 @@ theorem getKey!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] :
-    (∀ (a : α), m₁.contains a → m₂.contains a = false) →
+   (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
     (m₁ ∪ m₂).size = m₁.size + m₂.size :=
   @DHashMap.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _
 

src/Std/Data/HashMap/RawLemmas.lean

@@ -1460,7 +1460,7 @@ theorem getKey!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF)
-    (h₂ : m₂.WF) : (∀ (a : α), m₁.contains a → m₂.contains a = false) →
+    (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
     (m₁ ∪ m₂).size = m₁.size + m₂.size :=
   @DHashMap.Raw.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out
 

src/Std/Data/HashSet/Lemmas.lean

@@ -858,7 +858,7 @@ theorem get!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] :
-    (∀ (a : α), m₁.contains a → m₂.contains a = false) →
+    (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
     (m₁ ∪ m₂).size = m₁.size + m₂.size :=
   @HashMap.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -894,7 +894,7 @@ theorem get!_union_of_not_mem_right [Inhabited α]
 
 /- size -/
 theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF)
-    (h₂ : m₂.WF) : (∀ (a : α), m₁.contains a → m₂.contains a = false) →
+    (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) →
     (m₁ ∪ m₂).size = m₁.size + m₂.size :=
   @HashMap.Raw.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out