chore: bump toolchain to v4.28.0-rc1 (leanprover-community#34436)

* deprecation in lakefile

* chore: bump to nightly-2025-12-10

* Update lean-toolchain for testing leanprover/lean4#11581

* Update lean-toolchain for testing leanprover/lean4#11587

* chore: adaptations for nightly-2025-12-10

* fix

* fix for leanprover/lean4#11581

* deprecation

* remove unused argument

* feat: register mathlib tactics with try? (#136)

This PR adds `register_try?_tactic` calls for all finishing tactics currently registered with `register_hint`, which are not already covered by `grind` modules (i.e. I have not registered `linarith` or `ring`), using identical priority values:

**Common tactics** (Common.lean):
- tauto (priority 500)
- aesop (priority 80)
- fun_prop (priority 200)

**Domain-specific tactics**:
- norm_num (1000), noncomm_ring (1000)
- field (850), bound (70)
- finiteness (1000), compute_degree (1000), positivity (1000), field_simp (1000)


🤖 Prepared with Claude Code

* chore: adaptations for nightly-2025-12-10 (#141)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* fix deprecation in mk_all

* chore: adaptations for nightly-2025-12-10

* chore: bump to nightly-2025-12-11

* Kick CI

* lake update

* fix deps

* remove upstreamed

* workaround

* fix

* chore: bump to nightly-2025-12-12

* Update lean-toolchain for testing leanprover/lean4#11620

* more fix

* fix the fix

* lake update

* adding a prime to NameMapExtension

* adaptations for leanprover/lean4#11620

* revert spurious change

* warning

* Merge master into nightly-testing

* fixes

* fix

* deprecations

* chore: bump to nightly-2025-12-13

* lake update

* lake update

* fix merge

* revert a lia back to omega

* remove upstreamed

* deprecation

* fixes

* fix archive

* lint

* lake update aesop

* chore: adaptations for nightly-2025-12-13

* remove aliases for upstreamed lemmas

* deprecation

* revert a lia back to omega

* lake update

* cutsat to lia

* hm

* note

* adaptation notes

* chore: bump to nightly-2025-12-14

* remove @[grind =] from even_sign_iff

* chore: adaptations for nightly-2025-12-13 (#142)

* lake update

* chore: adaptations for nightly-2025-12-14 (#143)

* chore: adaptations for nightly-2025-12-14

* chore: update lean-toolchain to leanprover/lean4:nightly-2025-12-14

* chore: bump to nightly-2025-12-15

* chore: adaptations for nightly-2025-12-15 (#144)

* chore: bump to nightly-2025-12-16

* Update batteries

* Adapt to leanprover/lean4#11608

* Pull in aesop fixes (from my fork, sorry for that)

* chore: adaptations for nightly-2025-12-16

* fixes

* chore: bump to nightly-2025-12-17

* chore: adaptations for nightly-2025-12-17

* chore: adaptations for nightly-2025-12-16 (#145)

* chore: adaptations for nightly-2025-12-17 (#146)

* chore: adaptations for nightly-2025-12-17

* chore: bump to nightly-2025-12-18

* lake update

* chore: adaptations for nightly-2025-12-18

* chore: bump to nightly-2025-12-19

* remove upstreamed

* remove upstreamed

* fixes

* chore: bump to nightly-2025-12-20

* mk_all

* chore: adaptations for nightly-2025-12-20

* chore: adaptations for nightly-2025-12-20 (#148)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* chore: adaptations for nightly-2025-12-20

* chore: bump to nightly-2025-12-21

* chore: adaptations for nightly-2025-12-21

* chore: adaptations for nightly-2025-12-21 (#149)

* chore: adaptations for nightly-2025-12-21

* chore: bump to nightly-2025-12-22

* chore: adaptations for nightly-2025-12-22

* chore: bump to nightly-2025-12-23

* chore: bump to nightly-2025-12-24

* chore: adaptations for nightly-2025-12-24

* chore: bump to nightly-2025-12-25

* chore: adaptations for nightly-2025-12-25

* chore: bump to nightly-2025-12-26

* chore: adaptations for nightly-2025-12-26

* chore: bump to nightly-2025-12-27

* chore: bump to nightly-2025-12-28

* chore: bump to nightly-2025-12-29

* chore: bump to nightly-2025-12-30

* chore: bump to nightly-2025-12-31

* chore: bump to nightly-2026-01-01

* chore: bump to nightly-2026-01-02

* lake update

* chore: bump to nightly-2026-01-03

* chore: bump to nightly-2026-01-04

* merge lean-pr-testing-10059

* lake update

* deprecations

* Revert "merge lean-pr-testing-10387"

This reverts commit e166d33, reversing
changes made to cf6049c.

* fix

* Revert incorrectly merged lean-pr-testing branches

Reverts the following branches that were incorrectly merged due to a bug
in discover-lean-pr-testing.yml where an empty prs.txt caused grep to
match ALL lean-pr-testing branches:

- lean-pr-testing-2714 (from Oct 2023!)
- lean-pr-testing-11455
- lean-pr-testing-11163
- lean-pr-testing-10231
- lean-pr-testing-10178
- lean-pr-testing-10059

These PRs are not in nightly-2026-01-04, so their adaptations should not
be merged.

The bug fix is in: leanprover-community#33546

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* deprecations

* Update lean-toolchain for testing leanprover/lean4#11893

* fix

* chore: bump to nightly-2026-01-05

* remove upstreamed

* lake update

* fix

* chore: adaptations for nightly-2026-01-05

* chore: bump to nightly-2026-01-06

* chore: adaptations for nightly-2026-01-06

* chore: adaptations for nightly-2026-01-06

* chore: bump to nightly-2026-01-07

* chore: adaptations for nightly-2026-01-07

* chore: adaptations for nightly-2026-01-09 (#159)

* replace aesop proof

* chore: adaptations for nightly-2026-01-07

* chore: bump to nightly-2026-01-08

* chore: adaptations for nightly-2026-01-08

* chore: bump to nightly-2026-01-09

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

* chore: adaptations for nightly-2026-01-23 (#160)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-24 (#161)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-25 (#162)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: bump toolchain to v4.28.0-rc1

* fix: use main/master instead of nightly-testing for dependencies

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: leanprover-community-bot-assistant <97194829+leanprover-community-bot-assistant@users.noreply.github.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

Author: 13 people

.github/workflows/daily.yml

@@ -22,12 +22,12 @@ permissions:
 
 jobs:
   check-leanchecker:
-    runs-on: lean4checker
-    if: github.repository == 'leanprover-community/mathlib4'
+    runs-on: ubuntu-latest  # lean4checker
+    if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
     strategy:
       fail-fast: false
       matrix:
-        branch_type: [nightly] #[master, nightly]  # TODO: reactivate master when leanchecker has landed there (also below)
+        branch_type: [nightly] #[master, nightly]  # TODO: reactivate master when leanchecker has landed there
     steps:
       # Checkout repository, so that we can fetch tags to decide which branch we want.
       - name: Checkout branch or tag

Mathlib.lean

@@ -7493,7 +7493,6 @@ public import Mathlib.Topology.VectorBundle.Hom
 public import Mathlib.Topology.VectorBundle.Riemannian
 public import Mathlib.Util.AddRelatedDecl
 public import Mathlib.Util.AliasIn
-public import Mathlib.Util.AssertExists
 public import Mathlib.Util.AssertExistsExt
 public import Mathlib.Util.AssertNoSorry
 public import Mathlib.Util.AtLocation

Mathlib/Algebra/Group/Action/TransferInstance.lean

@@ -25,6 +25,7 @@ namespace Equiv
 variable {M N O α β : Type*}
 
 variable (M) [Monoid M] in
+set_option backward.proofsInPublic true in
 /-- Transfer `MulAction` across an `Equiv` -/
 @[to_additive /-- Transfer `AddAction` across an `Equiv` -/]
 protected abbrev mulAction (e : α ≃ β) [MulAction M β] : MulAction M α where

Mathlib/Algebra/Group/TypeTags/Basic.lean

@@ -10,7 +10,8 @@ public import Mathlib.Algebra.Notation.Pi.Basic
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Logic.Function.Iterate
 public import Mathlib.Logic.Equiv.Defs
-public import Mathlib.Util.AssertExists
+public import Mathlib.Tactic.Set
+public import Mathlib.Logic.Nontrivial.Basic
 
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa

Mathlib/Algebra/Notation/Defs.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Tactic.Lemma
 public import Mathlib.Tactic.TypeStar
 public import Mathlib.Tactic.ToAdditive
-public import Mathlib.Util.AssertExists
 
 /-!
 # Typeclasses for algebraic operations

Mathlib/Algebra/Notation/Lemmas.lean

@@ -9,7 +9,6 @@ public import Batteries.Tactic.Init
 public import Mathlib.Tactic.ToAdditive
 public import Mathlib.Tactic.Lemma
 public import Mathlib.Tactic.TypeStar
-public import Mathlib.Util.AssertExists
 
 /-! # Lemmas about inequalities with `1`. -/
 

Mathlib/Algebra/Notation/Pi/Defs.lean

@@ -6,7 +6,6 @@ Authors: Simon Hudon, Patrick Massot, Eric Wieser
 module
 
 public import Mathlib.Algebra.Notation.Defs
-public import Mathlib.Util.AssertExists
 public import Mathlib.Tactic.Push.Attr
 
 /-!

Mathlib/Algebra/Notation/Prod.lean

@@ -5,7 +5,6 @@ Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
 module
 
-public import Mathlib.Util.AssertExists
 public import Mathlib.Algebra.Notation.Defs
 public import Mathlib.Data.Prod.Basic
 

Mathlib/Algebra/Order/Group/Defs.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Order.Group.Unbundled.Basic
 public import Mathlib.Algebra.Order.Monoid.Defs
 public import Mathlib.Algebra.Order.Sub.Defs
-public import Mathlib.Util.AssertExists
 
 /-!
 # Ordered groups

Mathlib/Algebra/Order/Group/Unbundled/Basic.lean

@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
 public import Mathlib.Algebra.Order.Sub.Defs
-public import Mathlib.Util.AssertExists
 
 /-!
 # Ordered groups