Trigger CI for leanprover-community/batteries#813

.github/workflows/discover-lean-pr-testing.yml

@@ -102,13 +102,11 @@ jobs:
 
             # Check if the diff contains files other than the specified ones
             if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -e 'lean-toolchain'; then
-                # Extract the PR number and actual branch name
-                PR_NUMBER=$(echo "$BRANCH" | grep -oP '\d+$')
+                # Extract the actual branch name
                 ACTUAL_BRANCH=${BRANCH#origin/}
-                GITHUB_DIFF="https://github.com/leanprover-community/mathlib4/compare/nightly-testing...$ACTUAL_BRANCH"
 
                 # Append the branch details to RELEVANT_BRANCHES
-                RELEVANT_BRANCHES="$RELEVANT_BRANCHES"$'\n- '"$ACTUAL_BRANCH (lean4#$PR_NUMBER) ([diff with \`nightly-testing\`]($GITHUB_DIFF))"
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES""$ACTUAL_BRANCH"$' '
             fi
         done
 
@@ -133,7 +131,10 @@ jobs:
           printf $'```bash\n'
           for BRANCH in $BRANCHES; do
             PR_NUMBER=$(echo "$BRANCH" | grep -oP '\d+$')
+            GITHUB_DIFF="https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-$PR_NUMBER"
+            printf $'# Diff: %s\n' "$GITHUB_DIFF"
             printf $'scripts/merge-lean-testing-pr.sh %s   # %s\n' "$PR_NUMBER" "$BRANCH"
+            printf '\n'
           done
           printf $'```\n'
           printf "EOF"

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -61,7 +61,7 @@ condition needed to be a basis of a filter: moreover, the filter generated by th
 the condition for being a uniformity, and this is the uniformity we put on `ℕ`.
 
 For each `n`, the set `fundamentalEntourage n : Set (ℕ × ℕ)` consists of the `n+1` points
-`{(0,0),(1,1)...(n,n)}` on the diagonal; together with the half plane `{(x,y) | n ≤ x  ∧ n ≤ y}`
+`{(0,0),(1,1)...(n,n)}` on the diagonal; together with the half plane `{(x,y) | n ≤ x ∧ n ≤ y}`
 
 That this collection can be used as a filter basis is proven in the definition `counterBasis` and
 that the filter `counterBasis.filterBasis` is a uniformity is proven in the definition
@@ -98,7 +98,7 @@ noncomputable local instance : PseudoMetricSpace ℕ where
 lemma dist_def {n m : ℕ} : dist n m = |2 ^ (-n : ℤ) - 2 ^ (-m : ℤ)| := rfl
 
 lemma Int.eq_of_pow_sub_le {d : ℕ} {m n : ℤ} (hd1 : 1 < d)
-  (h : |(d : ℝ) ^ (-m) - d ^ (-n)| < d ^ (-n - 1)) : m = n := by
+    (h : |(d : ℝ) ^ (-m) - d ^ (-n)| < d ^ (-n - 1)) : m = n := by
   have hd0 : 0 < d := one_pos.trans hd1
   replace h : |(1 : ℝ) - d ^ (n - m)| < (d : ℝ)⁻¹ := by
     rw [← mul_lt_mul_iff_of_pos_left (a := (d : ℝ) ^ (-n)) (zpow_pos _ _),
@@ -114,17 +114,17 @@ lemma Int.eq_of_pow_sub_le {d : ℕ} {m n : ℤ} (hd1 : 1 < d)
     rw [ha, ← mul_lt_mul_iff_of_pos_left (a := (d : ℝ)) <| Nat.cast_pos'.mpr hd0,
       mul_inv_cancel₀ <| Nat.cast_ne_zero.mpr (ne_of_gt hd0),
       ← abs_of_nonneg (a := (d : ℝ)) <| Nat.cast_nonneg' d, ← abs_mul,
-      show |(d : ℝ) * (1 - |(d : ℝ)| ^ (a : ℤ))| = |(d : ℤ) * (1 - |(d : ℤ)| ^ a)| by
-      norm_cast, ← Int.cast_one (R := ℝ), Int.cast_lt, Int.abs_lt_one_iff, Int.mul_eq_zero,
+      show |(d : ℝ) * (1 - |(d : ℝ)| ^ (a : ℤ))| = |(d : ℤ) * (1 - |(d : ℤ)| ^ a)| by norm_cast,
+      ← Int.cast_one (R := ℝ), Int.cast_lt, Int.abs_lt_one_iff, Int.mul_eq_zero,
       sub_eq_zero, eq_comm (a := 1), pow_eq_one_iff_cases] at h
     simp only [Nat.cast_eq_zero, ne_of_gt hd0, Nat.abs_cast, Nat.cast_eq_one, ne_of_gt hd1,
       Int.reduceNeg, reduceCtorEq, false_and, or_self, or_false, false_or] at h
     rwa [h, Nat.cast_zero, sub_eq_zero, eq_comm] at ha
-  · have h1 : (d : ℝ) ^ (n - m) ≤ 1 - (d : ℝ)⁻¹ := by
-      calc (d : ℝ) ^ (n - m) ≤ (d : ℝ)⁻¹ := by
-            rw [← zpow_neg_one]
-            apply zpow_right_mono₀ <| Nat.one_le_cast.mpr hd0
-            linarith
+  · have h1 : (d : ℝ) ^ (n - m) ≤ 1 - (d : ℝ)⁻¹ := calc
+      (d : ℝ) ^ (n - m) ≤ (d : ℝ)⁻¹ := by
+        rw [← zpow_neg_one]
+        apply zpow_right_mono₀ <| Nat.one_le_cast.mpr hd0
+        linarith
       _ ≤ 1 - (d : ℝ)⁻¹ := by
         rw [inv_eq_one_div, one_sub_div <| Nat.cast_ne_zero.mpr (ne_of_gt hd0),
           div_le_div_iff_of_pos_right <| Nat.cast_pos'.mpr hd0, le_sub_iff_add_le]
@@ -149,15 +149,15 @@ theorem TopIsDiscrete : DiscreteTopology ℕ := by
 lemma idIsCauchy : CauchySeq (id : ℕ → ℕ) := by
   rw [Metric.cauchySeq_iff]
   refine fun ε ↦ Metric.cauchySeq_iff.mp
-    (@cauchySeq_of_le_geometric_two ℝ _ 1 (fun n ↦ 2 ^(-n : ℤ)) fun n ↦ ?_) ε
+    (@cauchySeq_of_le_geometric_two ℝ _ 1 (fun n ↦ 2 ^(-n : ℤ)) fun n ↦ le_of_eq ?_) ε
   simp only [zpow_natCast, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, one_div]
   rw [Real.dist_eq, zpow_add' <| Or.intro_left _ two_ne_zero]
-  calc |2 ^ (- n : ℤ) - 2 ^ (-1 : ℤ) * 2 ^ (- n : ℤ)| =
-        |(1 - (2 : ℝ)⁻¹) * 2 ^ (- n : ℤ)| := by rw [← one_sub_mul, zpow_neg_one]
-      _ = |2⁻¹ * 2 ^ (-(n : ℤ))| := by congr; rw [inv_eq_one_div 2, sub_half 1]
-      _ = 2⁻¹ / 2 ^ n := by rw [zpow_neg, abs_mul, abs_inv, abs_inv, inv_eq_one_div,
-          Nat.abs_ofNat, one_div, zpow_natCast, abs_pow, ← div_eq_mul_inv, Nat.abs_ofNat]
-  rfl
+  calc
+    |2 ^ (- n : ℤ) - 2 ^ (-1 : ℤ) * 2 ^ (- n : ℤ)|
+    _ = |(1 - (2 : ℝ)⁻¹) * 2 ^ (- n : ℤ)| := by rw [← one_sub_mul, zpow_neg_one]
+    _ = |2⁻¹ * 2 ^ (-(n : ℤ))| := by congr; rw [inv_eq_one_div 2, sub_half 1]
+    _ = 2⁻¹ / 2 ^ n := by rw [zpow_neg, abs_mul, abs_inv, abs_inv, inv_eq_one_div,
+        Nat.abs_ofNat, one_div, zpow_natCast, abs_pow, ← div_eq_mul_inv, Nat.abs_ofNat]
 
 end Metric
 
@@ -170,7 +170,7 @@ discrete. -/
 
 /-- The fundamental entourages (index by `n : ℕ`) used to construct a basis of the uniformity: for
 each `n`, the set `fundamentalEntourage n : Set (ℕ × ℕ)` consists of the `n+1` points
-`{(0,0),(1,1)...(n,n)}` on the diagonal; together with the half plane `{(x,y) | n ≤ x  ∧ n ≤ y}`-/
+`{(0,0),(1,1)...(n,n)}` on the diagonal; together with the half plane `{(x,y) | n ≤ x ∧ n ≤ y}`-/
 def fundamentalEntourage (n : ℕ) : Set (ℕ × ℕ) :=
   (⋃ i : Icc 0 n, {((i : ℕ), (i : ℕ))}) ∪ Set.Ici (n , n)
 
@@ -196,9 +196,9 @@ lemma mem_fundamentalEntourage (n : ℕ) (P : ℕ × ℕ) : P ∈ fundamentalEnt
       true_and, exists_prop', nonempty_prop, mem_Ici, fundamentalEntourage]
     rcases h with h | h
     · exact Or.inr h
-    · by_cases h_le : n ≤ P.1
-      · exact Or.inr ⟨h_le, h ▸ h_le⟩
-      · refine Or.inl ⟨P.1, ⟨le_of_lt <| not_le.mp h_le, congrArg _ h⟩⟩
+    · cases le_total n P.1 with
+      | inl h_le => exact Or.inr ⟨h_le, h ▸ h_le⟩
+      | inr h_le => exact Or.inl ⟨P.1, ⟨h_le, congrArg _ h⟩⟩
 
 /-- The collection `fundamentalEntourage` satisfies the axioms to be a basis for a filter on
  `ℕ × ℕ` and gives rise to a term in the relevant type.-/
@@ -262,10 +262,10 @@ def counterCoreUniformity : UniformSpace.Core ℕ := by
     aesop
 
 /--The topology on `ℕ` induced by the "crude" uniformity-/
-instance counterTopology: TopologicalSpace ℕ := counterCoreUniformity.toTopologicalSpace
+instance counterTopology : TopologicalSpace ℕ := counterCoreUniformity.toTopologicalSpace
 
 /-- The uniform structure on `ℕ` bundling together the "crude" uniformity and the topology-/
-instance counterUniformity: UniformSpace ℕ := UniformSpace.ofCore counterCoreUniformity
+instance counterUniformity : UniformSpace ℕ := UniformSpace.ofCore counterCoreUniformity
 
 lemma HasBasis_counterUniformity :
     (uniformity ℕ).HasBasis (fun _ ↦ True) fundamentalEntourage := by

Counterexamples/Phillips.lean

@@ -415,21 +415,17 @@ theorem continuousPart_evalCLM_eq_zero [TopologicalSpace α] [DiscreteTopology 
   calc
     f.continuousPart s = f.continuousPart (s \ {x}) :=
       (continuousPart_apply_diff _ _ _ (countable_singleton x)).symm
-    _ = f (univ \ f.discreteSupport ∩ (s \ {x})) := rfl
+    _ = f (univ \ f.discreteSupport ∩ (s \ {x})) := by simp [continuousPart]
     _ = indicator (univ \ f.discreteSupport ∩ (s \ {x})) 1 x := rfl
     _ = 0 := by simp
 
 theorem toFunctions_toMeasure [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] (s : Set α)
     (hs : MeasurableSet s) :
     μ.extensionToBoundedFunctions.toBoundedAdditiveMeasure s = (μ s).toReal := by
-  change
-    μ.extensionToBoundedFunctions
-        (ofNormedAddCommGroupDiscrete (indicator s 1) 1 (norm_indicator_le_one s)) =
-      (μ s).toReal
+  simp only [ContinuousLinearMap.toBoundedAdditiveMeasure]
   rw [extensionToBoundedFunctions_apply]
-  · change ∫ x, s.indicator (fun _ => (1 : ℝ)) x ∂μ = _
-    simp [integral_indicator hs]
-  · change Integrable (indicator s 1) μ
+  · simp [integral_indicator hs]
+  · simp only [coe_ofNormedAddCommGroupDiscrete]
     have : Integrable (fun _ => (1 : ℝ)) μ := integrable_const (1 : ℝ)
     apply
       this.mono' (Measurable.indicator (@measurable_const _ _ _ _ (1 : ℝ)) hs).aestronglyMeasurable

Counterexamples/SorgenfreyLine.lean

@@ -126,7 +126,7 @@ theorem exists_Ico_disjoint_closed {a : ℝₗ} {s : Set ℝₗ} (hs : IsClosed
 @[simp]
 theorem map_toReal_nhds (a : ℝₗ) : map toReal (𝓝 a) = 𝓝[≥] toReal a := by
   refine ((nhds_basis_Ico a).map _).eq_of_same_basis ?_
-  simpa only [toReal.image_eq_preimage] using nhdsWithin_Ici_basis_Ico (toReal a)
+  simpa only [toReal.image_eq_preimage] using nhdsGE_basis_Ico (toReal a)
 
 theorem nhds_eq_map (a : ℝₗ) : 𝓝 a = map toReal.symm (𝓝[≥] (toReal a)) := by
   simp_rw [← map_toReal_nhds, map_map, Function.comp_def, toReal.symm_apply_apply, map_id']