[Merged by Bors] - chore: removing unnecessary imports of Batteries.Logic

[kim-em]

No description provided.

[github-actions]

PR summary 5e64599669

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Use	1	2	+1 (+100.00%)
Mathlib.Init.Data.Quot	4	3	-1 (-25.00%)

Import changes for all files

Files	Import difference
Mathlib.Init.Data.Quot	-1
140 files Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Units Mathlib.Order.RelIso.Basic Mathlib.Data.Countable.Small Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Group.Units Mathlib.Data.Nat.Cast.WithTop Mathlib.Order.WithBot Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Order.Heyting.Regular Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.Circular Mathlib.Order.CompleteLattice Mathlib.Order.Interval.Set.WithBotTop Mathlib.Algebra.Order.Sub.Canonical Mathlib.Order.Bounded Mathlib.Order.RelIso.Group Mathlib.Algebra.Order.Group.MinMax Mathlib.Order.Bounds.Basic Mathlib.Data.Prod.Lex Mathlib.Data.Set.NAry Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Data.Set.List Mathlib.Logic.Relation Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Group.Instances Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Data.Set.Prod Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.Ring.Centralizer Mathlib.Order.Hom.Set Mathlib.Tactic.Use Mathlib.Data.Sigma.Order Mathlib.Order.MinMax Mathlib.Algebra.Ring.Regular Mathlib.Data.Set.Subsingleton Mathlib.Tactic.ApplyFun Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Group.Center Mathlib.Order.GaloisConnection Mathlib.Algebra.Order.Group.PosPart Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Monotone.Odd Mathlib.Order.Hom.Order Mathlib.Algebra.Ring.ULift Mathlib.Order.Hom.Lattice Mathlib.Order.Interval.Set.Image Mathlib.Data.Sum.Lattice Mathlib.Order.SymmDiff Mathlib.Order.PropInstances Mathlib.Data.Set.Function Mathlib.Algebra.Homology.ComplexShape Mathlib.Logic.Equiv.PartialEquiv Mathlib.Order.Directed Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Data.Bundle Mathlib.Order.Monotone.Basic Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Group.Lattice Mathlib.Order.Monotone.Monovary Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.BoundedOrder Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Order.Monotone.Union Mathlib.Data.Bool.Set Mathlib.Algebra.Field.ULift Mathlib.Order.Estimator Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Data.Set.Image Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Order.Hom.Basic Mathlib.Algebra.Order.Group.Prod Mathlib.Data.Setoid.Basic Mathlib.Algebra.Ring.Prod Mathlib.Logic.Small.Basic Mathlib.Algebra.Order.Group.WithTop Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Order.Booleanisation Mathlib.Algebra.Order.Group.Bounds Mathlib.Order.Hom.Bounded Mathlib.Data.Part Mathlib.Order.Heyting.Basic Mathlib.Order.RelClasses Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Data.PSigma.Order Mathlib.Data.Nat.Order.Lemmas Mathlib.Order.LatticeIntervals Mathlib.Data.SetLike.Basic Mathlib.RingTheory.RingInvo Mathlib.Logic.Equiv.Embedding Mathlib.Algebra.Order.Group.Cone Mathlib.Order.Antisymmetrization Mathlib.Algebra.Order.Group.Defs Mathlib.Order.Heyting.Hom Mathlib.Algebra.Order.Field.Defs Mathlib.Order.Iterate Mathlib.Algebra.Order.GroupWithZero.Unbundled Mathlib.Data.Nat.Size Mathlib.Order.IsWellOrderLimitElement Mathlib.Data.PEquiv Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Data.Set.BoolIndicator Mathlib.Data.Sigma.Lex Mathlib.Order.WellFounded Mathlib.Order.Interval.Set.Basic Mathlib.Data.Nat.Log Mathlib.Order.RelIso.Set Mathlib.Algebra.Order.Ring.Prod Mathlib.Order.BooleanAlgebra Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Group.InjSurj Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Order.InitialSeg Mathlib.Order.Lattice Mathlib.Order.Nat Mathlib.Logic.Equiv.Set Mathlib.Algebra.Order.Group.TypeTags Mathlib.Algebra.Order.Monoid.Basic Mathlib.Order.Bounds.OrderIso Mathlib.Data.Set.Basic Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Order.Ring.Cone Mathlib.Data.Sum.Order Mathlib.Algebra.Order.Group.Basic Mathlib.Data.Nat.Set Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Group.Centralizer Mathlib.Logic.Embedding.Set Mathlib.Order.Disjoint	1

---

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/no_lost_declarations.sh short <optional_commit>

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

[grunweg]

Sure, why not? (I'm not sure if/why this is important --- perhaps you have that context and I do not, but it surely doesn't hurt.)
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[j-loreaux]

bors merge

[j-loreaux]

bors r-

[mathlib-bors]

Canceled.

[j-loreaux]

bors d+

[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.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style