chore(Topology/{Paracompact + PartitionOfUnity + Algebra/Order/Compac…

…t}): restore a more faithful mathported proof, using the "newer" `push_neg` (#5132)

These are just three cases where a mathported proof had to be changed, due to unwanted behaviour with `push_neg/contradiction`.  Since #5082 is supposed to fix some issues with these tactics, some of these workarounds can be removed.

Note: this was not in any way systematic, I simply `grep`ped the line after a `contra`, then `grep`ped for a `not` and then selected 3 likely candidates.  There are potentially more situations like these.

Mathlib/Topology/Algebra/Order/Compact.lean

@@ -71,41 +71,56 @@ instance (priority := 100) ConditionallyCompleteLinearOrder.toCompactIccSpace (
     [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] :
     CompactIccSpace α := by
   refine' .mk'' fun {a b} hlt => ?_
+  cases' le_or_lt a b with hab hab
+  swap
+  · simp [hab]
   refine' isCompact_iff_ultrafilter_le_nhds.2 fun f hf => _
-  by_contra H
-  simp only [not_exists, not_and] at H -- porting note: `contrapose!` fails
-  rw [le_principal_iff] at hf
+  contrapose! hf
+  rw [le_principal_iff]
   have hpt : ∀ x ∈ Icc a b, {x} ∉ f := fun x hx hxf =>
-    H x hx ((le_pure_iff.2 hxf).trans (pure_le_nhds x))
+    hf x hx ((le_pure_iff.2 hxf).trans (pure_le_nhds x))
   set s := { x ∈ Icc a b | Icc a x ∉ f }
   have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
-  have ha : a ∈ s := by simp [hpt, hlt.le]
+  have sbd : BddAbove s := ⟨b, hsb⟩
+  have ha : a ∈ s := by simp [hpt, hab]
+  rcases hab.eq_or_lt with (rfl | _hlt)
+  · exact ha.2
+  -- porting note: the `obtain` below was instead
+  -- `set c := Sup s`
+  -- `have hsc : IsLUB s c := isLUB_csSup ⟨a, ha⟩ sbd`
   obtain ⟨c, hsc⟩ : ∃ c, IsLUB s c := ⟨sSup s, isLUB_csSup ⟨a, ha⟩ ⟨b, hsb⟩⟩
   have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
-  specialize H c hc
+  specialize hf c hc
   have hcs : c ∈ s := by
-    rcases hc.1.eq_or_lt with (rfl | hlt)
-    · assumption
-    refine' ⟨hc, fun hcf => H fun U hU => _⟩
-    rcases exists_Ioc_subset_of_mem_nhds' hU hlt with ⟨x, hxc, hxU⟩
-    rcases ((hsc.frequently_mem ⟨a, ha⟩).and_eventually (Ioc_mem_nhdsWithin_Iic' hxc.2)).exists with
-      ⟨y, ⟨-, hyf⟩, hy⟩
+    cases' hc.1.eq_or_lt with heq hlt
+    · rwa [← heq]
+    refine' ⟨hc, fun hcf => hf fun U hU => _⟩
+    rcases(mem_nhdsWithin_Iic_iff_exists_Ioc_subset' hlt).1 (mem_nhdsWithin_of_mem_nhds hU) with
+      ⟨x, hxc, hxU⟩
+    rcases((hsc.frequently_mem ⟨a, ha⟩).and_eventually
+          (Ioc_mem_nhdsWithin_Iic ⟨hxc, le_rfl⟩)).exists with
+      ⟨y, ⟨_hyab, hyf⟩, hy⟩
     refine' mem_of_superset (f.diff_mem_iff.2 ⟨hcf, hyf⟩) (Subset.trans _ hxU)
     rw [diff_subset_iff]
-    exact Icc_subset_Icc_union_Ioc.trans (union_subset_union_right _ (Ioc_subset_Ioc_left hy.1.le))
+    exact
+      Subset.trans Icc_subset_Icc_union_Ioc
+        (union_subset_union Subset.rfl <| Ioc_subset_Ioc_left hy.1.le)
   cases' hc.2.eq_or_lt with heq hlt
-  · exact hcs.2 (heq.symm ▸ hf)
-  obtain ⟨y, ⟨hcy, hyb⟩, hyf⟩ : ∃ y ∈ Ioc c b, Ico c y ∉ f
-  · contrapose! H
-    intro U hU
-    rcases exists_Ico_subset_of_mem_nhds' hU hlt with ⟨y, hy, hyU⟩
-    exact mem_of_superset (H _ hy) hyU
-  suffices : y ∈ s
-  · exact hcy.not_le (hsc.1 this)
-  have hy : y ∈ Icc a b := ⟨hc.1.trans hcy.le, hyb⟩
-  refine ⟨hy, fun hay => ?_⟩
-  simp only [← Icc_union_Icc_eq_Icc hc.1 hcy.le, ← Ico_union_right hcy.le,
-    Ultrafilter.union_mem_iff, hyf, hcs.2, hpt _ hy, false_or] at hay
+  · rw [← heq]
+    exact hcs.2
+  contrapose! hf
+  intro U hU
+  rcases(mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1
+      (mem_nhdsWithin_of_mem_nhds hU) with
+    ⟨y, hxy, hyU⟩
+  refine' mem_of_superset _ hyU
+  clear! U
+  have hy : y ∈ Icc a b := ⟨hc.1.trans hxy.1.le, hxy.2⟩
+  by_cases hay : Icc a y ∈ f
+  · refine' mem_of_superset (f.diff_mem_iff.2 ⟨f.diff_mem_iff.2 ⟨hay, hcs.2⟩, hpt y hy⟩) _
+    rw [diff_subset_iff, union_comm, Ico_union_right hxy.1.le, diff_subset_iff]
+    exact Icc_subset_Icc_union_Icc
+  · exact ((hsc.1 ⟨hy, hay⟩).not_lt hxy.1).elim
 #align conditionally_complete_linear_order.to_compact_Icc_space ConditionallyCompleteLinearOrder.toCompactIccSpace
 
 instance {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]

Mathlib/Topology/Paracompact.lean

@@ -245,10 +245,8 @@ theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set [LocallyComp
       rintro ⟨x, hxB : x ∈ B c (r k c), hxK⟩
       refine' ⟨k, _, ⟨c, hc⟩, rfl⟩
       have := (mem_compl_iff _ _).1 (hr k c hxB)
-      revert this
-      contrapose!
-      simp only [ge_iff_le, not_le]
-      exact fun hnk ↦ K.subset hnk (interior_subset hxK)
+      contrapose! this with hnk
+      exact K.subset hnk (interior_subset hxK)
 #align refinement_of_locally_compact_sigma_compact_of_nhds_basis_set refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
 
 /-- Let `X` be a locally compact sigma compact Hausdorff topological space. Suppose that for each

Mathlib/Topology/PartitionOfUnity.lean

@@ -161,7 +161,6 @@ that `0 < f i x`. -/
 theorem exists_pos {x : X} (hx : x ∈ s) : ∃ i, 0 < f i x := by
   have H := f.sum_eq_one hx
   contrapose! H
-  simp_rw [not_exists, not_lt] at H
   simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one
 #align partition_of_unity.exists_pos PartitionOfUnity.exists_pos