chore: convert to the module system

SphereEversion/Global/Gromov.lean

@@ -1,14 +1,18 @@
-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
 
 We prove the h-principle for open and ample first order differential relations.
 -/
 
+public section
+
 
 noncomputable section
 

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

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
 

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
 

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
 

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
 

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
 

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
 

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
 

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
 

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
 

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
 

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
 

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]

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

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
 

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