Update mathlib to version 4.9.0

- a few files moved; one file was split - the entire file Local/AmpleSet has landed in mathlib now! - arguments to Set.inter_subset_right and friends are now implicit. - move ToMathlib/Topology/Periodic to Algebra to reflect an upstream move. - need to specify one argument explicitly
leanprover-community · Jul 7, 2024 · 0092b9e · 0092b9e
1 parent 5c52693
commit 0092b9e
Show file tree

Hide file tree

Showing 23 changed files with 56 additions and 151 deletions.
diff --git a/SphereEversion.lean b/SphereEversion.lean
@@ -12,7 +12,6 @@ import SphereEversion.Global.TwistOneJetSec
 import SphereEversion.Indexing
 import SphereEversion.InductiveConstructions
 import SphereEversion.Local.AmpleRelation
-import SphereEversion.Local.AmpleSet
 import SphereEversion.Local.Corrugation
 import SphereEversion.Local.DualPair
 import SphereEversion.Local.HPrinciple
@@ -27,6 +26,7 @@ import SphereEversion.Loops.Reparametrization
 import SphereEversion.Loops.Surrounding
 import SphereEversion.Main
 import SphereEversion.Notations
+import SphereEversion.ToMathlib.Algebra.Periodic
 import SphereEversion.ToMathlib.Analysis.Calculus
 import SphereEversion.ToMathlib.Analysis.Calculus.AffineMap
 import SphereEversion.ToMathlib.Analysis.ContDiff
@@ -65,5 +65,4 @@ import SphereEversion.ToMathlib.Topology.HausdorffDistance
 import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Topology.Paracompact
 import SphereEversion.ToMathlib.Topology.Path
-import SphereEversion.ToMathlib.Topology.Periodic
 import SphereEversion.ToMathlib.Topology.Separation
diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
@@ -1,8 +1,8 @@
+import Mathlib.Analysis.Convex.AmpleSet
 import Mathlib.Geometry.Manifold.Instances.Sphere
 import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional
 import SphereEversion.ToMathlib.Geometry.Manifold.Immersion
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
-import SphereEversion.Local.AmpleSet
 import SphereEversion.Global.Gromov
 import SphereEversion.Global.TwistOneJetSec
 

diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
@@ -1,6 +1,5 @@
 import SphereEversion.Global.Relation
 import Mathlib.Analysis.Convex.AmpleSet
-import SphereEversion.Local.AmpleSet
 
 noncomputable section
 

diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
@@ -146,7 +146,7 @@ theorem forall_near [T2Space M'] {P : M → Prop} {P' : M' → Prop} {K : Set M}
   rw [show A = A ∩ range f ∪ A ∩ (range f)ᶜ by simp]
   apply Filter.Eventually.union
   · have : ∀ᶠ m' near A ∩ range f, m' ∈ range f :=
-      f.isOpen_range.mem_nhdsSet.mpr (inter_subset_right _ _)
+      f.isOpen_range.mem_nhdsSet.mpr inter_subset_right
     apply (this.and <| f.forall_near' hP).mono
     rintro _ ⟨⟨m, rfl⟩, hm⟩
     exact hPP' _ (hm _ rfl)

diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.Fin.Interval
+import Mathlib.Order.Interval.Finset.Fin
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Nat.SuccPred
 import Mathlib.Data.ZMod.Defs

diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean
@@ -174,29 +174,26 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X
   · exact IsOpen.union U₁_op U_op
   · exact IsOpen.sdiff U₂_op hK
   · refine IsCompact.union K₁_cpct ?_
-    refine K₂_cpct.closure_of_subset ?_
-    exact inter_subset_left K₂ U'
+    exact K₂_cpct.closure_of_subset inter_subset_left
   · exact IsCompact.diff K₂_cpct U'_op
-  · exact subset_union_left K₁ (closure (K₂ ∩ U'))
+  · exact subset_union_left
   · apply union_subset_union
     exact hK₁U₁
     apply subset_trans _ hU'U
     gcongr
-    exact inter_subset_right K₂ U'
+    exact inter_subset_right
   · exact diff_subset_diff hK₂U₂ hKU'
   · rw [union_assoc]
     congr
     apply subset_antisymm
-    · apply union_subset
-      · apply K₂_cpct.isClosed.closure_subset_iff.mpr
-        exact inter_subset_left K₂ U'
-      · exact diff_subset K₂ U'
+    · apply union_subset ?_ diff_subset
+      exact K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left
     · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_diff K₂ U').symm
         _     ⊆ closure (K₂ ∩ U') ∪ K₂ \ U' := union_subset_union_left (K₂ \ U') subset_closure
   · intro x hx hx'
     exact hx'.2 hx
   · rw [union_comm]
-  · exact diff_subset U₂ K
+  · exact diff_subset
 
 /-- We are given a suitably nice extended metric space `X` and three local constraints `P₀`,`P₀'`
 and `P₁` on maps from `X` to some type `Y`. All maps entering the discussion are required to

diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
-import SphereEversion.Local.AmpleSet
+import Mathlib.Analysis.Convex.AmpleSet
 import SphereEversion.Local.DualPair
 import SphereEversion.Local.Relation
 

diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean
diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean
@@ -2,7 +2,7 @@ import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.Analysis.Calculus.ParametricIntegral
-import SphereEversion.ToMathlib.Topology.Periodic
+import SphereEversion.ToMathlib.Algebra.Periodic
 import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
 import SphereEversion.Loops.Basic
 import SphereEversion.Local.DualPair

diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean
@@ -154,7 +154,7 @@ theorem smooth_g (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 ∞ (L.g 𝓕)
 
 theorem Accepts.rel {L : StepLandscape E} {𝓕 : JetSec E F} (h : L.Accepts R 𝓕) :
     ∀ᶠ x : E near L.K, (L.g 𝓕) x = (L.b 𝓕) x := by
-  apply (h.hC.filter_mono <| monotone_nhdsSet (inter_subset_right L.K₁ L.C)).mono
+  apply (h.hC.filter_mono <| monotone_nhdsSet inter_subset_right).mono
   intro x hx
   dsimp [JetSec.IsHolonomicAt] at hx
   dsimp [StepLandscape.g, StepLandscape.b]

diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
@@ -1,7 +1,7 @@
+import Mathlib.Analysis.Convex.AmpleSet
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual
 import SphereEversion.Local.ParametricHPrinciple
-import SphereEversion.Local.AmpleSet
 
 /-!
 This is file proves the existence of a sphere eversion from the local verson of the h-principle.

diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
@@ -3,7 +3,7 @@ import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.Analysis.Convolution
 import Mathlib.MeasureTheory.Measure.Haar.Unique
 import Mathlib.Analysis.Calculus.BumpFunction.Normed
-import SphereEversion.ToMathlib.Topology.Periodic
+import SphereEversion.ToMathlib.Algebra.Periodic
 import SphereEversion.ToMathlib.Analysis.ContDiff
 import SphereEversion.Loops.Basic
 
@@ -189,7 +189,7 @@ theorem intervalIntegral_periodize_smul (f : ℝ → ℝ) (γ : Loop E) {a b c d
   rw [h2]
   have : (support fun t ↦ f t • γ t) ⊆ Ioc a (a + 1) := by
     erw [support_smul]
-    exact ((inter_subset_left _ _).trans hf).trans (Ioc_subset_Ioc_right h)
+    exact (inter_subset_left.trans hf).trans (Ioc_subset_Ioc_right h)
   rw [← intervalIntegral.integral_eq_integral_of_support_subset this]
   simp_rw [periodize_smul_periodic _ γ.periodic,
     Function.Periodic.intervalIntegral_add_eq (periodic_periodize fun x : ℝ ↦ f x • γ x) c a]

diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean
@@ -147,8 +147,8 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
   have h2C₁ : ∀ (s : ℝ) (hs : fract s = 0), fract ⁻¹' C₁ ∈ 𝓝 s := by
     intro s hs
     refine fract_preimage_mem_nhds ?_ fun _ ↦ ?_
-    · rw [hs]; exact mem_of_superset (Iic_mem_nhds <| by norm_num) (subset_union_left _ _)
-    · exact mem_of_superset (Ici_mem_nhds <| by norm_num) (subset_union_right _ _)
+    · rw [hs]; exact mem_of_superset (Iic_mem_nhds <| by norm_num) subset_union_left
+    · exact mem_of_superset (Ici_mem_nhds <| by norm_num) subset_union_right
   let C : Set (E × ℝ × ℝ) := (fun x ↦ x.2.1) ⁻¹' Iic (5⁻¹ : ℝ) ∪ (fun x ↦ fract x.2.2) ⁻¹' C₁
   have hC : IsClosed C := by
     refine (isClosed_Iic.preimage continuous_snd.fst).union ?_
@@ -191,7 +191,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
         have :
           (fun x : E × ℝ × ℝ ↦ (x.1, smoothTransition x.2.1, fract x.2.2)) ⁻¹' C ∈ 𝓝 (x, t, s) := by
           simp_rw [C, preimage_union, preimage_preimage, fract_fract]
-          refine mem_of_superset ?_ (subset_union_right _ _)
+          refine mem_of_superset ?_ subset_union_right
           refine continuousAt_id.snd'.snd'.preimage_mem_nhds (h2C₁ s hs)
         filter_upwards [this] with x hx
         exact (hγ₅C hx).trans

diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
@@ -218,16 +218,15 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w :
   have hA : IsOpen A := by
     simp only [A, affineBases_findim ι ℝ F hι]
     exact isOpen_univ.prod (isOpen_affineIndependent ℝ F)
-  have hU₁ : U ⊆ A := Set.inter_subset_left _ _
   have hU₂ : IsOpen U := hW'.isOpen_inter_preimage hA hV
   have hU₃ : U ∈ 𝓝 (x, p) :=
     mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, Set.mem_inter (by simp [hp, A]) (mem_preimage.mpr hxp)⟩
   apply eventually_of_mem hU₃
   rintro ⟨y, q⟩ hyq
-  have hq : q ∈ affineBases ι ℝ F := by simpa [A] using hU₁ hyq
-  have hyq' : (y, q) ∈ W' ⁻¹' V := (Set.inter_subset_right _ _) hyq
-  refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩, (smooth_barycentric ι ℝ F hι).mono hU₁⟩,
-    ?_, ?_, ?_⟩
+  have hq : q ∈ affineBases ι ℝ F := by simpa [A] using inter_subset_left hyq
+  have hyq' : (y, q) ∈ W' ⁻¹' V := inter_subset_right hyq
+  refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩,
+    (smooth_barycentric ι ℝ F hι).mono inter_subset_left⟩, ?_, ?_, ?_⟩
   · simpa [V] using hyq'
   · simp [hq]
   · simp [hq]; exact AffineBasis.linear_combination_coord_eq_self _ y
@@ -671,7 +670,7 @@ theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈
         rw [hδx₀]
         show Ω ∈ 𝓝 (x₀, γ t s)
         exact mem_nhds_iff.mpr
-          ⟨_, inter_subset_left _ _, hU, ⟨h5γ t s, show x₀ ∈ U from mem_of_mem_nhds hUx₀⟩⟩
+          ⟨_, inter_subset_left, hU, ⟨h5γ t s, show x₀ ∈ U from mem_of_mem_nhds hUx₀⟩⟩
     refine this.mono ?_; intro x h t ht s hs; exact h (t, s) ⟨ht, hs⟩
   have hδsurr : ∀ᶠ x in 𝓝 x₀, (δ x 1).Surrounds (g x) := by
     rcases h6γ with ⟨p, w, h⟩
@@ -866,7 +865,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁
   have hV₀L₁ : Disjoint (closure V₀) L₁ := disjoint_sdiff_self_right.mono hVU₀ Subset.rfl
   obtain ⟨V₂, hV₂, hLV₂, h2V₂⟩ :=
     normal_exists_closure_subset hL₁ (isClosed_closure.isOpen_compl.inter hU₁)
-      (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| (diff_subset _ _).trans hKU₁)
+      (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| diff_subset.trans hKU₁)
   obtain ⟨V₁, hV₁, hLV₁, hV₁₂⟩ := normal_exists_closure_subset hL₁ hV₂ hLV₂
   rw [subset_inter_iff, subset_compl_iff_disjoint_left] at h2V₂
   rcases h2V₂ with ⟨hV₀₂, hV₂U₁⟩
@@ -875,21 +874,21 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁
     refine Disjoint.union_left (hV₀₂.mono_right (hV₁₂.trans subset_closure)) ?_
     rw [← subset_compl_iff_disjoint_left, compl_compl]; exact hV₁₂
   refine ⟨V₀ ∪ U₁ ∩ U₀ ∪ V₁, ((hV₀.union <| hU₁.inter hU₀).union hV₁).mem_nhdsSet.mpr ?_, ?_⟩
-  · refine union_subset (hKV₀.trans <| (subset_union_left _ _).trans <| subset_union_left _ _) ?_
+  · refine union_subset (hKV₀.trans <| subset_union_left.trans <| subset_union_left) ?_
     rw [← inter_union_diff K₁];
-    exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right _ _) hLV₁
+    exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right) hLV₁
   obtain ⟨ρ, h0ρ, h1ρ, -⟩ :=
     exists_continuous_zero_one_of_isClosed (isClosed_closure.union hV₂.isClosed_compl)
       isClosed_closure hdisj
-  let h₀' : SurroundingFamilyIn g b γ₀ (U₁ ∩ U₀) Ω := h₀.mono (inter_subset_right _ _)
-  let h₁' : SurroundingFamilyIn g b γ₁ (U₁ ∩ U₀) Ω := h₁.mono (inter_subset_left _ _)
+  let h₀' : SurroundingFamilyIn g b γ₀ (U₁ ∩ U₀) Ω := h₀.mono inter_subset_right
+  let h₁' : SurroundingFamilyIn g b γ₁ (U₁ ∩ U₀) Ω := h₁.mono inter_subset_left
   let γ := sfHomotopy h₀'.to_sf h₁'.to_sf
   have hγ : ∀ τ, SurroundingFamilyIn g b (γ τ) (U₁ ∩ U₀) Ω := surroundingFamilyIn_sfHomotopy h₀' h₁'
   have heq1 : ∀ x ∈ closure V₀ ∪ V₂ᶜ, γ (ρ x) x = γ₀ x := by
     intro x hx
     simp_rw [γ, h0ρ hx, Pi.zero_apply, sfHomotopy_zero]
   have heq2 : ∀ x ∈ V₀, γ (ρ x) x = γ₀ x := fun x hx ↦
-    heq1 x (subset_closure.trans (subset_union_left _ _) hx)
+    heq1 x (subset_closure.trans subset_union_left hx)
   refine ⟨fun x t ↦ γ (ρ x) x t, ?_, ?_, ?_⟩
   · refine ⟨⟨fun x ↦ (hγ <| ρ x).base x, fun x ↦ (hγ <| ρ x).t₀ x, fun x ↦ (hγ <| ρ x).projI x,
       ?_, ?_⟩, ?_⟩
@@ -905,7 +904,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁
         · exact hx
         · exact (hρx <| h1ρ <| subset_closure hx).elim
       · intro x hx t _ht s hρx; refine h₁.val_in ?_; rcases hx with ((hx | ⟨hx, -⟩) | hx)
-        · exact (hρx <| h0ρ <| subset_closure.trans (subset_union_left _ _) hx).elim
+        · exact (hρx <| h0ρ <| subset_closure.trans subset_union_left hx).elim
         · exact hx
         · exact hVU₁ hx
   · exact eventually_of_mem (hV₀.mem_nhdsSet.mpr hKV₀) heq2

diff --git a/...Eversion/ToMathlib/Topology/Periodic.lean → ...eEversion/ToMathlib/Algebra/Periodic.lean b/...Eversion/ToMathlib/Topology/Periodic.lean → ...eEversion/ToMathlib/Algebra/Periodic.lean
@@ -1,6 +1,6 @@
-import Mathlib.Algebra.Periodic
-import Mathlib.Analysis.Normed.Group.Basic
 import SphereEversion.ToMathlib.Topology.Separation
+import Mathlib.Analysis.Normed.Order.Lattice
+-- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately!
 
 /-!
 
@@ -101,8 +101,7 @@ theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Icc 0 1 = univ :=
 theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ :=
   continuous_quotient_mk'
 
-theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ :=
-  QuotientAddGroup.isOpenMap_coe ℤSubℝ
+theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpenMap_coe ℤSubℝ
 
 theorem quotientMap_id_proj𝕊₁ {X : Type*} [TopologicalSpace X] :
     QuotientMap fun p : X × ℝ ↦ (p.1, proj𝕊₁ p.2) :=

diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
@@ -7,6 +7,7 @@ Authors: Patrick Massot
 import Mathlib.Algebra.Ring.Subring.Order
 import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
 import Mathlib.Geometry.Manifold.MFDeriv.Basic
+import Mathlib.Order.Filter.Ring
 import Mathlib.Topology.Germ
 
 /-!

diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
@@ -36,17 +36,17 @@ theorem nhds_hasBasis_balls_of_open_cov [I.Boundaryless] (x : M) {ι : Type*} {s
     obtain ⟨r, hr₀, hr₁⟩ :=
       (Filter.hasBasis_iff.mp (@nhds_basis_ball E _ (extChartAt I x x)) _).mp hm
     refine ⟨r, ⟨hr₀, hr₁.trans ?_, ⟨j, ?_⟩⟩, ?_⟩
-    · exact ((extChartAt I x).mapsTo.mono (inter_subset_right _ _) Subset.rfl).image_subset
+    · exact ((extChartAt I x).mapsTo.mono inter_subset_right Subset.rfl).image_subset
     · suffices m ⊆ s j by
         refine Subset.trans ?_ this
         convert monotone_image (f := (extChartAt I x).symm) hr₁
-        exact (PartialEquiv.symm_image_image_of_subset_source _ (Set.inter_subset_right _ _)).symm
-      exact (Set.inter_subset_left _ _).trans (Set.inter_subset_left _ _)
+        exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm
+      exact inter_subset_left.trans inter_subset_left
     · suffices m ⊆ n by
         refine Subset.trans ?_ this
         convert monotone_image (f := (extChartAt I x).symm) hr₁
-        exact (PartialEquiv.symm_image_image_of_subset_source _ (Set.inter_subset_right _ _)).symm
-      exact (Set.inter_subset_left _ _).trans (Set.inter_subset_right _ _)
+        exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm
+      exact inter_subset_left.trans inter_subset_right
   · rintro ⟨r, ⟨hr₀, hr₁, -⟩, hr₂⟩
     replace hr₀ : Metric.ball (extChartAt I x x) r ∈ 𝓝 (extChartAt I x x) := ball_mem_nhds _ hr₀
     rw [← map_extChartAt_nhds_of_boundaryless, Filter.mem_map] at hr₀

diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
@@ -130,7 +130,7 @@ theorem hasFDerivAt_parametric_primitive_of_lip' (F : H → ℝ → E) (F' : ℝ
       rw [hasFDerivAt_iff_hasDerivAt, toSpanSingleton_apply, one_smul]
       exact intervalIntegral.integral_hasDerivAt_right (hF_int_ball x₀ x₀_in ha hsx₀)
         ⟨Ioo a₀ b₀, Ioo_nhds, hF_meas x₀ x₀_in⟩ hF_cont
-    have D₃ : HasFDerivAt (fun x ↦ ∫ t in s x₀..s x, F x t - F x₀ t) 0 x₀ := by
+    have D₃ : HasFDerivAt (𝕜 := ℝ) (fun x ↦ ∫ t in s x₀..s x, F x t - F x₀ t) 0 x₀ := by
       refine IsBigO.hasFDerivAt (𝕜 := ℝ) ?_ one_lt_two
       have O₁ : (fun x ↦ ∫ s in s x₀..s x, bound s) =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ := by
         have : (fun x ↦ s x - s x₀) =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ := s_diff.isBigO_sub.norm_right

diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -68,7 +68,7 @@ section
 
 /-! ## The standard ℤ action on ℝ is properly discontinuous
 
-TODO: use that in ToMathlib.Topology.Periodic?
+TODO: use that in ToMathlib.Algebra.Periodic?
 -/
 
 instance : VAdd ℤ ℝ :=
@@ -195,7 +195,7 @@ theorem fract_preimage_mem_nhds {s : Set ℝ} {x : ℝ} (h1 : s ∈ 𝓝 (fract
     obtain ⟨v, hvs, hv, h1v⟩ := mem_nhds_iff.mp (h2 hx)
     rw [mem_nhds_iff]
     exact ⟨fract ⁻¹' (u ∪ v), preimage_mono (union_subset hus hvs),
-      (hu.union hv).preimage_fract fun _ ↦ subset_union_right _ _ h1v, subset_union_left _ _ hxu⟩
+      (hu.union hv).preimage_fract fun _ ↦ subset_union_right h1v, subset_union_left hxu⟩
   · exact (continuousAt_fract (sub_ne_zero.1 hx)).preimage_mem_nhds h1
 
 end Fract

diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean
@@ -1,6 +1,6 @@
 import Mathlib.Topology.Separation
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Nat.Interval
+import Mathlib.Order.Interval.Finset.Nat
 
 open scoped Topology