mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hasForgetToAddMagmaCat.eq_1 : AddSemigrp.hasForgetToAddMagmaCat =
  {
    forget₂ :=
      { obj := fun R => AddMagmaCat.of ↑R, map := fun {X Y} f => AddMagmaCat.ofHom (AddSemigrp.Hom.hom f),
        map_id := AddSemigrp.hasForgetToAddMagmaCat._proof_1, map_comp := @AddSemigrp.hasForgetToAddMagmaCat._proof_2 },
    forget_comp := AddSemigrp.hasForgetToAddMagmaCat._proof_4 }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.covconv : ∀ {N : Type u_2} {r : N → N → Prop} [inst : AddGroup N] [CovariantClass N N (fun x1 x2 => x1 + x2) r],
  ContravariantClass N N (fun x1 x2 => x1 + x2) r
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi.eq_1 : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t')
  (val : Fin n) (h : val ∈ SimpleGraph.ErdosStone.filter✝ K t),
  SimpleGraph.ErdosStone.filter.pi✝ K ⟨val, h⟩ = ⟨fun p hp => ⋯.choose, ⋯⟩
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instLEInftyOfNatWithTopENat_2 : ENat.LEInfty 0
-- Mathlib.Order.WithBot
WithTop.lt_iff_exists : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α}, y < x ↔ ∃ b, y = ↑b ∧ ∀ (a : α), x = ↑a → b < a
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.prod` as a `LinearIsometryEquiv`.  -/
ContinuousAlternatingMap.prodLIE : (𝕜 : Type u) →
  (E : Type wE) →
    (F : Type wF) →
      (G : Type wG) →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [inst_7 : Fintype ι] → E [⋀^ι]→L[𝕜] F × E [⋀^ι]→L[𝕜] G ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] (F × G)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α}, t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospan_map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (a : J.R),
  I.multicospan.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst a) = I.fst a
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.inr_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B] (x : B), (NonUnitalStarAlgHom.inr R A B) x = (0, x)
-- Mathlib.Algebra.Module.SpanRank
Submodule.instNonemptySubtypeSetEqSpan : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  Nonempty { s // Submodule.span R s = p }
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.adj : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.Adj x y
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.coe_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  ↑(AlgebraicGeometry.Scheme.Hom.opensRange f) = Set.range ⇑f
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- See `intervalIntegrable_cpow` for a version applying to any locally finite measure, but with a
stronger hypothesis on `r`.  -/
intervalIntegral.intervalIntegrable_cpow' : ∀ {a b : ℝ} {r : ℂ}, -1 < r.re → IntervalIntegrable (fun x => ↑x ^ r) MeasureTheory.volume a b
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.mk : {α : Type u} →
  [τ : TopologicalSpace α] →
    [toEDist : EDist α] →
      (edist_self : ∀ (x : α), edist x x = 0) →
        (edist_comm : ∀ (x y : α), edist x y = edist y x) →
          (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) →
            (uniformSpaceOfEDist edist edist_self edist_comm edist_triangle).toTopologicalSpace ≤ τ →
              (∀ (x : α) (r : ENNReal), IsOpen (Subtype.val ⁻¹' Metric.eball x r)) → WeakPseudoEMetricSpace α
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact₂_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 2)
  (w :
    CategoryTheory.CategoryStruct.comp
        (S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4)
        (S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_5) =
      0),
  { X₁ := S.obj ⟨0, ⋯⟩, X₂ := S.obj ⟨1, ⋯⟩, X₃ := S.obj ⟨2, ⋯⟩,
        f :=
          S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2
            CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4,
        g :=
          S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4
            CategoryTheory.ComposableArrows.isComplex₂_iff._proof_5,
        zero := w }.Exact →
    S.Exact
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_one : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f : α → M},
  (∀ a ∈ s, f a ≤ 1) → ∀ (a : α), s.mulIndicator f a ≤ 1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_add_eq_right_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.natDegree < q.natDegree → (p + q).natDegree = q.natDegree
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_smul₀ : ∀ {G₀ : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [inst_3 : MeasurableConstSMul G₀ α] {c : G₀} (hc : c ≠ 0), ⇑(MeasurableEquiv.smul₀ c hc) = fun x => c • x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
/-- For `n ≠ 0` and `i ≤ n`, `node n i` is one of the extremal points of the Chebyshev `T`
polynomial over the interval `[-1, 1]`.  -/
Polynomial.Chebyshev.node : ℕ → ℕ → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
/-- A category `C` has iterations of shape a linearly ordered type `J`
when certain specific shapes of colimits exists: colimits indexed by `J`,
and by `Set.Iio j` for `j : J`.  -/
CategoryTheory.Limits.HasIterationOfShape : (J : Type w) → [LinearOrder J] → (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Alias** of `PowerSeries.weierstrassDiv_zero_right`. -/
PowerSeries.weierstrassDiv_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A], f /ʷ 0 = 0
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass provides support for the size function for ranges with closed lower bound
\(`Rcc.size`,
`Rco.size` and
`Rci.size`\).

The returned size should be equal to the number of elements returned by `toList`. This
condition is captured by the typeclass
`LawfulHasSize`.
 -/
Std.Rxc.HasSize : Type u → Type u
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x =
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).QuasiFinite
-- Mathlib.Geometry.Manifold.Submersion
/-- Given a submersion `f` at `x` w.r.t. a complement `F`, this construction provides
a continuous linear equivalence from `F` to the small complement of `F`:
mathematically, this is just the identity map; however, this is technically useful as it enables
us to always work with `hf.smallComplement`.  -/
Manifold.IsSubmersionAtOfComplement.smallEquiv : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsSubmersionAtOfComplement F I J n f x) →
                                                      F ≃L[𝕜] hf.smallComplement
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGT?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getKeyGT? k t₁ = Std.DTreeMap.Internal.Impl.getKeyGT? k t₂
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderRel.le : FirstOrder.Language.orderRel 2
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.uniformSpace : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → UniformSpace (ContDiffMapSupportedIn E F n K)
-- Init.Data.Int.DivMod.Basic
/-- Integer division using the F-rounding convention.

In the F-rounding convention (flooring division), `Int.fdiv x y` satisfies `Int.fdiv x y = ⌊x / y⌋`
and `Int.fmod` is the unique function satisfying `Int.fmod x y + (Int.fdiv x y) * y = x`.

Examples:
* `(7 : Int).fdiv (0 : Int) = 0`
* `(0 : Int).fdiv (7 : Int) = 0`
* `(12 : Int).fdiv (6 : Int) = 2`
* `(12 : Int).fdiv (-6 : Int) = -2`
* `(-12 : Int).fdiv (6 : Int) = -2`
* `(-12 : Int).fdiv (-6 : Int) = 2`
* `(12 : Int).fdiv (7 : Int) = 1`
* `(12 : Int).fdiv (-7 : Int) = -2`
* `(-12 : Int).fdiv (7 : Int) = -2`
* `(-12 : Int).fdiv (-7 : Int) = 1`
 -/
Int.fdiv : ℤ → ℤ → ℤ
-- Mathlib.Topology.MetricSpace.Antilipschitz
antilipschitzWith_iff_le_mul_nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_neg : ∀ (a : CauSeq.Completion.Cauchy abs), { cauchy := -a } = -{ cauchy := a }
-- Mathlib.Data.Nat.NthRoot.Defs
/-- Auxiliary definition for `Nat.nthRoot`.

Given natural numbers `n`, `a`, `fuel`, `guess`
such that `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊ ≤ guess ≤ fuel`,
returns `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊`.

The auxiliary number `guess` is the current approximation in Newton's method,
tracked in the arguments so that the definition uses a tail recursion
which is unfolded into a loop by the compiler.

The auxiliary number `fuel` is an upper estimate on the number of steps in Newton's method.
Any number `fuel ≥ guess` is guaranteed to work, but smaller numbers may work as well.
If `fuel` is too small, then `Nat.nthRoot.go` returns the result of the `fuel`th step
of Newton's method.
 -/
Nat.nthRoot.go : ℕ → ℕ → ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_associator_hom : ∀ (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] {E : Type u_5} [inst_4 : CategoryTheory.Category.{v_5, u_5} E]
  (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D E),
  CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (F.associator G H).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A (F.comp G) H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapCompRight A F G).hom
          (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).associator
              (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) G)
              (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H)).hom
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).whiskerLeft
              (CategoryTheory.Join.mapCompRight A G H).inv)
            (CategoryTheory.Join.mapCompRight A F (G.comp H)).inv)))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The equivalence `Comon (Mon C) ≌ Mon (Comon C)`  -/
CategoryTheory.Bimon.equivMonComon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Bimon C ≌ CategoryTheory.Mon (CategoryTheory.Comon C)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_eq_self : ∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t : Set α}, s ⊆ t → (μ.restrict t) s = μ s
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallNeg : ∀ {G : Type u_1} [inst : AddGroup G],
  CanLift (Set G) (AddSubgroup G) SetLike.coe fun s =>
    0 ∈ s ∧ (∀ {x y : G}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ {x : G}, x ∈ s → -x ∈ s
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_disconnect_objs_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C},
  c ∈ S.disconnect.objs ↔ c ∈ S.objs
-- Mathlib.Topology.LocallyConstant.Basic
/-- A function between topological spaces is locally constant if the preimage of any set is open.  -/
IsLocallyConstant : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → (X → Y) → Prop
-- Lean.Environment
/-- Participating in the module system?  -/
Lean.EnvironmentHeader.isModule : Lean.EnvironmentHeader → Bool
-- Mathlib.Order.RelIso.Basic
/-- The lexicographic sum of `r` plus an empty relation is isomorphic to `r`.  -/
RelIso.sumLexEmpty : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [IsEmpty β] → Sum.Lex r s ≃r r
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_comp_mk₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Abelian.Ext.mk₀ f).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯ =
    CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_le_right : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, I * J ≤ J
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_takeUntil_lt_length : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w} (h : u ∈ p.support),
  u ≠ w → (p.takeUntil u h).length < p.length
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Being finitely-presented is stable under base change.  -/
RingHom.finitePresentation_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.FinitePresentation
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabUniverse : Lean.Elab.Command.CommandElab
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.rankPos_of_nonempty : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → B.Nonempty → M.RankPos
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.jacobson_eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (I : Ideal R),
  I ≠ ⊤ → I.jacobson = IsLocalRing.maximalIdeal R
-- Std.Data.HashSet.Basic
Std.HashSet.instBEq : {α : Type u} → {x : Hashable α} → [inst : BEq α] → BEq (Std.HashSet α)
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instSub.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.instSub = { sub := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 - x2) ↑s ↑t, upper' := ⋯ } }
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The order of vanishing of a unit is `0`.
 -/
Ring.ord_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] {x : R}, IsUnit x → Ring.ord R x = 0
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.map_truncatedInf : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] [inst_2 : BoundedOrder β]
  [inst_3 : DecidableLE β] [inst_4 : DecidableLE α] [inst_5 : BoundedOrder α] (e : α ≃o β) (s : Finset α) (a : α),
  e (s.truncatedInf a) = (Finset.map e.toEmbedding s).truncatedInf (e a)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.instSMulCarrierXWithInfinity : {A B : GrpCat} → (f : A ⟶ B) → SMul (↑B) (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (s : Set ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace),
  x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f
-- Std.Async.Timer
/-- Return an `Async` computation that completes after `duration`.
 -/
Std.Async.sleep : Std.Time.Millisecond.Offset → Std.Async.Async Unit
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] {β : α → Type v} {k : α → Ordering} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (inner : Option ((a : α) × β a))
  (property : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner = some p → k p.fst = Ordering.eq),
  sizeOf { inner := inner, property := property } = 1 + sizeOf inner
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid
closure.  -/
AddMonoidHom.eqOn_closureM : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N} {s : Set M},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubmonoid.closure s)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instRing : {α : Type u_5} → [inst : NonUnitalNonAssocRing α] → Ring (CentroidHom α)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_eq_nsmul_single : ∀ {M : Type u_5} [inst : AddCommMonoid M] {s : Multiset M} [inst_1 : DecidableEq M] (a : M),
  (∀ (a' : M), a' ≠ a → a' ∈ s → a' = 0) → s.sum = Multiset.count a s • a
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.prime_generator_of_isPrime : ∀ {R : Type u} [inst : CommSemiring R] (S : Ideal R) [inst_1 : Submodule.IsPrincipal S] [is_prime : S.IsPrime],
  S ≠ ⊥ → Prime (Submodule.IsPrincipal.generator S)
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The one point compactification of a weakly locally compact R₁ space
is a normal topological space.  -/
OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X], NormalSpace (OnePoint X)
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry : Type
-- Mathlib.Algebra.Star.StarRingHom
/-- See Note [custom simps projection]  -/
StarRingEquiv.Simps.apply : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → (A ≃⋆+* B) → A → B
-- Mathlib.RingTheory.Flat.Basic
Submodule.toBaseChange.toLinearEquiv_apply : ∀ {R : Type u_1} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Module.Flat R A] {M : Type u_5} [inst_4 : AddCommMonoid M] [inst_5 : Module R M] (p : Submodule R M)
  (x : TensorProduct R A ↥p), (Submodule.toBaseChange.toLinearEquiv A p) x = (Submodule.toBaseChange A p) x
-- Qq.Match
Qq.Impl.floatQMatchPairs : Lean.Term → StateT (Array (Lean.Term × Lean.Ident)) Lean.MacroM Lean.Term
-- Lean.Compiler.LCNF.Basic
/-- `reuse x in ctor_i ys` instruction in the paper. `updateHeader` is set if the tag in the new
ctor differs from the one in the old ctor and thus needs to be updated.  -/
Lean.Compiler.LCNF.LetValue.reuse : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    Lean.Compiler.LCNF.CtorInfo →
      Bool →
        Array (Lean.Compiler.LCNF.Arg pu) →
          autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19 →
            Lean.Compiler.LCNF.LetValue pu
-- Mathlib.NumberTheory.Dioph
/-- Diophantine sets are closed under union.  -/
Dioph.«term_D∨_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_compAlternatingMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N₂ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N₂] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R N₂] {n : ℕ} (g : N →ₗ[R] N₂) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M),
  (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m)