Trigger CI for leanprover-community/batteries#1267

Author: leanprover-community-mathlib4-bot

.github/build.in.yml

@@ -136,9 +136,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -219,13 +218,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/bors.yml

@@ -146,9 +146,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -229,13 +228,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/build.yml

@@ -153,9 +153,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -236,13 +235,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/build_fork.yml

@@ -150,9 +150,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -233,13 +232,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

Mathlib.lean

@@ -1031,6 +1031,7 @@ import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.GrindInstances
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
+import Mathlib.Algebra.Ring.Hom.InjSurj
 import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Algebra.Ring.Identities
 import Mathlib.Algebra.Ring.InjSurj
@@ -3480,6 +3481,7 @@ import Mathlib.Deprecated.Cardinal.Continuum
 import Mathlib.Deprecated.Cardinal.Finite
 import Mathlib.Deprecated.Cardinal.PartENat
 import Mathlib.Deprecated.Order
+import Mathlib.Deprecated.RingHom
 import Mathlib.Dynamics.BirkhoffSum.Average
 import Mathlib.Dynamics.BirkhoffSum.Basic
 import Mathlib.Dynamics.BirkhoffSum.NormedSpace

Mathlib/Algebra/Equiv/TransferInstance.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Field.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Small.Defs
+import Mathlib.Algebra.Ring.Hom.InjSurj
 
 /-!
 # Transfer algebraic structures across `Equiv`s

Mathlib/Algebra/Polynomial/Div.lean

@@ -617,7 +617,8 @@ theorem eval₂_modByMonic_eq_self_of_root [CommRing S] {f : R →+* S} {p q : R
 
 theorem sub_dvd_eval_sub (a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b := by
   suffices X - C b ∣ p - C (p.eval b) by
-    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this
+    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
+      using (_root_.map_dvd (evalRingHom a)) this
   simp [dvd_iff_isRoot]
 
 @[simp]

Mathlib/Algebra/Polynomial/Eval/Defs.lean

@@ -215,7 +215,7 @@ theorem eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n :=
   (eval₂RingHom _ _).map_pow _ _
 
 theorem eval₂_dvd : p ∣ q → eval₂ f x p ∣ eval₂ f x q :=
-  (eval₂RingHom f x).map_dvd
+  map_dvd (eval₂RingHom f x)
 
 theorem eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (h : p ∣ q) (h0 : eval₂ f x p = 0) :
     eval₂ f x q = 0 :=
@@ -524,7 +524,7 @@ protected theorem map_ofNat (n : ℕ) [n.AtLeastTwo] :
 
 --TODO rename to `map_dvd_map`
 theorem map_dvd (f : R →+* S) {x y : R[X]} : x ∣ y → x.map f ∣ y.map f :=
-  (mapRingHom f).map_dvd
+  _root_.map_dvd (mapRingHom f)
 
 lemma mapRingHom_comp_C {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) :
     (mapRingHom f).comp C = C.comp f := by ext; simp

Mathlib/Algebra/Polynomial/Roots.lean

@@ -729,7 +729,7 @@ variable {A B : Type*} [CommRing A] [CommRing B]
 theorem le_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) :
     rootMultiplicity a p ≤ rootMultiplicity (f a) (p.map f) := by
   rw [le_rootMultiplicity_iff hmap]
-  refine _root_.trans ?_ ((mapRingHom f).map_dvd (pow_rootMultiplicity_dvd p a))
+  refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))
   rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]
 
 theorem eq_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hf : Function.Injective f) (a : A) :

Mathlib/Algebra/Ring/Hom/Basic.lean

@@ -3,54 +3,15 @@ Copyright (c) 2019 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Amelia Livingston, Jireh Loreaux
 -/
-import Mathlib.Algebra.Divisibility.Hom
-import Mathlib.Algebra.GroupWithZero.InjSurj
+
 import Mathlib.Algebra.Ring.Hom.Defs
-import Mathlib.Data.Set.Insert
 
 /-!
 # Additional lemmas about homomorphisms of semirings and rings
-
-These lemmas have been banished here to avoid unnecessary imports in
-`Mathlib/Algebra/Hom/Ring/Defs.lean`.
-
-They could be moved to more natural homes.
 -/
 
 assert_not_exists RelIso Field
 
-open Function
-
-variable {α β : Type*}
-
 namespace RingHom
 
-section
-
-variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β)
-
-/-- `f : α →+* β` has a trivial codomain iff its range is `{0}`. -/
-theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=
-  f.codomain_trivial_iff_range_trivial.trans
-    ⟨fun h =>
-      Set.ext fun y => ⟨fun ⟨x, hx⟩ => by simp [← hx, h x], fun hy => ⟨0, by simpa using hy.symm⟩⟩,
-      fun h x => Set.mem_singleton_iff.mp (h ▸ Set.mem_range_self x)⟩
-
-end
-
-section Semiring
-
-variable [Semiring α] [Semiring β]
-
-protected theorem map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
-  map_dvd f
-
-end Semiring
-
 end RingHom
-
-/-- Pullback `IsDomain` instance along an injective function. -/
-protected theorem Function.Injective.isDomain [Semiring α] [IsDomain α] [Semiring β] {F}
-    [FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F) (hf : Injective f) : IsDomain β where
-  __ := domain_nontrivial f (map_zero _) (map_one _)
-  __ := hf.isCancelMulZero f (map_zero _) (map_mul _)