chore(*): bump to lean 3.47.0 (#16252)

A major change is that notations now require names when they are shadowing another identical notation, even if it is a local notation. Also, because localized notations can be imported in a variety of contexts, there are some new best practices for them:

* localized notations should always have a `(name := ...)`. Notation names are unrelated to declaration names, but the declaration name is a reasonable base for the notation name.
* localized notations should never use `_` in the notation, because this gets desugared to a unique metavariable index, meaning that the notation will not be recognized as a duplicate of itself if `open_locale` is used when the notation is already available. Instead, you should use the `hole!` notation, which unfolds to `_`.

Another major change is that projection notation (`x.foo`) now always instantiates implicit arguments with metavariables, which is consistent with Lean 4. To simulate the older behavior, one can use either strict implicit arguments for the structure field (e.g. `∀ {{n}}, p n` instead of `∀ {n}, p n`) or, depending on specifics, writing `λ _, x.foo` to ensure the implicit argument is preserved as an argument.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

archive/imo/imo1998_q2.lean

@@ -190,16 +190,14 @@ end
 
 end
 
-local notation x `/` y := (x : ℚ) / y
-
 lemma clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
-  (b - 1) / (2 * b) ≤ k / a ↔ (b - 1) * a ≤ k * (2 * b) :=
+  (b - 1 : ℚ) / (2 * b) ≤ k / a ↔ (b - 1) * a ≤ k * (2 * b) :=
 by rw div_le_div_iff; norm_cast; simp [ha, hb]
 
 theorem imo1998_q2 [fintype J] [fintype C]
   (a b k : ℕ) (hC : fintype.card C = a) (hJ : fintype.card J = b) (ha : 0 < a) (hb : odd b)
   (hk : ∀ (p : judge_pair J), p.distinct → (agreed_contestants r p).card ≤ k) :
-  (b - 1) / (2 * b) ≤ k / a :=
+  (b - 1 : ℚ) / (2 * b) ≤ k / a :=
 begin
   rw clear_denominators ha hb.pos,
   obtain ⟨z, hz⟩ := hb, rw hz at hJ, rw hz,

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.46.0"
+lean_version = "leanprover-community/lean:3.47.0"
 path = "src"
 
 [dependencies]

src/algebra/algebra/subalgebra/basic.lean

@@ -68,8 +68,8 @@ to_subsemiring_injective.eq_iff
 equalities. -/
 protected def copy (S : subalgebra R A) (s : set A) (hs : s = ↑S) : subalgebra R A :=
 { carrier := s,
-  add_mem' := hs.symm ▸ S.add_mem',
-  mul_mem' := hs.symm ▸ S.mul_mem',
+  add_mem' := λ _ _, hs.symm ▸ S.add_mem',
+  mul_mem' := λ _ _, hs.symm ▸ S.mul_mem',
   algebra_map_mem' := hs.symm ▸ S.algebra_map_mem' }
 
 @[simp] lemma coe_copy (S : subalgebra R A) (s : set A) (hs : s = ↑S) :

src/algebra/big_operators/basic.lean

@@ -82,15 +82,15 @@ In practice, this means that parentheses should be placed as follows:
 -/
 library_note "operator precedence of big operators"
 
-localized "notation `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r"
-  in big_operators
-localized "notation `∏` binders `, ` r:(scoped:67 f, finset.prod finset.univ f) := r"
-  in big_operators
-
-localized "notation `∑` binders ` in ` s `, ` r:(scoped:67 f, finset.sum s f) := r"
-  in big_operators
-localized "notation `∏` binders ` in ` s `, ` r:(scoped:67 f, finset.prod s f) := r"
-  in big_operators
+localized "notation (name := finset.sum_univ)
+  `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r" in big_operators
+localized "notation (name := finset.prod_univ)
+  `∏` binders `, ` r:(scoped:67 f, finset.prod finset.univ f) := r" in big_operators
+
+localized "notation (name := finset.sum)
+  `∑` binders ` in ` s `, ` r:(scoped:67 f, finset.sum s f) := r" in big_operators
+localized "notation (name := finset.prod)
+  `∏` binders ` in ` s `, ` r:(scoped:67 f, finset.prod s f) := r" in big_operators
 
 open_locale big_operators
 

src/algebra/big_operators/finprod.lean

@@ -97,9 +97,11 @@ if h : (mul_support (f ∘ plift.down)).finite then ∏ i in h.to_finset, f i.do
 
 end
 
-localized "notation `∑ᶠ` binders `, ` r:(scoped:67 f, finsum f) := r" in big_operators
+localized "notation (name := finsum)
+  `∑ᶠ` binders `, ` r:(scoped:67 f, finsum f) := r" in big_operators
 
-localized "notation `∏ᶠ` binders `, ` r:(scoped:67 f, finprod f) := r" in big_operators
+localized "notation (name := finprod)
+  `∏ᶠ` binders `, ` r:(scoped:67 f, finprod f) := r" in big_operators
 
 @[to_additive] lemma finprod_eq_prod_plift_of_mul_support_to_finset_subset
   {f : α → M} (hf : (mul_support (f ∘ plift.down)).finite) {s : finset (plift α)}

src/algebra/category/Module/basic.lean

@@ -163,19 +163,19 @@ variables {X₁ X₂ : Type v}
 def Module.as_hom [add_comm_group X₁] [module R X₁] [add_comm_group X₂] [module R X₂] :
   (X₁ →ₗ[R] X₂) → (Module.of R X₁ ⟶ Module.of R X₂) := id
 
-localized "notation `↟` f : 1024 := Module.as_hom f" in Module
+localized "notation (name := Module.as_hom) `↟` f : 1024 := Module.as_hom f" in Module
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
 def Module.as_hom_right [add_comm_group X₁] [module R X₁] {X₂ : Module.{v} R} :
   (X₁ →ₗ[R] X₂) → (Module.of R X₁ ⟶ X₂) := id
 
-localized "notation `↾` f : 1024 := Module.as_hom_right f" in Module
+localized "notation (name := Module.as_hom_right) `↾` f : 1024 := Module.as_hom_right f" in Module
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
 def Module.as_hom_left {X₁ : Module.{v} R} [add_comm_group X₂] [module R X₂] :
   (X₁ →ₗ[R] X₂) → (X₁ ⟶ Module.of R X₂) := id
 
-localized "notation `↿` f : 1024 := Module.as_hom_left f" in Module
+localized "notation (name := Module.as_hom_left) `↿` f : 1024 := Module.as_hom_left f" in Module
 
 /-- Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s. -/
 @[simps]

src/algebra/direct_sum/basic.lean

@@ -36,7 +36,8 @@ def direct_sum [Π i, add_comm_monoid (β i)] : Type* := Π₀ i, β i
 instance [Π i, add_comm_monoid (β i)] : has_coe_to_fun (direct_sum ι β) (λ _, Π i : ι, β i) :=
 dfinsupp.has_coe_to_fun
 
-localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
+localized "notation (name := direct_sum)
+  `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
 
 namespace direct_sum
 

src/algebra/direct_sum/ring.lean

@@ -566,7 +566,7 @@ def lift_ring_hom :
     f (graded_monoid.ghas_one.one) = 1 ∧
     ∀ {i j} (ai : A i) (aj : A j), f (graded_monoid.ghas_mul.mul ai aj) = f ai * f aj} ≃
     ((⨁ i, A i) →+* R) :=
-{ to_fun := λ f, to_semiring f.1 f.2.1 f.2.2,
+{ to_fun := λ f, to_semiring (λ _, f.1) f.2.1 (λ _ _, f.2.2),
   inv_fun := λ F,
     ⟨λ i, (F : (⨁ i, A i) →+ R).comp (of _ i), begin
       simp only [add_monoid_hom.comp_apply, ring_hom.coe_add_monoid_hom],
@@ -578,7 +578,7 @@ def lift_ring_hom :
     end⟩,
   left_inv := λ f, begin
     ext xi xv,
-    exact to_add_monoid_of f.1 xi xv,
+    exact to_add_monoid_of (λ _, f.1) xi xv,
   end,
   right_inv := λ F, begin
     apply ring_hom.coe_add_monoid_hom_injective,

src/algebra/dual_number.lean

@@ -43,8 +43,8 @@ abbreviation dual_number (R : Type*) : Type* := triv_sq_zero_ext R R
 /-- The unit element $ε$ that squares to zero. -/
 def dual_number.eps [has_zero R] [has_one R] : dual_number R := triv_sq_zero_ext.inr 1
 
-localized "notation `ε` := dual_number.eps" in dual_number
-localized "postfix `[ε]`:1025 := dual_number" in dual_number
+localized "notation (name := dual_number.eps) `ε` := dual_number.eps" in dual_number
+localized "postfix (name := dual_number) `[ε]`:1025 := dual_number" in dual_number
 
 open_locale dual_number
 

src/algebra/hom/freiman.lean

@@ -66,8 +66,8 @@ structure freiman_hom (A : set α) (β : Type*) [comm_monoid α] [comm_monoid β
   (hs : s.card = n) (ht : t.card = n) (h : s.prod = t.prod) :
   (s.map to_fun).prod = (t.map to_fun).prod)
 
-notation A ` →+[`:25 n:25 `] `:0 β:0 := add_freiman_hom A β n
-notation A ` →*[`:25 n:25 `] `:0 β:0 := freiman_hom A β n
+notation (name := add_freiman_hom) A ` →+[`:25 n:25 `] `:0 β:0 := add_freiman_hom A β n
+notation (name := freiman_hom) A ` →*[`:25 n:25 `] `:0 β:0 := freiman_hom A β n
 
 /-- `add_freiman_hom_class F s β n` states that `F` is a type of `n`-ary sums-preserving morphisms.
 You should extend this class when you extend `add_freiman_hom`. -/

src/algebra/hom/group_action.lean

@@ -59,7 +59,7 @@ structure mul_action_hom :=
 (to_fun : X → Y)
 (map_smul' : ∀ (m : M') (x : X), to_fun (m • x) = m • to_fun x)
 
-notation X ` →[`:25 M:25 `] `:0 Y:0 := mul_action_hom M X Y
+notation (name := mul_action_hom) X ` →[`:25 M:25 `] `:0 Y:0 := mul_action_hom M X Y
 
 /-- `smul_hom_class F M X Y` states that `F` is a type of morphisms preserving
 scalar multiplication by `M`.

src/algebra/lie/quotient.lean

@@ -64,7 +64,7 @@ lemma is_quotient_mk (m : M) : quotient.mk' m = (mk m : M ⧸ N) := rfl
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural linear map from `L` to the endomorphisms of `M` leaving `N` invariant. -/
 def lie_submodule_invariant : L →ₗ[R] submodule.compatible_maps N.to_submodule N.to_submodule :=
-linear_map.cod_restrict _ (lie_module.to_endomorphism R L M) N.lie_mem
+linear_map.cod_restrict _ (lie_module.to_endomorphism R L M) $ λ _ _, N.lie_mem
 
 variables (N)
 

src/algebra/lie/subalgebra.lean

@@ -57,7 +57,7 @@ instance : set_like (lie_subalgebra R L) L :=
   coe_injective' := λ L' L'' h, by { rcases L' with ⟨⟨⟩⟩, rcases L'' with ⟨⟨⟩⟩, congr' } }
 
 instance : add_subgroup_class (lie_subalgebra R L) L :=
-{ add_mem := λ L', L'.add_mem',
+{ add_mem := λ L' _ _, L'.add_mem',
   zero_mem := λ L', L'.zero_mem',
   neg_mem := λ L' x hx, show -x ∈ (L' : submodule R L), from neg_mem hx }
 
@@ -258,7 +258,7 @@ lemma submodule.exists_lie_subalgebra_coe_eq_iff (p : submodule R L) :
   (∃ (K : lie_subalgebra R L), ↑K = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p :=
 begin
   split,
-  { rintros ⟨K, rfl⟩, exact K.lie_mem', },
+  { rintros ⟨K, rfl⟩ _ _, exact K.lie_mem', },
   { intros h, use { lie_mem' := h, ..p }, exact lie_subalgebra.coe_to_submodule_mk p _, },
 end
 

src/algebra/lie/submodule.lean

@@ -54,7 +54,7 @@ instance : set_like (lie_submodule R L M) M :=
   coe_injective' := λ N O h, by cases N; cases O; congr' }
 
 instance : add_subgroup_class (lie_submodule R L M) M :=
-{ add_mem := λ N, N.add_mem',
+{ add_mem := λ N _ _, N.add_mem',
   zero_mem := λ N, N.zero_mem',
   neg_mem := λ N x hx, show -x ∈ N.to_submodule, from neg_mem hx }
 
@@ -108,9 +108,9 @@ equalities. -/
 protected def copy (s : set M) (hs : s = ↑N) : lie_submodule R L M :=
 { carrier := s,
   zero_mem' := hs.symm ▸ N.zero_mem',
-  add_mem'  := hs.symm ▸ N.add_mem',
+  add_mem'  := λ _ _, hs.symm ▸ N.add_mem',
   smul_mem' := hs.symm ▸ N.smul_mem',
-  lie_mem   := hs.symm ▸ N.lie_mem, }
+  lie_mem   := λ _ _, hs.symm ▸ N.lie_mem, }
 
 @[simp] lemma coe_copy (S : lie_submodule R L M) (s : set M) (hs : s = ↑S) :
   (S.copy s hs : set M) = s := rfl
@@ -208,7 +208,7 @@ lemma submodule.exists_lie_submodule_coe_eq_iff (p : submodule R M) :
   (∃ (N : lie_submodule R L M), ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p :=
 begin
   split,
-  { rintros ⟨N, rfl⟩, exact N.lie_mem, },
+  { rintros ⟨N, rfl⟩ _ _, exact N.lie_mem, },
   { intros h, use { lie_mem := h, ..p }, exact lie_submodule.coe_to_submodule_mk p _, },
 end
 

src/algebra/module/submodule/basic.lean

@@ -77,7 +77,7 @@ equalities. -/
 protected def copy (p : submodule R M) (s : set M) (hs : s = ↑p) : submodule R M :=
 { carrier := s,
   zero_mem' := hs.symm ▸ p.zero_mem',
-  add_mem' := hs.symm ▸ p.add_mem',
+  add_mem' := λ _ _, hs.symm ▸ p.add_mem',
   smul_mem' := hs.symm ▸ p.smul_mem' }
 
 @[simp] lemma coe_copy (S : submodule R M) (s : set M) (hs : s = ↑S) :

src/algebra/monoid_algebra/basic.lean

@@ -893,13 +893,13 @@ def submodule_of_smul_mem (W : submodule k V) (h : ∀ (g : G) (v : V), v ∈ W
   submodule (monoid_algebra k G) V :=
 { carrier := W,
   zero_mem' := W.zero_mem',
-  add_mem' := W.add_mem',
+  add_mem' := λ _ _, W.add_mem',
   smul_mem' := begin
     intros f v hv,
     rw [←finsupp.sum_single f, finsupp.sum, finset.sum_smul],
     simp_rw [←smul_of, smul_assoc],
     exact submodule.sum_smul_mem W _ (λ g _, h g v hv)
-  end  }
+  end }
 
 end submodule
 

src/algebra/order/hom/ring.lean

@@ -215,15 +215,15 @@ variables [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_l
   [has_add γ] [has_le γ] [has_mul δ] [has_add δ] [has_le δ]
 
 /-- Reinterpret an ordered ring isomorphism as an order isomorphism. -/
-def to_order_iso (f : α ≃+*o β) : α ≃o β := ⟨f.to_ring_equiv.to_equiv, f.map_le_map_iff'⟩
+def to_order_iso (f : α ≃+*o β) : α ≃o β := ⟨f.to_ring_equiv.to_equiv, λ _ _, f.map_le_map_iff'⟩
 
 instance : order_ring_iso_class (α ≃+*o β) α β :=
 { coe := λ f, f.to_fun,
   inv := λ f, f.inv_fun,
   coe_injective' := λ f g h₁ h₂, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
   map_add := λ f, f.map_add',
   map_mul := λ f, f.map_mul',
-  map_le_map_iff := λ f, f.map_le_map_iff',
+  map_le_map_iff := λ f _ _, f.map_le_map_iff',
   left_inv := λ f, f.left_inv,
   right_inv := λ f, f.right_inv }
 

src/algebra/quandle.lean

@@ -110,9 +110,9 @@ class rack (α : Type u) extends shelf α :=
 (left_inv : ∀ x, function.left_inverse (inv_act x) (act x))
 (right_inv : ∀ x, function.right_inverse (inv_act x) (act x))
 
-localized "infixr ` ◃ `:65 := shelf.act" in quandles
-localized "infixr ` ◃⁻¹ `:65 := rack.inv_act" in quandles
-localized "infixr ` →◃ `:25 := shelf_hom" in quandles
+localized "infixr (name := shelf.act) ` ◃ `:65 := shelf.act" in quandles
+localized "infixr (name := rack.inv_act) ` ◃⁻¹ `:65 := rack.inv_act" in quandles
+localized "infixr (name := shelf_hom) ` →◃ `:25 := shelf_hom" in quandles
 
 open_locale quandles
 

src/algebra/quaternion.lean

@@ -52,7 +52,8 @@ Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`. -
 structure quaternion_algebra (R : Type*) (a b : R) :=
 mk {} :: (re : R) (im_i : R) (im_j : R) (im_k : R)
 
-localized "notation `ℍ[` R`,` a`,` b `]` := quaternion_algebra R a b" in quaternion
+localized "notation (name := quaternion_algebra) `ℍ[` R`,` a`,` b `]` :=
+  quaternion_algebra R a b" in quaternion
 
 namespace quaternion_algebra
 
@@ -341,7 +342,7 @@ end quaternion_algebra
 `re`, `im_i`, `im_j`, and `im_k`. -/
 def quaternion (R : Type*) [has_one R] [has_neg R] := quaternion_algebra R (-1) (-1)
 
-localized "notation `ℍ[` R `]` := quaternion R" in quaternion
+localized "notation (name := quaternion) `ℍ[` R `]` := quaternion R" in quaternion
 
 /-- The equivalence between the quaternions over R and R × R × R × R. -/
 def quaternion.equiv_prod (R : Type*) [has_one R] [has_neg R] : ℍ[R] ≃ R × R × R × R :=

src/algebra/star/basic.lean

@@ -284,7 +284,7 @@ case for `(↑star_ring_aut : R →* R)`. -/
 def star_ring_end [comm_semiring R] [star_ring R] : R →+* R := @star_ring_aut R _ _
 variables {R}
 
-localized "notation `conj` := star_ring_end _" in complex_conjugate
+localized "notation (name := star_ring_end) `conj` := star_ring_end hole!" in complex_conjugate
 
 /-- This is not a simp lemma, since we usually want simp to keep `star_ring_end` bundled.
  For example, for complex conjugation, we don't want simp to turn `conj x`

src/algebraic_topology/dold_kan/notations.lean

@@ -16,5 +16,7 @@ as `N[X]` for the normalized subcomplex in the case `C` is an abelian category.
 
 -/
 
-localized "notation `K[`X`]` := algebraic_topology.alternating_face_map_complex.obj X" in dold_kan
-localized "notation `N[`X`]` := algebraic_topology.normalized_Moore_complex.obj X" in dold_kan
+localized "notation (name := alternating_face_map_complex) `K[`X`]` :=
+  algebraic_topology.alternating_face_map_complex.obj X" in dold_kan
+localized "notation (name := normalized_Moore_complex) `N[`X`]` :=
+  algebraic_topology.normalized_Moore_complex.obj X" in dold_kan

src/algebraic_topology/fundamental_groupoid/basic.lean

@@ -323,12 +323,12 @@ def fundamental_groupoid_functor : Top ⥤ category_theory.Groupoid :=
     refl,
   end }
 
-localized "notation `π` := fundamental_groupoid.fundamental_groupoid_functor"
-  in fundamental_groupoid
-localized "notation `πₓ` := fundamental_groupoid.fundamental_groupoid_functor.obj"
-  in fundamental_groupoid
-localized "notation `πₘ` := fundamental_groupoid.fundamental_groupoid_functor.map"
-  in fundamental_groupoid
+localized "notation (name := fundamental_groupoid_functor)
+  `π` := fundamental_groupoid.fundamental_groupoid_functor" in fundamental_groupoid
+localized "notation (name := fundamental_groupoid_functor.obj)
+  `πₓ` := fundamental_groupoid.fundamental_groupoid_functor.obj" in fundamental_groupoid
+localized "notation (name := fundamental_groupoid_functor.map)
+  `πₘ` := fundamental_groupoid.fundamental_groupoid_functor.map" in fundamental_groupoid
 
 lemma map_eq {X Y : Top} {x₀ x₁ : X} (f : C(X, Y)) (p : path.homotopic.quotient x₀ x₁) :
   (πₘ f).map p = p.map_fn f := rfl

src/algebraic_topology/simplex_category.lean

@@ -51,7 +51,7 @@ local attribute [semireducible] simplex_category
 /-- Interpet a natural number as an object of the simplex category. -/
 def mk (n : ℕ) : simplex_category := n
 
-localized "notation `[`n`]` := simplex_category.mk n" in simplicial
+localized "notation (name := simplex_category.mk) `[`n`]` := simplex_category.mk n" in simplicial
 
 -- TODO: Make `len` irreducible.
 /-- The length of an object of `simplex_category`. -/

src/algebraic_topology/simplicial_object.lean

@@ -36,9 +36,8 @@ def simplicial_object := simplex_categoryᵒᵖ ⥤ C
 
 namespace simplicial_object
 
-localized
-  "notation X `_[`:1000 n `]` :=
-    (X : category_theory.simplicial_object _).obj (opposite.op (simplex_category.mk n))"
+localized "notation (name := simplicial_object.at) X `_[`:1000 n `]` :=
+  (X : category_theory.simplicial_object hole!).obj (opposite.op (simplex_category.mk n))"
   in simplicial
 
 instance {J : Type v} [small_category J] [has_limits_of_shape J C] :
@@ -237,7 +236,7 @@ end augmented
 
 open_locale simplicial
 
-/-- Aaugment a simplicial object with an object. -/
+/-- Augment a simplicial object with an object. -/
 @[simps]
 def augment (X : simplicial_object C) (X₀ : C) (f : X _[0] ⟶ X₀)
   (w : ∀ (i : simplex_category) (g₁ g₂ : [0] ⟶ i),
@@ -266,10 +265,8 @@ def cosimplicial_object := simplex_category ⥤ C
 
 namespace cosimplicial_object
 
-localized
-  "notation X `_[`:1000 n `]` :=
-    (X : category_theory.cosimplicial_object _).obj (simplex_category.mk n)"
-  in simplicial
+localized "notation (name := cosimplicial_object.at) X `_[`:1000 n `]` :=
+  (X : category_theory.cosimplicial_object hole!).obj (simplex_category.mk n)" in simplicial
 
 instance {J : Type v} [small_category J] [has_limits_of_shape J C] :
   has_limits_of_shape J (cosimplicial_object C) := by {dsimp [cosimplicial_object], apply_instance}