Bump mathlib again. PRs emptying two files were merged.

SphereEversion.lean

@@ -43,7 +43,6 @@ import SphereEversion.ToMathlib.Data.Set.Lattice
 import SphereEversion.ToMathlib.Data.Set.Prod
 import SphereEversion.ToMathlib.Equivariant
 import SphereEversion.ToMathlib.ExistsOfConvex
-import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.LieGroup
 import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
 import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
 import SphereEversion.ToMathlib.Geometry.Manifold.MiscManifold
@@ -69,4 +68,3 @@ import SphereEversion.ToMathlib.Topology.Paracompact
 import SphereEversion.ToMathlib.Topology.Path
 import SphereEversion.ToMathlib.Topology.Periodic
 import SphereEversion.ToMathlib.Topology.Separation
-import SphereEversion.ToMathlib.Topology.Support

SphereEversion/ToMathlib/Partition.lean

@@ -1,10 +1,10 @@
-import Mathlib.Geometry.Manifold.PartitionOfUnity
-import Mathlib.Geometry.Manifold.ContMDiff.Basic
 import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
-import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.LieGroup
 import SphereEversion.ToMathlib.Analysis.Convex.Basic
-import SphereEversion.ToMathlib.Topology.Support
 import SphereEversion.ToMathlib.Topology.LocallyFinite
+import Mathlib.Geometry.Manifold.PartitionOfUnity
+import Mathlib.Geometry.Manifold.ContMDiff.Basic
+import Mathlib.Geometry.Manifold.Algebra.LieGroup
+import Mathlib.Topology.Support
 
 noncomputable section
 
@@ -26,7 +26,7 @@ theorem SmoothPartitionOfUnity.contMDiffAt_sum (ρ : SmoothPartitionOfUnity ι I
   refine' contMDiffAt_finsum (ρ.locallyFinite.smul_left _) fun i => _
   by_cases hx : x₀ ∈ tsupport (ρ i)
   · exact ContMDiffAt.smul ((ρ i).smooth.of_le le_top).contMDiffAt (hφ i hx)
-  · exact contMDiffAt_of_not_mem (compl_subset_compl.mpr (tsupport_smul_left (ρ i) (φ i)) hx) n
+  · exact contMDiffAt_of_not_mem (compl_subset_compl.mpr (tsupport_smul_subset_left (ρ i) (φ i)) hx) n
 
 theorem SmoothPartitionOfUnity.contDiffAt_sum {s : Set E}
     (ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s) {n : ℕ∞} {x₀ : E} {φ : ι → E → F}

SphereEversion/ToMathlib/Topology/LocallyFinite.lean

@@ -39,7 +39,7 @@ open scoped Topology
 
 open Filter
 
--- submitted as PR #9813
+-- submitted as PR mathlib4#9813
 theorem LocallyFinite.eventually_subset {ι X : Type*} [TopologicalSpace X] {s : ι → Set X}
     (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) :
     ∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i} := by

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
+   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "1c638703ed1c0c42aed2687acbeda67cec801454",
+   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "e3c20cbbbbe7a771a4579587bc2326669e992ae1",
+   "rev": "a686ba8279292ac8c50a644ee7ee3c9ab178a649",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,