Doc tweaks; comment lemmas in Analysis/CutOff.

Not sure if the bundling is really needed; the core can go into mathlib.

SphereEversion/ToMathlib/Analysis/CutOff.lean

@@ -1,40 +1,43 @@
 import Mathlib.Geometry.Manifold.PartitionOfUnity
-import Mathlib.Topology.EMetricSpace.Paracompact
-import Mathlib.Topology.NhdsSet
 
+/-! results about smooth cut-off functions: move to PartitionOfUnity -/
 open Set Filter
 
 open scoped Manifold Topology
 
-theorem exists_contDiff_zero_one {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
+-- this is basically `exists_smooth_zero_one_of_closed` applied to the normed space E
+-- only difference is that one has bundled maps, and this is unbundled
+-- unsure if that's worth a lemma; shouldn't need specialisation to normed spaces...
+theorem exists_contDiff_zero_one {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {s t : Set E} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
-    ∃ f : E → ℝ, ContDiff ℝ ⊤ f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
+    ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
   let ⟨f, hfs, hft, hf01⟩ := exists_smooth_zero_one_of_closed 𝓘(ℝ, E) hs ht hd
   ⟨f, f.smooth.contDiff, hfs, hft, hf01⟩
 
-theorem exists_contDiff_zero_one_nhds {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
+-- variant of the above: with f being 0 resp 1 in nhds of s and t
+-- add! this version of exists_smooth_zero_one_of_closed to mathlib!
+theorem exists_contDiff_zero_one_nhds {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {s t : Set E} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
-    ∃ f : E → ℝ, ContDiff ℝ ⊤ f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ x in 𝓝ˢ t, f x = 1) ∧
+    ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ x in 𝓝ˢ t, f x = 1) ∧
       ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
-  rcases normal_exists_closure_subset hs ht.isOpen_compl
-      (subset_compl_iff_disjoint_left.mpr hd.symm)
-    with ⟨u, u_op, hsu, hut⟩
-  have hcu : IsClosed (closure u) := isClosed_closure
-  rcases normal_exists_closure_subset ht hcu.isOpen_compl (subset_compl_comm.mp hut) with
-    ⟨v, v_op, htv, hvu⟩
-  have hcv : IsClosed (closure v) := isClosed_closure
-  rcases exists_contDiff_zero_one hcu hcv (subset_compl_iff_disjoint_left.mp hvu) with
-    ⟨f, hfsmooth, hfu, hfv, hf⟩
-  refine' ⟨f, hfsmooth, _, _, hf⟩
-  apply eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu
-  apply eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv
+  obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl
+    (subset_compl_iff_disjoint_left.mpr hd.symm)
+  obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
+    (subset_compl_comm.mp hut)
+  obtain ⟨f, hfsmooth, hfu, hfv, hf⟩ := exists_contDiff_zero_one isClosed_closure isClosed_closure
+    (subset_compl_iff_disjoint_left.mp hvu)
+  refine ⟨f, hfsmooth, ?_, ?_, hf⟩
+  · exact eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu
+  · exact eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv
 
-theorem exists_contDiff_one_nhds_of_interior {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
+-- given s,t with s ⊆ interior t, construct a cutoff function f : E → [0,1] with
+-- f = 1 in a nhds of s and supp f ⊆ t
+-- generalise to manifolds, then upstream to PartitionOfUnity (maybe split those out)
+theorem exists_contDiff_one_nhds_of_interior {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {s t : Set E} (hs : IsClosed s) (hd : s ⊆ interior t) :
-    ∃ f : E → ℝ, ContDiff ℝ ⊤ f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x, x ∉ t → f x = 0) ∧
+    ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x, x ∉ t → f x = 0) ∧
       ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
-  have : IsClosed (interior t)ᶜ := isOpen_interior.isClosed_compl
-  rcases exists_contDiff_zero_one_nhds this hs
+  rcases exists_contDiff_zero_one_nhds isOpen_interior.isClosed_compl hs
     (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) with ⟨f, hfsmooth, h0, h1, hf⟩
   refine ⟨f, hfsmooth, h1, fun x hx ↦ ?_, hf⟩
   exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

SphereEversion/ToMathlib/Topology/Algebra/Order/Compact.lean

@@ -1,8 +1,8 @@
 import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.Instances.Real
 
-/-- A variant of `is_compact.exists_forall_le` for real-valued functions that does not require the
-assumption `s.nonempty`. -/
+/-- A variant of `IsCompact.exists_forall_le` for real-valued functions that does not require the
+assumption `s.Nonempty`. -/
 theorem IsCompact.exists_forall_le' {β : Type _} [TopologicalSpace β] {s : Set β} (hs : IsCompact s)
     {f : β → ℝ} (hf : ContinuousOn f s) {a : ℝ} (hf' : ∀ b ∈ s, a < f b) :
     ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b := by