merge bump/nightly-2026-05-03

kim-em · kim-em · commit 00b2942688a5 · 2026-05-05T09:16:36.000+10:00
diff --git a/.github/actions/get-mathlib-ci/action.yml b/.github/actions/get-mathlib-ci/action.yml
@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: d7b053bde8ef240c29f6724fa285dc5bb6bbe00a
+    default: 0efe1f98dd7e3b632b596b0360dd01cb7f4bc4c7
   path:
     description: Checkout destination path.
     required: false
diff --git a/.github/workflows/olean_report.yaml b/.github/workflows/olean_report.yaml
@@ -69,11 +69,12 @@ jobs:
         run: |
           pr_json=$(gh pr view "${{ github.event.issue.number }}" \
             --repo "${{ github.repository }}" \
-            --json headRefOid,baseRefOid,baseRefName)
+            --json headRefOid,baseRefOid,baseRefName,headRepository)
           {
             echo "head_sha=$(echo "$pr_json" | jq -r '.headRefOid')"
             echo "base_sha=$(echo "$pr_json" | jq -r '.baseRefOid')"
             echo "base_ref=$(echo "$pr_json" | jq -r '.baseRefName')"
+            echo "head_repo=$(echo "$pr_json" | jq -r '.headRepository.nameWithOwner')"
           } >> "$GITHUB_OUTPUT"
 
       # Using refs/pull/N/head works for both same-repo and fork PRs, since
@@ -175,6 +176,9 @@ jobs:
         run: |
           cd pr-branch
           lake env "$CACHE_BIN" get
+          # Run again with --repo in case this is a fork PR: fork PRs upload
+          # their oleans to the fork's Azure container, not the upstream one.
+          lake env "$CACHE_BIN" --repo="${{ steps.pr_info.outputs.head_repo }}" get
 
       - name: Check PR head oleans
         id: pr_oleans_check
diff --git a/Mathlib/Algebra/Category/Grp/Colimits.lean b/Mathlib/Algebra/Category/Grp/Colimits.lean
@@ -149,7 +149,7 @@ lemma quotUliftToQuot_ι [DecidableEq J] (j : J) (x : (F ⋙ uliftFunctor.{u'}).
   dsimp [quotUliftToQuot, Quot.ι]
   conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
     (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']
-  simp only [ DFinsupp.singleAddHom_apply,
+  simp only [DFinsupp.singleAddHom_apply,
     DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp, Function.comp_apply]
   rfl
 
diff --git a/Mathlib/Algebra/Category/ModuleCat/Stalk.lean b/Mathlib/Algebra/Category/ModuleCat/Stalk.lean
@@ -58,11 +58,7 @@ def colimit.smul (r : (R ⋙ forget _).ColimitType) (m : (M ⋙ forget _).Colimi
     refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
     simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]
 
-#adaptation_note /-- As of nightly-2026-02-10, we need to increase the maxHeartbeats limits here,
-and as of nightly-2026-02-23, we also need `backward.whnf.reducibleClassField`
-to avoid needing even more. (The maxHeartbeats limit was also bumped up a little 2026-03-22 because
-the meaning of maxHeartbeats changed -- level metavariables started allocating some more memory in
-general.) -/
+#adaptation_note /-- As of nightly-2026-02-10, we need to increase the maxHeartbeats limits here. -/
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 set_option maxHeartbeats 700000 in --
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
@@ -129,7 +129,6 @@ def Hσ (q : ℕ) : K[X] ⟶ K[X] :=
 def homotopyHσToZero (q : ℕ) : Homotopy (Hσ q : K[X] ⟶ K[X]) 0 :=
   nullHomotopy' (hσ' q)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- In degree `0`, the null homotopic map `Hσ` is zero. -/
 theorem Hσ_eq_zero (q : ℕ) : (Hσ q : K[X] ⟶ K[X]).f 0 = 0 := by
   unfold Hσ
diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -1270,7 +1270,7 @@ def uliftFunctorInclusion (S : Sieve X) :
 @[simps]
 def toUliftFunctor (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S f) :
     uliftYoneda.{w}.obj Y ⟶ Sieve.uliftFunctor.{w} S where
-  app Z := TypeCat.ofHom fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩
+  app Z := ↾fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩
 
 theorem uliftNatTransOfLe_comm {S T : Sieve X} (h : S ≤ T) :
     uliftNatTransOfLe.{w} h ≫ uliftFunctorInclusion.{w} _ = uliftFunctorInclusion.{w} _ :=
diff --git a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
@@ -415,7 +415,7 @@ theorem Cospherical.affineIndependent_of_mem_of_ne {s : Set P} (hs : Cospherical
     AffineIndependent ℝ ![p₁, p₂, p₃] := by
   refine hs.affineIndependent ?_ ?_
   · simp [h₁, h₂, h₃, Set.insert_subset_iff]
-  · erw [Fin.cons_injective_iff, Fin.cons_injective_iff]
+  · simp only [Matrix.vecCons, Fin.cons_injective_iff]
     simp [h₁₂, h₁₃, h₂₃, Function.Injective, eq_iff_true_of_subsingleton]
 
 /-- The three points of a cospherical set are affinely independent. -/
diff --git a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
@@ -295,7 +295,7 @@ functions `f : M → N` is `C^n` whenever the denominator is non-zero.
 -/
 section Div
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
   {H : Type*} [TopologicalSpace H] {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*}
   [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G]
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
@@ -94,8 +94,7 @@ lemma MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotie
     have meas_π : Measurable π := continuous_quotient_mk'.measurable
     obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
     have h𝓕_translate_fundom : IsFundamentalDomain Γ.op (g • 𝓕) ν := h𝓕.smul_of_comm g
-    -- TODO: why `rw` fails with both of these rewrites?
-    erw [h𝓕.projection_respects_measure_apply (μ := μ)
+    rw [h𝓕.projection_respects_measure_apply (μ := μ)
       (meas_π (measurableSet_preimage (measurable_const_smul g) hA)),
       h𝓕_translate_fundom.projection_respects_measure_apply (μ := μ) hA]
     change ν ((π ⁻¹' _) ∩ _) = ν ((π ⁻¹' _) ∩ _)
@@ -233,8 +232,7 @@ theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient [Loc
     ne_top_of_lt <| QuotientMeasureEqMeasurePreimage.covolume_ne_top μ (ν := ν)
   obtain ⟨s, fund_dom_s⟩ := i
   rw [fund_dom_s.covolume_eq_volume] at finiteCovol
-  -- TODO: why `rw` fails?
-  erw [fund_dom_s.projection_respects_measure_apply μ K'.isCompact.measurableSet]
+  rw [fund_dom_s.projection_respects_measure_apply μ K'.isCompact.measurableSet]
   apply IsHaarMeasure.smul
   · intro h
     have i' : IsOpenPosMeasure (ν : Measure G) := inferInstance
diff --git a/Mathlib/RingTheory/Flat/Equalizer.lean b/Mathlib/RingTheory/Flat/Equalizer.lean
@@ -284,10 +284,6 @@ lemma AlgHom.coe_tensorEqualizer (x : T ⊗[R] AlgHom.equalizer f g) :
       Algebra.TensorProduct.map (AlgHom.id S T) (AlgHom.equalizer f g).val x :=
   AlgHom.coe_tensorEqualizerAux S T f g x
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
-set_option backward.whnf.reducibleClassField false in
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- If `T` is `R`-flat, the canonical map
 `T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)` is an isomorphism. -/
 def AlgHom.tensorEqualizerEquiv [Module.Flat R T] :
diff --git a/Mathlib/Tactic/Replace.lean b/Mathlib/Tactic/Replace.lean
@@ -10,8 +10,8 @@ public import Mathlib.Tactic.Have
 /-!
 # Extending `replace`
 
-This file extends the `replace` tactic from `Batteries` to allow the addition of hypotheses to
-the context without requiring their proofs to be provided immediately.
+This file extends the `replace` tactic from the standard library to allow the addition of hypotheses
+to the context without requiring their proofs to be provided immediately.
 
 As a style choice, this should not be used in mathlib; but is provided for downstream users who
 preferred the old style.
@@ -24,36 +24,12 @@ namespace Mathlib.Tactic
 open Lean Elab.Tactic
 
 /--
-Acts like `have`, but removes a hypothesis with the same name as
-this one if possible. For example, if the state is:
-
-Then after `replace h : β` the state will be:
-
-```lean
-case h
-f : α → β
-h : α
-⊢ β
-
-f : α → β
-h : β
-⊢ goal
-```
-
-whereas `have h : β` would result in:
-
-```lean
-case h
-f : α → β
-h : α
-⊢ β
-
-f : α → β
-h✝ : α
-h : β
-⊢ goal
-```
+`replace h : t`, without a subsequent proof, creates a new main goal `case h : ... ⊢ t`.
+This form is considered deprecated in Mathlib: use `replace h : t := _` instead.
 -/
+tactic_extension Lean.Parser.Tactic.replace
+
+@[tactic_alt Lean.Parser.Tactic.replace]
 syntax (name := replace') "replace" haveIdLhs' : tactic
 
 elab_rules : tactic
diff --git a/Mathlib/Topology/Homotopy/Product.lean b/Mathlib/Topology/Homotopy/Product.lean
@@ -148,8 +148,7 @@ theorem proj_pi (i : ι) (paths : ∀ i, Path.Homotopic.Quotient (as i) (bs i))
 @[simp]
 theorem pi_proj (p : Path.Homotopic.Quotient as bs) : (pi fun i => proj i p) = p := by
   induction p using Quotient.inductionOn
-  simp_rw [Quotient.mk''_eq_mk, proj, ← Path.Homotopic.Quotient.mk_map]
-  erw [pi_lift]
+  simp only [Quotient.mk''_eq_mk, ← Path.Homotopic.Quotient.mk_map, pi_lift]
   congr
 
 end Pi
diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
@@ -372,17 +372,15 @@ def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) := by
 set_option backward.isDefEq.respectTransparency false in
 theorem interUnionPullbackConeLift_left :
     interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_left).op = s.fst := by
-  erw [Category.assoc]
-  simp_rw [← F.1.map_comp]
+  rw [interUnionPullbackConeLift, Category.assoc, ← F.1.map_comp]
   exact
     (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
       op <| Pairwise.single <| ULift.up WalkingPair.left
 
 set_option backward.isDefEq.respectTransparency false in
 theorem interUnionPullbackConeLift_right :
     interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_right).op = s.snd := by
-  erw [Category.assoc]
-  simp_rw [← F.1.map_comp]
+  rw [interUnionPullbackConeLift, Category.assoc, ← F.1.map_comp]
   exact
     (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
       op <| Pairwise.single <| ULift.up WalkingPair.right
@@ -410,12 +408,10 @@ def isLimitPullbackCone : IsLimit (interUnionPullbackCone F U V) := by
     rw [← cancel_mono (F.1.map (eqToHom hι.symm).op)]
     apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext
     rintro ((_ | _) | (_ | _)) <;>
-    rw [Category.assoc, Category.assoc]
-    · erw [← F.1.map_comp]
-      convert h₁
+    rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← F.1.map_comp]
+    · convert h₁
       apply interUnionPullbackConeLift_left
-    · erw [← F.1.map_comp]
-      convert h₂
+    · convert h₂
       apply interUnionPullbackConeLift_right
     all_goals
       dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op,
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.97",
+   "inputRev": "v0.0.98",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a5057d09bbda63aed64ee5b88d37b63da3e46a09",
+   "rev": "71e6f956598ed639a0977b016cf7322a673bf134",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lakefile.lean b/lakefile.lean
@@ -9,7 +9,7 @@ open Lake DSL
 require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
-require "leanprover-community" / "proofwidgets" @ git "v0.0.97"
+require "leanprover-community" / "proofwidgets" @ git "v0.0.98"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \
     Please report this issue on the Lean Zulip."
