diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index 30811a11..71e247fe 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -1,7 +1,9 @@
-import SphereEversion.Global.LocalisationData
-import SphereEversion.Global.LocalizedConstruction
-import SphereEversion.Global.ParametricityForFree
-import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
+module
+
+public import SphereEversion.Global.LocalisationData
+public import SphereEversion.Global.LocalizedConstruction
+public import SphereEversion.Global.ParametricityForFree
+public import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
 
 /-!
 # Gromov's theorem
@@ -9,6 +11,8 @@ import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
 We prove the h-principle for open and ample first order differential relations.
 -/
 
+public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index bec87cc3..437119c9 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -1,10 +1,14 @@
-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.Global.Gromov
-import SphereEversion.Global.TwistOneJetSec
+module
+
+public import Mathlib.Analysis.Convex.AmpleSet
+public import Mathlib.Geometry.Manifold.Instances.Sphere
+public import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional
+public import SphereEversion.ToMathlib.Geometry.Manifold.Immersion
+public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
+public import SphereEversion.Global.Gromov
+public import SphereEversion.Global.TwistOneJetSec
+
+@[expose] public section
 
 -- set_option trace.filter_inst_type true
 noncomputable section
diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean
index 687887f8..92b21c4c 100644
--- a/SphereEversion/Global/Localisation.lean
+++ b/SphereEversion/Global/Localisation.lean
@@ -1,5 +1,7 @@
-import SphereEversion.Local.AmpleRelation
-import SphereEversion.Global.Relation
+module
+
+public import SphereEversion.Local.AmpleRelation
+public import SphereEversion.Global.Relation
 
 /-! # Link with the local story
 
@@ -8,6 +10,8 @@ This file bridges the gap between Chapter 2 and Chapter 3. It builds on
 is about embedding any manifold into another one).
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
@@ -196,11 +200,11 @@ theorem ChartPair.mkHtpy_congr (F : FormalSol R) {𝓕 : (R.localize p.φ p.ψ).
     {t t' : ℝ} (h : 𝓕 t = 𝓕 t') : p.mkHtpy F 𝓕 t = p.mkHtpy F 𝓕 t' := by
   unfold ChartPair.mkHtpy
   by_cases hF : p.compat' F 𝓕
-  · simp only [dif_pos hF]
+  · simp only [dite_eq_left hF]
     apply FormalSol.coe_inj fun x ↦ ?_
     rw [p.φ.updateFormalSol_apply, p.φ.updateFormalSol_apply,
       RelLoc.HtpyFormalSol.unloc_congr' p h]
-  · simp only [dif_neg hF]; rfl
+  · simp only [dite_eq_right hF]; rfl
 
 theorem ChartPair.mkHtpy_eq_self (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol)
     {t m} (hm : ∀ hF : range (F.bs ∘ p.φ) ⊆ range p.ψ, ∀ x ∈ p.K₁,
@@ -250,7 +254,7 @@ theorem ChartPair.mkHtpy_eq_of_forall {F : FormalSol R}
 theorem ChartPair.mkHtpy_localize {F : FormalSol R} {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol}
     {t e} (h : p.compat' F 𝓕) (rg : range ((p.mkHtpy F 𝓕 t).bs ∘ p.φ) ⊆ range p.ψ) :
     (p.mkHtpy F 𝓕 t).toOneJetSec.localize p.φ p.ψ rg e = (𝓕 t).unloc e := by
-  simp_rw [ChartPair.mkHtpy, dif_pos h] at rg ⊢
+  simp_rw [ChartPair.mkHtpy, dite_eq_left h] at rg ⊢
   exact p.φ.Jupdate_localize p.ψ p.hK₁ (p.mkHtpy_aux h) t rg e
 
 theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R}
@@ -259,7 +263,7 @@ theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R}
   have rg : range ((p.mkHtpy F 𝓕 t).bs ∘ p.φ) ⊆ range p.ψ := by
     rintro - ⟨e, rfl⟩
     dsimp only [ChartPair.mkHtpy]
-    simp only [dif_pos h]
+    simp only [dite_eq_left h]
     rw [p.φ.updateFormalSol_bs p.ψ p.hK₁]
     simp only [Function.comp_apply, OpenSmoothEmbedding.update_apply_embedding, mem_range_self]
   rw [← isHolonomicAt_localize_iff _ p.φ p.ψ rg e, ← JetSec.unloc_hol_at_iff]
@@ -278,7 +282,7 @@ theorem ChartPair.dist_update' [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_
     intro 𝓕 h𝓕 t e
     change (p.mkHtpy F 𝓕 t (p.φ e)).1.2 = p.φ.update p.ψ bsF (fun e ↦ (𝓕.unloc p t).bs e) (p.φ e)
     dsimp only [ChartPair.mkHtpy]
-    rw [dif_pos h𝓕, OpenSmoothEmbedding.updateFormalSol_apply]
+    rw [dite_eq_left h𝓕, OpenSmoothEmbedding.updateFormalSol_apply]
     simp_rw [OpenSmoothEmbedding.update_apply_embedding, OneJetBundle.embedding_toFun,
       OpenSmoothEmbedding.transfer_proj_snd]
     rfl
diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean
index 2be6fd33..4208c2db 100644
--- a/SphereEversion/Global/LocalisationData.lean
+++ b/SphereEversion/Global/LocalisationData.lean
@@ -1,5 +1,9 @@
-import Mathlib.Topology.MetricSpace.PartitionOfUnity
-import SphereEversion.Global.SmoothEmbedding
+module
+
+public import Mathlib.Topology.MetricSpace.PartitionOfUnity
+public import SphereEversion.Global.SmoothEmbedding
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean
index 0e7a6228..3e50bd74 100644
--- a/SphereEversion/Global/LocalizedConstruction.lean
+++ b/SphereEversion/Global/LocalizedConstruction.lean
@@ -1,5 +1,9 @@
-import SphereEversion.Global.Localisation
-import SphereEversion.Local.HPrinciple
+module
+
+public import SphereEversion.Global.Localisation
+public import SphereEversion.Local.HPrinciple
+
+public section
 
 noncomputable section
 
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index ec4bb754..8f1053dd 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -5,16 +5,18 @@ Authors: Patrick Massot, Floris van Doorn
 
 ! This file was ported from Lean 3 source module global.one_jet_bundle
 -/
-import Mathlib.Tactic.Common
+module
 
-import Mathlib.Analysis.Normed.Module.Completion
-import Mathlib.Geometry.Manifold.Algebra.Monoid
-import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
-import Mathlib.Geometry.Manifold.Notation
-import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
-import Mathlib.Geometry.Manifold.VectorBundle.Hom
-import Mathlib.Geometry.Manifold.VectorBundle.Pullback
-import Mathlib.Tactic.Monotonicity.Lemmas
+public import Mathlib.Tactic.Common
+
+public import Mathlib.Analysis.Normed.Module.Completion
+public import Mathlib.Geometry.Manifold.Algebra.Monoid
+public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
+public import Mathlib.Geometry.Manifold.Notation
+public import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
+public import Mathlib.Geometry.Manifold.VectorBundle.Hom
+public import Mathlib.Geometry.Manifold.VectorBundle.Pullback
+public import Mathlib.Tactic.Monotonicity.Lemmas
 
 /-!
 # 1-jet bundles
@@ -31,6 +33,8 @@ We prove
   are smooth, then so is `x ↦ (f₁ x, f₃ x, ϕ₂ x ∘ ϕ₁ x) : N → J¹(M₁, M₃)`.
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean
index 8a948d01..9be0658a 100644
--- a/SphereEversion/Global/OneJetSec.lean
+++ b/SphereEversion/Global/OneJetSec.lean
@@ -5,10 +5,12 @@ Authors: Patrick Massot, Floris van Doorn
 
 ! This file was ported from Lean 3 source module global.one_jet_sec
 -/
-import Mathlib.Order.Filter.Germ.Basic
-import Mathlib.Geometry.Manifold.Notation
-import SphereEversion.ToMathlib.Topology.Algebra.Module
-import SphereEversion.Global.OneJetBundle
+module
+
+public import Mathlib.Order.Filter.Germ.Basic
+public import Mathlib.Geometry.Manifold.Notation
+public import SphereEversion.ToMathlib.Topology.Algebra.Module
+public import SphereEversion.Global.OneJetBundle
 
 /-!
 # Sections of 1-jet bundles
@@ -23,6 +25,8 @@ In this file we consider two manifolds `M` and `M'` with models `I` and `I'`
 * `OneJetSet I M I' M'`: smooth sections of `OneJetBundle I M I' M' → M`
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
@@ -148,7 +152,8 @@ def IsHolonomicGerm {x : M} (φ : Germ (𝓝 x) (OneJetBundle I M I' M')) : Prop
         intro f g hfg hf
         have hfg' : (fun x' ↦ (f x').1.2) =ᶠ[𝓝 x] fun x' ↦ (g x').1.2 :=
           hfg.fun_comp fun s ↦ s.1.2
-        rw [← hfg'.mfderiv_eq, hf, hfg.self_of_nhds]
+        rw [hfg'.symm.mfderiv_eq, hf, hfg.self_of_nhds]
+        rfl
       exact fun f g H ↦ propext ⟨key f g H, key g f H.symm⟩)
 
 /-- The one-jet extension of a function, seen as a section of the 1-jet bundle. -/
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
index 65fa455d..4d34139d 100644
--- a/SphereEversion/Global/ParametricityForFree.lean
+++ b/SphereEversion/Global/ParametricityForFree.lean
@@ -1,5 +1,9 @@
-import SphereEversion.Global.Relation
-import Mathlib.Analysis.Convex.AmpleSet
+module
+
+public import SphereEversion.Global.Relation
+public import Mathlib.Analysis.Convex.AmpleSet
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index eff4d325..facdbab1 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -1,8 +1,10 @@
-import Mathlib.Geometry.Manifold.Metrizable
-import SphereEversion.Local.DualPair
-import SphereEversion.Global.OneJetSec
-import SphereEversion.Global.SmoothEmbedding
-import Mathlib.Analysis.Convex.AmpleSet
+module
+
+public import Mathlib.Geometry.Manifold.Metrizable
+public import SphereEversion.Local.DualPair
+public import SphereEversion.Global.OneJetSec
+public import SphereEversion.Global.SmoothEmbedding
+public import Mathlib.Analysis.Convex.AmpleSet
 
 /-!
 # First order partial differential relations for maps between manifolds
@@ -16,6 +18,7 @@ for maps from `M` to `M'` is a set in the 1-jet bundle J¹(M, M'), also known as
 `OneJetBundle I M I' M'`.
 -/
 
+@[expose] public section
 
 noncomputable section
 
@@ -474,7 +477,10 @@ theorem OpenSmoothEmbedding.smooth_transfer :
     ContMDiffAt.mfderiv (fun _ ↦ φ.invFun) (fun x : OneJetBundle IX X IY Y ↦ φ x.1.1)
       ((φ.contMDiffAt_inv <| _).comp (x, φ x.1.1) contMDiffAt_snd)
       (φ.contMDiff_to.contMDiffAt.comp x (contMDiff_oneJetBundle_proj.fst x)) (mod_cast le_top)
-  · simp only [left_inv] at this; exact this
+  · convert this
+    · simp
+    · simp
+      rfl
   exact mem_range_self _
 
 theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) :=
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index 8062257f..25f6564e 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -1,14 +1,18 @@
-import Mathlib.Analysis.Normed.Order.Lattice
-import Mathlib.Geometry.Manifold.ContMDiff.Atlas
-import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
-import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
-import Mathlib.Geometry.Manifold.Notation
-import SphereEversion.Indexing
-import SphereEversion.Notations
-import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
-import SphereEversion.ToMathlib.Geometry.Manifold.IsManifold.ExtChartAt
-import SphereEversion.ToMathlib.Topology.Misc
-import SphereEversion.ToMathlib.Topology.Paracompact
+module
+
+public import Mathlib.Analysis.Normed.Order.Lattice
+public import Mathlib.Geometry.Manifold.ContMDiff.Atlas
+public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
+public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
+public import Mathlib.Geometry.Manifold.Notation
+public import SphereEversion.Indexing
+public import SphereEversion.Notations
+public import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
+public import SphereEversion.ToMathlib.Geometry.Manifold.IsManifold.ExtChartAt
+public import SphereEversion.ToMathlib.Topology.Misc
+public import SphereEversion.ToMathlib.Topology.Paracompact
+
+@[expose] public section
 
 noncomputable section
 
@@ -397,11 +401,11 @@ def update (m : M) : N :=
 end
 
 @[simp]
-theorem update_of_nmem_range {m : M} (hm : m ∉ range φ) : update φ ψ f g m = f m := if_neg hm
+theorem update_of_nmem_range {m : M} (hm : m ∉ range φ) : update φ ψ f g m = f m := ite_eq_right hm
 
 @[simp]
 theorem update_of_mem_range {m : M} (hm : m ∈ range φ) : update φ ψ f g m = ψ (g (φ.invFun m)) :=
-  if_pos hm
+  ite_eq_left hm
 
 theorem update_apply_embedding (x : X) : update φ ψ f g (φ x) = ψ (g x) := by simp
 
@@ -413,7 +417,7 @@ theorem nice_update_of_eq_outside_compact_aux {K : Set X} (g : X → Y)
   · obtain ⟨x, rfl⟩ := hm'
     replace hm : x ∉ K := by contrapose! hm; exact mem_image_of_mem φ hm
     simp [hg x hm]
-  · exact if_neg hm'
+  · exact ite_eq_right hm'
 
 open Function
 
@@ -433,7 +437,7 @@ theorem contMDiff_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M
     rw [← compl_subset_iff_union, compl_compl]
     exact image_subset_range φ K
   have h₄ (x) : k x ∈ U → update φ ψ (f x) (g x) (k x) = (ψ ∘ g x ∘ φ.invFun) (k x) :=
-    fun hm ↦ if_pos hm
+    fun hm ↦ ite_eq_left hm
   by_cases hx : k x ∈ U
   · exact ⟨k ⁻¹' U, φ.isOpen_range.preimage hk.continuous, hx,
       (contMDiffOn_congr h₄).mpr <| ψ.contMDiff_to.comp_contMDiffOn <| hg.comp_contMDiffOn
diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean
index 8ad573eb..99ffb483 100644
--- a/SphereEversion/Global/TwistOneJetSec.lean
+++ b/SphereEversion/Global/TwistOneJetSec.lean
@@ -5,7 +5,11 @@ Authors: Heather Macbeth
 
 ! This file was ported from Lean 3 source module global.twist_one_jet_sec
 -/
-import SphereEversion.Global.OneJetSec
+module
+
+public import SphereEversion.Global.OneJetSec
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean
index 158dda6e..032d4ab1 100644
--- a/SphereEversion/Indexing.lean
+++ b/SphereEversion/Indexing.lean
@@ -1,9 +1,11 @@
-import Mathlib.Order.Interval.Finset.Fin
-import Mathlib.Data.Fin.SuccPredOrder
-import Mathlib.Data.Nat.SuccPred
-import Mathlib.SetTheory.Cardinal.Basic
-import Mathlib.Tactic.Cases
-import SphereEversion.ToMathlib.Data.Nat.Basic
+module
+
+public import Mathlib.Order.Interval.Finset.Fin
+public import Mathlib.Data.Fin.SuccPredOrder
+public import Mathlib.Data.Nat.SuccPred
+public import Mathlib.SetTheory.Cardinal.Basic
+public import Mathlib.Tactic.Cases
+public import SphereEversion.ToMathlib.Data.Nat.Basic
 /-!
 # Indexing types
 
@@ -12,6 +14,8 @@ This file introduces `IndexType : ℕ → Type` such that `IndexType 0 = ℕ` an
 together with supporting lemmas.
 -/
 
+@[expose] public section
+
 
 open Fin Set
 
diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean
index 1df3a5e0..ee4ae08f 100644
--- a/SphereEversion/InductiveConstructions.lean
+++ b/SphereEversion/InductiveConstructions.lean
@@ -1,9 +1,13 @@
-import Mathlib.Topology.Germ
-import Mathlib.Analysis.Complex.Norm
-import Mathlib.Analysis.RCLike.Basic
-import SphereEversion.ToMathlib.Topology.Misc
-import SphereEversion.Indexing
-import SphereEversion.Notations
+module
+
+public import Mathlib.Topology.Germ
+public import Mathlib.Analysis.Complex.Norm
+public import Mathlib.Analysis.RCLike.Basic
+public import SphereEversion.ToMathlib.Topology.Misc
+public import SphereEversion.Indexing
+public import SphereEversion.Notations
+
+@[expose] public section
 
 -- set_option trace.filter_inst_type true
 
@@ -346,7 +350,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
       · have hp : ∀ᶠ p : ℝ × X in 𝓝 (t, x), p.1 ≤ T i.toNat :=
           continuousAt_fst (p := (t, x)) (Iic_mem_nhds ht)
         apply Quotient.sound
-        exact hp.mono fun p hp ↦ if_pos hp
+        exact hp.mono fun p hp ↦ ite_eq_left hp
     have loc₂ : ∀ p : ℝ × X, p.1 > T i.toNat →
         (F'' : Germ (𝓝 p) Y) = fun p : ℝ × X ↦
           F' ((2 : ℝ) ^ (i.toNat + 1) * (p.1 - T i.toNat)) p.2 := fun (t, x) ht ↦ by
@@ -355,7 +359,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
         apply mem_of_superset (prod_mem_nhds (Ioi_mem_nhds ht) univ_mem)
         rintro ⟨t', x'⟩ ⟨ht', -⟩
         simpa using ht'
-      exact hp.mono fun q hq ↦ if_neg hq
+      exact hp.mono fun q hq ↦ ite_eq_right hq
     refine ⟨F'', ?_, ?_, ?_, ?_⟩
     · intro p
       by_cases! ht : p.1 ≤ T i.toNat
@@ -373,7 +377,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
       rw [i.toNat_succ hi] at ht ⊢
       have h₂t : ¬t ≤ T i.toNat := ((T_lt_succ i.toNat).trans_le ht).not_ge
       dsimp only [F'']
-      rw [if_neg h₂t, if_neg]
+      rw [ite_eq_right h₂t, ite_eq_right]
       · rw [hfutur_F'.self_of_nhdsSet, mul_T_succ_sub]
         conv =>
           rw [mem_Ici]
diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean
index b25dbc82..ef717293 100644
--- a/SphereEversion/Local/AmpleRelation.lean
+++ b/SphereEversion/Local/AmpleRelation.lean
@@ -3,9 +3,11 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
-import Mathlib.Analysis.Convex.AmpleSet
-import SphereEversion.Local.DualPair
-import SphereEversion.Local.Relation
+module
+
+public import Mathlib.Analysis.Convex.AmpleSet
+public import SphereEversion.Local.DualPair
+public import SphereEversion.Local.Relation
 
 /-! # Slices of first order relations
 
@@ -27,6 +29,8 @@ order relations: a relation is ample if all its slices are ample sets.
 At the end of the file we consider 1-jet sections and slices corresponding to points in their image.
 -/
 
+@[expose] public section
+
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean
index 4a42ec65..de39ff70 100644
--- a/SphereEversion/Local/Corrugation.lean
+++ b/SphereEversion/Local/Corrugation.lean
@@ -1,11 +1,13 @@
-import Mathlib.Analysis.Asymptotics.Lemmas
-import Mathlib.LinearAlgebra.Dual.Lemmas
-import Mathlib.Analysis.Calculus.ParametricIntegral
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
-import SphereEversion.ToMathlib.Algebra.Ring.Periodic
-import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
-import SphereEversion.Loops.Basic
-import SphereEversion.Local.DualPair
+module
+
+public import Mathlib.Analysis.Asymptotics.Lemmas
+public import Mathlib.LinearAlgebra.Dual.Lemmas
+public import Mathlib.Analysis.Calculus.ParametricIntegral
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+public import SphereEversion.ToMathlib.Algebra.Ring.Periodic
+public import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
+public import SphereEversion.Loops.Basic
+public import SphereEversion.Local.DualPair
 
 /-! # Theillière's corrugation operation
 
@@ -30,6 +32,8 @@ The main definition is `corrugation`. The main results are:
 
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open Set Function Filter MeasureTheory ContinuousLinearMap
diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean
index b8cce50e..74c0df2b 100644
--- a/SphereEversion/Local/DualPair.lean
+++ b/SphereEversion/Local/DualPair.lean
@@ -1,10 +1,12 @@
-import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
-import Mathlib.Analysis.Complex.Norm
-import Mathlib.Analysis.Normed.Module.Completion
-import Mathlib.LinearAlgebra.Dual.Lemmas
-import SphereEversion.Notations
-import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
-import SphereEversion.ToMathlib.LinearAlgebra.Basic
+module
+
+public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
+public import Mathlib.Analysis.Complex.Norm
+public import Mathlib.Analysis.Normed.Module.Completion
+public import Mathlib.LinearAlgebra.Dual.Lemmas
+public import SphereEversion.Notations
+public import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
+public import SphereEversion.ToMathlib.LinearAlgebra.Basic
 
 /-! # Dual pairs
 
@@ -28,6 +30,8 @@ This is crucial in order to apply convex integration to immersions.
 Then we prove continuity and smoothness lemmas for this operation.
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean
index 8ab338a4..369f02b0 100644
--- a/SphereEversion/Local/HPrinciple.lean
+++ b/SphereEversion/Local/HPrinciple.lean
@@ -1,8 +1,10 @@
-import Mathlib.LinearAlgebra.Basis.Flag
-import Mathlib.LinearAlgebra.FreeModule.PID
-import SphereEversion.Loops.Exists
-import SphereEversion.Local.Corrugation
-import SphereEversion.Local.AmpleRelation
+module
+
+public import Mathlib.LinearAlgebra.Basis.Flag
+public import Mathlib.LinearAlgebra.FreeModule.PID
+public import SphereEversion.Loops.Exists
+public import SphereEversion.Local.Corrugation
+public import SphereEversion.Local.AmpleRelation
 
 /-!
 # Local h-principle for open and ample relations
@@ -50,6 +52,8 @@ need to access its components only once.
 
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
@@ -315,9 +319,9 @@ theorem bu_lt {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) (
   calc
     ‖(smoothStep t * L.ρ x) • v‖ = |smoothStep t| * |L.ρ x| * ‖v‖ := by
       rw [norm_smul, Real.norm_eq_abs, abs_mul]
-    _ ≤ ‖v‖ :=
-      (mul_le_of_le_one_left (norm_nonneg _)
-        (mul_le_one₀ (smoothStep.abs_le t) (abs_nonneg _) (L.ρ_le x)))
+    _ ≤ ‖v‖ := by
+      apply mul_le_of_le_one_left (norm_nonneg _)
+      exact Bound.mul_le_one (smoothStep.abs_le t) (L.ρ_le x) (by grind)
     _ < ε := hv
 
 theorem improveStep_c0_close {ε : ℝ} (ε_pos : 0 < ε) :
diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean
index 7724e567..5b2e1e18 100644
--- a/SphereEversion/Local/OneJet.lean
+++ b/SphereEversion/Local/OneJet.lean
@@ -1,6 +1,8 @@
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.SpecialFunctions.SmoothTransition
-import SphereEversion.Notations
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.Analysis.SpecialFunctions.SmoothTransition
+public import SphereEversion.Notations
 
 /-! # Spaces of 1-jets and their sections
 
@@ -22,6 +24,8 @@ more smoothness constraints at `t = 0` and `t = 1` (requiring flat functions), b
 for smooth concatenations anyway.
  -/
 
+@[expose] public section
+
 
 noncomputable section
 
@@ -251,7 +255,7 @@ theorem htpy_jet_sec_comp_aux {f g : ℝ → E → F} (hf : 𝒞 ∞ ↿f) (hg :
     obtain ⟨t, x⟩ := p
     replace hp : t < 1 / 2 := (prodMk_mem_set_prod_eq.mp hp).1
     change ite (t ≤ 1 / 2) (f (smoothStep (2 * t)) x) (g (smoothStep (2 * t - 1)) x) = _
-    rw [if_pos hp.le]
+    rw [ite_eq_left hp.le]
     rfl
   · apply (hf (1 / 2, x₀)).congr_of_eventuallyEq
     have : (Ioo (3 / 8) (5 / 8) : Set ℝ) ×ˢ univ ∈ 𝓝 (1 / (2 : ℝ), x₀) := by
@@ -273,7 +277,7 @@ theorem htpy_jet_sec_comp_aux {f g : ℝ → E → F} (hf : 𝒞 ∞ ↿f) (hg :
     obtain ⟨t, x⟩ := p
     replace hp : ¬t ≤ 1 / 2 := by push Not; exact (prodMk_mem_set_prod_eq.mp hp).1
     change ite (t ≤ 1 / 2) (f (smoothStep (2 * t)) x) (g (smoothStep (2 * t - 1)) x) = _
-    rw [if_neg hp]
+    rw [ite_eq_right hp]
     rfl
 
 /-- Concatenation of homotopies of formal solution. The result depend on our choice of
@@ -287,7 +291,7 @@ def HtpyJetSec.comp (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) : HtpyJet
 @[simp]
 theorem HtpyJetSec.comp_of_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : t ≤ 1 / 2) :
     𝓕.comp 𝓖 h t = 𝓕 (smoothStep <| 2 * t) := by
-  ext x : 2 <;> · dsimp [HtpyJetSec.comp]; exact if_pos ht
+  ext x : 2 <;> · dsimp [HtpyJetSec.comp]; exact ite_eq_left ht
 
 theorem HtpyJetSec.comp_le_0 (𝓕 𝓖 : HtpyJetSec E F) (h) :
     ∀ᶠ t near Iic 0, 𝓕.comp 𝓖 h t = 𝓕 0 := by
@@ -310,7 +314,7 @@ theorem HtpyJetSec.comp_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 0
 theorem HtpyJetSec.comp_of_not_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : ¬t ≤ 1 / 2) :
     𝓕.comp 𝓖 h t = 𝓖 (smoothStep <| 2 * t - 1) := by
   rw [one_div] at ht
-  ext x : 2 <;> simp [comp, if_neg ht] <;> rfl
+  ext x : 2 <;> simp [comp, ite_eq_right ht] <;> rfl
 
 theorem HtpyJetSec.comp_ge_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : ∀ᶠ t near Ici 1, 𝓕.comp 𝓖 h t = 𝓖 1 := by
   have : Ioi (7 / 8 : ℝ) ∈ 𝓝ˢ (Ici (1 : ℝ)) :=
diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean
index 04059ca6..6be928bd 100644
--- a/SphereEversion/Local/ParametricHPrinciple.lean
+++ b/SphereEversion/Local/ParametricHPrinciple.lean
@@ -1,5 +1,7 @@
-import SphereEversion.Local.HPrinciple
-import SphereEversion.ToMathlib.Topology.Algebra.Module
+module
+
+public import SphereEversion.Local.HPrinciple
+public import SphereEversion.ToMathlib.Topology.Algebra.Module
 
 /-!
 In this file we prove the parametric version of the local h-principle.
@@ -14,6 +16,8 @@ then there exists a homotopy `𝓕 : ℝ × P → J¹(E, F)` between `𝓕` and
 near `K`, that agrees with `𝓕₀` near `C` and is everywhere `ε`-close to `𝓕₀`
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open Set Function RelLoc
diff --git a/SphereEversion/Local/Relation.lean b/SphereEversion/Local/Relation.lean
index 12e85441..6436314c 100644
--- a/SphereEversion/Local/Relation.lean
+++ b/SphereEversion/Local/Relation.lean
@@ -1,5 +1,7 @@
-import Mathlib.Topology.MetricSpace.HausdorffDistance
-import SphereEversion.Local.OneJet
+module
+
+public import Mathlib.Topology.MetricSpace.HausdorffDistance
+public import SphereEversion.Local.OneJet
 
 /-!
 # Local partial differential relations and their formal solutions
@@ -15,6 +17,8 @@ The h-principle question is whether we can deform any formal solution into a sol
 The type of deformations is `HtpyJetSet E F` (homotopies of 1-jet sections).
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
index 7e351398..daf49543 100644
--- a/SphereEversion/Local/SphereEversion.lean
+++ b/SphereEversion/Local/SphereEversion.lean
@@ -1,7 +1,9 @@
-import Mathlib.Analysis.Convex.AmpleSet
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual
-import SphereEversion.Local.ParametricHPrinciple
+module
+
+public import Mathlib.Analysis.Convex.AmpleSet
+public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
+public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual
+public import SphereEversion.Local.ParametricHPrinciple
 
 /-!
 This is file proves the existence of a sphere eversion from the local verson of the h-principle.
@@ -20,6 +22,8 @@ Finally, we obtain the existence of sphere eversion from the parametric local h-
 proven in `Local/ParametricHPrinciple`.
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean
index 5a7092b7..d9a708cb 100644
--- a/SphereEversion/Loops/Basic.lean
+++ b/SphereEversion/Loops/Basic.lean
@@ -1,11 +1,15 @@
-import SphereEversion.Notations
-import SphereEversion.ToMathlib.Equivariant
-import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
+module
+
+public import SphereEversion.Notations
+public import SphereEversion.ToMathlib.Equivariant
+public import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
 
 /-!
 # Basic definitions and properties of loops
 -/
 
+@[expose] public section
+
 open Set Function FiniteDimensional Int TopologicalSpace
 
 open scoped Topology unitInterval
diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
index 3f79eb2a..d1f10e58 100644
--- a/SphereEversion/Loops/DeltaMollifier.lean
+++ b/SphereEversion/Loops/DeltaMollifier.lean
@@ -1,11 +1,13 @@
-import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
-import Mathlib.Analysis.Convolution
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
-import Mathlib.MeasureTheory.Measure.Haar.Unique
-import Mathlib.Analysis.Calculus.BumpFunction.Normed
-import SphereEversion.ToMathlib.Algebra.Ring.Periodic
-import SphereEversion.ToMathlib.Analysis.ContDiff
-import SphereEversion.Loops.Basic
+module
+
+public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
+public import Mathlib.Analysis.Convolution
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+public import Mathlib.MeasureTheory.Measure.Haar.Unique
+public import Mathlib.Analysis.Calculus.BumpFunction.Normed
+public import SphereEversion.ToMathlib.Algebra.Ring.Periodic
+public import SphereEversion.ToMathlib.Analysis.ContDiff
+public import SphereEversion.Loops.Basic
 
 /-!
 # Delta mollifiers
@@ -26,6 +28,8 @@ The key ingredients are the existence of smooth "bump functions" and a powerful
 convolutions.
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean
index 06199ee6..3afcadd8 100644
--- a/SphereEversion/Loops/Exists.lean
+++ b/SphereEversion/Loops/Exists.lean
@@ -1,6 +1,10 @@
-import SphereEversion.Loops.Reparametrization
-import SphereEversion.ToMathlib.Analysis.CutOff
-import Mathlib.Topology.MetricSpace.HausdorffDistance
+module
+
+public import SphereEversion.Loops.Reparametrization
+public import SphereEversion.ToMathlib.Analysis.CutOff
+public import Mathlib.Topology.MetricSpace.HausdorffDistance
+
+public section
 
 noncomputable section
 
@@ -124,23 +128,21 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
   let f : E → ℝ × ℝ → ℝ := fun x y ↦ if Ωᶜ.Nonempty then infDist (x, γ₃ x y.1 y.2) (Ωᶜ) else 1
   have hI : IsCompact (I ×ˢ I) := isCompact_Icc.prod isCompact_Icc
   have h1f : Continuous ↿f := (continuous_fst.prodMk hγ₃.cont).infDist.if_const _ continuous_const
-  have h2f : ∀ x : E, Continuous (f x) := fun x ↦ h1f.comp₂ continuous_const continuous_id
-  have h3f : ∀ {x y}, 0 < f x y := by
-    intro x y; by_cases hΩ : Ωᶜ.Nonempty
-    · simp_rw [f, if_pos hΩ, ← hΩ_op.isClosed_compl.notMem_iff_infDist_pos hΩ, notMem_compl_iff,
-        hγ₃.val_in (mem_univ _)]
-    · simp_rw [f, if_neg hΩ, zero_lt_one]
+  have h3f {x y} : 0 < f x y := by
+    by_cases hΩ : Ωᶜ.Nonempty
+    · simp_rw [f, ite_eq_left hΩ, ← hΩ_op.isClosed_compl.notMem_iff_infDist_pos hΩ,
+        notMem_compl_iff, hγ₃.val_in (mem_univ _)]
+    · simp_rw [f, ite_eq_right hΩ, zero_lt_one]
   let ε₂ : E → ℝ := fun x ↦ min (min ε₀ (ε₁ x)) (sInf (f x '' I ×ˢ I))
-  have hcε₂ : Continuous ε₂ := (continuous_const.min hcε₁).min (hI.continuous_sInf h1f)
+  have hcε₂ : Continuous ε₂ := by
+    have := hI.continuous_sInf h1f; unfold ε₂; fun_prop
   have hε₂ : ∀ {x}, 0 < ε₂ x := fun {x} ↦
     lt_min (lt_min hε₀ (hε₁ x))
       ((hI.lt_sInf_iff_of_continuous
-            ((nonempty_Icc.mpr zero_le_one).prod (nonempty_Icc.mpr zero_le_one))
-            (h2f x).continuousOn _).mpr
+          ((nonempty_Icc.mpr zero_le_one).prod (nonempty_Icc.mpr zero_le_one)) (by fun_prop) _).mpr
         fun x _ ↦ h3f)
   let γ₄ := ↿γ₃
   have h0γ₄ : ∀ x t s, γ₄ (x, t, s) = γ₃ x t s := fun x t s ↦ rfl
-  have hγ₄ : Continuous γ₄ := hγ₃.cont
   let C₁ : Set ℝ := Iic (5⁻¹ : ℝ) ∪ Ici (4 / 5)
   have h0C₁ : (0 : ℝ) ∈ C₁ := Or.inl (by rw [mem_Iic]; norm_num1)
   have h2C₁ : ∀ (s : ℝ) (hs : fract s = 0), fract ⁻¹' C₁ ∈ 𝓝 s := by
@@ -181,7 +183,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
       exact Or.imp le_of_lt le_of_lt hs
   have h3γ₄ : ContDiffOn ℝ ∞ γ₄ U := hb.fst'.contDiffOn.congr h2γ₄
   obtain ⟨γ₅, hγ₅, hγ₅₄, hγ₅C⟩ :=
-    exists_smooth_and_eqOn hγ₄ hcε₂.fst' (fun x ↦ hε₂) hC ⟨U, hUC, h3γ₄⟩
+    exists_smooth_and_eqOn hγ₃.cont hcε₂.fst' (fun x ↦ hε₂) hC ⟨U, hUC, h3γ₄⟩
   let γ : E → ℝ → Loop F := fun x t ↦
     ⟨fun s ↦ γ₅ (x, smoothTransition t, fract s), fun s ↦ by rw [fract_add_one s]⟩
   have hγ : 𝒞 ∞ ↿γ := by
@@ -225,15 +227,15 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
     · exact (x, γ₃ x (smoothTransition t) (fract s))
     · rw [dist_comm, dist_prod_same_left]
       refine (hγ₅₄ (x, _, fract s)).trans_le ((min_le_right _ _).trans <| csInf_le ?_ ?_)
-      · exact (isCompact_Icc.prod isCompact_Icc).bddBelow_image (h2f x).continuousOn
+      · exact (isCompact_Icc.prod isCompact_Icc).bddBelow_image (by fun_prop)
       · rw [← hγ₃.projI]
-        simp_rw [f, if_pos hΩ]
+        simp_rw [f, ite_eq_left hΩ]
         apply mem_image_of_mem _ (mk_mem_prod projI_mem_Icc (unitInterval.fract_mem s))
   · refine eventually_of_mem (Filter.inter_mem hV hγ₂₁) fun x hx t s ↦ ?_
     refine (closedBall_subset_ball ?_).trans (hΩ x hx.1)
     refine (dist_triangle ..).trans_lt (add_lt_add_of_le_of_lt
       ((hγ₅₄ (x, _, fract s)).le.trans <| (min_le_left _ _).trans <| min_le_left ..) ?_)
-    simp_rw [γ₄, γ₃, HasUncurry.uncurry, Loop.reparam_apply, show γ₂ x = γ₁ x from hx.2]
+    simp_rw [γ₃, HasUncurry.uncurry, Loop.reparam_apply, show γ₂ x = γ₁ x from hx.2]
     exact h2γ₁ x hx.1 ..
 
 variable (g b Ω U K)
diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean
index 52c973a4..351c255a 100644
--- a/SphereEversion/Loops/Reparametrization.lean
+++ b/SphereEversion/Loops/Reparametrization.lean
@@ -1,11 +1,13 @@
-import Mathlib.Analysis.Calculus.BumpFunction.Convolution
-import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
-import SphereEversion.Loops.Surrounding
-import SphereEversion.Loops.DeltaMollifier
-import SphereEversion.ToMathlib.ExistsOfConvex
-import SphereEversion.ToMathlib.Analysis.ContDiff
+module
+
+public import Mathlib.Analysis.Calculus.BumpFunction.Convolution
+public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+public import SphereEversion.Loops.Surrounding
+public import SphereEversion.Loops.DeltaMollifier
+public import SphereEversion.ToMathlib.ExistsOfConvex
+public import SphereEversion.ToMathlib.Analysis.ContDiff
 
 /-!
 # The reparametrization lemma
@@ -45,6 +47,8 @@ The key ingredients are theories of calculus, convex hulls, barycentric coordina
 existence of delta mollifiers, partitions of unity, and the inverse function theorem.
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
index 44fc05a0..d70ce5db 100644
--- a/SphereEversion/Loops/Surrounding.lean
+++ b/SphereEversion/Loops/Surrounding.lean
@@ -1,10 +1,12 @@
-import SphereEversion.InductiveConstructions
-import SphereEversion.Loops.Basic
-import SphereEversion.ToMathlib.ExistsOfConvex
-import SphereEversion.ToMathlib.SmoothBarycentric
-import SphereEversion.ToMathlib.Topology.Path
-import Mathlib.Analysis.Convex.Caratheodory
-import Mathlib.Analysis.Normed.Module.FiniteDimension
+module
+
+public import SphereEversion.InductiveConstructions
+public import SphereEversion.Loops.Basic
+public import SphereEversion.ToMathlib.ExistsOfConvex
+public import SphereEversion.ToMathlib.SmoothBarycentric
+public import SphereEversion.ToMathlib.Topology.Path
+public import Mathlib.Analysis.Convex.Caratheodory
+public import Mathlib.Analysis.Normed.Module.FiniteDimension
 
 /-!
 # Surrounding families of loops
@@ -31,6 +33,8 @@ The key results are:
  * `exists_surrounding_loops`
 -/
 
+@[expose] public section
+
 -- to obtain that normed spaces are locally connected
 open Set Function Module Int Prod Path Filter
 open scoped Topology unitInterval ContDiff
@@ -153,7 +157,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ
       basis.coord_apply_combination_of_mem (Finset.mem_univ i) w_sum]
     exact w_pos i
   · rintro ⟨b, h₀, h₁, h₂, h₃⟩
-    have : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype
+    have : Fintype b := ((finiteDimensional_iff_setFinite ℝ h₁).mp (by infer_instance)).fintype
     have hb : Fintype.card b = d + 1 := by
       rw [← h₁.affineSpan_eq_top_iff_card_eq_finrank_add_one, Subtype.range_coe_subtype,
         ofPred_mem_eq, h₂]
@@ -184,7 +188,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} (
     exact hsf
   have htne : (t : Set F).Nonempty := convexHull_nonempty_iff.mp ⟨f, hf⟩
   obtain ⟨b, hb₁, hb₂, hb₃, hb₄⟩ := hs.exists_between_affineIndependent_span_eq_top hts htne hai
-  have hb₀ : b.Finite := finite_set_of_fin_dim_affineIndependent ℝ hb₃
+  have hb₀ : b.Finite := ((finiteDimensional_iff_setFinite ℝ hb₃).mp (by infer_instance))
   obtain ⟨c, hc⟩ := interior_convexHull_nonempty_iff_affineSpan_eq_top.mpr hb₄
   rw [← hs.interior_eq] at hb₂
   obtain ⟨ε, hε, hcs⟩ :=
@@ -193,7 +197,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} (
   rw [AffineMap.image_convexHull] at hbε
   let t : Units ℝ := Units.mk0 ε (by linarith)
   refine ⟨AffineMap.homothety c (t : ℝ) '' b, hcs, ?_, ?_, hbε (convexHull_mono hb₁ hf)⟩
-  · rw [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff]; assumption
+  · rwa [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff]
   · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
diff --git a/SphereEversion/Main.lean b/SphereEversion/Main.lean
index 4b838809..2c83edaa 100644
--- a/SphereEversion/Main.lean
+++ b/SphereEversion/Main.lean
@@ -1,4 +1,8 @@
-import SphereEversion.Global.Immersion
+module
+
+public import SphereEversion.Global.Immersion
+
+public section
 
 open Metric FiniteDimensional Set ModelWithCorners
 
diff --git a/SphereEversion/Notations.lean b/SphereEversion/Notations.lean
index c0727f94..7f4adf89 100644
--- a/SphereEversion/Notations.lean
+++ b/SphereEversion/Notations.lean
@@ -1,4 +1,8 @@
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+module
+
+public import Mathlib.Analysis.Calculus.ContDiff.Basic
+
+public section
 
 open scoped Topology ContDiff
 
diff --git a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean
index 817ee571..b292864b 100644
--- a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean
+++ b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean
@@ -1,6 +1,8 @@
-import Mathlib.Analysis.Normed.Order.Lattice
-import Mathlib.Algebra.Ring.Periodic
-import Mathlib.Topology.Separation.Hausdorff
+module
+
+public import Mathlib.Analysis.Normed.Order.Lattice
+public import Mathlib.Algebra.Ring.Periodic
+public import Mathlib.Topology.Separation.Hausdorff
 
 -- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately!
 
@@ -21,6 +23,8 @@ Patrick is not sure this is the optimal version.
 In the first part, generalize many lemmas to any period and add to `Algebra.Ring.Periodic.lean`?
 -/
 
+@[expose] public section
+
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean
index d8c43cd1..eb9d32d9 100644
--- a/SphereEversion/ToMathlib/Analysis/Calculus.lean
+++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean
@@ -1,6 +1,10 @@
-import Mathlib.Analysis.Normed.Module.Completion
-import Mathlib.Analysis.SpecialFunctions.SmoothTransition
-import SphereEversion.ToMathlib.Topology.Misc
+module
+
+public import Mathlib.Analysis.Normed.Module.Completion
+public import Mathlib.Analysis.SpecialFunctions.SmoothTransition
+public import SphereEversion.ToMathlib.Topology.Misc
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
index cae80c77..a99b8166 100644
--- a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
+++ b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
@@ -1,4 +1,6 @@
-import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
+module
+
+public import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
 
 /-!
 
@@ -8,6 +10,8 @@ TODO Generalise these lemmas appropriately.
 
 -/
 
+public section
+
 
 open Set Function Metric AffineMap
 
diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
index 6da0e5b0..8313cf6b 100644
--- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean
+++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
@@ -1,10 +1,14 @@
-import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.Calculus.Deriv.MeanValue
-import Mathlib.Analysis.InnerProductSpace.Calculus
-import Mathlib.Analysis.InnerProductSpace.Dual
-import SphereEversion.ToMathlib.Analysis.Calculus
-import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
+module
+
+public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+public import Mathlib.Analysis.Calculus.ContDiff.Basic
+public import Mathlib.Analysis.Calculus.Deriv.MeanValue
+public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Analysis.InnerProductSpace.Dual
+public import SphereEversion.ToMathlib.Analysis.Calculus
+public import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
index 96f375c4..1120e1b5 100644
--- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
+++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -1,6 +1,10 @@
-import Mathlib.Analysis.Convex.Combination
-import Mathlib.Algebra.Module.BigOperators
-import Mathlib.Algebra.Order.Hom.Ring
+module
+
+public import Mathlib.Analysis.Convex.Combination
+public import Mathlib.Algebra.Module.BigOperators
+public import Mathlib.Algebra.Order.Hom.Ring
+
+@[expose] public section
 
 open Function Set
 
@@ -28,7 +32,7 @@ theorem finite_of_finprod_ne_one {M : Type*} {ι : Sort _} [CommMonoid M] {f : 
   classical
   rw [finprod_def] at h
   contrapose h
-  rw [dif_neg (by exact h)]
+  rw [dite_eq_right (by exact h)]
 
 theorem support_finite_of_finsum_eq_of_neZero {M : Type*} {ι : Sort _} [AddCommMonoid M]
     {f : ι → M} {x : M} [NeZero x] (h : ∑ᶠ i, f i = x) : (support f).Finite := by
diff --git a/SphereEversion/ToMathlib/Analysis/CutOff.lean b/SphereEversion/ToMathlib/Analysis/CutOff.lean
index d195cd29..e5a43f51 100644
--- a/SphereEversion/ToMathlib/Analysis/CutOff.lean
+++ b/SphereEversion/ToMathlib/Analysis/CutOff.lean
@@ -1,4 +1,8 @@
-import Mathlib.Geometry.Manifold.PartitionOfUnity
+module
+
+public import Mathlib.Geometry.Manifold.PartitionOfUnity
+
+public section
 
 open Set Filter
 
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
index 4ad6ea37..7d035f6d 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
@@ -3,12 +3,16 @@ Copyright (c) 2022 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Analysis.InnerProductSpace.Dual
-import Mathlib.Analysis.InnerProductSpace.Orientation
-import Mathlib.LinearAlgebra.Alternating.Curry
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Dual
+public import Mathlib.Analysis.InnerProductSpace.Orientation
+public import Mathlib.LinearAlgebra.Alternating.Curry
 
 /-! # The cross-product on an oriented real inner product space of dimension three -/
 
+public section
+
 noncomputable section
 
 open scoped RealInnerProductSpace
@@ -74,7 +78,7 @@ def crossProduct' : E →L[ℝ] E →L[ℝ] E :=
 @[simp]
 theorem crossProduct'_apply (v : E) :
     ω.crossProduct' v = LinearMap.toContinuousLinearMap (ω.crossProduct v) :=
-  rfl
+  (rfl)
 
 theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖ * ‖v‖ := by
   classical
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean
index 965e58f6..21f0c3ef 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean
@@ -1,5 +1,9 @@
-import Mathlib.Analysis.InnerProductSpace.Dual
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Dual
+public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule
+
+public section
 
 open scoped RealInnerProductSpace
 
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
index 714ca6a5..83db98d0 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
@@ -1,4 +1,8 @@
-import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean
index e365eec5..bc1ddad0 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean
@@ -5,13 +5,17 @@ Authors: Heather Macbeth
 
 ! This file was ported from Lean 3 source module to_mathlib.analysis.inner_product_space.rotation
 -/
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
-import SphereEversion.ToMathlib.Analysis.ContDiff
-import SphereEversion.ToMathlib.LinearAlgebra.Basic
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+public import SphereEversion.ToMathlib.Analysis.ContDiff
+public import SphereEversion.ToMathlib.LinearAlgebra.Basic
+public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct
 
 /-! # Rotation about an axis, considered as a function in that axis -/
 
+@[expose] public section
+
 noncomputable section
 
 open scoped RealInnerProductSpace
@@ -49,7 +53,7 @@ theorem rot_eq_aux : ω.rot = ω.rotAux := by
   ext1 p
   dsimp [rot, rotAux]
   rw [id_eq_sum_starProjection_self_orthogonalComplement (K := ℝ ∙ p.2)]
-  simp only [smul_add, sub_smul, one_smul, starProjection]
+  simp only [smul_add, sub_smul, one_smul, starProjection, crossProduct'_apply]
   abel
 
 /-- The map `rot` is smooth on `ℝ × (E \ {0})`. -/
diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
index 6bd50bb3..cc6882f0 100644
--- a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
+++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
@@ -1,5 +1,9 @@
-import Mathlib.Analysis.InnerProductSpace.EuclideanDist
-import Mathlib.Topology.OpenPartialHomeomorph.Constructions
+module
+
+public import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+public import Mathlib.Topology.OpenPartialHomeomorph.Constructions
+
+@[expose] public section
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
index bb5aa8c6..ec7d3fc5 100644
--- a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
+++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
@@ -1,6 +1,10 @@
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
-import Mathlib.Analysis.Normed.Operator.Prod
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
+public import Mathlib.Analysis.Normed.Operator.Prod
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Data/Nat/Basic.lean b/SphereEversion/ToMathlib/Data/Nat/Basic.lean
index 7945d3f8..2611a014 100644
--- a/SphereEversion/ToMathlib/Data/Nat/Basic.lean
+++ b/SphereEversion/ToMathlib/Data/Nat/Basic.lean
@@ -1,6 +1,10 @@
-import Mathlib.Data.Nat.Notation
-import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Choose
+module
+
+public import Mathlib.Data.Nat.Notation
+public import Mathlib.Logic.Function.Basic
+public import Mathlib.Tactic.Choose
+
+public section
 
 -- The next lemma won't be used, it's a warming up exercise for the one below.
 -- It could go to mathlib.
diff --git a/SphereEversion/ToMathlib/Equivariant.lean b/SphereEversion/ToMathlib/Equivariant.lean
index 216fa200..28c7af13 100644
--- a/SphereEversion/ToMathlib/Equivariant.lean
+++ b/SphereEversion/ToMathlib/Equivariant.lean
@@ -1,5 +1,9 @@
-import Mathlib.Topology.Algebra.Order.Floor
-import SphereEversion.ToMathlib.Topology.Misc
+module
+
+public import Mathlib.Topology.Algebra.Order.Floor
+public import SphereEversion.ToMathlib.Topology.Misc
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean
index d6e0f696..048904de 100644
--- a/SphereEversion/ToMathlib/ExistsOfConvex.lean
+++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean
@@ -1,5 +1,9 @@
-import SphereEversion.ToMathlib.Partition
-import Mathlib.Geometry.Manifold.Notation
+module
+
+public import SphereEversion.ToMathlib.Partition
+public import Mathlib.Geometry.Manifold.Notation
+
+public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
index 36e175a0..860b9fdb 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
@@ -3,20 +3,23 @@ Copyright (c) 2023 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
+module
 
-import Mathlib.Algebra.Ring.Subring.Order
-import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
-import Mathlib.Geometry.Manifold.MFDeriv.Basic
-import Mathlib.Geometry.Manifold.Notation
-import Mathlib.Order.Filter.Ring
-import Mathlib.Tactic.Cases
-import Mathlib.Topology.Germ
+public import Mathlib.Algebra.Ring.Subring.Order
+public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
+public import Mathlib.Geometry.Manifold.MFDeriv.Basic
+public import Mathlib.Geometry.Manifold.Notation
+public import Mathlib.Order.Filter.Ring
+public import Mathlib.Tactic.Cases
+public import Mathlib.Topology.Germ
 
 /-!
 ## Germs of smooth functions
 under construction: might need further refactoring to be usable!
 -/
 
+@[expose] public section
+
 -- TODO: please confirm authorship and copyright are appropriate
 
 noncomputable section
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
index 170ce05c..61e649fb 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
@@ -3,9 +3,11 @@ Copyright (c) 2024 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
-import Mathlib.Geometry.Manifold.ContMDiff.Defs
-import Mathlib.Geometry.Manifold.MFDeriv.Defs
-import Mathlib.Geometry.Manifold.Notation
+module
+
+public import Mathlib.Geometry.Manifold.ContMDiff.Defs
+public import Mathlib.Geometry.Manifold.MFDeriv.Defs
+public import Mathlib.Geometry.Manifold.Notation
 
 /-! ## Smooth immersions
 
@@ -33,6 +35,8 @@ but in finite dimensions, the general definition is equivalent to the one in thi
 manifold, immersion
 
 -/
+
+public section
 noncomputable section
 
 open Set Function
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index 9281516b..05520ae7 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -1,4 +1,8 @@
-import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
+module
+
+public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
+
+@[expose] public section
 
 open scoped Topology
 
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
index 484d5884..bb4be091 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
@@ -1,4 +1,8 @@
-import Mathlib.Geometry.Manifold.Metrizable
+module
+
+public import Mathlib.Geometry.Manifold.Metrizable
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
index a719d8af..08cea64e 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
@@ -5,13 +5,17 @@ Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module to_mathlib.geometry.manifold.vector_bundle.misc
 -/
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
-import Mathlib.Topology.VectorBundle.Hom
+module
+
+public import Mathlib.Geometry.Manifold.VectorBundle.Basic
+public import Mathlib.Topology.VectorBundle.Hom
 
 /-!
 # Various operations on and properties of smooth vector bundles
 -/
 
+public section
+
 noncomputable section
 
 open Bundle Set
@@ -81,7 +85,7 @@ theorem trivialization_continuousLinearMapAt (x : B) :
     (Trivial.trivialization B F).continuousLinearMapAt 𝕜 x = ContinuousLinearMap.id 𝕜 F := by
   ext v
   simp_rw [Trivialization.continuousLinearMapAt_apply, Trivialization.coe_linearMapAt]
-  rw [if_pos]
+  rw [ite_eq_left]
   exacts [rfl, mem_univ _]
 
 end Bundle.Trivial
@@ -138,7 +142,7 @@ theorem pullback_symm (e : Trivialization F (π F E)) (x : B') :
   simp_rw [Trivialization.symm, Pretrivialization.symm]
   congr; ext (hx : f x ∈ e.toPretrivialization.baseSet)
   change cast _ (e.symm (f x) y) = cast _ (e.toOpenPartialHomeomorph.symm (f x, y)).2
-  simp_rw [Trivialization.symm, Pretrivialization.symm, dif_pos hx, cast_cast]
+  simp_rw [Trivialization.symm, Pretrivialization.symm, dite_eq_left hx, cast_cast]
   rfl
 
 end Trivialization
diff --git a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
index 4101b697..c5b500ab 100644
--- a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
+++ b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
@@ -1,8 +1,12 @@
-import Mathlib.Algebra.Module.Submodule.Ker
-import Mathlib.LinearAlgebra.Span.Defs
+module
+
+public import Mathlib.Algebra.Module.Submodule.Ker
+public import Mathlib.LinearAlgebra.Span.Defs
 
 /-! Note: some results should go to `LinearAlgebra.Span`. -/
 
+public section
+
 
 open Submodule Function
 
diff --git a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean
index 1f1cd90f..4cc56e1b 100644
--- a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean
+++ b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean
@@ -1,4 +1,8 @@
-import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+module
+
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+
+public section
 
 open Module Submodule
 
diff --git a/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean b/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean
index 5115b99f..57dff6c7 100644
--- a/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean
+++ b/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean
@@ -1,4 +1,8 @@
-import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+module
+
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+
+public section
 
 variable (X : Type*) [TopologicalSpace X]
 
diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
index 65d80026..84f5def6 100644
--- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
+++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
@@ -1,7 +1,11 @@
-import Mathlib.Analysis.Calculus.ParametricIntegral
-import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
-import SphereEversion.ToMathlib.Analysis.Calculus
+module
+
+public import Mathlib.Analysis.Calculus.ParametricIntegral
+public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+public import SphereEversion.ToMathlib.Analysis.Calculus
+
+public section
 
 open TopologicalSpace MeasureTheory Filter FirstCountableTopology Metric Set Function
 open scoped Topology
diff --git a/SphereEversion/ToMathlib/Order/Filter/Basic.lean b/SphereEversion/ToMathlib/Order/Filter/Basic.lean
index 617feb19..936c919d 100644
--- a/SphereEversion/ToMathlib/Order/Filter/Basic.lean
+++ b/SphereEversion/ToMathlib/Order/Filter/Basic.lean
@@ -1,4 +1,8 @@
-import Mathlib.Order.Filter.Basic
+module
+
+public import Mathlib.Order.Filter.Basic
+
+public section
 
 theorem Filter.EventuallyEq.eventuallyEq_ite {X Y : Type*} {l : Filter X} {f g : X → Y}
     {P : X → Prop} [DecidablePred P] (h : f =ᶠ[l] g) :
diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
index 921df6bb..03135fb5 100644
--- a/SphereEversion/ToMathlib/Partition.lean
+++ b/SphereEversion/ToMathlib/Partition.lean
@@ -1,6 +1,10 @@
-import Mathlib.Geometry.Manifold.PartitionOfUnity
-import SphereEversion.ToMathlib.Analysis.Convex.Basic
-import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
+module
+
+public import Mathlib.Geometry.Manifold.PartitionOfUnity
+public import SphereEversion.ToMathlib.Analysis.Convex.Basic
+public import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean
index e753822f..365ba03c 100644
--- a/SphereEversion/ToMathlib/SmoothBarycentric.lean
+++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean
@@ -1,7 +1,11 @@
-import Mathlib.Analysis.Calculus.AddTorsor.Coord
-import Mathlib.Analysis.Matrix.Normed
-import Mathlib.LinearAlgebra.AffineSpace.Matrix
-import Mathlib.Tactic.Cases
+module
+
+public import Mathlib.Analysis.Calculus.AddTorsor.Coord
+public import Mathlib.Analysis.Matrix.Normed
+public import Mathlib.LinearAlgebra.AffineSpace.Matrix
+public import Mathlib.Tactic.Cases
+
+@[expose] public section
 
 noncomputable section
 
@@ -41,12 +45,12 @@ def evalBarycentricCoords [DecidablePred (· ∈ affineBases ι R P)] (p : P) (v
 theorem evalBarycentricCoords_apply_of_mem_bases [DecidablePred (· ∈ affineBases ι R P)] (p : P)
     {v : ι → P} (h : v ∈ affineBases ι R P) :
     evalBarycentricCoords ι R P p v = (AffineBasis.mk v h.1 h.2).coords p :=
-  dif_pos h
+  dite_eq_left h
 
 @[simp]
 theorem evalBarycentricCoords_apply_of_not_mem_bases [DecidablePred (· ∈ affineBases ι R P)] (p : P)
     {v : ι → P} (h : v ∉ affineBases ι R P) : evalBarycentricCoords ι R P p v = 0 :=
-  dif_neg h
+  dite_eq_right h
 
 variable {ι R P}
 
@@ -56,7 +60,7 @@ theorem evalBarycentricCoords_eq_det [Fintype ι] [DecidableEq ι] (S : Type*) [
       (b.toMatrix v).det⁻¹ • (b.toMatrix v)ᵀ.cramer (b.coords p) := by
   ext i
   by_cases h : v ∈ affineBases ι S P
-  · simp only [evalBarycentricCoords, h, dif_pos, smul_eq_mul, Pi.smul_apply,
+  · simp only [evalBarycentricCoords, h, dite_eq_left, smul_eq_mul, Pi.smul_apply,
       AffineBasis.coords_apply]
     erw [← b.det_smul_coords_eq_cramer_coords ⟨v, h.1, h.2⟩ p]
     simp only [Pi.smul_apply, AffineBasis.coords_apply, smul_eq_mul]
@@ -64,7 +68,7 @@ theorem evalBarycentricCoords_eq_det [Fintype ι] [DecidableEq ι] (S : Type*) [
     rw [Matrix.isUnit_iff_isUnit_det] at hu
     erw [← mul_assoc, ← Ring.inverse_eq_inv, Ring.inverse_mul_cancel _ hu, one_mul]
   · simp only [evalBarycentricCoords, h, smul_eq_mul, Pi.zero_apply, inv_eq_zero,
-      dif_neg, not_false_iff, zero_eq_mul, Pi.smul_apply]
+      dite_eq_right, not_false_iff, zero_eq_mul, Pi.smul_apply]
     left
     rwa [mem_affineBases_iff ι S P b v, Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero,
       Classical.not_not] at h
@@ -144,9 +148,9 @@ theorem smooth_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Finit
     simp only [Matrix.updateRow_apply]
     simp only [AffineBasis.toMatrix_apply, AffineBasis.coords_apply]
     by_cases hij : j = i
-    · simp only [hij, if_true]
+    · simp only [hij, ite_true]
       exact (smooth_barycentric_coord b j').fst'.of_le le_top
-    · simp only [hij, if_false]
+    · simp only [hij, ite_false]
       exact ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j)
 
 end smooth_barycentric
diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean
index 7d0a3de3..2b4c8622 100644
--- a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean
+++ b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean
@@ -1,4 +1,8 @@
-import Mathlib.Topology.Algebra.Module.Equiv
+module
+
+public import Mathlib.Topology.Algebra.Module.Equiv
+
+public section
 
 namespace ContinuousLinearMap
 
diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
index 004223f2..b40cf2f3 100644
--- a/SphereEversion/ToMathlib/Topology/Misc.lean
+++ b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -1,9 +1,13 @@
-import Mathlib.Algebra.Ring.Periodic
-import Mathlib.Analysis.Normed.Affine.Convex
-import Mathlib.Tactic.Cases
-import Mathlib.Topology.Algebra.Order.Floor
-import Mathlib.Topology.EMetricSpace.Paracompact
-import Mathlib.Topology.ShrinkingLemma
+module
+
+public import Mathlib.Algebra.Ring.Periodic
+public import Mathlib.Analysis.Normed.Affine.Convex
+public import Mathlib.Tactic.Cases
+public import Mathlib.Topology.Algebra.Order.Floor
+public import Mathlib.Topology.EMetricSpace.Paracompact
+public import Mathlib.Topology.ShrinkingLemma
+
+@[expose] public section
 
 noncomputable section
 
@@ -185,7 +189,7 @@ open scoped Classical in
 theorem isOpen_slice_of_isOpen_over {Ω : Set (α × β)} {x₀ : α}
     (hΩ_op : ∃ U ∈ 𝓝 x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) : IsOpen (Prod.mk x₀ ⁻¹' Ω) := by
   rcases hΩ_op with ⟨U, hU, hU_op⟩; convert hU_op.preimage (Continuous.prodMk_right x₀) using 1
-  simp_rw [preimage_inter, preimage_preimage, preimage_const, mem_of_mem_nhds hU, if_pos,
+  simp_rw [preimage_inter, preimage_preimage, preimage_const, mem_of_mem_nhds hU, ite_eq_left,
     inter_univ]
 
 end
@@ -411,9 +415,9 @@ theorem cover_nat_nhdsWithin' {α} [TopologicalSpace α] [SecondCountableTopolog
     {f : ∀ x ∈ s, Set α} (hf : ∀ (x) (hx : x ∈ s), f x hx ∈ 𝓝[s] x) (hs : s.Nonempty) :
     ∃ (x : ℕ → α) (hx : range x ⊆ s), s ⊆ ⋃ n, f (x n) (range_subset_iff.mp hx n) := by
   let g x := if hx : x ∈ s then f x hx else ∅
-  have hg : ∀ x ∈ s, g x ∈ 𝓝[s] x := fun x hx ↦ by simp_rw [g, dif_pos hx]; exact hf x hx
+  have hg : ∀ x ∈ s, g x ∈ 𝓝[s] x := fun x hx ↦ by simp_rw [g, dite_eq_left hx]; exact hf x hx
   obtain ⟨x, hx, h⟩ := TopologicalSpace.cover_nat_nhdsWithin hg hs
-  simp_rw [g, dif_pos (range_subset_iff.mp hx _)] at h
+  simp_rw [g, dite_eq_left (range_subset_iff.mp hx _)] at h
   exact ⟨x, hx, h⟩
 
 end TopologicalSpace
diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean
index f9d5f945..57e6871a 100644
--- a/SphereEversion/ToMathlib/Topology/Paracompact.lean
+++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean
@@ -1,6 +1,10 @@
-import Mathlib.Topology.Separation.Hausdorff
-import Mathlib.Data.Real.Basic
-import Mathlib.Order.Interval.Finset.Nat
+module
+
+public import Mathlib.Topology.Separation.Hausdorff
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Order.Interval.Finset.Nat
+
+public section
 
 open scoped Topology
 
diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean
index f09fd795..531ec5d0 100644
--- a/SphereEversion/ToMathlib/Topology/Path.lean
+++ b/SphereEversion/ToMathlib/Topology/Path.lean
@@ -1,6 +1,10 @@
-import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.Analysis.Normed.Order.Lattice
-import Mathlib.Topology.Connected.PathConnected
+module
+
+public import Mathlib.Analysis.Normed.Field.Basic
+public import Mathlib.Analysis.Normed.Order.Lattice
+public import Mathlib.Topology.Connected.PathConnected
+
+@[expose] public section
 
 open Set Function
 
@@ -62,11 +66,11 @@ theorem strans_zero (γ γ' : Path x x) : γ.strans γ' 0 = γ' := by
 @[simp]
 theorem strans_one {x : X} (γ γ' : Path x x) : γ.strans γ' 1 = γ := by
   ext t
-  simp only [strans, unitInterval.le_one', Path.coe_mk_mk, if_pos, div_one, extend_extends',
+  simp only [strans, unitInterval.le_one', Path.coe_mk_mk, ite_eq_left, div_one, extend_extends',
     Icc.coe_one]
 
 theorem strans_self {x : X} (γ γ' : Path x x) (t₀ : I) : γ.strans γ' t₀ t₀ = x := by
-  simp only [strans, Path.coe_mk_mk, extend_div_self, if_pos, le_rfl]
+  simp only [strans, Path.coe_mk_mk, extend_div_self, ite_eq_left, le_rfl]
 
 @[simp]
 theorem refl_strans_refl {x : X} {t₀ : I} : (refl x).strans (refl x) t₀ = refl x := by
@@ -95,8 +99,8 @@ theorem range_strans_subset {x : X} {γ γ' : Path x x} {t₀ : I} :
     range (γ.strans γ' t₀) ⊆ range γ ∪ range γ' := by
   rintro _ ⟨t, rfl⟩
   by_cases h : t ≤ t₀
-  · rw [strans_def, dif_pos h]; exact Or.inl (mem_range_self _)
-  · rw [strans_def, dif_neg h]; exact Or.inr (mem_range_self _)
+  · rw [strans_def, dite_eq_left h]; exact Or.inl (mem_range_self _)
+  · rw [strans_def, dite_eq_right h]; exact Or.inr (mem_range_self _)
 
 theorem Continuous.path_strans {X Y : Type*} [UniformSpace X]
     [LocallyCompactSpace X] [UniformSpace Y] {f : X → Y} {t : X → I} {s : X → I}
diff --git a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean
index 08710c5f..029d7fff 100644
--- a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean
+++ b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean
@@ -5,8 +5,10 @@ Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module to_mathlib.unused.eventually_constant
 -/
-import Mathlib.Data.Nat.Lattice
-import Mathlib.Topology.Separation.Basic
+module
+
+public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Topology.Separation.Hausdorff
 
 /-!
 # Eventually constant sequences
@@ -14,6 +16,8 @@ import Mathlib.Topology.Separation.Basic
 Related: `monotonic_sequence_limit_index`
 -/
 
+@[expose] public section
+
 
 -- in mathlib, this should probably import
 -- import Order.Filter.atTop_bot
@@ -33,11 +37,11 @@ def unionElim [DecidablePred (· ∈ s)] (f : s → β) (g : t → β) (x : s 
 
 theorem unionElim_eq_left [DecidablePred (· ∈ s)] (hx : x ∈ s) :
     unionElim f g ⟨x, mem_union_left _ hx⟩ = f ⟨x, hx⟩ :=
-  dif_pos hx
+  dite_eq_left hx
 
 theorem unionElim_eq_right [DecidablePred (· ∈ s)] (h1x : x ∈ s ∪ t) (h2x : x ∉ s) :
     unionElim f g ⟨x, h1x⟩ = g ⟨x, h1x.resolve_left h2x⟩ :=
-  dif_neg h2x
+  dite_eq_right h2x
 
 theorem unionElim_eq_right_of_eq [DecidablePred (· ∈ s)] (hxt : x ∈ t)
     (hfg : ∀ (x) (hxs : x ∈ s) (hxt : x ∈ t), f ⟨x, hxs⟩ = g ⟨x, hxt⟩) :
@@ -45,7 +49,7 @@ theorem unionElim_eq_right_of_eq [DecidablePred (· ∈ s)] (hxt : x ∈ t)
   if hxs : x ∈ s then (unionElim_eq_left hxs).trans (hfg x hxs hxt) else unionElim_eq_right _ hxs _
 
 theorem unionElim_restrict [DecidablePred (· ∈ s)] (f : α → β) :
-    unionElim (s.restrict f) (t.restrict f) = (s ∪ t).restrict f := by
+    unionElim (s.domRestrict f) (t.domRestrict f) = (s ∪ t).domRestrict f := by
   ext ⟨x, hx⟩
   --cases (mem_union _ _ _).mp hx <;> simp [union_elim_eq_left, union_elim_eq_right_of_eq, h]
 
@@ -63,16 +67,18 @@ variable {α β γ : Type*} {g : α → β} {f : Filter α} {x : α} {y : β}
 def EventuallyConstant (g : α → β) (f : Filter α) : Prop :=
   ∃ y : β, ∀ᶠ x in f, g x = y
 
-theorem eventuallyConstant_iff_tendsto : EventuallyConstant g f ↔ ∃ x : β, Tendsto g f (pure x) := by simp_rw [EventuallyConstant, tendsto_pure]
+theorem eventuallyConstant_iff_tendsto :
+    EventuallyConstant g f ↔ ∃ x : β, Tendsto g f (pure x) := by
+  simp_rw [EventuallyConstant, tendsto_pure]
 
 theorem EventuallyConstant.nonempty (h : EventuallyConstant g f) : Nonempty β :=
   nonempty_of_exists h
 
 theorem eventuallyConstant_const (y₀ : β) : EventuallyConstant (fun _ ↦ y₀) f :=
-  ⟨y₀, eventually_of_forall fun _ ↦ rfl⟩
+  ⟨y₀, Eventually.of_forall fun _ ↦ rfl⟩
 
 theorem eventuallyConstant_of_unique [Unique β] : EventuallyConstant g f :=
-  ⟨default, eventually_of_forall fun _ ↦ Unique.uniq _ _⟩
+  ⟨default, Eventually.of_forall fun _ ↦ Unique.uniq _ _⟩
 
 theorem eventuallyConstant_atTop [SemilatticeSup α] [Nonempty α] :
     (∃ i, ∀ j, i ≤ j → g j = g i) ↔ EventuallyConstant g atTop := by
@@ -86,12 +92,17 @@ theorem eventuallyConstant_atTop_nat {g : ℕ → α} :
   rw [← eventuallyConstant_atTop]
   apply exists_congr; intro n
   constructor
-  · intro h m hm; induction' hm with m hm ih; rfl; rw [Nat.succ_eq_add_one, h m hm, ih]
+  · intro h m hm
+    induction hm with
+    | refl => rfl
+    | step hm ih =>
+      rename_i m0
+      rw [Nat.succ_eq_add_one, h m0 hm, ih]
   · intro h m hm; rw [h m hm, h (m + 1) hm.step]
 
 theorem EventuallyConstant.compose (h : EventuallyConstant g f) (g' : β → γ) :
     EventuallyConstant (g' ∘ g) f := by
-  cases' h with y hy;
+  obtain ⟨y, hy⟩ := h
   exact ⟨g' y, hy.mono fun x ↦ congr_arg g'⟩
 
 theorem EventuallyConstant.apply {ι : Type*} {p : ι → Type*} {g : α → ∀ x, p x}
@@ -137,7 +148,7 @@ theorem EventuallyConstant.tendsto [Nonempty β] (h : EventuallyConstant g f) :
 theorem eventualValue_compose [f.NeBot] (h : EventuallyConstant g f) (g' : β → γ) :
     @eventualValue _ _ (h.compose g').nonempty (g' ∘ g) f =
       g' (@eventualValue _ _ h.nonempty g f) :=
-  (eventualValue_unique <| (eventually_eq_eventualValue h).mono fun x ↦ congr_arg g').symm
+  (eventualValue_unique <| (eventually_eq_eventualValue h).mono fun _x ↦ congr_arg g').symm
 
 theorem eventualValue_apply {ι : Type*} {p : ι → Type*} [f.NeBot] {g : α → ∀ x, p x}
     (h : EventuallyConstant g f) (i : ι) :
@@ -184,11 +195,11 @@ section EventuallyConstantOn
   `g` restricted to `O` is eventually constant.
 -/
 def EventuallyConstantOn (g : α → β → γ) (f : Filter α) (O : Set β) : Prop :=
-  EventuallyConstant (fun n ↦ O.restrict (g n)) f
+  EventuallyConstant (fun n ↦ O.domRestrict (g n)) f
 
 theorem EventuallyConstantOn.eventuallyConstant (hg : EventuallyConstantOn g f O) (hx : x ∈ O) :
     EventuallyConstant (fun n ↦ g n x) f := by
-  cases' hg with y hg;
+  obtain ⟨y, hg⟩ := hg
   exact ⟨y ⟨x, hx⟩, hg.mono fun n hn ↦ (Function.funext_iff.mp hn ⟨x, hx⟩ : _)⟩
 
 theorem EventuallyConstantOn.nonempty (hg : EventuallyConstantOn g f O) (hx : x ∈ O) : Nonempty γ :=
@@ -196,11 +207,11 @@ theorem EventuallyConstantOn.nonempty (hg : EventuallyConstantOn g f O) (hx : x
 
 theorem eventuallyConstantOn_atTop [SemilatticeSup α] [Nonempty α] :
     (∃ x, ∀ x', x ≤ x' → ∀ y ∈ O, g x' y = g x y) ↔ EventuallyConstantOn g atTop O := by
-  simp_rw [EventuallyConstantOn, ← eventuallyConstant_atTop, restrict_eq_restrict_iff, eq_on]
+  simp_rw [EventuallyConstantOn, ← eventuallyConstant_atTop, domRestrict_eq_domRestrict_iff, EqOn]
 
 theorem EventuallyConstantOn.exists_eventualValue_eq [f.NeBot] (hg : EventuallyConstantOn g f O) :
     ∃ i, ∀ (x) (hx : x ∈ O), @eventualValue _ _ (hg.nonempty hx) (fun n ↦ g n x) f = g i x := by
-  simpa only [@eq_restrict_iff β fun _ ↦ γ, eventualValue_apply hg] using
+  simpa only [@eq_domRestrict_iff β fun _ ↦ γ, eventualValue_apply hg] using
     hg.exists_eventualValue_eq
 
 -- lemma EventuallyConstantOn.exists_eventualValue_eq [f.NeBot] (h : EventuallyConstant g f) :
diff --git a/SphereEversion/ToMathlib/Unused/Fin.lean b/SphereEversion/ToMathlib/Unused/Fin.lean
index b06b17e4..cb21a9cf 100644
--- a/SphereEversion/ToMathlib/Unused/Fin.lean
+++ b/SphereEversion/ToMathlib/Unused/Fin.lean
@@ -1,4 +1,8 @@
-import Mathlib.Data.Fin.SuccPred
+module
+
+public import Mathlib.Data.Fin.SuccPred
+
+public section
 
 -- not directly used
 theorem Fin.coe_succ_le_iff_le {n : ℕ} {j k : Fin n} : j.castSucc ≤ k.castSucc ↔ j ≤ k :=
diff --git a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
index 74a3522a..5916e6d3 100644
--- a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
+++ b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
@@ -1,6 +1,10 @@
-import Mathlib.Geometry.Manifold.VectorBundle.Tangent
-import Mathlib.Geometry.Manifold.MFDeriv.Defs
-import Mathlib.Analysis.Calculus.ContDiff.Defs
+module
+
+public import Mathlib.Geometry.Manifold.VectorBundle.Tangent
+public import Mathlib.Geometry.Manifold.MFDeriv.Defs
+public import Mathlib.Analysis.Calculus.ContDiff.Defs
+
+public section
 
 open Bundle Set Function Filter ContinuousLinearMap
 
diff --git a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean
index 9f8c2e56..43dde897 100644
--- a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean
+++ b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean
@@ -1,7 +1,11 @@
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+module
+
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+
+@[expose] public section
 
 noncomputable section
 
diff --git a/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean b/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean
index 4d036115..19b260c0 100644
--- a/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean
+++ b/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean
@@ -1,4 +1,8 @@
-import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
+module
+
+public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
+
+@[expose] public section
 
 /-
 Multilinear map stuff that was meant as preliminaries for smooth functions gluing.
diff --git a/lake-manifest.json b/lake-manifest.json
index cf559274..49feddd3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
+   "rev": "5bc1283b23926af94593ce7c66fccdbbe49f4d12",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "ba67e212be1197b84c1f1f6299488a10a3002713",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "1681d78dd6e65e38b143f9740d829c826673807c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "SphereEversion",
diff --git a/lakefile.toml b/lakefile.toml
index 5aafe34f..f2a95077 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -11,7 +11,6 @@ weak.linter.style.header = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.33.0"
 
 [[require]]
 name = "checkdecls"
diff --git a/lean-toolchain b/lean-toolchain
index 6a884ba1..d5ae4e31 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.0
\ No newline at end of file
+leanprover/lean4:v4.34.0-rc2
\ No newline at end of file