Auto-resolved conflicts in lean-toolchain and lake-manifest.json

Author: mathlib4-bot

.github/workflows/PR_summary.yml

@@ -13,9 +13,19 @@ jobs:
       uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       with:
         fetch-depth: 0
+        path: pr-branch
+
+    # Checkout the master branch into a subdirectory
+    - name: Checkout master branch
+      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      with:
+        # When testing the scripts, comment out the "ref: master"
+        ref: master
+        path: master-branch
 
     - name: Update the merge-conflict label
       run: |
+        cd pr-branch
         printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
         if git merge origin/master --no-ff --no-commit
         then
@@ -27,7 +37,7 @@ jobs:
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
         else
-          echo "This PR has merge conflicts with main."
+          echo "This PR has merge conflicts with master."
           # we use curl rather than octokit/request-action so that the job won't fail
           # (and send an annoying email) if the labels don't exist
           curl --request POST \
@@ -36,7 +46,6 @@ jobs:
             --header 'X-GitHub-Api-Version: 2022-11-28' \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
             --data '{"labels":["merge-conflict"]}'
-
         fi
 
     - name: Set up Python
@@ -52,6 +61,7 @@ jobs:
 
     - name: Get changed and removed/renamed files
       run: |
+        cd pr-branch
         git fetch origin ${{ github.base_ref }}  # fetch the base branch
 
         # Get the list of all changed files.
@@ -87,6 +97,7 @@ jobs:
 
     - name: Compute (re)moved files without deprecation
       run: |
+        cd pr-branch
         touch moved_without_deprecation.txt
         git checkout ${{ github.base_ref }}
         while IFS= read -r file
@@ -112,19 +123,20 @@ jobs:
 
     - name: Compute transitive imports
       run: |
+        cd pr-branch
         # the checkout dance, to avoid a detached head
         git checkout master
         git checkout -
         currentHash="$(git rev-parse HEAD)"
 
         # Compute the counts for the HEAD of the PR
-        python ./scripts/count-trans-deps.py "Mathlib/" > head.json
+        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > head.json
 
         # Checkout the merge base
         git checkout "$(git merge-base master ${{ github.sha }})"
 
         # Compute the counts for the merge base
-        python ./scripts/count-trans-deps.py "Mathlib/" > base.json
+        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > base.json
 
         # switch back to the current branch: the `declarations_diff` script should be here
         git checkout "${currentHash}"
@@ -134,15 +146,16 @@ jobs:
         GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         BRANCH_NAME: ${{ github.head_ref }}
       run: |
+        cd pr-branch
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
-        graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+        graphAndHighPercentReports=$(python ../master-branch/scripts/import-graph-report.py base.json head.json changed_files.txt)
 
         ## Import count comment
         importCount=$(
           printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
-          ./scripts/import_trans_difference.sh
+          ../master-branch/scripts/import_trans_difference.sh
         )
 
         ## High percentage imports
@@ -166,7 +179,7 @@ jobs:
         fi
 
         ## Declarations' diff comment
-        declDiff=$(./scripts/declarations_diff.sh)
+        declDiff=$(../master-branch/scripts/declarations_diff.sh)
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
           declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
@@ -178,7 +191,7 @@ jobs:
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
         ## Technical debt changes
-        techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
+        techDebtVar="$(../master-branch/scripts/technical-debt-metrics.sh pr_summary)"
 
         # store in a file, to avoid "long arguments" error.
         printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
@@ -191,10 +204,11 @@ jobs:
         fi
 
         cat please_merge_master.md
-        ./scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
+        ../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
 
     - name: Update the file-removed label
       run: |
+        cd pr-branch
         undeprecatedMoves="$(cat moved_without_deprecation.txt)"
         if [ -n "$undeprecatedMoves" ]; then
           echo "This PR has undeprecated module (re)movals."

.github/workflows/maintainer_merge.yml

@@ -113,7 +113,8 @@ jobs:
         if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
         uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
         with:
-          github-token: ${{secrets.GITHUB_TOKEN}}
+          # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
+          github-token: ${{secrets.TRIAGE_TOKEN}}
           script: |
             const { owner, repo, number: issue_number } = context.issue;
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });

Counterexamples/AharoniKorman.lean

@@ -67,10 +67,6 @@ aim of reaching a contradiction (as then, no such partition can exist). We may f
   we have a contradiction (`no_spinalMap`), and therefore show that no spinal map exists.
 -/
 
-#adaptation_note /-- 2025-03-12
-We temporarily comment out this file on `nightly-testing`, awaiting fixes for a complex
-interaction between `omega`, `aesop`, and asynchronous elaboration.
-
 attribute [aesop norm 10 tactic] Lean.Elab.Tactic.Omega.omegaDefault
 attribute [aesop 2 simp] Set.subset_def Finset.subset_iff
 
@@ -1253,5 +1249,3 @@ theorem aharoni_korman_false :
     rw [Hollom.exists_partition_iff_nonempty_spinalMap hC] at h
     obtain ⟨f⟩ := h
     exact Hollom.no_spinalMap hC f
-
--/

Mathlib.lean

@@ -1608,8 +1608,10 @@ import Mathlib.Analysis.MellinTransform
 import Mathlib.Analysis.Meromorphic.Basic
 import Mathlib.Analysis.Meromorphic.Divisor
 import Mathlib.Analysis.Meromorphic.FactorizedRational
+import Mathlib.Analysis.Meromorphic.IsolatedZeros
 import Mathlib.Analysis.Meromorphic.NormalForm
 import Mathlib.Analysis.Meromorphic.Order
+import Mathlib.Analysis.Meromorphic.TrailingCoefficient
 import Mathlib.Analysis.Normed.Affine.AddTorsor
 import Mathlib.Analysis.Normed.Affine.AddTorsorBases
 import Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
@@ -1706,6 +1708,7 @@ import Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
 import Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
 import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
 import Mathlib.Analysis.NormedSpace.Alternating.Basic
+import Mathlib.Analysis.NormedSpace.Alternating.Curry
 import Mathlib.Analysis.NormedSpace.BallAction
 import Mathlib.Analysis.NormedSpace.ConformalLinearMap
 import Mathlib.Analysis.NormedSpace.Connected
@@ -4563,6 +4566,7 @@ import Mathlib.NumberTheory.MulChar.Lemmas
 import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.NumberField.AdeleRing
 import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.NumberTheory.NumberField.CMField
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
@@ -4999,6 +5003,7 @@ import Mathlib.RepresentationTheory.GroupCohomology.Functoriality
 import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
 import Mathlib.RepresentationTheory.GroupCohomology.LowDegree
 import Mathlib.RepresentationTheory.GroupCohomology.Resolution
+import Mathlib.RepresentationTheory.Induced
 import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RepresentationTheory.Rep
@@ -6085,8 +6090,10 @@ import Mathlib.Topology.Closure
 import Mathlib.Topology.ClusterPt
 import Mathlib.Topology.Coherent
 import Mathlib.Topology.CompactOpen
+import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePoint.Basic
 import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
+import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -36,18 +36,21 @@ universe v u
 
 namespace CoalgCat
 
-open CategoryTheory MonoidalCategory
+open CategoryTheory MonoidalCategory Comon_Class
 
 variable {R : Type u} [CommRing R]
 
-/-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
-@[simps X counit comul] def toComonObj (X : CoalgCat R) : Comon_ (ModuleCat R) where
-  X := ModuleCat.of R X
+@[simps counit comul]
+noncomputable instance (X : CoalgCat R) : Comon_Class (ModuleCat.of R X) where
   counit := ModuleCat.ofHom Coalgebra.counit
   comul := ModuleCat.ofHom Coalgebra.comul
-  counit_comul := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
-  comul_counit := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
-  comul_assoc := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
+  counit_comul' := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
+  comul_counit' := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
+  comul_assoc' := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
+
+/-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
+@[simps X]
+noncomputable def toComonObj (X : CoalgCat R) : Comon_ (ModuleCat R) := ⟨ModuleCat.of R X⟩
 
 variable (R) in
 /-- The natural functor from `R`-coalgebras to comonoid objects in the category of `R`-modules. -/
@@ -62,26 +65,26 @@ def toComon : CoalgCat R ⥤ Comon_ (ModuleCat R) where
 /-- A comonoid object in the category of `R`-modules has a natural comultiplication
 and counit. -/
 @[simps]
-noncomputable instance ofComonObjCoalgebraStruct (X : Comon_ (ModuleCat R)) :
-    CoalgebraStruct R X.X where
-  comul := X.comul.hom
-  counit := X.counit.hom
+noncomputable instance ofComonObjCoalgebraStruct (X : ModuleCat R) [Comon_Class X] :
+    CoalgebraStruct R X where
+  comul := Δ[X].hom
+  counit := ε[X].hom
 
 /-- A comonoid object in the category of `R`-modules has a natural `R`-coalgebra
 structure. -/
-def ofComonObj (X : Comon_ (ModuleCat R)) : CoalgCat R :=
-  { ModuleCat.of R X.X with
+noncomputable def ofComonObj (X : ModuleCat R) [Comon_Class X] : CoalgCat R :=
+  { ModuleCat.of R X with
     instCoalgebra :=
       { ofComonObjCoalgebraStruct X with
-        coassoc := ModuleCat.hom_ext_iff.mp X.comul_assoc.symm
-        rTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp X.counit_comul
-        lTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp X.comul_counit } }
+        coassoc := ModuleCat.hom_ext_iff.mp (comul_assoc X).symm
+        rTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp (counit_comul X)
+        lTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp (comul_counit X) } }
 
 variable (R)
 
 /-- The natural functor from comonoid objects in the category of `R`-modules to `R`-coalgebras. -/
-def ofComon : Comon_ (ModuleCat R) ⥤ CoalgCat R where
-  obj X := ofComonObj X
+noncomputable def ofComon : Comon_ (ModuleCat R) ⥤ CoalgCat R where
+  obj X := ofComonObj X.X
   map f :=
     { toCoalgHom' :=
       { f.hom.hom with
@@ -122,8 +125,10 @@ theorem tensorObj_comul (K L : CoalgCat R) :
       ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul := by
   rw [ofComonObjCoalgebraStruct_comul]
   dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]
-  simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, ModuleCat.of_coe, toComonObj_comul,
-    tensorμ_eq_tensorTensorTensorComm]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse,
+    comonEquivalence_functor, toComon_obj, toComonObj_X, ModuleCat.of_coe, comul_def,
+    tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp, ModuleCat.hom_ofHom,
+    LinearEquiv.comp_toLinearMap_eq_iff]
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
@@ -158,9 +163,7 @@ theorem comul_tensorObj_tensorObj_right :
       (CoalgCat.of R N ⊗ CoalgCat.of R P) : CoalgCat R))
       = Coalgebra.comul (A := M ⊗[R] N ⊗[R] P) := by
   rw [ofComonObjCoalgebraStruct_comul]
-  dsimp
-  simp only [Comon_.monoidal_tensorObj_comul, toComonObj_comul]
-  rw [ofComonObjCoalgebraStruct_comul]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, toComonObj]
   simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
     AlgebraTensorModule.tensorTensorTensorComm_eq]
   rfl
@@ -171,8 +174,7 @@ theorem comul_tensorObj_tensorObj_left :
       = Coalgebra.comul (A := (M ⊗[R] N) ⊗[R] P) := by
   rw [ofComonObjCoalgebraStruct_comul]
   dsimp
-  simp only [Comon_.monoidal_tensorObj_comul, toComonObj_comul]
-  rw [ofComonObjCoalgebraStruct_comul]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, toComonObj]
   simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
     AlgebraTensorModule.tensorTensorTensorComm_eq]
   rfl

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -62,6 +62,8 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
   ObjectProperty.lift _ inverseAux inferInstance
 
+open scoped Mon_Class
+
 attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
 /-- Implementation, see `leftExactFunctorForgetEquivalence`.
 This is the complicated bit, where we show that forgetting the group structure in the image of
@@ -72,10 +74,14 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F
       (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
   letI : (F ⋙ forget AddCommGrp).Braided := .ofChosenFiniteProducts _
   letI : F.Monoidal := .ofChosenFiniteProducts _
-  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by aesop_cat) ?_
+  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by
+    erw [Functor.mapCommGrp_obj_grp_one]
+    aesop_cat) ?_
   dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_coe, -forget_map]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
-  rw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrp) X X,
+  simp only [Category.id_comp]
+  erw [Functor.mapCommGrp_obj_grp_mul]
+  erw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrp) X X,
     Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
     Functor.Monoidal.μ_snd]
   aesop_cat

Mathlib/Algebra/DualNumber.lean

@@ -157,6 +157,13 @@ set_option linter.unusedVariables false in
     lift fe (inl a : A[ε]) = fe.val.1 a := by
   rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]
 
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/5338
+The new unused variable linter flags `{fe : (A →ₐ[R] B) × B // _}`. -/
+set_option linter.unusedVariables false in
+@[simp] theorem lift_comp_inlHom (fe : {fe : (A →ₐ[R] B) × B // _}) :
+    (lift fe).comp (inlAlgHom R A A) = fe.val.1 :=
+  AlgHom.ext <| lift_apply_inl fe
+
 #adaptation_note /-- https://github.com/leanprover/lean4/pull/5338
 The new unused variable linter flags `{fe : (A →ₐ[R] B) × B // _}`. -/
 set_option linter.unusedVariables false in
@@ -185,6 +192,24 @@ theorem lift_inlAlgHom_eps :
     lift ⟨(inlAlgHom _ _ _, ε), eps_mul_eps, fun _ => commute_eps_left _⟩ = AlgHom.id R A[ε] :=
   lift.apply_symm_apply <| AlgHom.id R A[ε]
 
+@[simp]
+theorem range_inlAlgHom_sup_adjoin_eps :
+    (inlAlgHom R A A).range ⊔ Algebra.adjoin R {ε} = ⊤ := by
+  refine top_unique fun x hx => ?_; clear hx
+  rw [← x.inl_fst_add_inr_snd_eq, inr_eq_smul_eps, ← inl_mul_eq_smul]
+  refine add_mem ?_ (mul_mem ?_ ?_)
+  · exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.fst
+  · exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.snd
+  · refine le_sup_right (α := Subalgebra R _) <| Algebra.subset_adjoin <| Set.mem_singleton ε
+
+@[simp]
+theorem range_lift
+    (fe : {fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a)}) :
+    (lift fe).range = fe.1.1.range ⊔ Algebra.adjoin R {fe.1.2} := by
+  simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
+    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
+    Algebra.map_top]
+
 /-- Show DualNumber with values x and y as an "x + y*ε" string -/
 instance instRepr [Repr R] : Repr (DualNumber R) where
   reprPrec f p :=

Mathlib/Algebra/Group/Action/Sigma.lean

@@ -28,7 +28,7 @@ namespace Sigma
 
 section SMul
 
-variable [∀ i, SMul M (α i)] [∀ i, SMul N (α i)] (a : M) (i : ι) (b : α i) (x : Σi, α i)
+variable [∀ i, SMul M (α i)] [∀ i, SMul N (α i)] (a : M) (i : ι) (b : α i) (x : Σ i, α i)
 
 @[to_additive Sigma.VAdd]
 instance : SMul M (Σi, α i) :=

Mathlib/Algebra/Group/Ext.lean

@@ -78,7 +78,7 @@ theorem RightCancelMonoid.toMonoid_injective {M : Type u} :
 
 @[to_additive (attr := ext)]
 theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄
-    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))  :
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
     m₁ = m₂ :=
   RightCancelMonoid.toMonoid_injective <| Monoid.ext h_mul
 

Mathlib/Algebra/Group/Submonoid/MulAction.lean

@@ -27,7 +27,7 @@ section SetLike
 variable {S' : Type*} [SetLike S' M'] (s : S')
 
 @[to_additive]
-instance (priority := low) [SMul M' α]  : SMul s α where
+instance (priority := low) [SMul M' α] : SMul s α where
   smul m a := (m : M') • a
 
 section MulOneClass