chore(*): ensure all open_locales work without any open namespaces (#…

…10913)

Inspired by #10905 we clean up the localized notation in all locales by using the full names of declarations, this should mean that `open_locale blah` should almost never error.

The cases I'm aware of where this doesn't hold still are the locales:
- `witt` which hard codes the variable name `p`, if there is no `p` in context this will fail
- `list.func` and `topological_space` opening `list.func` breaks the notation in `topological_space` due to ``notation as `{` m ` ↦ ` a `}` := list.func.set a as m`` in `list.func` and ``localized "notation `𝓝[≠] ` x:100 := nhds_within x {x}ᶜ" in topological_space``
- likewise for `parser` and `kronecker` due to ``localized "infix ` ⊗ₖ `:100 := matrix.kronecker_map (*)" in kronecker``

But we don't fix these in this PR.

There may be others instances like this too as these errors can depend on the ordering chosen and  I didn't check them all.

A very basic script to check this sort of thing is at https://github.com/leanprover-community/mathlib/tree/alexjbest/check_localized

src/category_theory/types.lean

@@ -62,7 +62,8 @@ congr_fun f.inv_hom_id y
 -- Unfortunately without this wrapper we can't use `category_theory` idioms, such as `is_iso f`.
 abbreviation as_hom {α β : Type u} (f : α → β) : α ⟶ β := f
 -- If you don't mind some notation you can use fewer keystrokes:
-localized "notation  `↾` f : 200 := as_hom f" in category_theory.Type -- type as \upr in VScode
+localized "notation  `↾` f : 200 := category_theory.as_hom f"
+  in category_theory.Type -- type as \upr in VScode
 
 section -- We verify the expected type checking behaviour of `as_hom`.
 variables (α β γ : Type u) (f : α → β) (g : β → γ)

src/data/nat/count.lean

@@ -40,7 +40,7 @@ begin
   refl,
 end
 
-localized "attribute [instance] count_set.fintype" in count
+localized "attribute [instance] nat.count_set.fintype" in count
 
 lemma count_eq_card_filter_range (n : ℕ) : count p n = ((range n).filter p).card :=
 by { rw [count, list.countp_eq_length_filter], refl, }

src/data/vector3.lean

@@ -34,7 +34,7 @@ namespace vector3
 /- We do not want to make the following notation global, because then these expressions will be
 overloaded, and only the expected type will be able to disambiguate the meaning. Worse: Lean will
 try to insert a coercion from `vector3 α _` to `list α`, if a list is expected. -/
-localized "notation `[` l:(foldr `, ` (h t, vector3.cons h t) nil `]`) := l" in vector3
+localized "notation `[` l:(foldr `, ` (h t, vector3.cons h t) vector3.nil `]`) := l" in vector3
 notation a :: b := cons a b
 
 @[simp] theorem cons_fz {α} {n} (a : α) (v : vector3 α n) : (a :: v) fz = a := rfl

src/dynamics/omega_limit.lean

@@ -47,8 +47,8 @@ def omega_limit [topological_space β] (f : filter τ) (ϕ : τ → α → β) (
 
 localized "notation `ω` := omega_limit" in omega_limit
 
-localized "notation `ω⁺` := omega_limit at_top" in omega_limit
-localized "notation `ω⁻` := omega_limit at_bot" in omega_limit
+localized "notation `ω⁺` := omega_limit filter.at_top" in omega_limit
+localized "notation `ω⁻` := omega_limit filter.at_bot" in omega_limit
 
 variables [topological_space β]
 variables (f : filter τ) (ϕ : τ → α → β) (s s₁ s₂: set α)

src/linear_algebra/special_linear_group.lean

@@ -62,7 +62,7 @@ def special_linear_group := { A : matrix n n R // A.det = 1 }
 
 end
 
-localized "notation `SL(` n `,` R `)`:= special_linear_group (fin n) R" in matrix_groups
+localized "notation `SL(` n `,` R `)`:= matrix.special_linear_group (fin n) R" in matrix_groups
 
 namespace special_linear_group
 

src/number_theory/arithmetic_function.lean

@@ -299,7 +299,7 @@ section zeta
 def zeta : arithmetic_function ℕ :=
 ⟨λ x, ite (x = 0) 0 1, rfl⟩
 
-localized "notation `ζ` := zeta" in arithmetic_function
+localized "notation `ζ` := nat.arithmetic_function.zeta" in arithmetic_function
 
 @[simp]
 lemma zeta_apply {x : ℕ} : ζ x = if (x = 0) then 0 else 1 := rfl
@@ -581,7 +581,7 @@ end
 def sigma (k : ℕ) : arithmetic_function ℕ :=
 ⟨λ n, ∑ d in divisors n, d ^ k, by simp⟩
 
-localized "notation `σ` := sigma" in arithmetic_function
+localized "notation `σ` := nat.arithmetic_function.sigma" in arithmetic_function
 
 @[simp]
 lemma sigma_apply {k n : ℕ} : σ k n = ∑ d in divisors n, d ^ k := rfl
@@ -633,7 +633,7 @@ end
 def card_factors : arithmetic_function ℕ :=
 ⟨λ n, n.factors.length, by simp⟩
 
-localized "notation `Ω` := card_factors" in arithmetic_function
+localized "notation `Ω` := nat.arithmetic_function.card_factors" in arithmetic_function
 
 lemma card_factors_apply {n : ℕ} :
   Ω n = n.factors.length := rfl
@@ -674,7 +674,7 @@ end
 def card_distinct_factors : arithmetic_function ℕ :=
 ⟨λ n, n.factors.erase_dup.length, by simp⟩
 
-localized "notation `ω` := card_distinct_factors" in arithmetic_function
+localized "notation `ω` := nat.arithmetic_function.card_distinct_factors" in arithmetic_function
 
 lemma card_distinct_factors_zero : ω 0 = 0 := by simp
 
@@ -698,7 +698,7 @@ end
 def moebius : arithmetic_function ℤ :=
 ⟨λ n, if squarefree n then (-1) ^ (card_factors n) else 0, by simp⟩
 
-localized "notation `μ` := moebius" in arithmetic_function
+localized "notation `μ` := nat.arithmetic_function.moebius" in arithmetic_function
 
 @[simp]
 lemma moebius_apply_of_squarefree {n : ℕ} (h : squarefree n): μ n = (-1) ^ (card_factors n) :=

src/number_theory/dioph.lean

@@ -460,7 +460,7 @@ localized "notation x ` D∨ `:35 y := dioph.or_dioph x y" in dioph
 
 localized "notation `D∃`:30 := dioph.vec_ex1_dioph" in dioph
 
-localized "prefix `&`:max := of_nat'" in dioph
+localized "prefix `&`:max := fin2.of_nat'" in dioph
 theorem proj_dioph_of_nat {n : ℕ} (m : ℕ) [is_lt m n] : dioph_fn (λv : vector3 ℕ n, v &m) :=
 proj_dioph &m
 localized "prefix `D&`:100 := dioph.proj_dioph_of_nat" in dioph

src/number_theory/modular.lean

@@ -320,7 +320,7 @@ def S : SL(2,ℤ) := ⟨![![0, -1], ![1, 0]], by norm_num [matrix.det_fin_two]
 def fundamental_domain : set ℍ :=
 {z | 1 ≤ (complex.norm_sq z) ∧ |z.re| ≤ (1 : ℝ) / 2}
 
-localized "notation `𝒟` := fundamental_domain" in modular
+localized "notation `𝒟` := modular_group.fundamental_domain" in modular
 
 /-- If `|z|<1`, then applying `S` strictly decreases `im` -/
 lemma im_lt_im_S_smul {z : ℍ} (h: norm_sq z < 1) : z.im < (S • z).im :=