bump to nightly-2023-02-22-00

mathlib commit leanprover-community/mathlib@bd9851c

Mathbin/Topology/Algebra/Group/Compact.lean

@@ -36,11 +36,12 @@ section
 
 variable [TopologicalSpace G] [Group G] [TopologicalGroup G]
 
+#print TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_Group /-
 /-- Every separated topological group in which there exists a compact set with nonempty interior
 is locally compact. -/
 @[to_additive
       "Every separated topological group in which there exists a compact set with nonempty\ninterior is locally compact."]
-theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group [T2Space G]
+theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_Group [T2Space G]
     (K : PositiveCompacts G) : LocallyCompactSpace G :=
   by
   refine' locally_compact_of_compact_nhds fun x => _
@@ -54,15 +55,17 @@ theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group [T2Space
   have : F.symm x = y := by simp [F, Homeomorph.mulLeft_symm]
   rw [this]
   exact mem_interior_iff_mem_nhds.1 hy
-#align topological_space.positive_compacts.locally_compact_space_of_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
-#align topological_space.positive_compacts.locally_compact_space_of_add_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_add_group
+#align topological_space.positive_compacts.locally_compact_space_of_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_Group
+#align topological_space.positive_compacts.locally_compact_space_of_add_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_AddGroup
+-/
 
 end
 
 section Quotient
 
 variable [Group G] [TopologicalSpace G] [TopologicalGroup G] {Γ : Subgroup G}
 
+#print QuotientGroup.continuousSMul /-
 @[to_additive]
 instance QuotientGroup.continuousSMul [LocallyCompactSpace G] : ContinuousSMul G (G ⧸ Γ)
     where continuous_smul :=
@@ -75,7 +78,8 @@ instance QuotientGroup.continuousSMul [LocallyCompactSpace G] : ContinuousSMul G
       refine' continuous_coinduced_rng.comp continuous_mul
     exact QuotientMap.continuous_lift_prod_right quotientMap_quotient_mk' H
 #align quotient_group.has_continuous_smul QuotientGroup.continuousSMul
-#align quotient_add_group.has_continuous_vadd quotientAddGroup.has_continuous_vadd
+#align quotient_add_group.has_continuous_vadd QuotientAddGroup.continuousVAdd
+-/
 
 end Quotient
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "95755ad5e0a450a58043e00f4f3573c0c10f487d",
+    "rev": "5188d4951566bd9f46c8c10439ee7bc19bda2736",
     "name": "lean3port",
-    "inputRev?": "95755ad5e0a450a58043e00f4f3573c0c10f487d"}},
+    "inputRev?": "5188d4951566bd9f46c8c10439ee7bc19bda2736"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e7e49c8a41239716cb79fa187a6bf66e7d82d710",
+    "rev": "e94a78db0cbd821cd781781019cbc9c87186d81d",
     "name": "mathlib",
-    "inputRev?": "e7e49c8a41239716cb79fa187a6bf66e7d82d710"}},
+    "inputRev?": "e94a78db0cbd821cd781781019cbc9c87186d81d"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-02-21-22"
+def tag : String := "nightly-2023-02-22-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"95755ad5e0a450a58043e00f4f3573c0c10f487d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5188d4951566bd9f46c8c10439ee7bc19bda2736"
 
 @[default_target]
 lean_lib Mathbin where