Remove now-superfluous open statements; fix one proof in Unused/.

leanprover-community · Jul 22, 2024 · a689675 · a689675
1 parent a0266b4
commit a689675
Show file tree

Hide file tree

Showing 12 changed files with 18 additions and 40 deletions.
diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean
@@ -11,7 +11,6 @@ import SphereEversion.Notations
 attribute [gcongr] nhdsSet_mono
 
 open Set Filter Function
-
 open scoped Topology unitInterval
 
 /-!
@@ -252,8 +251,6 @@ section Htpy
 
 private noncomputable def T : ℕ → ℝ := fun n ↦ Nat.rec 0 (fun k x ↦ x + 1 / (2 : ℝ) ^ (k + 1)) n
 
-open scoped BigOperators
-
 -- Note this is more painful than Patrick hoped for. Maybe this should be the definition of T.
 private theorem T_eq (n : ℕ) : T n = 1 - (1 / 2 : ℝ) ^ n := by
   unfold T

diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
@@ -29,9 +29,8 @@ convolutions.
 
 noncomputable section
 
-open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap Filter
-
-open scoped Topology BigOperators Filter Convolution
+open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap
+open scoped Topology Filter Convolution
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
   [MeasurableSpace F] [BorelSpace F]

diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean
@@ -48,8 +48,7 @@ existence of delta mollifiers, partitions of unity, and the inverse function the
 noncomputable section
 
 open Set Function MeasureTheory intervalIntegral Filter
-
-open scoped Topology unitInterval Manifold BigOperators
+open scoped Topology Manifold
 
 variable {E F : Type*}
   [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]

diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
@@ -32,14 +32,9 @@ The key results are:
  * `exists_surrounding_loops`
 -/
 
-
--- to obtain that normed spaces are locally connected
--- to obtain that normed spaces are locally connected
 -- to obtain that normed spaces are locally connected
--- to obtain that normed spaces are locally connected
-open Set Function FiniteDimensional Int Prod Function Path Filter TopologicalSpace
-
-open scoped Classical Topology unitInterval BigOperators
+open Set Function FiniteDimensional Int Prod Path Filter
+open scoped Topology unitInterval
 
 namespace IsPathConnected
 

diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
@@ -8,7 +8,6 @@ import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm
 noncomputable section
 
 open scoped Topology Filter
-
 open Function
 
 section
@@ -288,8 +287,6 @@ end Arithmetic
 
 section
 
-open scoped BigOperators
-
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 

diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -2,11 +2,9 @@ import Mathlib.Analysis.Convex.Combination
 import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Order.Hom.Ring
 
-open scoped BigOperators
-
 open Function Set
 
--- move
+-- TODO: move this lemma and the following one
 theorem map_finsum {β α γ : Type*} [AddCommMonoid β] [AddCommMonoid γ] {G : Type*}
     [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) {f : α → β} (hf : (Function.support f).Finite) :
     g (∑ᶠ i, f i) = ∑ᶠ i, g (f i) :=
@@ -17,7 +15,6 @@ theorem finprod_eq_prod_of_mulSupport_subset_of_finite {α M} [CommMonoid M] (f
     (h : mulSupport f ⊆ s) (hs : s.Finite) : ∏ᶠ i, f i = ∏ i in hs.toFinset, f i := by
   apply finprod_eq_prod_of_mulSupport_subset f; rwa [Set.Finite.coe_toFinset]
 
--- end move
 section
 
 variable {𝕜 𝕜' : Type*} {E : Type*} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E]

diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean
@@ -2,7 +2,7 @@ import SphereEversion.ToMathlib.Partition
 
 noncomputable section
 
-open scoped Topology Filter Manifold BigOperators
+open scoped Topology Manifold
 
 open Set Function Filter
 

diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
@@ -21,7 +21,7 @@ noncomputable section
 
 open Filter Set
 
-open scoped Manifold Topology BigOperators
+open scoped Manifold Topology
 
 -- FIXME: move to `Manifold/Algebra/SmoothFunctions`, around line 46
 section

diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
@@ -4,8 +4,7 @@ import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
 
 noncomputable section
 
-open scoped Topology Filter BigOperators
-
+open scoped Topology
 open Set Function Filter
 
 variable {ι : Type*}

diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean
@@ -1,9 +1,5 @@
 import Mathlib.Topology.Algebra.Module.Basic
 
-open Filter ContinuousLinearMap Function
-
-open scoped Topology BigOperators Filter
-
 namespace ContinuousLinearMap
 
 variable {R₁ M₁ M₂ M₃ : Type*} [Semiring R₁]

diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean
@@ -1,9 +1,9 @@
 import Mathlib.Topology.Connected.PathConnected
 import Mathlib.Analysis.Normed.Field.Basic
 
-open Set Function Int TopologicalSpace
+open Set Function
 
-open scoped BigOperators Topology unitInterval
+open scoped Topology unitInterval
 
 noncomputable section
 

diff --git a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean
@@ -3,9 +3,7 @@ import Mathlib.MeasureTheory.Integral.Periodic
 
 noncomputable section
 
-open TopologicalSpace MeasureTheory Filter FirstCountableTopology Metric Set Function
-
-open scoped Topology Filter NNReal BigOperators Interval
+open MeasureTheory Set
 
 section
 
@@ -47,7 +45,7 @@ theorem integral_mono_of_le {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} (
     (hfg : f ≤ᵐ[μ.restrict (Ι a b)] g) : ∫ u in a..b, f u ∂μ ≤ ∫ u in a..b, g u ∂μ := by
   rw [uIoc_of_le hab] at hfg
   let H := hfg.filter_mono (ae_mono le_rfl)
-  simpa only [integral_of_le hab] using set_integral_mono_ae_restrict hf.1 hg.1 H
+  simpa only [integral_of_le hab] using setIntegral_mono_ae_restrict hf.1 hg.1 H
 
 theorem integral_mono_of_le_of_nonneg {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} (hab : a ≤ b)
     (hf : AEStronglyMeasurable f <| μ.restrict (Ι a b))
@@ -62,12 +60,13 @@ theorem integral_antimono_of_le {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure
     (hfg : f ≤ᵐ[μ.restrict (Ι a b)] g) : ∫ u in a..b, g u ∂μ ≤ ∫ u in a..b, f u ∂μ := by
   cases' hab.eq_or_lt with hab hab
   · simp [hab]
-  · rw [uIoc_of_lt hab] at hfg
-    rw [integral_symm b a]
-    rw [integral_symm b a]
+  · rw [uIoc_of_ge hab.le] at hfg
+    rw [integral_symm b a, integral_symm b a]
     apply neg_le_neg
     apply integral_mono_of_le hab.le hf.symm hg.symm
-    rwa [uIoc_swap, uIoc_of_lt hab]
+    have : Ioc b a = uIoc b a := by rw [uIoc_of_le hab.le]
+    rw [← this]
+    exact hfg
 
 theorem integral_antimono_of_le_of_nonneg {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} (hab : b ≤ a)
     (hf : AEStronglyMeasurable f <| μ.restrict (Ι a b))