[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod

src/algebra/order/to_interval_mod.lean

@@ -27,7 +27,12 @@ interval.
 * `to_Ioc_div hp a b` (where `hp : 0 < p`): The unique integer such that this multiple of `p`,
   subtracted from `b`, is in `Ioc a (a + p)`.
 * `to_Ioc_mod hp a b` (where `hp : 0 < p`): Reduce `b` to the interval `Ioc a (a + p)`.
+* `add_comm_group.modeq p a b`: `a` and `b` are congruent modulo a multiple of `p`. See also
+  `smodeq` which is a more general version in arbitrary submodules.
 
+## TODO
+
+Unify `smodeq` and `add_comm_group.modeq`, which were originally developed independently.
 -/
 
 noncomputable theory
@@ -338,118 +343,118 @@ end
 /-! ### Links between the `Ico` and `Ioc` variants applied to the same element -/
 
 section Ico_Ioc
-variables (a b)
 
+namespace add_comm_group
+variables (a b)
 omit hα
-/-- `mem_Ioo_mod p a b` means that `b` lies in the open interval `(a, a + p)` modulo `p`.
-Equivalently (as shown below), `b` is not congruent to `a` modulo `p`, or `to_Ico_mod hp a` agrees
-with `to_Ioc_mod hp a` at `b`, or `to_Ico_div hp a` agrees with `to_Ioc_div hp a` at `b`. -/
-def mem_Ioo_mod (p a b : α) : Prop := ∃ z : ℤ, b - z • p ∈ set.Ioo a (a + p)
+/-- `add_comm_group.modeq p a b` means that `b` does not lie in the open interval `(a, a + p)`
+modulo `p`.
+
+Equivalently (as shown below), `b` is congruent to `a` modulo `p`, or `to_Ico_mod hp a` disagrees
+with `to_Ioc_mod hp a` at `b`, or `to_Ico_div hp a` disagrees with `to_Ioc_div hp a` at `b`. -/
+def modeq (p a b : α) : Prop := ∀ z : ℤ, b - z • p ∉ set.Ioo a (a + p)
 include hα
 
-lemma tfae_mem_Ioo_mod :
-  tfae [mem_Ioo_mod p a b,
-    to_Ico_mod hp a b = to_Ioc_mod hp a b,
-    to_Ico_mod hp a b + p ≠ to_Ioc_mod hp a b,
-    to_Ico_mod hp a b ≠ a] :=
+lemma tfae_modeq :
+  tfae [modeq p a b,
+    to_Ico_mod hp a b ≠ to_Ioc_mod hp a b,
+    to_Ico_mod hp a b + p = to_Ioc_mod hp a b,
+    to_Ico_mod hp a b = a] :=
 begin
-  tfae_have : 1 → 2,
-  { exact λ ⟨i, hi⟩,
+  rw modeq,
+  tfae_have : 2 → 1,
+  { rw [←not_exists, not_imp_not],
+    exact λ ⟨i, hi⟩,
       ((to_Ico_mod_eq_iff hp).2 ⟨set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
       ((to_Ioc_mod_eq_iff hp).2 ⟨set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm },
-  tfae_have : 2 → 3,
-  { intro h, rw [h, ne, add_right_eq_self], exact hp.ne' },
-  tfae_have : 3 → 4,
-  { refine mt (λ h, _),
+  tfae_have : 3 → 2,
+  { intro h, rw [←h, ne, eq_comm, add_right_eq_self], exact hp.ne' },
+  tfae_have : 4 → 3,
+  { intro h,
     rw [h, eq_comm, to_Ioc_mod_eq_iff, set.right_mem_Ioc],
     refine ⟨lt_add_of_pos_right a hp, to_Ico_div hp a b - 1, _⟩,
     rw [sub_one_zsmul, add_add_add_comm, add_right_neg, add_zero],
     conv_lhs { rw [← to_Ico_mod_add_to_Ico_div_zsmul hp a b, h] } },
-  tfae_have : 4 → 1,
-  { have h' := to_Ico_mod_mem_Ico hp a b, exact λ h, ⟨_, h'.1.lt_of_ne' h, h'.2⟩ },
+  tfae_have : 1 → 4,
+  { rw [←not_exists, not_imp_comm],
+    have h' := to_Ico_mod_mem_Ico hp a b,
+    exact λ h, ⟨_, h'.1.lt_of_ne' h, h'.2⟩ },
   tfae_finish,
 end
 
 variables {a b}
 
-lemma mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod :
-  mem_Ioo_mod p a b ↔ to_Ico_mod hp a b = to_Ioc_mod hp a b := (tfae_mem_Ioo_mod hp a b).out 0 1
-lemma mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod :
-  mem_Ioo_mod p a b ↔ to_Ico_mod hp a b + p ≠ to_Ioc_mod hp a b := (tfae_mem_Ioo_mod hp a b).out 0 2
-lemma mem_Ioo_mod_iff_to_Ico_mod_ne_left :
-  mem_Ioo_mod p a b ↔ to_Ico_mod hp a b ≠ a := (tfae_mem_Ioo_mod hp a b).out 0 3
+lemma modeq_iff_to_Ico_mod_ne_to_Ioc_mod :
+  modeq p a b ↔ to_Ico_mod hp a b ≠ to_Ioc_mod hp a b := (tfae_modeq hp a b).out 0 1
+lemma modeq_iff_to_Ico_mod_add_period_eq_to_Ioc_mod :
+  modeq p a b ↔ to_Ico_mod hp a b + p = to_Ioc_mod hp a b := (tfae_modeq hp a b).out 0 2
+lemma modeq_iff_to_Ico_mod_eq_left :
+  modeq p a b ↔ to_Ico_mod hp a b = a := (tfae_modeq hp a b).out 0 3
 
-lemma not_mem_Ioo_mod_iff_to_Ico_mod_add_period_eq_to_Ioc_mod :
-  ¬mem_Ioo_mod p a b ↔ to_Ico_mod hp a b + p = to_Ioc_mod hp a b :=
-(mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod hp).not_left
+lemma not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod :
+  ¬modeq p a b ↔ to_Ico_mod hp a b = to_Ioc_mod hp a b :=
+(modeq_iff_to_Ico_mod_ne_to_Ioc_mod _).not_left
 
-lemma not_mem_Ioo_mod_iff_to_Ico_mod_eq_left : ¬mem_Ioo_mod p a b ↔ to_Ico_mod hp a b = a :=
-(mem_Ioo_mod_iff_to_Ico_mod_ne_left hp).not_left
-
-lemma mem_Ioo_mod_iff_to_Ioc_mod_ne_right : mem_Ioo_mod p a b ↔ to_Ioc_mod hp a b ≠ a + p :=
+lemma modeq_iff_to_Ioc_mod_eq_right : modeq p a b ↔ to_Ioc_mod hp a b = a + p :=
 begin
-  rw [mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod, to_Ico_mod_eq_iff hp],
+  rw [modeq_iff_to_Ico_mod_ne_to_Ioc_mod hp, ne, to_Ico_mod_eq_iff hp, not_iff_comm],
   obtain ⟨h₁, h₂⟩ := to_Ioc_mod_mem_Ioc hp a b,
-  exact ⟨λ h, h.1.2.ne, λ h, ⟨⟨h₁.le, h₂.lt_of_ne h⟩, _,
-    (to_Ioc_mod_add_to_Ioc_div_zsmul _ _ _).symm⟩⟩,
+  exact ⟨λ h, ⟨⟨h₁.le, h₂.lt_of_ne h⟩, _, (to_Ioc_mod_add_to_Ioc_div_zsmul _ _ _).symm⟩,
+    λ h, h.1.2.ne⟩,
 end
 
-lemma not_mem_Ioo_mod_iff_to_Ioc_eq_right : ¬mem_Ioo_mod p a b ↔ to_Ioc_mod hp a b = a + p :=
-(mem_Ioo_mod_iff_to_Ioc_mod_ne_right hp).not_left
-
-lemma mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div :
-  mem_Ioo_mod p a b ↔ to_Ico_div hp a b = to_Ioc_div hp a b :=
-by rw [mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod hp,
+lemma not_modeq_iff_to_Ico_div_eq_to_Ioc_div :
+  ¬modeq p a b ↔ to_Ico_div hp a b = to_Ioc_div hp a b :=
+by rw [not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp,
        to_Ico_mod, to_Ioc_mod, sub_right_inj, (zsmul_strict_mono_left hp).injective.eq_iff]
 
-lemma mem_Ioo_mod_iff_to_Ico_div_ne_to_Ioc_div_add_one :
-  mem_Ioo_mod p a b ↔ to_Ico_div hp a b ≠ to_Ioc_div hp a b + 1 :=
-by rw [mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod hp, ne, ne, to_Ico_mod, to_Ioc_mod,
+lemma modeq_iff_to_Ico_div_eq_to_Ioc_div_add_one :
+  modeq p a b ↔ to_Ico_div hp a b = to_Ioc_div hp a b + 1 :=
+by rw [modeq_iff_to_Ico_mod_add_period_eq_to_Ioc_mod hp, to_Ico_mod, to_Ioc_mod,
        ← eq_sub_iff_add_eq, sub_sub, sub_right_inj, ← add_one_zsmul,
        (zsmul_strict_mono_left hp).injective.eq_iff]
 
-lemma not_mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div_add_one :
-  ¬mem_Ioo_mod p a b ↔ to_Ico_div hp a b = to_Ioc_div hp a b + 1 :=
-(mem_Ioo_mod_iff_to_Ico_div_ne_to_Ioc_div_add_one hp).not_left
-
 include hp
 
-lemma mem_Ioo_mod_iff_ne_add_zsmul : mem_Ioo_mod p a b ↔ ∀ z : ℤ, b ≠ a + z • p :=
+lemma modeq_iff_eq_add_zsmul : modeq p a b ↔ ∃ z : ℤ, b = a + z • p :=
 begin
-  rw [mem_Ioo_mod_iff_to_Ico_mod_ne_left hp, ← not_iff_not],
-  push_neg, split; intro h,
+  rw [modeq_iff_to_Ico_mod_eq_left hp],
+  split; intro h,
   { rw ← h,
     exact ⟨_, (to_Ico_mod_add_to_Ico_div_zsmul _ _ _).symm⟩ },
   { rw [to_Ico_mod_eq_iff, set.left_mem_Ico],
     exact ⟨lt_add_of_pos_right a hp, h⟩, },
 end
 
-lemma not_mem_Ioo_mod_iff_eq_add_zsmul : ¬mem_Ioo_mod p a b ↔ ∃ z : ℤ, b = a + z • p :=
-by simpa only [not_forall, not_ne_iff] using (mem_Ioo_mod_iff_ne_add_zsmul hp).not
+lemma not_modeq_iff_ne_add_zsmul : ¬modeq p a b ↔ ∀ z : ℤ, b ≠ a + z • p :=
+by rw [modeq_iff_eq_add_zsmul hp, not_exists]
 
-lemma not_mem_Ioo_mod_iff_eq_mod_zmultiples :
-  ¬mem_Ioo_mod p a b ↔ (b : α ⧸ add_subgroup.zmultiples p) = a :=
-by simp_rw [not_mem_Ioo_mod_iff_eq_add_zsmul hp, quotient_add_group.eq_iff_sub_mem,
+lemma modeq_iff_eq_mod_zmultiples :
+  modeq p a b ↔ (b : α ⧸ add_subgroup.zmultiples p) = a :=
+by simp_rw [modeq_iff_eq_add_zsmul hp, quotient_add_group.eq_iff_sub_mem,
     add_subgroup.mem_zmultiples_iff, eq_sub_iff_add_eq', eq_comm]
 
-lemma mem_Ioo_mod_iff_ne_mod_zmultiples :
-  mem_Ioo_mod p a b ↔ (b : α ⧸ add_subgroup.zmultiples p) ≠ a :=
-(not_mem_Ioo_mod_iff_eq_mod_zmultiples hp).not_right
+lemma not_modeq_iff_ne_mod_zmultiples :
+  ¬modeq p a b ↔ (b : α ⧸ add_subgroup.zmultiples p) ≠ a :=
+(modeq_iff_eq_mod_zmultiples hp).not
+
+end add_comm_group
 
 lemma Ico_eq_locus_Ioc_eq_Union_Ioo :
   {b | to_Ico_mod hp a b = to_Ioc_mod hp a b} = ⋃ z : ℤ, set.Ioo (a + z • p) (a + p + z • p) :=
 begin
-  ext1, simp_rw [set.mem_set_of, set.mem_Union, ← set.sub_mem_Ioo_iff_left],
-  exact (mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod hp).symm,
+  ext1, simp_rw [set.mem_set_of, set.mem_Union, ← set.sub_mem_Ioo_iff_left,
+    ←add_comm_group.not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod, add_comm_group.modeq, not_forall,
+    not_not],
 end
 
 lemma to_Ioc_div_wcovby_to_Ico_div (a b : α) : to_Ioc_div hp a b ⩿ to_Ico_div hp a b :=
 begin
   suffices : to_Ioc_div hp a b = to_Ico_div hp a b ∨ to_Ioc_div hp a b + 1 = to_Ico_div hp a b,
   { rwa [wcovby_iff_eq_or_covby, ←order.succ_eq_iff_covby] },
-  rw [eq_comm, ←mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div,
-    eq_comm, ←not_mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div_add_one],
-  exact em _,
+  rw [eq_comm, ←add_comm_group.not_modeq_iff_to_Ico_div_eq_to_Ioc_div,
+    eq_comm, ←add_comm_group.modeq_iff_to_Ico_div_eq_to_Ioc_div_add_one],
+  exact em' _,
 end
 
 lemma to_Ico_mod_le_to_Ioc_mod (a b : α) : to_Ico_mod hp a b ≤ to_Ioc_mod hp a b :=

src/topology/instances/add_circle.lean

@@ -89,7 +89,8 @@ variables {x} (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a)
 
 lemma to_Ico_mod_eventually_eq_to_Ioc_mod : to_Ico_mod hp a =ᶠ[𝓝 x] to_Ioc_mod hp a :=
 is_open.mem_nhds (by {rw Ico_eq_locus_Ioc_eq_Union_Ioo, exact is_open_Union (λ i, is_open_Ioo)}) $
-  (mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod hp).1 ((mem_Ioo_mod_iff_ne_mod_zmultiples hp).2 hx)
+  (add_comm_group.not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp).1 $
+    (add_comm_group.not_modeq_iff_ne_mod_zmultiples hp).2 hx
 
 lemma continuous_at_to_Ico_mod : continuous_at (to_Ico_mod hp a) x :=
 let h := to_Ico_mod_eventually_eq_to_Ioc_mod hp a hx in continuous_at_iff_continuous_left_right.2 $
@@ -498,11 +499,11 @@ lemma equiv_Icc_quot_comp_mk_eq_to_Ioc_mod : equiv_Icc_quot p a ∘ quotient.mk'
   λ x, quot.mk _ ⟨to_Ioc_mod hp.out a x, Ioc_subset_Icc_self $ to_Ioc_mod_mem_Ioc _ _ x⟩ :=
 begin
   rw equiv_Icc_quot_comp_mk_eq_to_Ico_mod, funext,
-  by_cases mem_Ioo_mod p a x,
-  { simp_rw (mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod hp.out).1 h },
-  { simp_rw [not_imp_comm.1 (mem_Ioo_mod_iff_to_Ico_mod_ne_left hp.out).2 h,
-             not_imp_comm.1 (mem_Ioo_mod_iff_to_Ioc_mod_ne_right hp.out).2 h],
+  by_cases add_comm_group.modeq p a x,
+  { simp_rw [(add_comm_group.modeq_iff_to_Ico_mod_eq_left hp.out).1 h,
+             (add_comm_group.modeq_iff_to_Ioc_mod_eq_right hp.out).1 h],
     exact quot.sound endpoint_ident.mk },
+  { simp_rw (add_comm_group.not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp.out).1 h },
 end
 
 /-- The natural map from `[a, a + p] ⊂ 𝕜` with endpoints identified to `𝕜 / ℤ • p`, as a