mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : α → β} (p : Set β → Prop) {s : Set β}
  [HasCountableSeparatingOn β p s],
  (∀ᶠ (x : α) in l, f x ∈ s) →
    s.Nonempty →
      (∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U) → ∃ a ∈ s, f =ᶠ[l] Function.const α a
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_zero_one : ∀ (t : ↑unitInterval), Set.Icc.convexComb 0 1 t = t
-- Mathlib.Topology.UniformSpace.Path
/-- If `{U i | p i}` form a basis of entourages of `X`,
then the entourages `{V i | p i}`, `V i = {(γ₁, γ₂) | ∀ t, (γ₁ t, γ₂ t) ∈ U i}`,
form a basis of entourages of paths between `x` and `y`.  -/
Filter.HasBasis.uniformityPath : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X} {ι : Sort u_2} {p : ι → Prop} {U : ι → Set (X × X)},
  (uniformity X).HasBasis p U →
    (uniformity (Path x y)).HasBasis p fun i => {γ | ∀ (t : ↑unitInterval), (γ.1 t, γ.2 t) ∈ U i}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k' hc =
    if heq : compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get ⋯
    else Std.DTreeMap.Internal.Impl.Const.get t k' ⋯
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_inv : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V), ↑A⁻¹ = (↑A)⁻¹
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.coe_mk : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃* B)
  (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)), ⇑{ toMulEquiv := e, map_star' := h₁ } = ⇑e
-- Mathlib.LinearAlgebra.Ray
/-- A positive multiple of a vector is in the same ray as that vector.  -/
SameRay.sameRay_pos_smul_left : ∀ {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] {S : Type u_5} [inst_5 : CommSemiring S] [inst_6 : PartialOrder S]
  [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M),
  0 < a → SameRay R (a • v) v
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_isLocalized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_6 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_7 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_7 : ∀ (P : Ideal R) [inst_7 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7) [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_10 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M →ₗ[R] N),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Function.Surjective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) →
    Function.Surjective ⇑F
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter.eq_1 : ∀ {n : ℕ} (i₁ i₂ : Fin (n + 3)) (a : Fin (n + 2 + 1)),
  Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂
      (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) =
    if a = i₁ ∨ a = i₂ then (↑(n + 1))⁻¹ else 0
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedProblem : Inhabited Lean.Meta.Match.Problem
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst_2 : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.ofList l) k' = v
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- **Alias** of `ContDiffAt.eventually_apply_eq_iff_implicitFunction`. -/
IsContDiffImplicitAt.eventually_implicitFunction_apply_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (v : E₁ × E₂) in nhds u, f v = f u ↔ cdf.implicitFunction pn if₂ v.1 = v.2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonMulHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α], ⇑Finset.singletonMulHom = singleton
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
/-- The trivial valuative relation on a domain `R`, such that all non-zero elements are related.
The domain condition is necessary so that the relation is closed when multiplying.
 -/
ValuativeRel.trivialRel : {R : Type} → [inst : Semiring R] → [DecidableEq R] → [IsDomain R] → ValuativeRel R
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.IsNonZero.neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  α.IsNonZero → (-α).IsNonZero
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_mk_coe : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (i : ιₚ) (g : G), ↑{ index := i, groupElts := ↑g } = g • ↑(↑ps i)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hr_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.insertMin k v Std.DTreeMap.Internal.Impl.leaf hr_2 =
    { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
      balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial] {Z : ModuleCat k}
  (h : ModuleCat.of k ↑A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H0IsoOfIsTrivial A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom h)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Morphisms between objects in the image of the functor `F.toDescentData f`
identify to compatible families of sections of the presheaf `F.presheafHom M N` on
the object `Over.mk (𝟙 S)`, relatively to the family of morphisms in `Over S`
corresponding to the family `f`.  -/
CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            (f : (i : ι) → X i ⟶ S) →
              {M N : ↑(F.obj { as := Opposite.op S })} →
                Subtype
                    (CategoryTheory.Presieve.Arrows.Compatible (F.presheafHom M N) fun i =>
                      CategoryTheory.Over.homMk (f i) ⋯) ≃
                  ((F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The `CorepresentableBy` structure asserting that the Type-valued functor
`Y ↦ ((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ Y)` is corepresented by
`(F ⊛ G) ⊛ H`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F G : CategoryTheory.Functor C V) →
              [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                (H : CategoryTheory.Functor C V) →
                  [inst_5 :
                      CategoryTheory.MonoidalCategory.DayConvolution
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] →
                    [∀ (v : V) (d : C),
                          CategoryTheory.Limits.PreservesColimitsOfShape
                            (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                            (CategoryTheory.MonoidalCategory.tensorRight v)] →
                      (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                                (CategoryTheory.MonoidalCategory.tensor C)).comp
                            (((CategoryTheory.Functor.whiskeringLeft ((C × C) × C) (C × C) V).obj
                                  ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C))).comp
                              (CategoryTheory.coyoneda.obj
                                (Opposite.op
                                  (CategoryTheory.MonoidalCategory.externalProduct
                                    (CategoryTheory.MonoidalCategory.externalProduct F G) H))))).CorepresentableBy
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution
                          (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {a : α} {fallback : β}, a ∈ m → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.getD m a fallback)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_app : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C),
  CategoryTheory.CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X)) (α.app X) =
    CategoryTheory.CategoryStruct.comp (α'.app X) (τ.app X)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans_source : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z),
  (f.trans g).source = (f.symm.restrictSource (f.target ⊓ g.source) ⋯ ⋯).target
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [IsDomain R] (x : W'.CoordinateRing),
  ((Algebra.norm (Polynomial R)) x).natDegree ≠ 1
-- Mathlib.Order.JordanHolder
/-- A `CompositionSeries X` is a finite nonempty series of elements of a
`JordanHolderLattice` such that each element is maximal inside the next. The length of a
`CompositionSeries X` is one less than the number of elements in the series.
Note that there is no stipulation that a series start from the bottom of the lattice and finish at
the top. For a composition series `s`, `s.last` is the largest element of the series,
and `s.head` is the least element.
 -/
CompositionSeries : (X : Type u) → [inst : Lattice X] → [JordanHolderLattice X] → Type u
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.brecOn.eq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {motive : (a : P.last.M) → (a_1 : Fin2 n) → MvPFunctor.M.Path P a a_1 → Sort u_1}
  {a : P.last.M} {a_1 : Fin2 n} (t : MvPFunctor.M.Path P a a_1)
  (F_1 :
    (a : P.last.M) → (a_2 : Fin2 n) → (t : MvPFunctor.M.Path P a a_2) → MvPFunctor.M.Path.below t → motive a a_2 t),
  MvPFunctor.M.Path.brecOn t F_1 = F_1 a a_1 t (MvPFunctor.M.Path.brecOn.go t F_1).2
-- Mathlib.Data.Analysis.Filter
CFilter.mk.inj : ∀ {α : Type u_1} {σ : Type u_2} {inst : PartialOrder α} {f : σ → α} {pt : σ} {inf : σ → σ → σ}
  {inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a} {inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b} {f_1 : σ → α}
  {pt_1 : σ} {inf_1 : σ → σ → σ} {inf_le_left_1 : ∀ (a b : σ), f_1 (inf_1 a b) ≤ f_1 a}
  {inf_le_right_1 : ∀ (a b : σ), f_1 (inf_1 a b) ≤ f_1 b},
  { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right } =
      { f := f_1, pt := pt_1, inf := inf_1, inf_le_left := inf_le_left_1, inf_le_right := inf_le_right_1 } →
    f = f_1 ∧ pt = pt_1 ∧ inf = inf_1
-- Lean.Server.References
/-- Whether this reference declares `ident`.  -/
Lean.Server.Reference.isBinder : Lean.Server.Reference → Bool
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.isContinuous_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F₁ : CategoryTheory.Functor C D)
  (F₂ : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology E) [F₁.IsContinuous J K]
  [F₂.IsContinuous K L], (F₁.comp F₂).IsContinuous J L
-- Mathlib.Algebra.MvPolynomial.Eval
/-- Evaluate a polynomial `p` given a valuation `g` of all the variables
and a ring hom `f` from the scalar ring to the target  -/
MvPolynomial.eval₂ : {R : Type u} →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] → [inst_1 : CommSemiring S₁] → (R →+* S₁) → (σ → S₁) → MvPolynomial σ R → S₁
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.mk.injEq : ∀ (overwrite ignoreIfExists overwrite_1 ignoreIfExists_1 : Bool),
  ({ overwrite := overwrite, ignoreIfExists := ignoreIfExists } =
      { overwrite := overwrite_1, ignoreIfExists := ignoreIfExists_1 }) =
    (overwrite = overwrite_1 ∧ ignoreIfExists = ignoreIfExists_1)
-- Lean.Elab.Tactic.RCases
/-- This introduces the pattern `pat`. It has the same arguments as `rcasesCore`, plus:
* `ty?`: the nearest enclosing type ascription on the current pattern
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rintroCore : {α : Type} →
  Lean.MVarId →
    Lean.Meta.FVarSubst →
      Array Lean.FVarId →
        α →
          Lean.Syntax →
            Lean.TSyntax `rintroPat →
              Option Lean.Term →
                (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) →
                  Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A cokernel cofork for the cokernel of `biprod.inl`. It consists of the
morphism `biprod.snd`.  -/
CategoryTheory.Limits.biprod.inlCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.CokernelCofork CategoryTheory.Limits.biprod.inl
-- Mathlib.Data.Fintype.EquivFin
Finset.card_eq_of_equiv_fintype : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : Fintype β] (i : ↥s ≃ β), s.card = Fintype.card β
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.leadCoeff.eq_1 : ∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add a v p_2).leadCoeff = a
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- In a category with weak equivalences, a path object is the
data of a weak equivalence `ι : A ⟶ P` equipped with two retractions.  -/
HomotopicalAlgebra.PathObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → C → Type (max u v)
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of yoneda lemma when `C` is small.  -/
CategoryTheory.curriedYonedaLemma : {C : Type u₁} →
  [inst : CategoryTheory.SmallCategory C] →
    CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ CategoryTheory.evaluation Cᵒᵖ (Type u₁)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_toList_eq_length : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toList.length = it.length
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.IsLocallyNoetherian.component_noetherian : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocallyNoetherian X] (U : ↑X.affineOpens),
  IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑U))
-- Init.Prelude
/-- Constructs a new empty byte array with initial capacity `0`.

Use `ByteArray.emptyWithCapacity` to create an array with a greater initial capacity.
 -/
ByteArray.empty : ByteArray
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntryIfNew_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = true → Std.Internal.List.insertEntryIfNew k v l = l
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.toTopEdgeLabeling.congr_simp : ∀ {V : Type u_1} (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] (a a_1 : ↑⊤.edgeSet),
      a = a_1 → G.toTopEdgeLabeling a = G_1.toTopEdgeLabeling a_1
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the left respects higher differentiability on
domains.  -/
ContinuousLinearEquiv.comp_contDiffOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} (e : F ≃L[𝕜] G),
  ContDiffOn 𝕜 n (⇑e ∘ f) s ↔ ContDiffOn 𝕜 n f s
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.nil : Lean.Meta.Grind.PendingSolverPropagationsData✝
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.mk_len : ∀ (n : SimplexCategory), { len := n.len } = n
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instEnoughInjectivesOppositeOfEnoughProjectives : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughProjectives C],
  CategoryTheory.EnoughInjectives Cᵒᵖ
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.homMk.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (η η_1 : s.extension ⟶ t.extension) (e_η : η = η_1)
  (w : CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerLeft f η) = t.unit),
  CategoryTheory.Bicategory.LeftExtension.homMk η w = CategoryTheory.Bicategory.LeftExtension.homMk η_1 ⋯
-- Init.Data.List.MinMax
List.max?_eq_some_iff_legacy : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] [anti : Std.Antisymm fun x1 x2 => x1 ≤ x2],
  (∀ (a : α), a ≤ a) →
    (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) →
      (∀ (a b c : α), b ⊔ c ≤ a ↔ b ≤ a ∧ c ≤ a) → ∀ {xs : List α}, xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], (↑p).valuation = 1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
/-- This is an auxiliary summand used to define the Eisenstein series `G2`.  -/
EisensteinSeries.e2Summand : ℤ → UpperHalfPlane → ℂ
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.trans_dvd : ∀ {α : Type u_1} {f : α → α} {x : α} {m : ℕ},
  Function.IsPeriodicPt f m x → ∀ {n : ℕ}, m ∣ n → Function.IsPeriodicPt f n x
-- Mathlib.Order.Circular
Set.compl_cIcc : ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, (Set.cIcc a b)ᶜ = Set.cIoo b a
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_iff_pow_mul_le_pow : ∀ {a n m : ℕ}, 1 < a → (a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- The function `expNegInvGlue` is nonnegative.  -/
expNegInvGlue.nonneg : ∀ (x : ℝ), 0 ≤ expNegInvGlue x
-- Init.Omega.IntList
Lean.Omega.IntList.mul_neg_left : ∀ (xs ys : Lean.Omega.IntList), -xs * ys = -(xs * ys)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk.inj : ∀ {G : Type u_3} {inst : AddGroup G} {toAddSubmonoid : AddSubmonoid G}
  {neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier} {toAddSubmonoid_1 : AddSubmonoid G}
  {neg_mem'_1 : ∀ {x : G}, x ∈ toAddSubmonoid_1.carrier → -x ∈ toAddSubmonoid_1.carrier},
  { toAddSubmonoid := toAddSubmonoid, neg_mem' := neg_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, neg_mem' := neg_mem'_1 } →
    toAddSubmonoid = toAddSubmonoid_1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {X Y : B} (f : X ⟶ Y),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.id B).map f = f
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N)
  (hmul : ∀ (x y : M), f (x * y) = f x * f y), { toFun := ⇑f, map_mul' := hmul } = f
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) {r : NNReal}, r < ‖f‖₊ → ∃ x, ‖x‖₊ = 1 ∧ r < ‖f x‖₊
-- Mathlib.Algebra.GradedMonoid
/-- Optional field to allow definitional control of natural powers  -/
GradedMonoid.GMonoid.gnpow : {ι : Type u_1} →
  {A : ι → Type u_2} → {inst : AddMonoid ι} → [self : GradedMonoid.GMonoid A] → (n : ℕ) → {i : ι} → A i → A (n • i)
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.Finite.toFiniteDimensional : ∀ {X : Type u_1} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.Finite C], Topology.RelCWComplex.FiniteDimensional C
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_of_subsingleton : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Subsingleton R] (p : MvPolynomial σ R),
  m.Monic p
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_some_above : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, i ≤ m.castSucc → (finSuccEquiv' i).symm (some m) = m.succ