[Merged by Bors] - chore: move liftReflToEq and rel_of_eq_and_refl from core

[kim-em]

This PR moves Lean.MVarId.liftReflToEq and its helper theorem Lean.Meta.Rfl.rel_of_eq_and_refl from core into Mathlib/Tactic/Relation/Rfl.lean, where they become Mathlib.Tactic.liftReflToEq and Mathlib.Tactic.rel_of_eq_and_refl. Mathlib is the only user of either declaration, so core deprecates them in leanprover/lean4#15080.

The new names avoid a clash with the deprecated core declarations, so the two call sites in Mathlib.Tactic.CongrM and Mathlib.Tactic.CongrExclamation no longer use dot notation.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CH8QxMAJ7CEKkYq6z2DuUp

[github-actions]

PR summary ff6c54ce33

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.CongrM	99	100	+1 (+1.01%)
Mathlib.Tactic.CongrExclamation	109	110	+1 (+0.92%)

Import changes for all files

Files

Import difference

447 files Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.ModEq Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Pointwise.Set.SelfInv Mathlib.Algebra.Group.Pointwise.Set.Small Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.MulOpposite Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.TypeTags.Pointwise Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero Mathlib.Algebra.GroupWithZero.Submonoid.Instances Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Notation.Indicator Mathlib.Algebra.Notation.Support Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.Archimedean.Defs Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Basic Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Defs Mathlib.Algebra.Order.GroupWithZero.OrderIso Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Submonoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.IsBotOne Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Ring.Int.Defs Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.Basic.Countable.Small Mathlib.Basic.Logic.Lemmas Mathlib.Basic.Rel.Cover Mathlib.Basic.Rel.Separated Mathlib.Basic.Rel Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Weight Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Control.EquivFunctor Mathlib.Control.Fix Mathlib.Data.Bool.Set Mathlib.Data.Bundle Mathlib.Data.Countable.Small Mathlib.Data.ENat.Basic Mathlib.Data.FP.Basic Mathlib.Data.FunLike.Graded Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.NatAbs Mathlib.Data.Int.Range Mathlib.Data.List.DropRight Mathlib.Data.List.Find Mathlib.Data.List.Iterate Mathlib.Data.List.SplitLengths Mathlib.Data.List.TakeWhile Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Pairing Mathlib.Data.Nat.Set Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PFun Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PSigma.Order Mathlib.Data.Part Mathlib.Data.Prod.Lex Mathlib.Data.Rel.Cover Mathlib.Data.Rel.Separated Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Basic Mathlib.Data.Set.BoolIndicator Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Lattice.Bounded Mathlib.Data.Set.Lattice.Disjoint Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice.Indexed Mathlib.Data.Set.Lattice.Order Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Order Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Chain Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.Subsingleton Mathlib.Data.Set.SymmDiff Mathlib.Data.Set.UnionLift Mathlib.Data.SetLike.Basic Mathlib.Data.Setoid.Basic Mathlib.Data.Sigma.Order Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.Data.ULift Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.GroupTheory.Subsemigroup.Lemmas Mathlib.InformationTheory.Coding.PrefixFree Mathlib.Logic.Embedding.Basic Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Basic Mathlib.Logic.Equiv.Bool Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.Nat Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Equiv.Sigma Mathlib.Logic.Function.Const Mathlib.Logic.Function.DependsOn Mathlib.Logic.Function.FiberPartition Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Antichain Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra.Basic Mathlib.Order.BooleanAlgebra.Defs Mathlib.Order.BooleanAlgebra.Set Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Bounded Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Circular Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.ConditionallyCompletePartialOrder.Basic Mathlib.Order.ConditionallyCompletePartialOrder.Defs Mathlib.Order.ConditionallyCompletePartialOrder.Indexed Mathlib.Order.Copy Mathlib.Order.Directed Mathlib.Order.Disjoint Mathlib.Order.Extension.Linear Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Defs Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Lift Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Prod Mathlib.Order.Filter.SmallSets Mathlib.Order.Filter.Tendsto Mathlib.Order.GaloisConnection.Basic Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Hom Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.Lex Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Hom.WithTopBot Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Lex Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.LinearOrder Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.Iterate Mathlib.Order.Lattice.Congruence Mathlib.Order.LatticeIntervals Mathlib.Order.Lattice Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Minimal Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Monovary Mathlib.Order.Monotone.Odd Mathlib.Order.Monotone.Union Mathlib.Order.Nat Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.OrderDual Mathlib.Order.Preorder.Chain Mathlib.Order.Prod.Lex.Hom Mathlib.Order.PropInstances Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity.Complete Mathlib.Order.ScottContinuity.Prod Mathlib.Order.ScottContinuity Mathlib.Order.SemiconjSup Mathlib.Order.SetIsMax Mathlib.Order.Set Mathlib.Order.SymmDiff Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.UpperLower.Relative Mathlib.Order.WellFounded Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.Order.Zorn Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.RingInvo Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.Lists Mathlib.SetTheory.ZFC.PSet Mathlib.Tactic.ApplyFun Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.CongrExclamation Mathlib.Tactic.CongrM Mathlib.Tactic.Convert Mathlib.Tactic.DeriveCountable Mathlib.Tactic.Inclusion.Core.Core Mathlib.Tactic.Inclusion.Core.Elab Mathlib.Tactic.Inclusion.Core.Expr Mathlib.Tactic.Inclusion.Core.Inclusion Mathlib.Tactic.Inclusion.Core.ToSet Mathlib.Tactic.Inclusion.Extension.Core.Core Mathlib.Tactic.Inclusion.Extension.Interval Mathlib.Tactic.Inclusion.ExtensionAPI.Attr Mathlib.Tactic.Inclusion.ExtensionAPI.Basic Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Result Mathlib.Tactic.Order.CollectFacts Mathlib.Tactic.Order.Graph.Basic Mathlib.Tactic.Order.Graph.Tarjan Mathlib.Tactic.Order.Preprocessing Mathlib.Tactic.Order.ToInt Mathlib.Tactic.Order Mathlib.Tactic.Peel Mathlib.Tactic.TautoSet Mathlib.Tactic.Zify Mathlib.Testing.Plausible.Sampleable Mathlib.Topology.Defs.Filter Mathlib.Topology.Defs.Sequences

1

---

Declarations diff (regex)

+ liftReflToEq
+ rel_of_eq_and_refl

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ff6c54c).

• +2 new declarations
• −0 removed declarations

+Mathlib.Tactic.liftReflToEq
+Mathlib.Tactic.rel_of_eq_and_refl

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit ff6c54ce33
Reference commit a2ba36bc2c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

Let's open Mathlib here so we don't need to write out Mathlib.Tactic below.

Suggested change

	open Lean Mathlib Meta Elab Tactic

[Vierkantor]

LGTM, thanks!

bors d+

[mathlib-bors]

✌️ kim-em can now approve this pull request until 2026-09-23 09:41 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step