Trigger CI for leanprover/lean4#2722

.github/workflows/bors.yml

@@ -179,7 +179,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build.yml

@@ -185,7 +185,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build.yml.in

@@ -165,7 +165,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build_fork.yml

@@ -183,7 +183,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/nightly_detect_failure.yml

@@ -23,3 +23,24 @@ jobs:
         topic: 'CI failure on the nightly-testing branch'
         content: |
           The latest CI for branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+
+  handle_success:
+    if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v2
+      with:
+        ref: nightly-testing # checkout nightly-testing branch
+        token: ${{ secrets.NIGHTLY_TESTING }}
+    - name: Update the nightly-testing-YYYY-MM-DD branch
+      run: |
+        toolchain=$(<lean-toolchain)
+        if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
+          version=${BASH_REMATCH[1]}
+          git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
+        else
+          echo "Error: The file lean-toolchain does not contain the expected pattern."
+          exit 1
+        fi

Counterexamples/Phillips.lean

@@ -571,7 +571,7 @@ theorem countable_ne (Hcont : #ℝ = aleph 1) (φ : (DiscreteCopy ℝ →ᵇ ℝ
       {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} := by
     intro x hx
     contrapose! hx
-    simp only [Classical.not_not, mem_setOf_eq] at hx
+    simp only [Classical.not_not, mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
     simp [apply_f_eq_continuousPart Hcont φ x hx]
   have B :
     {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} ⊆

Mathlib.lean

@@ -2122,6 +2122,7 @@ import Mathlib.GroupTheory.Perm.Subgroup
 import Mathlib.GroupTheory.Perm.Support
 import Mathlib.GroupTheory.Perm.ViaEmbedding
 import Mathlib.GroupTheory.PresentedGroup
+import Mathlib.GroupTheory.PushoutI
 import Mathlib.GroupTheory.QuotientGroup
 import Mathlib.GroupTheory.Schreier
 import Mathlib.GroupTheory.SchurZassenhaus
@@ -3239,6 +3240,7 @@ import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
+import Mathlib.Tactic.RewriteSearch
 import Mathlib.Tactic.Rewrites
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic

Mathlib/Algebra/Group/TypeTags.lean

@@ -132,6 +132,10 @@ instance [h: Infinite α] : Infinite (Additive α) := h
 
 instance [h: Infinite α] : Infinite (Multiplicative α) := h
 
+instance [h : DecidableEq α] : DecidableEq (Multiplicative α) := h
+
+instance [h : DecidableEq α] : DecidableEq (Additive α) := h
+
 instance instNontrivialAdditive [Nontrivial α] : Nontrivial (Additive α) :=
   ofMul.injective.nontrivial
 #align additive.nontrivial instNontrivialAdditive

Mathlib/Algebra/Order/CompleteField.lean

@@ -156,7 +156,7 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b :=
       exact_mod_cast sub_lt_comm.mp hq₁q
   · rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩
     -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-    refine' ⟨qa + qb, _, by dsimp; norm_cast⟩
+    refine' ⟨qa + qb, _, by beta_reduce; norm_cast⟩
     rw [mem_setOf_eq, cast_add]
     exact add_lt_add ha hb
 #align linear_ordered_field.cut_map_add LinearOrderedField.cutMap_add

Mathlib/Algebra/Support.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Pi
 import Mathlib.Algebra.Module.Basic
 import Mathlib.GroupTheory.GroupAction.Pi
+import Mathlib.Order.Cover
 
 #align_import algebra.support from "leanprover-community/mathlib"@"29cb56a7b35f72758b05a30490e1f10bd62c35c1"
 
@@ -124,6 +125,12 @@ theorem range_subset_insert_image_mulSupport (f : α → M) :
 #align function.range_subset_insert_image_mul_support Function.range_subset_insert_image_mulSupport
 #align function.range_subset_insert_image_support Function.range_subset_insert_image_support
 
+@[to_additive]
+lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mulSupport f ⊆ k) :
+    range f = f '' k ∨ range f = insert 1 (f '' k) := by
+  apply (wcovby_insert _ _).eq_or_eq (image_subset_range _ _)
+  exact (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_subset f h))
+
 @[to_additive (attr := simp)]
 theorem mulSupport_one' : mulSupport (1 : α → M) = ∅ :=
   mulSupport_eq_empty_iff.2 rfl

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -298,7 +298,7 @@ theorem zeroLocus_empty_iff_eq_top {I : Ideal R} : zeroLocus (I : Set R) = ∅ 
   · contrapose!
     intro h
     rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩
-    exact Set.Nonempty.ne_empty ⟨⟨M, hM.isPrime⟩, hIM⟩
+    exact ⟨⟨M, hM.isPrime⟩, hIM⟩
   · rintro rfl
     apply zeroLocus_empty_of_one_mem
     trivial

Mathlib/Analysis/Analytic/Composition.lean

@@ -1045,7 +1045,6 @@ theorem blocksFun_sigmaCompositionAux (a : Composition n) (b : Composition a.len
     rw [get_of_eq (get_splitWrtComposition _ _ _), get_drop', get_take']; rfl
 #align composition.blocks_fun_sigma_composition_aux Composition.blocksFun_sigmaCompositionAux
 
-set_option linter.deprecated false in
 /-- Auxiliary lemma to prove that the composition of formal multilinear series is associative.
 
 Consider a composition `a` of `n` and a composition `b` of `a.length`. Grouping together some
@@ -1076,7 +1075,7 @@ theorem sizeUpTo_sizeUpTo_add (a : Composition n) (b : Composition a.length) {i
           take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
         rw [take_take, min_eq_left]
         apply monotone_sum_take _ (Nat.le_succ _)
-      rw [this, nthLe_map', nthLe, get_splitWrtComposition, ←
+      rw [this, get_map, get_splitWrtComposition, ←
         take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
         sum_append]
       congr

Mathlib/Analysis/Convex/StoneSeparation.lean

@@ -107,6 +107,6 @@ theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜
       hCmax _ ⟨convex_convexHull _ _, h⟩ ((subset_insert _ _).trans <| subset_convexHull _ _)] at hc
     exact hc (subset_convexHull _ _ <| mem_insert _ _)
   rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]
-  refine' disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inf_le.mpr fun b hb => h a _ ⟨b, hb⟩
+  refine disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inter_eq_empty.2 (h a ?_)
   rwa [← hC.1.convexHull_eq]
 #align exists_convex_convex_compl_subset exists_convex_convex_compl_subset

Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

@@ -234,7 +234,7 @@ protected theorem IsClosed.balancedCore (hU : IsClosed U) : IsClosed (balancedCo
     exact isClosedMap_smul_of_ne_zero ha' U hU
   · have : balancedCore 𝕜 U = ∅ := by
       contrapose! h
-      exact balancedCore_nonempty_iff.mp (Set.nonempty_iff_ne_empty.2 h)
+      exact balancedCore_nonempty_iff.mp h
     rw [this]
     exact isClosed_empty
 #align is_closed.balanced_core IsClosed.balancedCore

Mathlib/Analysis/MeanInequalities.lean

@@ -610,7 +610,7 @@ theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjugateExponent q) (hf :
   lift f to ι → ℝ≥0 using hf
   lift g to ι → ℝ≥0 using hg
   -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-  dsimp at *
+  beta_reduce at *
   norm_cast at *
   exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum
 #align real.inner_le_Lp_mul_Lq_tsum_of_nonneg Real.inner_le_Lp_mul_Lq_tsum_of_nonneg
@@ -640,7 +640,7 @@ theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.IsConjugateExponent q) {A B
   lift A to ℝ≥0 using hA
   lift B to ℝ≥0 using hB
   -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-  dsimp at *
+  beta_reduce at *
   norm_cast at hf_sum hg_sum
   obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
   refine' ⟨C, C.prop, hC, _⟩
@@ -679,7 +679,7 @@ theorem Lp_add_le_tsum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : 
   lift f to ι → ℝ≥0 using hf
   lift g to ι → ℝ≥0 using hg
   -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-  dsimp at *
+  beta_reduce at *
   norm_cast0 at *
   exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum
 #align real.Lp_add_le_tsum_of_nonneg Real.Lp_add_le_tsum_of_nonneg
@@ -709,12 +709,12 @@ theorem Lp_add_le_hasSum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg :
   lift A to ℝ≥0 using hA
   lift B to ℝ≥0 using hB
   -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-  dsimp at hfA hgB
+  beta_reduce at hfA hgB
   norm_cast at hfA hgB
   obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
   use C
   -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
-  dsimp
+  beta_reduce
   norm_cast
   exact ⟨zero_le _, hC₁, hC₂⟩
 #align real.Lp_add_le_has_sum_of_nonneg Real.Lp_add_le_hasSum_of_nonneg

Mathlib/CategoryTheory/Extensive.lean

@@ -77,7 +77,7 @@ class PreservesPullbacksOfInclusions {C : Type*} [Category C] {D : Type*} [Categ
 attribute [instance] PreservesPullbacksOfInclusions.preservesPullbackInl
 
 /-- A category is (finitary) pre-extensive if it has finite coproducts,
-and binary coproducts are van Kampen. -/
+and binary coproducts are universal. -/
 class FinitaryPreExtensive (C : Type u) [Category.{v} C] : Prop where
   [hasFiniteCoproducts : HasFiniteCoproducts C]
   [HasPullbacksOfInclusions : HasPullbacksOfInclusions C]

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -184,8 +184,6 @@ theorem fac (x : J) : lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x := by
   simp [lift, ← Functor.map_comp]
 #align category_theory.preserves_finite_limits_of_flat.fac CategoryTheory.PreservesFiniteLimitsOfFlat.fac
 
-attribute [local simp] eqToHom_map
-
 theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     (f₁ f₂ : s.pt ⟶ F.obj c.pt) (h₁ : ∀ j : J, f₁ ≫ (F.mapCone c).π.app j = s.π.app j)
     (h₂ : ∀ j : J, f₂ ≫ (F.mapCone c).π.app j = s.π.app j) : f₁ = f₂ := by
@@ -208,7 +206,7 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     intro j
     injection c₀.π.naturality (BiconeHom.left j) with _ e₁
     injection c₀.π.naturality (BiconeHom.right j) with _ e₂
-    simpa using e₁.symm.trans e₂
+    convert e₁.symm.trans e₂ <;> simp
   have : c.extend g₁.right = c.extend g₂.right := by
     unfold Cone.extend
     congr 1