Commit 2025-06-03 08:51 4e57d17b

View on Github →

chore: bump toolchain to v4.21.0-rc1 (#25384)

Estimated changes

Modified Archive/Examples/IfNormalization/WithoutAesop.lean

Modified Archive/Imo/Imo2015Q6.lean

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Modified Mathlib/Algebra/Field/Rat.lean

Modified Mathlib/Algebra/FreeAlgebra.lean

Modified Mathlib/Algebra/Group/Defs.lean

deleted def npowRec

deleted def nsmulRec

Modified Mathlib/Algebra/Group/Fin/Basic.lean

Modified Mathlib/Algebra/Homology/AlternatingConst.lean

Modified Mathlib/Algebra/Homology/Double.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/Algebra/Lie/Weights/Chain.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

Modified Mathlib/Algebra/Notation/Defs.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/Algebra/Ring/GrindInstances.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Faces.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Comp.lean

Modified Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

Modified Mathlib/CategoryTheory/IsomorphismClasses.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Pi/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean

Modified Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

Modified Mathlib/Computability/Halting.lean

Modified Mathlib/Computability/PartrecCode.lean

Modified Mathlib/Computability/PostTuringMachine.lean

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Control/Bitraversable/Instances.lean

Modified Mathlib/Control/Random.lean

Modified Mathlib/Control/Traversable/Equiv.lean

Modified Mathlib/Control/Traversable/Instances.lean

Modified Mathlib/Data/BitVec.lean

deleted theorem BitVec.ofFin_natCast

deleted theorem BitVec.ofFin_neg

deleted theorem BitVec.toFin_natCast

added theorem Fin.val_intCast

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.castSucc_natAdd

deleted theorem Fin.neg_def

deleted theorem Fin.ofNat'_eq_cast

added theorem Fin.ofNat_eq_cast

deleted theorem Fin.val_eq_zero_iff

deleted theorem Fin.val_ne_zero_iff

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.append_left'

Modified Mathlib/Data/Int/Basic.lean

deleted theorem Int.natCast_dvd_natCast

Modified Mathlib/Data/Int/Init.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Duplicate.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Lookmap.lean

Modified Mathlib/Data/List/ModifyLast.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

Modified Mathlib/Data/List/OfFn.lean

deleted theorem List.ofFn_add

Modified Mathlib/Data/List/Scan.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/Multiset/Replicate.lean

Modified Mathlib/Data/Nat/Cast/SetInterval.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Modified Mathlib/Data/Nat/MaxPowDiv.lean

Modified Mathlib/Data/Option/Basic.lean

modified theorem Option.none_bind'

modified theorem Option.orElse_eq_none

modified theorem Option.some_bind'

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Rat/Cast/Lemmas.lean

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/Logic/Function/Defs.lean

deleted theorem Function.comp_id

deleted theorem Function.id_comp

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/Order/Filter/AtTopBot/Field.lean

Modified Mathlib/Order/Filter/Bases/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Fin/Basic.lean

Modified Mathlib/Order/Interval/Basic.lean

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/Order/RelSeries.lean

Modified Mathlib/Tactic/Basic.lean

deleted def Lean.MVarId.clearValue

Modified Mathlib/Tactic/DeriveTraversable.lean

Modified Mathlib/Tactic/ExtractGoal.lean

Modified Mathlib/Tactic/Linter/DeprecatedModule.lean

Modified Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean

Modified Mathlib/Tactic/Linter/DocPrime.lean

Modified Mathlib/Tactic/Linter/DocString.lean

Modified Mathlib/Tactic/Linter/FlexibleLinter.lean

Modified Mathlib/Tactic/Linter/GlobalAttributeIn.lean

modified def Mathlib.Linter.globalAttributeInLinter.getLinterGlobalAttributeIn

Modified Mathlib/Tactic/Linter/HashCommandLinter.lean

Modified Mathlib/Tactic/Linter/Header.lean

Modified Mathlib/Tactic/Linter/Lint.lean

Modified Mathlib/Tactic/Linter/MinImports.lean

Modified Mathlib/Tactic/Linter/Multigoal.lean

Modified Mathlib/Tactic/Linter/OldObtain.lean

Modified Mathlib/Tactic/Linter/PPRoundtrip.lean

Modified Mathlib/Tactic/Linter/Style.lean

Modified Mathlib/Tactic/Linter/TextBased.lean

modified def Mathlib.Linter.TextBased.lintFile

modified def Mathlib.Linter.TextBased.lintModules

modified def Mathlib.Linter.TextBased.modulesNotUpperCamelCase

Modified Mathlib/Tactic/Linter/UnusedTactic.lean

Modified Mathlib/Tactic/Linter/UpstreamableDecl.lean

Modified Mathlib/Tactic/ModCases.lean

Modified Mathlib/Tactic/Recall.lean

Modified Mathlib/Tactic/Sat/FromLRAT.lean

Modified Mathlib/Tactic/Subsingleton.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Topology/Basic.lean

modified theorem le_nhds_lim

Modified Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Util/CountHeartbeats.lean

Modified MathlibTest/Check.lean

Modified MathlibTest/ErwQuestion.lean

Modified MathlibTest/ExtractGoal.lean

Modified MathlibTest/MinImports.lean

Modified MathlibTest/ModuleCasing.lean

Modified MathlibTest/Simps.lean

Modified MathlibTest/StringDiagram.lean

Modified MathlibTest/TCSynth.lean

Modified MathlibTest/abel.lean

Modified MathlibTest/fast_instance.lean

Modified MathlibTest/fin_cases.lean

Modified MathlibTest/fun_prop_dev.lean

Created MathlibTest/grind/trig.lean

Modified MathlibTest/lift.lean

Modified MathlibTest/linear_combination'.lean

Modified MathlibTest/linear_combination.lean

Modified MathlibTest/notation3.lean

Modified MathlibTest/renameBvar.lean

Modified MathlibTest/ring.lean

Modified lake-manifest.json

Modified lakefile.lean

Modified lean-toolchain

Modified scripts/lint-style.lean

modified def missingInitImports

modified def undocumentedScripts

Modified scripts/noshake.json