diff --git a/SphereEversion.lean b/SphereEversion.lean
index 409e2fc3..6a1d48f0 100644
--- a/SphereEversion.lean
+++ b/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
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/LieGroup.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/LieGroup.lean
deleted file mode 100644
index a29553a5..00000000
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/LieGroup.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-import Mathlib.Geometry.Manifold.Algebra.LieGroup
-
-open scoped Topology Filter Manifold BigOperators
-
-open Set Function Filter
-
-section
-
-variable {ι : Type _} {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type _}
-  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type _} [TopologicalSpace M]
-  [ChartedSpace H M] {s : Set M} {F : Type _} [NormedAddCommGroup F] [NormedSpace ℝ F]
-
-theorem ContMDiffWithinAt.sum {ι : Type _} {f : ι → M → F} {J : Finset ι} {n : ℕ∞} {s : Set M}
-    {x₀ : M} (h : ∀ i ∈ J, ContMDiffWithinAt I 𝓘(ℝ, F) n (f i) s x₀) :
-    ContMDiffWithinAt I 𝓘(ℝ, F) n (fun x => ∑ i in J, f i x) s x₀ := by
-  classical
-  induction' J using Finset.induction_on with i K iK IH
-  · simp [contMDiffWithinAt_const]
-  · simp only [iK, Finset.sum_insert, not_false_iff]
-    exact (h _ (Finset.mem_insert_self i K)).add (IH fun j hj => h _ <| Finset.mem_insert_of_mem hj)
-
-theorem ContMDiffAt.sum {ι : Type _} {f : ι → M → F} {J : Finset ι} {n : ℕ∞} {x₀ : M}
-    (h : ∀ i ∈ J, ContMDiffAt I 𝓘(ℝ, F) n (f i) x₀) :
-    ContMDiffAt I 𝓘(ℝ, F) n (fun x => ∑ i in J, f i x) x₀ := by
-  simp only [← contMDiffWithinAt_univ] at *
-  exact ContMDiffWithinAt.sum h
-
-theorem ContMDiff.sum {ι : Type _} {f : ι → M → F} {J : Finset ι} {n : ℕ∞}
-    (h : ∀ i ∈ J, ContMDiff I 𝓘(ℝ, F) n (f i)) : ContMDiff I 𝓘(ℝ, F) n fun x => ∑ i in J, f i x :=
-  fun x => ContMDiffAt.sum fun j hj => h j hj x
-
-theorem contMDiffWithinAt_finsum {ι : Type _} {f : ι → M → F}
-    (lf : LocallyFinite fun i => support <| f i) {n : ℕ∞} {s : Set M} {x₀ : M}
-    (h : ∀ i, ContMDiffWithinAt I 𝓘(ℝ, F) n (f i) s x₀) :
-    ContMDiffWithinAt I 𝓘(ℝ, F) n (fun x => ∑ᶠ i, f i x) s x₀ :=
-  let ⟨_I, hI⟩ := finsum_eventually_eq_sum lf x₀
-  ContMDiffWithinAt.congr_of_eventuallyEq (ContMDiffWithinAt.sum fun i _hi => h i)
-    (eventually_nhdsWithin_of_eventually_nhds hI) hI.self_of_nhds
-
-theorem contMDiffAt_finsum {ι : Type _} {f : ι → M → F} (lf : LocallyFinite fun i => support <| f i)
-    {n : ℕ∞} {x₀ : M} (h : ∀ i, ContMDiffAt I 𝓘(ℝ, F) n (f i) x₀) :
-    ContMDiffAt I 𝓘(ℝ, F) n (fun x => ∑ᶠ i, f i x) x₀ :=
-  contMDiffWithinAt_finsum lf h
-
-end
-
diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
index 9b992ac5..ee1b7375 100644
--- a/SphereEversion/ToMathlib/Partition.lean
+++ b/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}
diff --git a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean b/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
index 340bb373..79fe409f 100644
--- a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
+++ b/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
diff --git a/SphereEversion/ToMathlib/Topology/Support.lean b/SphereEversion/ToMathlib/Topology/Support.lean
deleted file mode 100644
index 809357d3..00000000
--- a/SphereEversion/ToMathlib/Topology/Support.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import Mathlib.Topology.Support
-
-noncomputable section
-
-open Set Function
-
-section
-
-theorem tsupport_smul_left {α : Type _} [TopologicalSpace α] {M : Type _} {R : Type _} [Semiring R]
-    [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] (f : α → R) (g : α → M) :
-    tsupport (f • g) ⊆ tsupport f := by
-  apply closure_mono
-  erw [support_smul]
-  exact inter_subset_left _ _
-
-theorem tsupport_smul_right {α : Type _} [TopologicalSpace α] {M : Type _} {R : Type _} [Semiring R]
-    [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] (f : α → R) (g : α → M) :
-    tsupport (f • g) ⊆ tsupport g := by
-  apply closure_mono
-  erw [support_smul]
-  exact inter_subset_right _ _
-
-end
diff --git a/lake-manifest.json b/lake-manifest.json
index 11748ecc..07ba04f1 100644
--- a/lake-manifest.json
+++ b/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,