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
 
@@ -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

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
 
@@ -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. -/

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
 
@@ -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 ψ) :=

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

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
 
@@ -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]