chore: minimize more imports

- InteractiveExpr doesn't exist; remove that commented import.
- Remove two duplicate lines (presumably from a merge conflict).
- Minimize open's in InductiveConstruction.

SphereEversion/Global/Immersion.lean

@@ -4,9 +4,6 @@ import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
 import SphereEversion.Global.Gromov
 import SphereEversion.Global.TwistOneJetSec
 
--- import interactive_expr
--- import interactive_expr
--- set_option trace.filter_inst_type true
 -- set_option trace.filter_inst_type true
 noncomputable section
 

SphereEversion/Global/OneJetBundle.lean

@@ -11,7 +11,6 @@ import Mathlib.Analysis.NormedSpace.Completion
 import Mathlib.Geometry.Manifold.Algebra.Monoid
 import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
--- import SphereEversion.InteractiveExpr
 
 /-!
 # 1-jet bundles

SphereEversion/Global/SmoothEmbedding.lean

@@ -1,15 +1,12 @@
-import Mathlib.Topology.MetricSpace.HausdorffDistance
-import Mathlib.Topology.NhdsSet
-import Mathlib.Topology.UniformSpace.Separation
-import Mathlib.Geometry.Manifold.ChartedSpace
-import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
-import SphereEversion.Notations
 import SphereEversion.Indexing
-import SphereEversion.ToMathlib.Topology.Paracompact
-import SphereEversion.ToMathlib.Topology.Algebra.Order.Compact
-import SphereEversion.ToMathlib.Topology.Misc
-import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners
+import SphereEversion.Notations
 import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
+import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners
+import SphereEversion.ToMathlib.Topology.Misc
+import SphereEversion.ToMathlib.Topology.Paracompact
+import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
+import Mathlib.Order.Filter.Basic
+
 
 noncomputable section
 

SphereEversion/InductiveConstructions.lean

@@ -1,16 +1,13 @@
-import SphereEversion.ToMathlib.Data.Set.Prod
-import SphereEversion.ToMathlib.Data.Set.Lattice
 import SphereEversion.ToMathlib.Topology.Germ
 import SphereEversion.ToMathlib.Topology.Misc
-import SphereEversion.ToMathlib.Order.Filter.Basic
+import SphereEversion.ToMathlib.Data.Set.Lattice
 import SphereEversion.Indexing
 import SphereEversion.Notations
--- import SphereEversion.InteractiveExpr
 -- import Mathlib.Tactic.Induction
 
 -- set_option trace.filter_inst_type true
 
-open Set Filter Prod TopologicalSpace Function
+open Set Filter Function
 
 open scoped Topology unitInterval