mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.ScaleRoots
/-- Multiplication and `scaleRoots` commute up to a power of `r`. The factor disappears if we
assume that the product of the leading coeffs does not vanish. See `Polynomial.mul_scaleRoots'`.  -/
Polynomial.mul_scaleRoots : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.fixedSubmodule_comp_inf_fixedSubmodule_le : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (f g : V →ₗ[R] V),
  (f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule ≤ f.fixedSubmodule
-- Init.Data.Int.Order
Int.lt.dest : ∀ {a b : ℤ}, a < b → ∃ n, a + ↑n.succ = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.Subcomplex.instHasDimensionLTToSSet : ∀ {X : SSet} (d : ℕ) [X.HasDimensionLT d] (A : X.Subcomplex), A.toSSet.HasDimensionLT d
-- Mathlib.Order.Interval.Finset.Box
Finset.box_zero : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α] [inst_3 : DecidableEq α],
  Finset.box 0 = {0}
-- Mathlib.Data.Set.Image
Set.preimage_iterate_eq : ∀ {α : Type u_1} {f : α → α} {n : ℕ}, Set.preimage f^[n] = (Set.preimage f)^[n]
-- Init.Data.AC
Lean.Data.AC.EvalInformation.evalVar : {α : Sort u} → {β : Sort v} → [self : Lean.Data.AC.EvalInformation α β] → α → ℕ → β
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α], -∅ = ∅
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A continuous function with compact support is in L^p.  -/
Continuous.memLp_of_hasCompactSupport : ∀ {E : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup E] {X : Type u_3} [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [OpensMeasurableSpace X] {f : X → E}, Continuous f → HasCompactSupport f → MeasureTheory.MemLp f p μ
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Adjunction.fromKleisli_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (X : CategoryTheory.Kleisli T),
  (CategoryTheory.Kleisli.Adjunction.fromKleisli T).obj X = T.obj X.of
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_le_mul_of_one_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : MulOneClass α] [MulLeftMono α] {a b : α}, 1 ≤ b → min a b ≤ a * b
-- Lean.Meta.Closure
Lean.Meta.Closure.mkBinding : Bool → Array Lean.LocalDecl → Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
instMeasurableEqOfMeasurableSingletonClassOfCountable : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [Countable α], MeasurableEq α
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_2.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_3 t (Lean.Elab.InfoTree.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
AlternatingMap.constOfIsEmpty.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ι : Type u_7) [inst_5 : IsEmpty ι] (m m_1 : N),
  m = m_1 → AlternatingMap.constOfIsEmpty R M ι m = AlternatingMap.constOfIsEmpty R M ι m_1
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G],
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftPropOn Q (↑(chartAt H x).symm) (chartAt H x).target
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A subrepresentation of `G` of the `A`-module `W` is a submodule of `W`
which is stable under the `G`-action.
 -/
Subrepresentation : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid W] → [inst_3 : Module A W] → Representation A G W → Type u_3
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.whiskerLeft_def : ∀ (R : Type u) [inst : CommRing R] (X x x_1 : HopfAlgCat R) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = HopfAlgCat.ofHom (BialgHom.lTensor X.carrier f.toBialgHom')
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- A charted space has an atlas in a groupoid `G` if the change of coordinates belong to the
groupoid.  -/
HasGroupoid : {H : Type u_5} →
  [inst : TopologicalSpace H] →
    (M : Type u_6) → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → StructureGroupoid H → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_insert_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insert k v).toArray.Perm ((Array.filter (fun x => decide ¬(k == x.fst) = true) t.toArray).push ⟨k, v⟩)
-- Init.Data.BitVec.Basic
/-- Returns the `i`th least significant bit, or `none` if `i ≥ w`.  -/
BitVec.getLsb? : {w : ℕ} → BitVec w → ℕ → Option Bool
-- Qq.ForLean.ToExpr
instToExprBinderInfo_qq : Lean.ToExpr Lean.BinderInfo
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_iff_comp_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a : 𝕜}, DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (-x)) (-a)
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.ExtTreeMap.getEntryGE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α × β
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer.eq_1 : ∀ {G : Type u_1} [inst : Group G] (s : Set G),
  Subgroup.centralizer s = { toSubmonoid := Submonoid.centralizer s, inv_mem' := ⋯ }
-- Mathlib.Analysis.Analytic.IteratedFDeriv
AnalyticOn.domDomCongr_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {x : E},
  AnalyticOn 𝕜 f s →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)),
          ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x
-- Lean.Data.SSet
Lean.SSet.contains : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SSet α → α → Bool
-- Mathlib.MeasureTheory.Function.L2Space
integral_inner : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [CompleteSpace E] [inst_4 : NormedSpace ℝ E]
  {f : α → E}, MeasureTheory.Integrable f μ → ∀ (c : E), ∫ (x : α), inner 𝕜 c (f x) ∂μ = inner 𝕜 c (∫ (x : α), f x ∂μ)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.instInhabited : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Inhabited (Geometry.SimplicialComplex 𝕜 E)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa_sq : ∀ {n : ℕ} (i : ZMod (2 * n)), QuaternionGroup.xa i ^ 2 = QuaternionGroup.a ↑n
-- Init.Data.SInt.Basic
instComplementInt64 : Complement Int64
-- Lean.Elab.Util
/-- If `ref` does not have position information, then try to use macroStack  -/
Lean.Elab.getBetterRef : Lean.Syntax → Lean.Elab.MacroStack → Lean.Syntax
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_finset_inf : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} {s : Finset ι} {f : ι → Ideal R} {i : ι},
  i ∈ s → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).radical = (f i).radical
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A)
  (x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)
      (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.Γgerm x) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
        ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrictStalkIso ⋯ x).inv)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.associator_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ M₃ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).inv
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.adj_of_infix_support : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v}, [u', v'] <:+: p.support → G.Adj u' v'
-- Mathlib.Topology.Category.Compactum
Compactum.instCreatesLimitsForget : CategoryTheory.CreatesLimits Compactum.forget
-- Batteries.Recycling.RBTree.Basic
/-- Changes the color of the root to `black`.  -/
RBTree.RBNode.setBlack : {α : Type u_1} → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
integrable_one_add_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {r : ℝ},
  ↑(Module.finrank ℝ E) < r → MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-r)) μ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_prop_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.endsWith P = true ↔ ∃ (h : s.endPos ≠ s.startPos), P ((s.endPos.prev h).get ⋯)
-- Mathlib.Algebra.Group.Action.End
Function.End.smul_def : ∀ {α : Type u_5} (f : Function.End α) (a : α), f • a = f a
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasColimitsOfShape : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.ShortComplex C)
-- Mathlib.RepresentationTheory.Character
/-- The character of a representation `ρ : Representation k G V` is the function associating to
`g : G` the trace of the linear map `ρ g`.  -/
Representation.character : {G : Type u_1} →
  {k : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Field k] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → G → k
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprStdWall.repr : Std.Time.TimeZone.StdWall → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.PSLAction.toPermHom.eq_1 : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  Projectivization.PSLAction.toPermHom =
    QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup ι K))
      (MulAction.toPermHom (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))) ⋯
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat⌜_⌝» : Lean.ParserDescr
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkImpCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.instMonadMCtxM : Lean.MonadMCtx Lean.DependsOn.M✝
-- Mathlib.CategoryTheory.Filtered.Basic
/-- For every universe `w`, `C` is filtered if and only if every finite diagram in `C` with shape
in `w` admits a cocone.  -/
CategoryTheory.IsFiltered.iff_cocone_nonempty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsFiltered C ↔
    ∀ {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)
-- Std.Http.Data.Body.Stream
Std.Http.Body.instCoeContextAsyncResponseStreamAny : Coe (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Stream))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.BisimO.eq_1 : ∀ {α : Type u} (R : Stream'.WSeq α → Stream'.WSeq α → Prop),
  Stream'.WSeq.BisimO R = Stream'.WSeq.LiftRelO (fun x1 x2 => x1 = x2) R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {a : α},
  Std.ExtDTreeMap.Const.get! ∅ a = default
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp a (b + m • p) = toIocMod hp a b
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_dual : ∀ {α : Type u_1} [inst : PartialOrder α] (s : NonemptyInterval α), ↑(NonemptyInterval.dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Rci.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Rci.HasRcoIntersection α}
  [self : Std.Rci.LawfulRcoIntersection α] {a : α} {r : Std.Rci α} {s : Std.Rco α},
  a ∈ Std.Rci.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- `f : ContDiffBump c`, where `c` is a point in a normed vector space, is a
bundled smooth function such that

- `f` is equal to `1` in `Metric.closedBall c f.rIn`;
- `support f = Metric.ball c f.rOut`;
- `0 ≤ f x ≤ 1` for all `x`.

The structure `ContDiffBump` contains the data required to construct the function:
real numbers `rIn`, `rOut`, and proofs of `0 < rIn < rOut`. The function itself is available through
`CoeFun` when the space is nice enough, i.e., satisfies the `HasContDiffBump` typeclass.  -/
ContDiffBump : {E : Type u_1} → E → Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.lanCompIsoOfPreserves_inv_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C)
  [inst_4 : G.PreservesLeftKanExtensions L] [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] (X : CategoryTheory.Functor A B),
  (G.lanCompIsoOfPreserves L).inv.app X = (G.leftKanExtensionCompIsoOfPreserves X L).inv
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- Auxiliary function for Szemerédi's regularity lemma. Blowing up a partition of size `n` during
the induction results in a partition of size at most `stepBound n`.  -/
SzemerediRegularity.stepBound : ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J] (F : CategoryTheory.Functor J (Type u)),
  CategoryTheory.Limits.HasLimit F
-- Init.Data.UInt.BasicAux
/-- Converts 8-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.toUInt32 : UInt8 → UInt32
-- Init.Data.Int.DivMod.Lemmas
Int.mul_ediv_mul_of_pos_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), 0 < b → a * b / (c * b) = a / c
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.copy.dropWhile pat).copy = (s.dropWhile pat).copy
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toLinearOrder : {α : Type u_1} → [i : CompleteLinearOrder α] → LinearOrder α
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.preΨ n = preNormEDS (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_comp_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : α → M) (g : α → N), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerived.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) (n : ℕ),
  CategoryTheory.NatTrans.rightDerived α n =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α)
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
-- Mathlib.Data.Stream.Init
Stream'.append_left_injective : ∀ {α : Type u} (x y : List α) (a b : Stream' α), x ++ₛ a = y ++ₛ b → x.length = y.length → x = y
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu'_eq_sum_Ioc_of_ne : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] {a b : α},
  a ≠ b → (IncidenceAlgebra.mu'✝ 𝕜) a b = -∑ x ∈ Finset.Ioc a b, (IncidenceAlgebra.mu'✝ 𝕜) x b
-- Init.Data.Iterators.Basic
/-- Converts an `IterM.Step` into an `Iter.Step`.
 -/
Std.IterM.Step.toPure : {α β : Type w} → [inst : Std.Iterator α Id β] → {it : Std.IterM Id β} → it.Step → it.toIter.Step
-- Std.Data.HashMap.Basic
Std.HashMap.instForInProdOfMonad : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → {m : Type w → Type w'} → [Monad m] → ForIn m (Std.HashMap α β) (α × β)
-- Mathlib.Analysis.Convex.Segment
insert_endpoints_openSegment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (x y : E), insert x (insert y (openSegment 𝕜 x y)) = segment 𝕜 x y
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_conj_symm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_union_of_notMem : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α]
  [inst_3 : DecidableEq α], a ∉ upperClosure ↑s → a ∉ upperClosure ↑t → (s ∪ t).truncatedInf a = ⊥
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (X : CategoryTheory.Sheaf J A) (X_1 : (CategoryTheory.Sheaf J A)ᵒᵖ)
  (a : (CategoryTheory.yoneda.obj X).obj X_1),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.inv.app X).app X_1))
      a =
    Equiv.ulift.toIso.hom.hom'
      ((CategoryTheory.CategoryStruct.comp Equiv.ulift.toIso.inv
            (((CategoryTheory.fullyFaithfulSheafToPresheaf J A).compUliftYonedaCompWhiskeringLeft.inv.app X).app
              X_1)).hom'
        a)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.comp_def : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {X Y Z : CategoryTheory.BasedCategory 𝒮}
  (F : CategoryTheory.BasedFunctor X Y) (G : CategoryTheory.BasedFunctor Y Z),
  CategoryTheory.CategoryStruct.comp F G = F.comp G
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_if : ∀ {α : Type u_1} {p : Prop} [inst : Decidable p] (s : Set α), ⋂ (_ : p), s = if p then s else Set.univ
-- Mathlib.LinearAlgebra.Ray
Module.Ray.map_symm : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (e : M ≃ₗ[R] N), (Module.Ray.map e).symm = Module.Ray.map e.symm
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n → (UInt32.ofNatClamp n).toBitVec = (UInt32.size - 1)#'UInt32.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_eq_bot : ∀ {M : Type u_2} [inst : AddZeroClass M] {S : AddSubmonoid M}, S.op = ⊥ ↔ S = ⊥
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasInaccessiblePattern : Lean.Meta.Match.Problem → Bool
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (f : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {𝒢' : CategoryTheory.Sheaf K A} (g : ℱ' ⟶ 𝒢'),
  CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom
      (CategoryTheory.CategoryStruct.comp f (G.op.whiskerLeft g.hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom f) g.hom