From 3e0c4d76b6ebe9dfafb67d16f7286d2731ed6064 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 8 Mar 2023 09:51:00 +0000
Subject: [PATCH] chore(topology/algebra/with_zero_topology): move to a new NS,
 used `localized` (#18560)

This way we can naturally use `scoped instance` in Lean 4.
---
 src/topology/algebra/valued_field.lean       | 12 +++----
 src/topology/algebra/with_zero_topology.lean | 34 +++++++++++---------
 2 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/src/topology/algebra/valued_field.lean b/src/topology/algebra/valued_field.lean
index 00eeec0472942..9bf06e431ca65 100644
--- a/src/topology/algebra/valued_field.lean
+++ b/src/topology/algebra/valued_field.lean
@@ -114,8 +114,8 @@ begin
 end
 
 section
-local attribute [instance] linear_ordered_comm_group_with_zero.topological_space
 
+open_locale with_zero_topology
 open valued
 
 lemma valued.continuous_valuation [valued K Γ₀] : continuous (v : K → Γ₀) :=
@@ -123,12 +123,12 @@ begin
   rw continuous_iff_continuous_at,
   intro x,
   rcases eq_or_ne x 0 with rfl|h,
-  { rw [continuous_at, map_zero, linear_ordered_comm_group_with_zero.tendsto_zero],
+  { rw [continuous_at, map_zero, with_zero_topology.tendsto_zero],
     intros γ hγ,
     rw [filter.eventually, valued.mem_nhds_zero],
     use [units.mk0 γ hγ, subset.rfl] },
   { have v_ne : (v x : Γ₀) ≠ 0, from (valuation.ne_zero_iff _).mpr h,
-    rw [continuous_at, linear_ordered_comm_group_with_zero.tendsto_of_ne_zero v_ne],
+    rw [continuous_at, with_zero_topology.tendsto_of_ne_zero v_ne],
     apply valued.loc_const v_ne },
 end
 end
@@ -193,7 +193,7 @@ instance completable : completable_top_field K :=
   end,
   ..valued_ring.separated }
 
-local attribute [instance] linear_ordered_comm_group_with_zero.topological_space
+open_locale with_zero_topology
 
 /-- The extension of the valuation of a valued field to the completion of the field. -/
 noncomputable def extension : hat K → Γ₀ :=
@@ -255,7 +255,7 @@ lemma continuous_extension : continuous (valued.extension : hat K → Γ₀) :=
     rcases this with ⟨z₀, y₀, y₀_in, hz₀, z₀_ne⟩,
     have vz₀_ne: (v z₀ : Γ₀) ≠ 0 := by rwa valuation.ne_zero_iff,
     refine ⟨v z₀, _⟩,
-    rw [linear_ordered_comm_group_with_zero.tendsto_of_ne_zero vz₀_ne, eventually_comap],
+    rw [with_zero_topology.tendsto_of_ne_zero vz₀_ne, eventually_comap],
     filter_upwards [nhds_right] with x x_in a ha,
     rcases x_in with ⟨y, y_in, rfl⟩,
     have : (v (a * z₀⁻¹) : Γ₀) = 1,
@@ -326,7 +326,7 @@ begin
     { exact this h, }, },
   intros h,
   have hγ₀ : extension ⁻¹' {γ₀} ∈ 𝓝 x := continuous_extension.continuous_at.preimage_mem_nhds
-    (linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_ne_zero h),
+    (with_zero_topology.singleton_mem_nhds_of_ne_zero h),
   rw mem_closure_iff_nhds',
   refine ⟨λ hx, _, λ hx s hs, _⟩,
   { obtain ⟨⟨-, y, hy₁ : v y < (γ : Γ₀), rfl⟩, hy₂⟩ := hx _ hγ₀,
diff --git a/src/topology/algebra/with_zero_topology.lean b/src/topology/algebra/with_zero_topology.lean
index a0c786b819171..4332d27a9da56 100644
--- a/src/topology/algebra/with_zero_topology.lean
+++ b/src/topology/algebra/with_zero_topology.lean
@@ -25,17 +25,15 @@ absolute value (resp. `p`-adic absolute value) on `ℚ` is extended to `ℝ` (re
 
 ## Implementation notes
 
-This topology is not defined as an instance since it may not be the desired topology on
-a linearly ordered commutative group with zero. You can locally activate this topology using
-`local attribute [instance] linear_ordered_comm_group_with_zero.topological_space`
-All other instances will (`ordered_topology`, `t3_space`, `has_continuous_mul`) then follow.
-
+This topology is not defined as a global instance since it may not be the desired topology on a
+linearly ordered commutative group with zero. You can locally activate this topology using
+`open_locale with_zero_topology`.
 -/
 
 open_locale topology filter
 open topological_space filter set function
 
-namespace linear_ordered_comm_group_with_zero
+namespace with_zero_topology
 
 variables {α Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] {γ γ₁ γ₂ : Γ₀} {l : filter α}
   {f : α → Γ₀}
@@ -45,7 +43,7 @@ A subset U is open if 0 ∉ U or if there is an invertible element γ₀ such th
 protected def topological_space : topological_space Γ₀ :=
 topological_space.mk_of_nhds $ update pure 0 $ ⨅ γ ≠ 0, 𝓟 (Iio γ)
 
-local attribute [instance] linear_ordered_comm_group_with_zero.topological_space
+localized "attribute [instance] with_zero_topology.topological_space" in with_zero_topology
 
 lemma nhds_eq_update : (𝓝 : Γ₀ → filter Γ₀) = update pure 0 (⨅ γ ≠ 0, 𝓟 (Iio γ)) :=
 funext $ nhds_mk_of_nhds_single $ le_infi₂ $ λ γ h₀, le_principal_iff.2 $ zero_lt_iff.2 h₀
@@ -134,8 +132,7 @@ is_open_iff.mpr $ imp_iff_not_or.mp $ λ ha, ⟨a, ne_of_gt ha, subset.rfl⟩
 
 /-- The topology on a linearly ordered group with zero element adjoined is compatible with the order
 structure: the set `{p : Γ₀ × Γ₀ | p.1 ≤ p.2}` is closed. -/
-@[priority 100]
-instance order_closed_topology : order_closed_topology Γ₀ :=
+protected lemma order_closed_topology : order_closed_topology Γ₀ :=
 { is_closed_le' :=
   begin
     simp only [← is_open_compl_iff, compl_set_of, not_le, is_open_iff_mem_nhds],
@@ -144,9 +141,10 @@ instance order_closed_topology : order_closed_topology Γ₀ :=
     exact Iio_mem_nhds hab
   end }
 
+localized "attribute [instance] with_zero_topology.order_closed_topology" in with_zero_topology
+
 /-- The topology on a linearly ordered group with zero element adjoined is T₃. -/
-@[priority 100]
-instance t3_space : t3_space Γ₀ :=
+lemma t3_space : t3_space Γ₀ :=
 { to_regular_space := regular_space.of_lift'_closure $ λ γ,
     begin
       rcases ne_or_eq γ 0 with h₀|rfl,
@@ -156,10 +154,11 @@ instance t3_space : t3_space Γ₀ :=
         (λ x hx, is_closed_iff.2 $ or.inl $ zero_lt_iff.2 hx) },
     end }
 
+localized "attribute [instance] with_zero_topology.t3_space" in with_zero_topology
+
 /-- The topology on a linearly ordered group with zero element adjoined makes it a topological
 monoid. -/
-@[priority 100]
-instance : has_continuous_mul Γ₀ :=
+protected lemma has_continuous_mul : has_continuous_mul Γ₀ :=
 ⟨begin
   rw continuous_iff_continuous_at,
   rintros ⟨x, y⟩,
@@ -182,8 +181,11 @@ instance : has_continuous_mul Γ₀ :=
     exact pure_le_nhds (x * y) }
 end⟩
 
-@[priority 100]
-instance : has_continuous_inv₀ Γ₀ :=
+localized "attribute [instance] with_zero_topology.has_continuous_mul" in with_zero_topology
+
+protected lemma has_continuous_inv₀ : has_continuous_inv₀ Γ₀ :=
 ⟨λ γ h, by { rw [continuous_at, nhds_of_ne_zero h], exact pure_le_nhds γ⁻¹ }⟩
 
-end linear_ordered_comm_group_with_zero
+localized "attribute [instance] with_zero_topology.has_continuous_inv₀" in with_zero_topology
+
+end with_zero_topology