chore: bump mathlib

FLT/AutomorphicRepresentation/Example.lean

@@ -546,7 +546,7 @@ instance : Zero 𝓞 := ⟨zero⟩
 @[simp] lemma zero_im_oi : im_oi (0 : 𝓞) = 0 := rfl
 
 lemma toQuaternion_zero : toQuaternion 0 = 0 := by
-  ext <;> simp [toQuaternion]
+  ext <;> (simp [toQuaternion]; aesop)
 
 @[simp]
 lemma toQuaternion_eq_zero_iff {z} : toQuaternion z = 0 ↔ z = 0 :=
@@ -568,7 +568,7 @@ instance : One 𝓞 := ⟨one⟩
 @[simp] lemma one_im_oi : im_oi (1 : 𝓞) = 0 := rfl
 
 lemma toQuaternion_one : toQuaternion 1 = 1 := by
-  ext <;> simp [toQuaternion]
+  ext <;> (simp [toQuaternion]; aesop)
 
 /-! ## Neg (-) -/
 

FLT/DivisionAlgebra/Finiteness.lean

@@ -45,7 +45,7 @@ local instance : IsModuleTopology (FiniteAdeleRing (𝓞 K) K) (D ⊗[K] (Finite
 
 variable [FiniteDimensional K D]
 
-instance : TopologicalRing (D ⊗[K] (FiniteAdeleRing (𝓞 K) K)) :=
+instance : IsTopologicalRing (D ⊗[K] (FiniteAdeleRing (𝓞 K) K)) :=
   IsModuleTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
 
 variable [Algebra.IsCentral K D]

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -91,7 +91,7 @@ lemma FiniteAdeleRing.clear_denominator (a : FiniteAdeleRing R K) :
 instance : TopologicalSpace (FiniteAdeleRing ℤ ℚ) := sorry
 
 
-instance instTopologicalRingFiniteAdeleRing : TopologicalRing (FiniteAdeleRing ℤ ℚ) := sorry
+instance instTopologicalRingFiniteAdeleRing : IsTopologicalRing (FiniteAdeleRing ℤ ℚ) := sorry
 
 end PR13703
 

FLT/HaarMeasure/DistribHaarChar/Basic.lean

@@ -30,7 +30,7 @@ variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
   [MeasurableSMul G A] -- only need `MeasurableConstSMul` but we don't have this class.
 variable {μ ν : Measure A} {g : G}
 
-variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCompactSpace A]
+variable [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A]
   [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
 
 variable (μ A) in

FLT/HaarMeasure/DomMulActMeasure.lean

@@ -26,7 +26,7 @@ lemma integral_domSMul {α} [NormedAddCommGroup α] [NormedSpace ℝ α] (g : G
     ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ :=
   integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f
 
-variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCompactSpace A]
+variable [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A]
   [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
 
 instance : SMulCommClass ℝ≥0 Gᵈᵐᵃ (Measure A) where

FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean

@@ -71,7 +71,7 @@ lemma smul_submodule_finiteRelIndex (hx : x ≠ 0) (s : Submodule ℤ_[p] ℚ_[p
 
 -- Yaël: Do we really want this as a coercion?
 noncomputable instance : Coe ℤ_[p]⁰ ℚ_[p]ˣ where
-  coe x := .mk0 x.1 <| map_ne_zero_of_mem_nonZeroDivisors (M := ℤ_[p]) Coe.ringHom coe_injective x.2
+  coe x := .mk0 x.1 <| map_ne_zero_of_mem_nonZeroDivisors (M₀ := ℤ_[p]) Coe.ringHom coe_injective x.2
 
 /-- Non-zero p-adic integers generate non-zero p-adic numbers as a group. -/
 lemma closure_nonZeroDivisors_padicInt :

FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -12,7 +12,7 @@ def ContinuousAddEquiv.toIntContinuousLinearEquiv {M M₂ : Type*} [AddCommGroup
 
 def ContinuousAddEquiv.quotientPi {ι : Type*} {G : ι → Type*} [(i : ι) → AddCommGroup (G i)]
     [(i : ι) → TopologicalSpace (G i)]
-    [(i : ι) → TopologicalAddGroup (G i)]
+    [(i : ι) → IsTopologicalAddGroup (G i)]
     [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] :
     ((i : ι) → G i) ⧸ AddSubgroup.pi (_root_.Set.univ) p ≃ₜ+ ((i : ι) → G i ⧸ p i) :=
   (Submodule.quotientPiContinuousLinearEquiv

FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean

@@ -49,7 +49,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
   haveI : ContinuousAdd C := toContinuousAdd R C
   exact continuous_finsum (fun i ↦ by fun_prop) (locallyFinite_of_finite _)
 
-theorem Module.continuous_bilinear_of_finite_free [TopologicalSemiring R] [Module.Finite R A]
+theorem Module.continuous_bilinear_of_finite_free [IsTopologicalSemiring R] [Module.Finite R A]
     [Module.Free R A] (bil : A →ₗ[R] B →ₗ[R] C) :
     Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
   let ι := Module.Free.ChooseBasisIndex R A
@@ -72,7 +72,7 @@ end semiring_bilinear
 
 section ring_bilinear
 
-variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [TopologicalRing R]
+variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [IsTopologicalRing R]
 
 variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A]
 variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B]
@@ -107,20 +107,20 @@ section semiring_algebra
 open scoped TensorProduct
 
 -- these shouldn't be rings, they should be semirings
-variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+variable (R) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
 variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D]
 variable [TopologicalSpace D] [IsModuleTopology R D]
 
 open scoped TensorProduct
 
 @[continuity, fun_prop]
 theorem continuous_mul'
-    (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+    (R : Type*) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
     (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D] [TopologicalSpace D]
     [IsModuleTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) :=
   Module.continuous_bilinear_of_finite (LinearMap.mul R D)
 
-def topologicalSemiring : TopologicalSemiring D where
+def topologicalSemiring : IsTopologicalSemiring D where
   continuous_add := (toContinuousAdd R D).1
   continuous_mul := continuous_mul' R D
 
@@ -130,7 +130,7 @@ section ring_algebra
 
 -- confusion about whether these are rings or semirings should ideally be resolved
 -- Is it: for D finite free R can be a semiring but for D finite it has to be a ring?
-variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+variable (R) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
 variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D]
 variable [TopologicalSpace D] [IsModuleTopology R D]
 
@@ -143,7 +143,7 @@ theorem continuous_mul : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := b
   haveI : IsModuleTopology R (D ⊗[R] D) := { eq_moduleTopology' := rfl }
   convert Module.continuous_bilinear_of_finite <| (LinearMap.mul R D : D →ₗ[R] D →ₗ[R] D)
 
-def Module.topologicalRing : TopologicalRing D where
+def Module.topologicalRing : IsTopologicalRing D where
   continuous_add := (toContinuousAdd R D).1
   continuous_mul := continuous_mul R D
   continuous_neg := continuous_neg R D
@@ -155,8 +155,8 @@ end ring_algebra
 section trans
 
 variable (R S M : Type*)
-  [CommRing R] [TopologicalSpace R] [TopologicalRing R]
-  [CommRing S] [TopologicalSpace S] [TopologicalRing S]
+  [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
+  [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
     [Algebra R S] [Module.Finite R S] [IsModuleTopology R S]
   [AddCommGroup M]
     [Module R M]
@@ -193,8 +193,8 @@ end trans
 section opensubring
 
 variable (R S : Type*)
-  [CommRing R] [TopologicalSpace R] [TopologicalRing R]
-  [CommRing S] [TopologicalSpace S] [TopologicalRing S]
+  [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
+  [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
     [Algebra R S]
 
 example (hcont : Continuous (algebraMap R S))

FLT/Mathlib/Topology/Algebra/Module/Quotient.lean

@@ -17,7 +17,7 @@ def Submodule.Quotient.continuousLinearEquiv {R : Type*} [Ring R] (G H : Type*)
 
 def Submodule.quotientPiContinuousLinearEquiv {R ι : Type*} [CommRing R] {G : ι → Type*}
     [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] [(i : ι) → TopologicalSpace (G i)]
-    [(i : ι) → TopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι]
+    [(i : ι) → IsTopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι]
     (p : (i : ι) → Submodule R (G i)) :
     (((i : ι) → G i) ⧸ Submodule.pi Set.univ p) ≃L[R] ((i : ι) → G i ⧸ p i) where
   toLinearEquiv := Submodule.quotientPi p

FLT/Mathlib/Topology/Algebra/UniformRing.lean

@@ -7,8 +7,8 @@ import FLT.Mathlib.Algebra.Algebra.Hom
 
 namespace UniformSpace.Completion
 
-variable {α : Type*} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α]
-  {β : Type*} [UniformSpace β] [Ring β] [UniformAddGroup β] [TopologicalRing β]
+variable {α : Type*} [Ring α] [UniformSpace α] [IsTopologicalRing α] [UniformAddGroup α]
+  {β : Type*} [UniformSpace β] [Ring β] [UniformAddGroup β] [IsTopologicalRing β]
   (f : α →+* β) (hf : Continuous f)
 
 theorem mapRingHom_apply {x : UniformSpace.Completion α} :
@@ -21,8 +21,8 @@ theorem mapRingHom_coe (hf : UniformContinuous f) (a : α) :
   rw [mapRingHom_apply, map_coe hf]
 
 noncomputable def mapSemialgHom {α : Type*} [CommRing α] [UniformSpace α]
-    [TopologicalRing α] [UniformAddGroup α] {β : Type*} [UniformSpace β] [CommRing β]
-    [UniformAddGroup β] [TopologicalRing β] (f : α →+* β) (hf : Continuous f) :
+    [IsTopologicalRing α] [UniformAddGroup α] {β : Type*} [UniformSpace β] [CommRing β]
+    [UniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous f) :
     Completion α →ₛₐ[f] Completion β where
   __ := UniformSpace.Completion.mapRingHom f hf
   map_smul' m x := by

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6b28ba204395930a138b9e9151ba8c473ac7d811",
+   "rev": "2836c275479466837c2593377bb54ae9fafc41d2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b18855cb0f9a19bd4d7e21f3e5525272e377f431",
+   "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",