Bump Mathlib

Most of the changes from the following Mathlib PRs:
leanprover-community/mathlib#15619 chore(*): Rename normed_group to normed_add_comm_group
leanprover-community/mathlib#15625 refactor(*): rename nondiscrete_normed_field
leanprover-community/mathlib#15632 feat(order/filter/*): filter.pi is countably generated
leanprover-community/mathlib#15634 feat(topology/metric_space/lipschitz): add several lemmas
leanprover-community/mathlib#15627 fix(*): fix typos I made yesterday
leanprover-community/mathlib#15523 feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv
leanprover-community/mathlib#15640 chore(topology/locally_finite): move from topology.basic

leanpkg.toml

@@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.45.0"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ab6bcd632cf3abadff895730a9f2f690ef2d333f"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "0bd4faeefa19bd012a18e5fe23bf46d3def25043"}

src/global/immersion.lean

@@ -10,11 +10,11 @@ open_locale manifold
 section general
 
 variables
-{E : Type*} [normed_group E] [normed_space ℝ E]
+{E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
 {H : Type*} [topological_space H] (I : model_with_corners ℝ E H)
 {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
 
-{E' : Type*} [normed_group E'] [normed_space ℝ E']
+{E' : Type*} [normed_add_comm_group E'] [normed_space ℝ E']
 {H' : Type*} [topological_space H'] (I' : model_with_corners ℝ E' H')
 {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
 

src/global/indexing.lean

@@ -1,6 +1,6 @@
 import tactic.linarith
 import algebra.order.with_zero
-import topology.basic
+import topology.locally_finite
 
 import to_mathlib.set_theory.cardinal.basic
 

src/global/localisation_data.lean

@@ -8,12 +8,12 @@ open_locale manifold
 open metric
 
 section
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
   {H : Type*} [topological_space H]
   (I : model_with_corners 𝕜 E H)
   {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
-  {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
   {H' : Type*} [topological_space H']
   (I' : model_with_corners 𝕜 E' H')
   {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
@@ -33,11 +33,11 @@ structure localisation_data (f : continuous_map M M') :=
 end
 
 section
-variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables (𝕜 : Type*) [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
   {M : Type*} [topological_space M] [sigma_compact_space M] [locally_compact_space M] [t2_space M]
   [nonempty M] [charted_space E M] [smooth_manifold_with_corners 𝓘(𝕜, E) M]
-  (E' : Type*) [normed_group E'] [normed_space 𝕜 E']
+  (E' : Type*) [normed_add_comm_group E'] [normed_space 𝕜 E']
   {M' : Type*} [topological_space M'] [sigma_compact_space M'] [locally_compact_space M']
   [t2_space M'] [nonempty M'] [charted_space E' M']
   [smooth_manifold_with_corners 𝓘(𝕜, E') M']

src/global/one_jet_bundle.lean

@@ -10,19 +10,19 @@ noncomputable theory
 open set equiv
 open_locale manifold
 
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
   {H : Type*} [topological_space H]
   (I : model_with_corners 𝕜 E H)
   (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
-  {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
   {H' : Type*} [topological_space H']
   (I' : model_with_corners 𝕜 E' H')
   (M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
-  {F : Type*} [normed_group F] [normed_space 𝕜 F]
+  {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
   {G : Type*} [topological_space G] (J : model_with_corners 𝕜 F G)
   {N : Type*} [topological_space N] [charted_space G N] [smooth_manifold_with_corners J N]
-  {F' : Type*} [normed_group F'] [normed_space 𝕜 F']
+  {F' : Type*} [normed_add_comm_group F'] [normed_space 𝕜 F']
   {G' : Type*} [topological_space G'] (J' : model_with_corners 𝕜 F' G')
   {N' : Type*} [topological_space N'] [charted_space G' N'] [smooth_manifold_with_corners J' N']
 
@@ -73,7 +73,7 @@ section
 
 variables {M} (p : M × M')
 
-instance : normed_group (one_jet_space I I' p) := by delta_instance one_jet_space
+instance : normed_add_comm_group (one_jet_space I I' p) := by delta_instance one_jet_space
 instance : normed_space 𝕜 (one_jet_space I I' p) := by delta_instance one_jet_space
 instance : inhabited (one_jet_space I I' p) := ⟨0⟩
 

src/global/one_jet_sec.lean

@@ -26,13 +26,13 @@ open_locale topological_space manifold
 
 section general
 
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 -- declare a smooth manifold `M` over the pair `(E, H)`.
-{E : Type*} [normed_group E] [normed_space 𝕜 E]
+{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
 {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
 {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
 -- declare a smooth manifold `M'` over the pair `(E', H')`.
-{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+{E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
 {H' : Type*} [topological_space H'] (I' : model_with_corners 𝕜 E' H')
 {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
 
@@ -99,16 +99,16 @@ end general
 
 section real
 variables
-{E : Type*} [normed_group E] [normed_space ℝ E]
+{E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
 {H : Type*} [topological_space H] (I : model_with_corners ℝ E H)
 (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
-{E' : Type*} [normed_group E'] [normed_space ℝ E']
+{E' : Type*} [normed_add_comm_group E'] [normed_space ℝ E']
 {H' : Type*} [topological_space H'] (I' : model_with_corners ℝ E' H')
 (M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
-{F : Type*} [normed_group F] [normed_space ℝ F]
+{F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
 {G : Type*} [topological_space G] (J : model_with_corners ℝ F G)
 (N : Type*) [topological_space N] [charted_space G N] [smooth_manifold_with_corners J N]
-{F' : Type*} [normed_group F'] [normed_space ℝ F']
+{F' : Type*} [normed_add_comm_group F'] [normed_space ℝ F']
 {G' : Type*} [topological_space G'] (J' : model_with_corners ℝ F' G')
 (N' : Type*) [topological_space N'] [charted_space G' N'] [smooth_manifold_with_corners J' N']
 

src/global/relation.lean

@@ -28,16 +28,16 @@ section defs
 /-! ## Fundamental definitions -/
 
 variables
-{E : Type*} [normed_group E] [normed_space ℝ E]
+{E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
 {H : Type*} [topological_space H] (I : model_with_corners ℝ E H)
 (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
-{E' : Type*} [normed_group E'] [normed_space ℝ E']
+{E' : Type*} [normed_add_comm_group E'] [normed_space ℝ E']
 {H' : Type*} [topological_space H'] (I' : model_with_corners ℝ E' H')
 (M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
-{F : Type*} [normed_group F] [normed_space ℝ F]
+{F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
 {G : Type*} [topological_space G] (J : model_with_corners ℝ F G)
 (N : Type*) [topological_space N] [charted_space G N] [smooth_manifold_with_corners J N]
-{F' : Type*} [normed_group F'] [normed_space ℝ F']
+{F' : Type*} [normed_add_comm_group F'] [normed_space ℝ F']
 {G' : Type*} [topological_space G'] (J' : model_with_corners ℝ F' G')
 (N' : Type*) [topological_space N'] [charted_space G' N'] [smooth_manifold_with_corners J' N']
 
@@ -133,19 +133,19 @@ Note: Patrick doesn't know whether we really need to allow different `E`, `H` an
 manifolds `X` and `M` (and for `Y` and `N`). We use maximal generality just in case.
 -/
 variables
-  {EX : Type*} [normed_group EX] [normed_space ℝ EX]
+  {EX : Type*} [normed_add_comm_group EX] [normed_space ℝ EX]
   {HX : Type*} [topological_space HX] {IX : model_with_corners ℝ EX HX}
   {X : Type*} [topological_space X] [charted_space HX X] [smooth_manifold_with_corners IX X]
 
-  {EM : Type*} [normed_group EM] [normed_space ℝ EM]
+  {EM : Type*} [normed_add_comm_group EM] [normed_space ℝ EM]
   {HM : Type*} [topological_space HM] {IM : model_with_corners ℝ EM HM}
   {M : Type*} [topological_space M] [charted_space HM M] [smooth_manifold_with_corners IM M]
 
-  {EY : Type*} [normed_group EY] [normed_space ℝ EY]
+  {EY : Type*} [normed_add_comm_group EY] [normed_space ℝ EY]
   {HY : Type*} [topological_space HY] {IY : model_with_corners ℝ EY HY}
   {Y : Type*} [topological_space Y] [charted_space HY Y] [smooth_manifold_with_corners IY Y]
 
-  {EN : Type*} [normed_group EN] [normed_space ℝ EN]
+  {EN : Type*} [normed_add_comm_group EN] [normed_space ℝ EN]
   {HN : Type*} [topological_space HN] {IN : model_with_corners ℝ EN HN}
   {N : Type*} [topological_space N] [charted_space HN N] [smooth_manifold_with_corners IN N]
 
@@ -284,8 +284,8 @@ section loc
 Now we really bridge the gap all the way to vector spaces.
 -/
 
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-variables {E' : Type*} [normed_group E'] [normed_space ℝ E']
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+variables {E' : Type*} [normed_add_comm_group E'] [normed_space ℝ E']
 
 /-- For maps between vector spaces, `one_jet_ext` is the obvious thing. -/
 @[simp] theorem one_jet_ext_eq_fderiv {f : E → E'} {x : E} :

src/global/smooth_embedding.lean

@@ -9,12 +9,12 @@ open set equiv
 open_locale manifold topological_space
 
 section general
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
   {H : Type*} [topological_space H]
   (I : model_with_corners 𝕜 E H)
   (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
-  {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
   {H' : Type*} [topological_space H']
   (I' : model_with_corners 𝕜 E' H')
   (M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
@@ -93,8 +93,8 @@ open metric (hiding mem_nhds_iff) function
 
 universe u
 
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
   (M : Type u) [topological_space M] [charted_space E M] [smooth_manifold_with_corners 𝓘(𝕜, E) M]
   [t2_space M] [locally_compact_space M] [sigma_compact_space M]
 

src/local/corrugation.lean

@@ -4,7 +4,6 @@ import measure_theory.integral.interval_integral
 import analysis.calculus.parametric_integral
 
 import to_mathlib.topology.periodic
-import to_mathlib.topology.bases
 import to_mathlib.analysis.calculus
 import to_mathlib.measure_theory.parametric_interval_integral
 
@@ -22,11 +21,11 @@ open set function finite_dimensional asymptotics filter topological_space int me
 open_locale topological_space unit_interval
 
 
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-          {F : Type*} [normed_group F] [normed_space ℝ F] [measurable_space F] [borel_space F]
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+          {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [measurable_space F] [borel_space F]
           [finite_dimensional ℝ F]
-          {G : Type*} [normed_group G] [normed_space ℝ G] [finite_dimensional ℝ G]
-          {H : Type*} [normed_group H] [normed_space ℝ H] [finite_dimensional ℝ H]
+          {G : Type*} [normed_add_comm_group G] [normed_space ℝ G] [finite_dimensional ℝ G]
+          {H : Type*} [normed_add_comm_group H] [normed_space ℝ H] [finite_dimensional ℝ H]
           {π : E →L[ℝ] ℝ} (N : ℝ) (γ : E → loop F)
 
 

src/local/dual_pair.lean

@@ -14,7 +14,7 @@ open function
 
 section no_norm
 variables (E : Type*) [add_comm_group E] [module ℝ E] [topological_space E] (F : Type*)
-                        [normed_group F] [normed_space ℝ F]
+                        [normed_add_comm_group F] [normed_space ℝ F]
 
 -- TODO: move mathlib's dual_pair out of the root namespace!
 
@@ -103,14 +103,14 @@ end dual_pair'
 end no_norm
 
 namespace dual_pair'
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-          {F : Type*} [normed_group F] [normed_space ℝ F]
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+          {F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
 
 
 /- In the next two lemmas, finite dimensionality of `E` is clearly uneeded, but allows
 to use `cont_diff_clm_apply` and `continuous_clm_apply`. -/
 
-lemma smooth_update [finite_dimensional ℝ E] (p : dual_pair' E) {G : Type*} [normed_group G] [normed_space ℝ G]
+lemma smooth_update [finite_dimensional ℝ E] (p : dual_pair' E) {G : Type*} [normed_add_comm_group G] [normed_space ℝ G]
   {φ : G → (E →L[ℝ] F)} (hφ : 𝒞 ∞ φ) {w : G → F} (hw : 𝒞 ∞ w) :
   𝒞 ∞ (λ g, p.update (φ g) (w g)) :=
 begin

src/local/h_principle.lean

@@ -19,10 +19,10 @@ noncomputable theory
 open_locale unit_interval classical filter topological_space
 open filter set rel_loc
 
-variables (E : Type*) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
-          {F : Type*} [normed_group F] [normed_space ℝ F] [measurable_space F] [borel_space F]
+variables (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
+          {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [measurable_space F] [borel_space F]
           [finite_dimensional ℝ F]
-          {G : Type*} [normed_group G] [normed_space ℝ G]
+          {G : Type*} [normed_add_comm_group G] [normed_space ℝ G]
 
 open_locale unit_interval
 /--

src/local/relation.lean

@@ -35,8 +35,8 @@ noncomputable theory
 open set function module (dual) real filter
 open_locale unit_interval topological_space
 
-variables (E : Type*) [normed_group E] [normed_space ℝ E] (F : Type*)
-                        [normed_group F] [normed_space ℝ F]
+variables (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] (F : Type*)
+                        [normed_add_comm_group F] [normed_space ℝ F]
 
 
 @[derive metric_space]
@@ -82,7 +82,7 @@ end
 
 variables (E)
 
-@[ext] structure jet_sec (F : Type*) [normed_group F] [normed_space ℝ F] :=
+@[ext] structure jet_sec (F : Type*) [normed_add_comm_group F] [normed_space ℝ F] :=
 (f : E → F)
 (f_diff : 𝒞 ∞ f)
 (φ : E → E →L[ℝ] F)

src/loops/basic.lean

@@ -22,9 +22,9 @@ noncomputable theory
 
 variables {K X X' Y Z : Type*}
 -- variables [topological_space X'] [topological_space Y] [topological_space Z]
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-          {F : Type*} [normed_group F] [normed_space ℝ F]
-          {F' : Type*} [normed_group F'] [normed_space ℝ F']
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+          {F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
+          {F' : Type*} [normed_add_comm_group F'] [normed_space ℝ F']
 
 set_option old_structure_cmd true
 

src/loops/delta_mollifier.lean

@@ -17,7 +17,7 @@ open_locale topological_space big_operators filter convolution
 
 
 
-variables {F : Type*} [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
+variables {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
 variables [measurable_space F] [borel_space F]
 
 section
@@ -100,7 +100,7 @@ begin
   { rwa finsum_of_infinite_support },
 end
 
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
 
 lemma cont_diff.periodize {f : ℝ → E} {n : with_top ℕ} (h : cont_diff ℝ n f)
   (h' : has_compact_support f) : cont_diff ℝ n (periodize f) :=

src/loops/exists.lean

@@ -9,8 +9,8 @@ open set function finite_dimensional prod int topological_space metric filter
 open measure_theory measure_theory.measure real
 open_locale topological_space unit_interval
 
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-          {F : Type*} [normed_group F]
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+          {F : Type*} [normed_add_comm_group F]
           {g b : E → F} {Ω : set (E × F)} {U K C : set E}
 variables [normed_space ℝ F] [measurable_space F] [borel_space F] [finite_dimensional ℝ F]
 

src/loops/reparametrization.lean

@@ -17,8 +17,8 @@ open set function measure_theory interval_integral filter
 open_locale topological_space unit_interval manifold big_operators
 
 variables {E F : Type*}
-variables [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
-variables [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
+variables [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
+variables [normed_add_comm_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
 variables [measurable_space F] [borel_space F]
 
 local notation `ι` := fin (finite_dimensional.finrank ℝ F + 1)
@@ -272,7 +272,7 @@ begin
     have h₁ := smooth_barycentric ι ℝ F (fintype.card_fin _),
     have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := cont_diff_apply _ _ i,
     refine (h₂.comp_cont_diff_on h₁).comp _ _,
-    { have h₃ := (diag_preimage_prod_sellf (γ.local_centering_density_nhd x)).symm.subset,
+    { have h₃ := (diag_preimage_prod_self (γ.local_centering_density_nhd x)).symm.subset,
       refine cont_diff_on.comp _ (cont_diff_id.prod cont_diff_id).cont_diff_on h₃,
       refine (γ.smooth_surrounded).cont_diff_on.prod_map (cont_diff.cont_diff_on _),
       exact γ.approx_surrounding_points_at_smooth x _, },

src/loops/surrounding.lean

@@ -59,8 +59,8 @@ end is_path_connected
 
 noncomputable theory
 
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
-          {F : Type*} [normed_group F] [normed_space ℝ F]
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
+          {F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
 
 local notation `d` := finrank ℝ F
 local notation `smooth_on` := cont_diff_on ℝ ⊤