chore: bump mathlib to v4.23.0-rc2 (#699)

Author: kbuzzard

FLT.lean

@@ -74,7 +74,6 @@ import FLT.Mathlib.MeasureTheory.Measure.OpenPos
 import FLT.Mathlib.MeasureTheory.Measure.Regular
 import FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite
 import FLT.Mathlib.NumberTheory.NumberField.Completion
-import FLT.Mathlib.NumberTheory.NumberField.Embeddings
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
 import FLT.Mathlib.NumberTheory.RamificationInertia.Basic
 import FLT.Mathlib.RepresentationTheory.Basic

FLT/AutomorphicRepresentation/Example.lean

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

FLT/Mathlib/NumberTheory/NumberField/Embeddings.lean

@@ -337,23 +337,6 @@ theorem of_inverse (f : N →ₗ[R] M) (g : M → N) (hc : Continuous g) (hi : F
   apply of_isQuotientMap N f
   exact Topology.IsQuotientMap.of_inverse hc (continuous_of_linearMap f) hi
 
-omit [ContinuousAdd M] [ContinuousSMul R M] in
-/-- A linear surjection between modules with the module topology is an open quotient map. -/
-theorem isOpenQuotientMap_of_surjective [IsModuleTopology R M] {φ : M →ₗ[R] N}
-    (hφ : Function.Surjective φ) : IsOpenQuotientMap φ :=
-  have := toContinuousAdd R M
-  AddMonoidHom.isOpenQuotientMap_of_isQuotientMap <| isQuotientMap_of_surjective hφ
-
-/-- A linear surjection to a module with the module topology is open. -/
-theorem isOpenMap_of_surjective {φ : M →ₗ[R] N} (hφ : Function.Surjective φ) :
-    IsOpenMap φ := by
-  have hOpenMap :=
-    letI : TopologicalSpace M := moduleTopology R M
-    have : IsModuleTopology R M := isModuleTopology R M
-    isOpenQuotientMap_of_surjective N hφ |>.isOpenMap
-  intro U hU
-  exact hOpenMap U <| moduleTopology_le R M U hU
-
 end quotientMap
 
 /-

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

@@ -6,7 +6,6 @@ Authors: Salvatore Mercuri
 import Mathlib.NumberTheory.NumberField.Completion
 import FLT.NumberField.InfinitePlace.Extension
 import FLT.Mathlib.Analysis.Normed.Ring.WithAbs
-import FLT.Mathlib.NumberTheory.NumberField.Embeddings
 
 /-!
 # Dimensions of completions at infinite places

FLT/NumberField/InfinitePlace/Dimension.lean

@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "rev": "9e0bebc63f8bcc1df0884cafebaab2673c6d57b0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -45,57 +45,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.68",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.23.0-rc2