/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module -- shake: keep-all --deprecated_module: ignore public import FormalConjecturesForMathlib.Algebra.GCDMonoid.Finset public import FormalConjecturesForMathlib.Algebra.Group.Action.Pointwise.Set.Basic public import FormalConjecturesForMathlib.Algebra.Group.GrowthFunction public import FormalConjecturesForMathlib.Algebra.Group.Indicator public import FormalConjecturesForMathlib.Algebra.MvPolynomial.PoissonBracket public import FormalConjecturesForMathlib.Algebra.MvPolynomial.RegularFunction public import FormalConjecturesForMathlib.Algebra.Order.Group.Pointwise.Interval public import FormalConjecturesForMathlib.Algebra.Polynomial.Algebra public import FormalConjecturesForMathlib.Algebra.Polynomial.Basic public import FormalConjecturesForMathlib.Algebra.Polynomial.HasseDeriv public import FormalConjecturesForMathlib.Algebra.Powerfree public import FormalConjecturesForMathlib.Algebra.QuadraticAlgebra.Instances public import FormalConjecturesForMathlib.AlgebraicGeometry.ProjectiveSpace public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets public import FormalConjecturesForMathlib.Analysis.HasGaps public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum public import FormalConjecturesForMathlib.Analysis.Real.Cardinality public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot public import FormalConjecturesForMathlib.Combinatorics.AP.Basic public import FormalConjecturesForMathlib.Combinatorics.Additive.Basis public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution public import FormalConjecturesForMathlib.Combinatorics.Additive.Coset public import FormalConjecturesForMathlib.Combinatorics.Additive.DifferenceBasis public import FormalConjecturesForMathlib.Combinatorics.Additive.RestrictedSumset public import FormalConjecturesForMathlib.Combinatorics.Additive.VCDim public import FormalConjecturesForMathlib.Combinatorics.Basic public import FormalConjecturesForMathlib.Combinatorics.Digraph.Tournament public import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform public import FormalConjecturesForMathlib.Combinatorics.LatinSquare public import FormalConjecturesForMathlib.Combinatorics.LimitObjects.Graphon public import FormalConjecturesForMathlib.Combinatorics.LimitObjects.Tournamenton public import FormalConjecturesForMathlib.Combinatorics.Ramsey public import FormalConjecturesForMathlib.Combinatorics.Ramsey.Diagonal public import FormalConjecturesForMathlib.Combinatorics.SetFamily.PropertyB public import FormalConjecturesForMathlib.Combinatorics.SetFamily.Sunflower public import FormalConjecturesForMathlib.Combinatorics.SetFamily.UnionFree public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim public import FormalConjecturesForMathlib.Combinatorics.SetTheory.PartitionRelation public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Circumference public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Coloring.Vertex public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CompleteGraphEdgeCount public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Cvetkovic public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Cycle public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CycleRank public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Eccentricity public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.EdgeColouring public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.FractionalAlpha public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LargestInducedTree public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LovaszTheta public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Matching public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.PathCover public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.QuasiLineGraph public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SpanningTree public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SubgraphIsomorphism public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SzegedIndex public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Temperature public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WellTotallyDominated public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WienerIndex public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram public import FormalConjecturesForMathlib.Computability.BitstringEncoding public import FormalConjecturesForMathlib.Computability.Complexity public import FormalConjecturesForMathlib.Computability.DFA public import FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers public import FormalConjecturesForMathlib.Computability.TuringMachine.Notation public import FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine public import FormalConjecturesForMathlib.Data.Bool.Basic public import FormalConjecturesForMathlib.Data.Finset.Card public import FormalConjecturesForMathlib.Data.Finset.Powerset public import FormalConjecturesForMathlib.Data.Finset.ReciprocalSum public import FormalConjecturesForMathlib.Data.Int.IntermediateValue public import FormalConjecturesForMathlib.Data.Int.Order.Basic public import FormalConjecturesForMathlib.Data.Nat.Factorization.Basic public import FormalConjecturesForMathlib.Data.Nat.Full public import FormalConjecturesForMathlib.Data.Nat.Init public import FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac public import FormalConjecturesForMathlib.Data.Nat.PerfectPower public import FormalConjecturesForMathlib.Data.Nat.Prime.Composite public import FormalConjecturesForMathlib.Data.Nat.Prime.Defs public import FormalConjecturesForMathlib.Data.Nat.Prime.Finset public import FormalConjecturesForMathlib.Data.Nat.Prime.Infinite public import FormalConjecturesForMathlib.Data.Nat.Squarefree public import FormalConjecturesForMathlib.Data.Real.Constants public import FormalConjecturesForMathlib.Data.Real.NearestInt public import FormalConjecturesForMathlib.Data.Set.Density public import FormalConjecturesForMathlib.Data.Set.Interval public import FormalConjecturesForMathlib.Data.Set.Triplewise public import FormalConjecturesForMathlib.Data.Sym.Sym2 public import FormalConjecturesForMathlib.Data.ZMod.Fp public import FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet public import FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs public import FormalConjecturesForMathlib.Geometry.Euclidean public import FormalConjecturesForMathlib.Geometry.Metric public import FormalConjecturesForMathlib.Geometry.«2d» public import FormalConjecturesForMathlib.Geometry.«3d» public import FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util public import FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic public import FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup public import FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup public import FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate public import FormalConjecturesForMathlib.NumberTheory.AdditionChain public import FormalConjecturesForMathlib.NumberTheory.AdditiveComplement public import FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete public import FormalConjecturesForMathlib.NumberTheory.AlmostPrime public import FormalConjecturesForMathlib.NumberTheory.Amicable public import FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes public import FormalConjecturesForMathlib.NumberTheory.Carmichael public import FormalConjecturesForMathlib.NumberTheory.CoveringSystem public import FormalConjecturesForMathlib.NumberTheory.DiophantineApproximation.ZNumber public import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic public import FormalConjecturesForMathlib.NumberTheory.Divisors public import FormalConjecturesForMathlib.NumberTheory.Harmonic public import FormalConjecturesForMathlib.NumberTheory.Lacunary public import FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic public import FormalConjecturesForMathlib.NumberTheory.NormalNumber public import FormalConjecturesForMathlib.NumberTheory.NumberField.FundamentalDiscriminant public import FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic public import FormalConjecturesForMathlib.NumberTheory.PisotNumber public import FormalConjecturesForMathlib.NumberTheory.PracticalNumbers public import FormalConjecturesForMathlib.NumberTheory.PrimeGap public import FormalConjecturesForMathlib.NumberTheory.Primitive public import FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber public import FormalConjecturesForMathlib.NumberTheory.SmoothScale public import FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes public import FormalConjecturesForMathlib.Order.Bounds.Basic public import FormalConjecturesForMathlib.Order.Filter.Cofinite public import FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset public import FormalConjecturesForMathlib.Order.Interval.Finset.Basic public import FormalConjecturesForMathlib.Order.Interval.Finset.Nat public import FormalConjecturesForMathlib.Order.Nat public import FormalConjecturesForMathlib.Order.Unimodular public import FormalConjecturesForMathlib.Probability.FiniteMethod public import FormalConjecturesForMathlib.RingTheory.Ideal.Basic public import FormalConjecturesForMathlib.RingTheory.Ideal.Defs public import FormalConjecturesForMathlib.RingTheory.Ideal.Maximal public import FormalConjecturesForMathlib.RingTheory.Noetherian.Defs public import FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic public import FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum public import FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph public import FormalConjecturesForMathlib.Tactic.Linter.Term public import FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract public import FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Group public import FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Order public import FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Real public import FormalConjecturesForMathlib.Topology.Discrete public import FormalConjecturesForMathlib.Topology.GDelta public import FormalConjecturesForMathlib.Topology.Homogeneous public import FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension public import FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated