mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
/-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`, functorially in `F`.  -/
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              [inst_3 :
                  ∀ (J : CategoryTheory.Limits.MulticospanShape),
                    CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                [inst_4 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                    [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                      (P : CategoryTheory.Functor Cᵒᵖ D) →
                        [∀ (F : CategoryTheory.Functor D E) (X : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                          [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X)
                                (P : CategoryTheory.Functor Cᵒᵖ D),
                                CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                            (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj (J.plusObj P) ≅
                              ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.plusFunctor E)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  s.Nonempty → (a +ᵥ s).Nonempty
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.termĒ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instInhabited.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.instInhabited = { default := ⊥ }
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- A category has finite products if there exists a limit for every diagram
with shape `Discrete J`, where we have `[Finite J]`.

We require this condition only for `J = Fin n` in the definition, then deduce a version for any
`J : Type*` as a corollary of this definition.
 -/
CategoryTheory.Limits.HasFiniteProducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- A multiplicative ring norm is power-multiplicative.  -/
MulRingNorm.isPowMul : ∀ {A : Type u_2} [inst : Ring A] (f : MulRingNorm A), IsPowMul ⇑f
-- Mathlib.RingTheory.Ideal.Colon
/-- If `S ⊆ N₂`, then intersecting with `N₂` does not change the colon ideal.  -/
Submodule.colon_inf_eq_left_of_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N₁ N₂ : Submodule R M} {S : Set M}, S ⊆ ↑N₂ → (N₁ ⊓ N₂).colon S = N₁.colon S
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.trans : ∀ (n m : ℕ) (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_1)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Algebra.IsStandardSmoothOfRelativeDimension n R S] [Algebra.IsStandardSmoothOfRelativeDimension m S T],
  Algebra.IsStandardSmoothOfRelativeDimension (m + n) R T
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The definition of divided powers on `A ⧸ J`. Tagged as noncomputable because it makes use of
`Function.extend`, but under `IsSubDPIdeal hI (J ⊓ I)`, `dividedPowers_unique` proves that no
choices are involved.  -/
DividedPowers.Quotient.dpow : {A : Type u_1} → [inst : CommRing A] → {I : Ideal A} → DividedPowers I → (J : Ideal A) → ℕ → A ⧸ J → A ⧸ J
-- Mathlib.Algebra.Order.Floor.Defs
/-- `Int.ceil a` is the smallest integer `z` such that `a ≤ z`. It is denoted with `⌈a⌉`.  -/
Int.ceil : {α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → α → ℤ
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunLinear_one_tmul_one : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (PolyEquivTensor.toFunLinear R A) (1 ⊗ₜ[R] 1) = 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.instBoundedSpaceStream' : ∀ {α : Type u_1}, BoundedSpace (Stream' α)
-- Init.Data.List.Lemmas
List.head_eq_iff_head?_eq_some : ∀ {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []), xs.head h = a ↔ xs.head? = some a
-- Mathlib.Topology.Algebra.GroupWithZero
Homeomorph.mulRight₀_symm_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c : α)
  (hc : c ≠ 0), ⇑(Homeomorph.mulRight₀ c hc).symm = fun x => x * c⁻¹
-- Init.Data.SInt.Bitwise
ISize.and_not_self : ∀ {a : ISize}, a &&& ~~~a = 0
-- Mathlib.Algebra.Notation.Defs
ite_div_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a b c d : α),
  ((if P then a else b) / if P then c else d) = if P then a / c else b / d
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_ι_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.op.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = (c.π.app CategoryTheory.Limits.WalkingParallelPair.one).op
-- Init.Data.Vector.Lemmas
Vector.mem_ite_empty_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : Vector α 0}, (x ∈ if p then xs else #v[]) ↔ p ∧ x ∈ xs
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.unop_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.LeftHomologyData), h.unop.g' = h.f'.unop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.inlineAttr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Init.Core
instInhabitedPUnit : Inhabited PUnit.{u_1}
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.add_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], (μ + ν).mconv ρ = μ.mconv ρ + ν.mconv ρ
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_of_sub : ∀ {n k : ℕ}, (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_top_bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.IsComplement' ⊥
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (lhsPrec : ℕ) (newPos : String.Pos.Raw) (errorMsg : Option Lean.Parser.Error),
  sizeOf { stx := stx, lhsPrec := lhsPrec, newPos := newPos, errorMsg := errorMsg } =
    1 + sizeOf stx + sizeOf lhsPrec + sizeOf newPos + sizeOf errorMsg
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_intCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (z : ℤ), ⇑↑z = ↑z
-- Mathlib.Algebra.Ring.BooleanRing
/-- Ring isomorphism between `α` considered as a Boolean algebra considered as a Boolean ring and
`α`.  -/
RingEquiv.asBoolRingAsBoolAlg : (α : Type u_4) → [inst : BooleanRing α] → AsBoolRing (AsBoolAlg α) ≃+* α
-- Lean.MetavarContext
/-- A delayed assignment for a metavariable `?m`. It represents an assignment of the form `?m := (fun fvars => (mkMVar mvarIdPending))`.
`mvarIdPending` is a `syntheticOpaque` metavariable that has not been synthesized yet. The delayed assignment becomes a real one
as soon as `mvarIdPending` has been fully synthesized.
`fvars` are variables in the `mvarIdPending` local context.

See the comment below `assignDelayedMVar ` for the rationale of delayed assignments.

Recall that we use a locally nameless approach when dealing with binders. Suppose we are
trying to synthesize `?n` in the expression `e`, in the context of `(fun x => e)`.
The metavariable `?n` might depend on the bound variable `x`. However, since we are locally nameless,
the bound variable `x` is in fact represented by some free variable `fvar_x`. Thus, when we exit
the scope, we must rebind the value of `fvar_x` in `?n` to the de-bruijn index of the bound variable `x`.
 -/
Lean.DelayedMetavarAssignment : Type
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `(f : A ⟶ B) ⋔ (W ⟶ ⋆) ≅ (B ⟹ W ⟶ A ⟹ W)` in a monoidal closed
category with pullbacks and a terminal object.  -/
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [inst_3 : CategoryTheory.MonoidalClosed C] →
          (X : CategoryTheory.Arrow C) →
            {T : C} →
              (t : CategoryTheory.Limits.IsTerminal T) →
                {W : C} →
                  (Opposite.op X ⋔ CategoryTheory.Arrow.mk (t.from W)) ≅
                    CategoryTheory.Arrow.mk ((CategoryTheory.MonoidalClosed.pre X.hom).app W)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_const_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {c : ENNReal}, c ≠ ⊤ → ∫⁻ (x : α), c ∂μ < ⊤
-- Mathlib.Data.Rat.Cast.OfScientific
instLawfulOfScientificOfCharZero : ∀ {K : Type u_1} [inst : Field K] [CharZero K], Lean.Grind.LawfulOfScientific K
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.ae_dirac_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α),
  MeasureTheory.ae (MeasureTheory.Measure.dirac a) = pure a
-- Init.Data.SInt.Bitwise
Int16.neg_one_or : ∀ {a : Int16}, -1 ||| a = -1
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.getD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (a : α) (fallback : β a)
  (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getCastD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0 : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.CostructuredArrow.projectQuotient_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [inst_2 : CategoryTheory.Limits.HasFiniteColimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T}
  {P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} (f : P ⟶ Opposite.op A) [inst_4 : CategoryTheory.Mono f],
  CategoryTheory.CostructuredArrow.projectQuotient (CategoryTheory.Subobject.mk f) =
    CategoryTheory.Subobject.mk f.unop.left.op
-- Init.Prelude
/-- Returns the provided value `a`, ignoring the reader monad's local value. Typically used via
`Pure.pure`.
 -/
ReaderT.pure : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → α → ReaderT ρ m α
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], LipschitzWith 2 (Function.uncurry dist)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.sq_norm_lt_one : ∀ (z : Complex.UnitDisc), ‖↑z‖ ^ 2 < 1
-- Mathlib.Algebra.Group.Center
Set.centralizer_eq_univ : ∀ (M : Type u_1) {S : Set M} [inst : CommSemigroup M], S.centralizer = Set.univ
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.restrict_empty : ∀ {α : Type u_1} (M : Matroid α), M.restrict ∅ = Matroid.emptyOn α
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- Given an embedding `e : Embedding c c'` of complex shapes which satisfy `e.IsTruncGE`,
this is the (canonical) truncation functor
`HomologicalComplex C c' ⥤ HomologicalComplex C c'`.  -/
ComplexShape.Embedding.truncGEFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [e.IsTruncGE] →
            (C : Type u_4) →
              [inst : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [CategoryTheory.Limits.HasZeroObject C] →
                    [CategoryTheory.CategoryWithHomology C] →
                      CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c')
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- Equivalent precoherent categories give equivalent coherent toposes.
 -/
CategoryTheory.Equivalence.sheafCongrPrecoherent : {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] →
        [inst_2 : CategoryTheory.Precoherent C] →
          (A : Type u_3) →
            [inst_3 : CategoryTheory.Category.{v_3, u_3} A] →
              (e : C ≌ D) →
                CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌
                  CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.subset_pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, IsPathConnected F → x ∈ F → F ⊆ pathComponent x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool} {k : α},
  (Std.DTreeMap.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).get!
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getElem_sdiv.match_1.eq_3 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_3 ()
-- Mathlib.Topology.Perfect
Preperfect.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] (C : Set α), Preperfect C = ∀ x ∈ C, AccPt x (Filter.principal C)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v : P`, we have
`f.lift hg z = v ↔ g x = g y * v`, where `x : M, y ∈ S` are such that `z * f y = f x`.  -/
Submonoid.LocalizationMap.lift_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (v : P),
  (f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 * v
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_eq : ∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
  (MvPolynomial.monomial s) a = MvPolynomial.C a * s.prod fun n e => MvPolynomial.X n ^ e
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toBoundedContinuousFunction_le : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), ‖f.toBoundedContinuousFunction‖ ≤ (SchwartzMap.seminorm ℝ 0 0) f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ArbitraryShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Order.PartialSups
Monotone.partialSups_eq : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  {f : ι → α}, Monotone f → ⇑(partialSups f) = f
-- Init.Data.Vector.MapIdx
Vector.mapIdx_setIfInBounds : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Vector α n} {i : ℕ} {a : α},
  Vector.mapIdx f (xs.setIfInBounds i a) = (Vector.mapIdx f xs).setIfInBounds i (f i a)
-- Mathlib.AlgebraicGeometry.Restrict
/-- The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.
 -/
AlgebraicGeometry.morphismRestrictStalkMap : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (x : ↥↑((TopologicalSpace.Opens.map f.base).obj U)) →
        CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap (f ∣_ U) x) ≅
          CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f ↑x)
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β} {s t : Set β}, s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g
-- Mathlib.Topology.Sets.Compacts
/-- Reinterpret a nonempty compact as a closed set.  -/
TopologicalSpace.NonemptyCompacts.toCloseds : {α : Type u_1} →
  [inst : TopologicalSpace α] → [T2Space α] → TopologicalSpace.NonemptyCompacts α → TopologicalSpace.Closeds α
-- Mathlib.Data.Part
Part.mem_some_iff : ∀ {α : Type u_1} {a b : α}, b ∈ Part.some a ↔ b = a
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the modules in which constants used in the current file were defined.

Note that this will *not* account for tactics and syntax used in the file,
so the results may not suffice as imports.
 -/
Lean.Environment.requiredModules : Lean.Environment → Lean.NameSet
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_def : ∀ (x : Lean.Grind.CommRing.Expr),
  x.toPoly =
    match x with
    | Lean.Grind.CommRing.Expr.num k => Lean.Grind.CommRing.Poly.num k
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num k
    | Lean.Grind.CommRing.Expr.natCast k => Lean.Grind.CommRing.Poly.num ↑k
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => a.toPoly.combine b.toPoly
    | a.mul b => a.toPoly.mul b.toPoly
    | a.neg => Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly
    | a.sub b => a.toPoly.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly)
    | a.pow k =>
      bif k == 0 then Lean.Grind.CommRing.Poly.num 1
      else
        match a with
        | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (n ^ k)
        | Lean.Grind.CommRing.Expr.intCast n => Lean.Grind.CommRing.Poly.num (n ^ k)
        | Lean.Grind.CommRing.Expr.natCast n => Lean.Grind.CommRing.Poly.num (↑n ^ k)
        | Lean.Grind.CommRing.Expr.var x =>
          Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
        | x => a.toPoly.pow k
-- Lean.Syntax
Lean.Syntax.antiquotKinds : Lean.Syntax → List (Lean.SyntaxNodeKind × Bool)
-- Lean.Elab.Tactic.RCases
/-- Parses a `Syntax` into the `RCasesPatt` type used by the `RCases` tactic.  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.parse : Lean.Syntax → Lean.MetaM Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_intCast_div : ∀ {x : ℝ} (m : ℤ), Irrational (↑m / x) → Irrational x
-- Mathlib.Order.Defs.Unbundled
MaximalFor.le_of_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {P : ι → Prop} {f : ι → α} {i j : ι},
  MaximalFor P f i → P j → f i ≤ f j → f j ≤ f i
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinset.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (i : α)
  (h_1 : (i : α) → motive (FirstOrder.Language.var i))
  (h_2 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.var i with
    | FirstOrder.Language.var i => h_1 i
    | FirstOrder.Language.func _f ts => h_2 l _f ts) =
    h_1 i
-- Std.Time.Date.PlainDate
Std.Time.instDecidableEqPlainDate : DecidableEq Std.Time.PlainDate
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A version of `padicValRat.pow` for `padicValNat`.  -/
padicValNat.pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (a n : ℕ), padicValNat p (a ^ n) = n * padicValNat p a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.instMonoRightHomologyι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology], CategoryTheory.Mono S.rightHomologyι
-- Mathlib.Computability.Primrec.List
/-- Filtering a list for elements that satisfy a decidable predicate is primitive recursive.  -/
Primrec.listFilter : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  PrimrecPred p → Primrec fun L => List.filter (fun x => decide (p x)) L
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc : ∀ {R : CommRingCat} (x : PrimeSpectrum ↑R) {Z : CommRingCat} (h : CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.stalkIso R x).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
      (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))) h)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulAction.eq_1 : ∀ {M : Type u_1} {X : Type u_2} [inst : Monoid M] [inst_1 : MulAction M X] [inst_2 : TopologicalSpace X]
  [inst_3 : ContinuousConstSMul M X],
  SeparationQuotient.instMulAction = Function.Surjective.mulAction SeparationQuotient.mk ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ {Z : C} (h : X.obj { len := n + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.σ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.convexCombPair_iConvexComb_iConvexComb.match_1_3.splitter : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    (motive : (a : Fin 0) → ![ULift.{max u_1 u_2, u_1} J₁, ULift.{max u_1 u_2, u_2} J₂] a.succ.succ → Sort u_3) →
      (a : Fin 0) → (a_1 : ![ULift.{max u_1 u_2, u_1} J₁, ULift.{max u_1 u_2, u_2} J₂] a.succ.succ) → motive a a_1
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_sInter : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)},
  (∀ s ∈ S, IsClopen s) → IsClopen (⋂₀ S)
-- Mathlib.Order.CompleteLattice.Basic
iSup_comm : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {f : ι → ι' → α},
  ⨆ i, ⨆ j, f i j = ⨆ j, ⨆ i, f i j
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
divisorsAntidiagonalFactors_eq : ∀ {n : ℕ+} (x : ↥(↑n).divisorsAntidiagonal),
  ↑(divisorsAntidiagonalFactors n x).1 * ↑(divisorsAntidiagonalFactors n x).2 = ↑n
-- Init.Data.SInt.Bitwise
Int64.ne_not_self : ∀ {a : Int64}, a ≠ ~~~a
-- Mathlib.Data.EReal.Operations
EReal.mul_eq_bot : ∀ (a b : EReal), a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤