[Merged by Bors] - chore: replace 'import Batteries' with finer imports

[kim-em]

No description provided.

[github-actions]

PR summary 0379d5fc92

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Basic	13	12	-1 (-7.69%)
Mathlib.Tactic.Lift	15	16	+1 (+6.67%)
Mathlib.Tactic.FunProp.Core	112	116	+4 (+3.57%)
Mathlib.Data.Seq.WSeq	273	281	+8 (+2.93%)
Mathlib.Tactic.FunProp.Theorems	111	114	+3 (+2.70%)
Mathlib.Data.Seq.Seq	270	277	+7 (+2.59%)
Mathlib.Data.List.Range	326	334	+8 (+2.45%)
Mathlib.Data.PEquiv	211	216	+5 (+2.37%)
Mathlib.Data.Set.Image	215	220	+5 (+2.33%)
Mathlib.Data.List.Join	265	271	+6 (+2.26%)
Mathlib.Data.List.ProdSigma	266	272	+6 (+2.26%)
Mathlib.Data.List.Defs	48	49	+1 (+2.08%)
Mathlib.Data.List.Basic	264	269	+5 (+1.89%)
Mathlib.Testing.SlimCheck.Gen	333	339	+6 (+1.80%)
Mathlib.Tactic.RewriteSearch	502	510	+8 (+1.59%)
Mathlib.CategoryTheory.Limits.IsLimit	315	320	+5 (+1.59%)
Mathlib.Data.Fin.Tuple.Basic	315	320	+5 (+1.59%)
Mathlib.Data.PFun	333	338	+5 (+1.50%)
Mathlib.Testing.SlimCheck.Functions	671	681	+10 (+1.49%)
Mathlib.Order.RelClasses	135	137	+2 (+1.48%)
Mathlib.Data.Fin.Basic	313	317	+4 (+1.28%)
Mathlib.Tactic.Linarith.Oracle.FourierMotzkin	491	497	+6 (+1.22%)
Mathlib.Data.Rat.Defs	250	253	+3 (+1.20%)
Mathlib.Algebra.Group.Pi.Basic	98	99	+1 (+1.02%)
Mathlib.Order.Basic	116	117	+1 (+0.86%)
Mathlib.Control.Bifunctor	237	239	+2 (+0.84%)
Mathlib.CategoryTheory.Pi.Basic	274	276	+2 (+0.73%)
Mathlib.Combinatorics.Quiver.Symmetric	140	141	+1 (+0.71%)

Import changes for all files

Files	Import difference
Too many changes (4287)!

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[mattrobball]

bors delegate+

[mathlib-bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kim-em]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Merge conflict.

[kim-em]

bors merge

[mathlib-bors]

Canceled.

[kim-em]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed:

• Build

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style