mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The functions `S ⊗[R] M → S ⊗[R] N` underlying a polynomial law  -/
PolynomialLaw.toFun' : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (M →ₚₗ[R] N) →
                  (S : Type u) →
                    [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.map_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G) {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D] (H : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post F H)
      (H.map (CategoryTheory.Limits.colim.map α)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Functor.whiskerRight α H))
      (CategoryTheory.Limits.colimit.post G H)
-- Init.Data.Array.Count
Array.count_le_size : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, Array.count a xs ≤ xs.size
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- In a vector space with dimension 1, each set `{v}` is a basis for `v ≠ 0`.  -/
FiniteDimensional.basisSingleton : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          (ι : Type u_1) → [Unique ι] → Module.finrank K V = 1 → (v : V) → v ≠ 0 → Module.Basis ι K V
-- Init.Data.List.MinMax
List.max?_mem : ∀ {α : Type u_1} {a : α} [inst : Max α] [Std.MaxEqOr α] {xs : List α}, xs.max? = some a → a ∈ xs
-- Mathlib.Algebra.Group.Prod
Commute.prod : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] {x y : M × N},
  Commute x.1 y.1 → Commute x.2 y.2 → Commute x y
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.obj ⟶ G) (U : TopologicalSpace.Opens ↑X),
  (∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))
-- Mathlib.Algebra.Notation.Pi.Defs
/-- **Alias** of `Function.prod_fst_snd`. -/
Pi.prod_fst_snd : ∀ {α : Type u_1} {β : Type u_2}, Function.prod Prod.fst Prod.snd = id
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams.mk : Array Lean.Lsp.FileEvent → Lean.Lsp.DidChangeWatchedFilesParams
-- Init.Data.BitVec.Lemmas
BitVec.sle_eq_slt_or_eq : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = (x.slt y || x == y)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.Indep.restrict_eq_freeOn : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.restrict I = Matroid.freeOn I
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α), ∫⁻ (x : α) in s, 1 ∂μ = μ s
-- Lean.Elab.DocString
/-- An argument provided to a docstring extension  -/
Lean.Doc.DocArg : Type
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈.eq_1 : CartanMatrix.E₈ =
  !![2, 0, -1, 0, 0, 0, 0, 0;
    0, 2, 0, -1, 0, 0, 0, 0;
    -1, 0, 2, -1, 0, 0, 0, 0;
    0, -1, -1, 2, -1, 0, 0, 0;
    0, 0, 0, -1, 2, -1, 0, 0;
    0, 0, 0, 0, -1, 2, -1, 0;
    0, 0, 0, 0, 0, -1, 2, -1;
    0, 0, 0, 0, 0, 0, -1, 2]
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBase.cardinalMk_eq : ∀ {α : Type u} {M : Matroid α} {B B' : Set α} [M.InvariantCardinalRank],
  M.IsBase B → M.IsBase B' → Cardinal.mk ↑B = Cardinal.mk ↑B'
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsStarConvexSet.neg : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] {x : M} {s : Set M},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R (-x) (-s)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.conv_add : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], μ.conv (ν + ρ) = μ.conv ν + μ.conv ρ
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] [F.Full]
  [F.Faithful], F.mapTriangle.Full
-- Std.Time.Zoned.Database.TZdb
/-- Extracts a timezone ID from a file path.
 -/
Std.Time.Database.TZdb.idFromPath : System.FilePath → Option String
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
writtenInExtChartAt_sumInr_eventuallyEq_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q' : M'},
  writtenInExtChartAt I I q' Sum.inr =ᶠ[nhdsWithin (↑(extChartAt I q') q') (Set.range ↑I)] id
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.fib_greatestFib_le : ∀ (n : ℕ), Nat.fib n.greatestFib ≤ n
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_copy : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.RingTheory.Unramified.LocalStructure
/-- The predicate "there exists a standard etale algebra `A` over `R` that surjects onto `S[1/f]`".
We shall show if `S` is `R`-unramified at `Q` then there exists `f ∉ Q` satisfying it.  -/
HasStandardEtaleSurjectionOn : (R : Type u_1) → {S : Type u_3} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism to an initial object is split epi.  -/
CategoryTheory.Limits.IsInitial.isSplitEpi_to : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X)
  (f : Y ⟶ X), CategoryTheory.IsSplitEpi f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Condition for `B` to be a filter basis on `A`.  -/
SubmodulesRingBasis.inter : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
-- Mathlib.Order.Closure
/-- A closure operator is equal to the closure operator obtained by feeding `c.closed` into the
`ofPred` constructor.  -/
ClosureOperator.eq_ofPred_closed : ∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α), c = ClosureOperator.ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯
-- Mathlib.Data.Finset.Option
Option.card_toFinset : ∀ {α : Type u_1} (o : Option α), o.toFinset.card = o.elim 0 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ W₀ : C₀}
  (a : F.obj W₀ ⟶ F.obj X₀) {i : (data (F.obj X₀)).I₀} (p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)),
  CategoryTheory.CategoryStruct.comp p ((data (F.obj X₀)).f i) = a →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom data G₀ X₀)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ a) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_const_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E} {c : 𝕜},
  DifferentiableAt 𝕜 W x → VectorField.lieBracket 𝕜 V (c • W) x = c • VectorField.lieBracket 𝕜 V W x
-- Mathlib.Data.Finsupp.Basic
/-- On a `Fintype η`, `Finsupp.split` is an additive equivalence between
`(Σ (j : η), ιs j) →₀ α` and `Π j, (ιs j →₀ α)`.

This is the `AddEquiv` version of `Finsupp.sigmaFinsuppEquivPiFinsupp`.
 -/
Finsupp.sigmaFinsuppAddEquivPiFinsupp : {η : Type u_13} →
  [Fintype η] →
    {α : Type u_15} → {ιs : η → Type u_16} → [inst : AddMonoid α] → ((j : η) × ιs j →₀ α) ≃+ ((j : η) → ιs j →₀ α)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_def : ∀ (a x : ℝ), ↑(HurwitzZeta.oddKernel (↑a) x) = HurwitzZeta.jacobiTheta₂'' (↑a) (Complex.I * ↑x)
-- Aesop.Search.ExpandSafePrefix
Aesop.safeExpansionFailedExceptionId : Lean.InternalExceptionId
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.supSpanSingleton_apply_self : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain), ↑(f.supSpanSingleton x y hx) ⟨x, ⋯⟩ = y
-- Init.Data.SInt.Basic
instShiftRightInt32 : ShiftRight Int32
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCategory : CategoryTheory.Category.{u, u + 1} AddCommMonCat
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.uliftFunctor_obj_coe : ∀ (X : CommMonCat), ↑(CommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The `stalkToFiber` map is injective at `x` if any two allowed sections which agree at `x`
agree on some neighborhood of `x`.
 -/
TopCat.stalkToFiber_injective : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T) (x : ↑X),
  (∀ (U V : TopologicalSpace.OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
      P.pred fU →
        ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.stalkToFiber P x))
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The embedding into the `R`-linear completion, followed by the lift,
is isomorphic to the original functor.
 -/
CategoryTheory.Free.embeddingLiftIso : (R : Type u_1) →
  [inst : CommRing R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [inst_4 : CategoryTheory.Linear R D] →
                (F : CategoryTheory.Functor C D) →
                  (CategoryTheory.Free.embedding R C).comp (CategoryTheory.Free.lift R F) ≅ F
-- Mathlib.Order.Hom.Lex
/-- A relation is isomorphic to the lexicographic sum of elements less than `x` and elements not
less than `x`.  -/
RelIso.sumLexComplLeft : {α : Type u_1} →
  (r : α → α → Prop) →
    (x : α) →
      [IsTrans α r] →
        [Std.Trichotomous r] →
          [DecidableRel r] → Sum.Lex (Subrel r fun x_1 => r x_1 x) (Subrel r fun x_1 => ¬r x_1 x) ≃r r
-- Mathlib.Data.List.Infix
List.mem_inits : ∀ {α : Type u_1} (s t : List α), s ∈ t.inits ↔ s <+: t
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_eq_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {hst : s = t},
  Function.Bijective ⇑(SubAddAction.ofFixingAddSubgroup_of_eq M hst)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.ofIso_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q'),
  (b.ofIso eP eQ).snd = CategoryTheory.CategoryStruct.comp b.snd eQ.hom
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.normThreshold.eq_1 : ∀ (a : ℝ), ProbabilityTheory.Fernique.normThreshold a = arithGeom (√2) a a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_bot : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α],
  Finset.Ico ⊥ a = Finset.Iio a
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.uncountable : Uncountable Ordinal.{u}
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.Hom.ext : ∀ {A B : GrpCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : C) (d : ↑(F.obj X)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X).comp G) d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X)
        (CategoryTheory.Limits.colimitFiberwiseColimitIso G).hom) =
    CategoryTheory.Limits.colimit.ι G { base := X, fiber := d }
-- Mathlib.Topology.Covering.Quotient
isQuotientCoveringMap_iff_isCoveringMap_and : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : Group G] [inst_3 : MulAction G E],
  IsQuotientCoveringMap f G ↔
    IsCoveringMap f ∧
      Function.Surjective f ∧
        ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.map_zero_mem_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.closedCell n i
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.proceed : Bool → Lean.Language.SnapshotTree.foldSnaps.Control
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.NormedSpaceInfo.mk : Lean.Expr → Lean.Expr → Manifold.Elab.NormedSpaceInfo
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (φ φ_1 : G ≃ₜ* G),
  φ = φ_1 → MeasureTheory.mulEquivHaarChar φ = MeasureTheory.mulEquivHaarChar φ_1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.stableUnderGeneralization_singleton : ∀ {R : Type u} [inst : CommSemiring R] {x : PrimeSpectrum R},
  StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R
-- Mathlib.Order.Interval.Finset.Basic
Set.infinite_iff_exists_gt : ∀ {α : Type u_2} [inst : LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} [Nonempty α],
  s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, a < b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_eq_one_iff_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ}
  [ZeroLEOneClass M₀], 0 ≤ a → n ≠ 0 → (a ^ n = 1 ↔ a = 1)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.withSeminorms : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n : ℕ∞) (K : TopologicalSpace.Compacts E),
  WithSeminorms (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_div_const_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α}, a ≠ 0 → (Summable (fun i => f i / a) L ↔ Summable f L)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.succ_nsmul : ∀ {α : Type u_1} {t : FirstOrder.Language.presburger.Term α} {n : ℕ}, (n + 1) • t = n • t + t
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : One R] {a : Γ},
  HahnSeries.coeff 1 a = if a = 0 then 1 else 0
-- Mathlib.Algebra.Category.Ring.Limits
/-- An auxiliary declaration to speed up typechecking.
 -/
SemiRingCat.forget₂MonPreservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] →
        CategoryTheory.Limits.IsLimit
          ((CategoryTheory.forget₂ SemiRingCat MonCat).mapCone (SemiRingCat.HasLimits.limitCone F))
-- Init.MetaTypes
Lean.Meta.TransparencyMode.reducible.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.reducible = 1
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instZeroLEOneClass : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R], ZeroLEOneClass ↑(Set.Icc 0 1)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, we can define a family
of measures indexed by `Finset ℕ` by projecting the measures.  -/
MeasureTheory.inducedFamily : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    ((n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) →
      (S : Finset ℕ) → MeasureTheory.Measure ((k : ↥S) → X ↑k)
-- Lean.Elab.Match
/-- Auxiliary function for combining the `matchType` and all patterns into a single expression.
We use it before we abstract all patterns variables.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.packMatchTypePatterns : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.image_span_subset_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  (f : M →ₛₗ[σ₁₂] M₂) (s : Set M), ⇑f '' ↑(Submodule.span R s) ⊆ ↑(Submodule.span R₂ (⇑f '' s))
-- Mathlib.Topology.Algebra.Group.Basic
inv_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] (s : Set G),
  (closure s)⁻¹ = closure s⁻¹
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Iio : ∀ {n : ℕ} (i : Fin n), Fin.succ '' Set.Iio i = Set.Ioo 0 i.succ
-- Init.Data.Ord.Vector
Vector.instLawfulBEqOrd : ∀ {α : Type u_1} [inst : Ord α] [inst_1 : BEq α] [Std.LawfulBEqOrd α] {n : ℕ}, Std.LawfulBEqOrd (Vector α n)
-- Init.Data.BitVec.Bitblast
BitVec.smulOverflow_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.smulOverflow y =
    (decide (0 < w) &&
      ((BitVec.signExtend (w * 2) (BitVec.intMax w)).slt (BitVec.signExtend (w * 2) x * BitVec.signExtend (w * 2) y) ||
        (BitVec.signExtend (w * 2) x * BitVec.signExtend (w * 2) y).slt (BitVec.signExtend (w * 2) (BitVec.intMin w))))
-- Mathlib.Order.Hom.Set
OrderIso.symm_preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set β), ⇑e.symm ⁻¹' ⇑e ⁻¹' s = s
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_sq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.reflection i ^ 2 = 1
-- Mathlib.Order.RelSeries
RelSeries.append.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r),
  p.append q connect =
    { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceUnivIso_symm_apply_coe : ∀ {V : Type u_1} (G : SimpleGraph V) (a : V), ↑((RelIso.symm G.induceUnivIso) a) = a
-- Mathlib.Topology.Order.LeftRight
nhdsWithinLT_sup_nhdsWithinGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Iio a) ⊔ nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a (s \ {a})
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_mk₂ : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (L R : List Γ), Turing.Tape.map f (Turing.Tape.mk₂ L R) = Turing.Tape.mk₂ (List.map f.f L) (List.map f.f R)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Antitone.mul_const_of_nonpos : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → a ≤ 0 → Monotone fun x => f x * a
-- Init.Data.SInt.Lemmas
UInt64.toInt64_neg : ∀ (a : UInt64), (-a).toInt64 = -a.toInt64
-- Mathlib.RingTheory.Localization.Defs
/-- See note [partially-applied ext lemmas]  -/
IsLocalization.ringHom_ext : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {P : Type u_4} [inst_4 : Semiring P] ⦃j k : S →+* P⦄,
  j.comp (algebraMap R S) = k.comp (algebraMap R S) → j = k
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_map : ∀ {K : Type u} {L : Type v} {M : Type w} [inst : DivisionRing K] [inst_1 : DivisionRing L] [inst_2 : DivisionRing M]
  (s : Subfield K) (g : L →+* M) (f : K →+* L), Subfield.map g (Subfield.map f s) = Subfield.map (g.comp f) s
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] [inst : Inhabited α] {k : α},
  m.contains k = true → m.get! k = k