Shake imports: this requires removing all deprecated syntax I missed.

Add a noshake.json file to remove any false positives (only few of them).
leanprover-community · Mar 9, 2024 · 47afe76 · 47afe76
1 parent 6b4a1f4
commit 47afe76
Show file tree

Hide file tree

Showing 27 changed files with 43 additions and 39 deletions.
diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean
@@ -1,5 +1,3 @@
-import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
-import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.Topology.MetricSpace.PartitionOfUnity
 import SphereEversion.Global.SmoothEmbedding
 

diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean
@@ -36,8 +36,8 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ
     isOpen_of_isOpen _ (hRopen.preimage <| OneJetBundle.continuous_transfer _ _)
   have hRloc_ample : Rloc.IsAmple := ample_of_ample _ (hRample.localize _ _)
   -- TODO: try to be consistent about how to state the hFφψ condition
-  replace hFφψ : range (F.bs ∘ φ) ⊆ range ψ
-  · rw [range_comp]
+  replace hFφψ : range (F.bs ∘ φ) ⊆ range ψ := by
+    rw [range_comp]
     exact hFφψ
   let p : ChartPair IM M IX X :=
     { φ
@@ -106,7 +106,7 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ
         apply this.mono
         exact hF'relK₁ _
       · have : ∀ᶠ x near φ '' K₀, x ∈ p.φ '' K₁ := by
-          suffices : ∀ᶠ x near φ '' K₀, x ∈ interior (p.φ '' K₁); exact this.mono interior_subset
+          suffices ∀ᶠ x near φ '' K₀, x ∈ interior (p.φ '' K₁) from this.mono interior_subset
           exact isOpen_interior.mem_nhdsSet.mpr
             ((image_subset φ hK₀K₁).trans (φ.open_map.image_interior_subset K₁))
         exact this.mono (fun a hx hx' ↦ (hx' hx).elim)

diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
@@ -11,6 +11,8 @@ import Mathlib.Analysis.NormedSpace.Completion
 import Mathlib.Geometry.Manifold.Algebra.Monoid
 import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
+import Mathlib.Geometry.Manifold.VectorBundle.Pullback
+import Mathlib.Geometry.Manifold.VectorBundle.Hom
 
 /-!
 # 1-jet bundles

diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
@@ -405,7 +405,7 @@ theorem nice_update_of_eq_outside_compact_aux {K : Set X} (g : X → Y)
     (hg : ∀ x : X, x ∉ K → f (φ x) = ψ (g x)) {m : M} (hm : m ∉ φ '' K) : φ.update ψ f g m = f m := by
   by_cases hm' : m ∈ range φ
   · obtain ⟨x, rfl⟩ := hm'
-    replace hm : x ∉ K; · contrapose! hm; exact mem_image_of_mem φ hm
+    replace hm : x ∉ K := by contrapose! hm; exact mem_image_of_mem φ hm
     simp [hg x hm]
   · exact if_neg hm'
 

diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean
@@ -1,9 +1,8 @@
-import Mathlib.Tactic.Linarith
-import Mathlib.Tactic -- for run_cmd, FIXME minimise
 import Mathlib.Algebra.Order.WithZero
-import Mathlib.Topology.LocallyFinite
 import Mathlib.Data.Fin.Interval
 import Mathlib.Data.Fin.SuccPred
+import Mathlib.Data.Nat.SuccPred
+import Mathlib.Data.ZMod.Defs
 import SphereEversion.ToMathlib.Data.Nat.Basic
 import SphereEversion.ToMathlib.SetTheory.Cardinal.Basic
 /-!

diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean
@@ -1,9 +1,10 @@
-import SphereEversion.ToMathlib.Topology.Germ
+import Mathlib.Topology.Germ
+import Mathlib.Data.Complex.Abs
+import Mathlib.Data.IsROrC.Basic
 import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Data.Set.Lattice
 import SphereEversion.Indexing
 import SphereEversion.Notations
--- import Mathlib.Tactic.Induction
 
 -- set_option trace.filter_inst_type true
 
@@ -275,8 +276,8 @@ theorem inductive_htpy_construction {X Y : Type*} [TopologicalSpace X] {N : ℕ}
       ∃ f' : ℝ × X → Y, (∀ p, PP₀ p f') ∧ (¬IsMax i → PP₂ i.succ f') ∧
         (∀ j ≤ i, ∀ p, PP₁ j p f') ∧ ∀ p ∉ Ici (T i.toNat) ×ˢ U i, f' p = f p := by
     rintro i F h₀F h₂F h₁F
-    replace h₁F : ∀ᶠ x : X near ⋃ j < i, K j, P₁ x fun x ↦ F (T i.toNat, x)
-    · rw [eventually_nhdsSet_iUnion₂]
+    replace h₁F : ∀ᶠ x : X near ⋃ j < i, K j, P₁ x fun x ↦ F (T i.toNat, x) := by
+      rw [eventually_nhdsSet_iUnion₂]
       intro j hj
       have : ∀ x : X, RestrictGermPredicate P₁ (K j) x fun x' ↦ F (1, x') := fun x ↦
         h₁F j hj (1, x) rfl
@@ -293,8 +294,8 @@ theorem inductive_htpy_construction {X Y : Type*} [TopologicalSpace X] {N : ℕ}
       rintro ⟨t, x⟩ (ht : t ≤ _)
       rcases eq_or_lt_of_le ht with (rfl | ht)
       · apply Quotient.sound
-        replace hpast_F' : ↿F' =ᶠ[𝓝 (0, x)] fun q : ℝ × X ↦ F (T i.toNat, q.2)
-        · have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet right_mem_Iic
+        replace hpast_F' : ↿F' =ᶠ[𝓝 (0, x)] fun q : ℝ × X ↦ F (T i.toNat, q.2) := by
+          have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet right_mem_Iic
           apply mem_of_superset (prod_mem_nhds (hpast_F'.filter_mono this) univ_mem)
           rintro ⟨t', x'⟩ ⟨ht', -⟩
           exact (congr_fun ht' x' : _)

diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean
@@ -2,7 +2,10 @@ import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
 import Mathlib.LinearAlgebra.Dual
 import SphereEversion.Notations
 import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm
-import SphereEversion.ToMathlib.Analysis.Calculus
+import Mathlib.Data.Complex.Module
+import Mathlib.Data.Complex.Abs
+import Mathlib.Data.IsROrC.Basic
+import Mathlib.Analysis.NormedSpace.Completion
 import SphereEversion.ToMathlib.LinearAlgebra.Basic
 
 /-! # Dual pairs

diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean
@@ -1,3 +1,4 @@
+import Mathlib.LinearAlgebra.FreeModule.PID
 import SphereEversion.ToMathlib.LinearAlgebra.Basis
 import SphereEversion.Loops.Exists
 import SphereEversion.Local.Corrugation

diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean
@@ -1,5 +1,5 @@
-import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
-import SphereEversion.ToMathlib.Topology.HausdorffDistance
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.SpecialFunctions.SmoothTransition
 import SphereEversion.Notations
 
 /-! # Spaces of 1-jets and their sections

diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean
@@ -153,8 +153,8 @@ theorem FamilyJetSec.uncurry_mem_relativize (S : FamilyJetSec E F P) {s : P} {x
     ((s, x), S.uncurry (s, x)) ∈ R.relativize P ↔ (x, S s x) ∈ R := by
   rw [RelLoc.relativize, mem_preimage, oneJetSnd_eq, JetSec.coe_apply,  JetSec.coe_apply, S.uncurry_f, S.uncurry_φ']
   dsimp only
-  suffices : ((D (fun z ↦ f S z x) s).comp (fst ℝ P E) + (φ S s x).comp (snd ℝ P E)).comp (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x
-  rw [this]; rfl
+  suffices ((D (fun z ↦ f S z x) s).comp (fst ℝ P E) + (φ S s x).comp (snd ℝ P E)).comp (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x by
+    rw [this]; rfl
   ext v
   simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',

diff --git a/SphereEversion/Local/Relation.lean b/SphereEversion/Local/Relation.lean
@@ -1,4 +1,3 @@
-import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 import Mathlib.Topology.MetricSpace.HausdorffDistance
 import SphereEversion.Local.OneJet
 

diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
@@ -218,7 +218,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank
       have eq₁ : dim (ℝ ∙ x)ᗮ = n := finrank_orthogonal_span_singleton x_ne
       have eq₂ : ker p.π ⊓ (ℝ ∙ x)ᗮ ⊓ span ℝ {v'} = (⊥ : Submodule ℝ E) := by
         erw [inf_left_right_swap, inf_comm, ← inf_assoc, p'.inf_eq_bot, bot_inf_eq]
-      have eq₃ : dim (span ℝ {v'}) = 1; apply finrank_span_singleton p'.v_ne_zero
+      have eq₃ : dim (span ℝ {v'}) = 1 := finrank_span_singleton p'.v_ne_zero
       rw [← hv', eq₁, eq₃, eq₂] at eq
       simpa only [finrank_bot] using eq.symm
     have : dim E = n + 1 := Fact.out

diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean
@@ -1,3 +1,4 @@
+import SphereEversion.Notations
 import SphereEversion.ToMathlib.Equivariant
 import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
 

diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
@@ -1,6 +1,8 @@
 import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 import Mathlib.MeasureTheory.Integral.Periodic
-import Mathlib.Analysis.Calculus.BumpFunction.Convolution
+import Mathlib.Analysis.Convolution
+import Mathlib.MeasureTheory.Measure.Haar.Unique
+import Mathlib.Analysis.Calculus.BumpFunction.Normed
 import SphereEversion.ToMathlib.Topology.Periodic
 import SphereEversion.ToMathlib.Analysis.ContDiff
 import SphereEversion.Loops.Basic

diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean
@@ -1,3 +1,4 @@
+import Mathlib.Analysis.Calculus.BumpFunction.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 import Mathlib.MeasureTheory.Integral.Periodic
 import SphereEversion.Loops.Surrounding

diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
@@ -1,4 +1,4 @@
-import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.InnerProductSpace.Calculus
 import Mathlib.Analysis.InnerProductSpace.Dual

diff --git a/SphereEversion/ToMathlib/Data/Nat/Basic.lean b/SphereEversion/ToMathlib/Data/Nat/Basic.lean
@@ -1,5 +1,5 @@
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Choose
 
 -- 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
@@ -1,4 +1,3 @@
-import SphereEversion.Notations
 import Mathlib.Topology.Algebra.Order.Floor
 import SphereEversion.ToMathlib.Topology.Misc
 

diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
@@ -5,9 +5,8 @@ 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.Pullback
-import Mathlib.Geometry.Manifold.VectorBundle.Hom
-import SphereEversion.ToMathlib.Geometry.Manifold.MiscManifold
+import Mathlib.Geometry.Manifold.VectorBundle.Basic
+import Mathlib.Topology.VectorBundle.Hom
 
 /-!
 # Various operations on and properties of smooth vector bundles

diff --git a/SphereEversion/ToMathlib/Logic/Basic.lean b/SphereEversion/ToMathlib/Logic/Basic.lean
@@ -1,5 +1,3 @@
-import Mathlib.Logic.Basic
-
 -- `by simp [forall_and]` works in Lean 4
 theorem forall₂_and_distrib {α β : Sort _} {p q : α → β → Prop} :
     (∀ x y, p x y ∧ q x y) ↔ (∀ x y, p x y) ∧ ∀ x y, q x y :=

diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
@@ -1,8 +1,6 @@
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import SphereEversion.ToMathlib.Analysis.Convex.Basic
 import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
-import Mathlib.Algebra.Algebra.Subalgebra.Order
-
 
 noncomputable section
 

diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean
@@ -1,7 +1,6 @@
 import Mathlib.Analysis.Matrix
 import Mathlib.LinearAlgebra.AffineSpace.Matrix
 import Mathlib.Analysis.NormedSpace.AddTorsorBases
-import SphereEversion.ToMathlib.Analysis.Calculus
 
 noncomputable section
 

diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -1,8 +1,6 @@
 import Mathlib.Topology.Connected.PathConnected
-import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.UniformSpace.Separation
 import Mathlib.LinearAlgebra.AffineSpace.Independent
-import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Topology.Algebra.Order.Floor
 import Mathlib.Topology.ShrinkingLemma
 import Mathlib.Topology.EMetricSpace.Paracompact

diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean
@@ -1,4 +1,4 @@
-import Mathlib.Topology.Compactness.Paracompact
+import Mathlib.Topology.Separation
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Nat.Interval
 

diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean
@@ -1,5 +1,5 @@
 import Mathlib.Topology.Connected.PathConnected
-import SphereEversion.ToMathlib.Topology.Misc
+import Mathlib.Analysis.Normed.Field.Basic
 
 open Set Function Int TopologicalSpace
 

diff --git a/SphereEversion/ToMathlib/Topology/Periodic.lean b/SphereEversion/ToMathlib/Topology/Periodic.lean
@@ -1,5 +1,5 @@
 import Mathlib.Algebra.Periodic
-import Mathlib.Analysis.NormedSpace.Basic
+import Mathlib.Analysis.Normed.Group.Basic
 import SphereEversion.ToMathlib.Topology.Separation
 
 /-!

diff --git a/noshake.json b/noshake.json
@@ -0,0 +1,6 @@
+{"ignoreImport": ["Init", "Lean", "SphereEversion.Notations"],
+ "ignore":
+ {"SphereEversion.ToMathlib.Data.Nat.Basic": ["Mathlib.Tactic.Choose"],
+  "SphereEversion.Notations": ["Mathlib.Analysis.Calculus.ContDiff.Basic"],
+  "SphereEversion.Local.Corrugation":
+  ["SphereEversion.ToMathlib.MeasureTheory.BorelSpace"]}}