mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addEquiv_apply : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₁ i)]
  [inst_1 : (i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) (x : Π₀ (i : ι), β₁ i),
  (DFinsupp.mapRange.addEquiv e) x = DFinsupp.mapRange (fun i x => (e i) x) ⋯ x
-- Mathlib.Topology.Algebra.UniformField
/-- extension of inversion to the completion of a field.  -/
UniformSpace.Completion.hatInv : {K : Type u_1} → [Field K] → [inst : UniformSpace K] → UniformSpace.Completion K → UniformSpace.Completion K
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.bijective : ∀ {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] {Q : Type u_4} [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [IsLocalization M Q] (f : S →+* Q), f.comp (algebraMap R S) = algebraMap R Q → Function.Bijective ⇑f
-- Mathlib.Control.Monad.Cont
instMonadContStateT : {m : Type u → Type v} → {σ : Type u} → [MonadCont m] → MonadCont (StateT σ m)
-- Mathlib.Algebra.Group.End
Equiv.zpow_mulLeft : ∀ {α : Type u_4} [inst : Group α] (a : α) (n : ℤ), Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Nonempty α] [inst_2 : One β],
  MeasureTheory.SimpleFunc.range 1 = {1}
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- Construct an element of `E →SWOT[σ] F` from a continuous linear map.  -/
ContinuousLinearMapWOT.ofCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : Semiring 𝕜₁] →
      [inst_1 : Semiring 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] → [inst_7 : Module 𝕜₂ F] → (E →SL[σ] F) → E →SWOT[σ] F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
/-- The function `sin x / x` modified to take the value 1 at 0, which makes it continuous.  -/
Real.sinc : ℝ → ℝ
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limitCone_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))),
  (CategoryTheory.Limits.Types.limitCone F).pt = ↑F.sections
-- Mathlib.Algebra.Order.Hom.Basic
/-- `RingNormClass F α` states that `F` is a type of `β`-valued norms on the ring `α`.

You should extend this class when you extend `RingNorm`.  -/
RingNormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [NonUnitalNonAssocRing α] → [Semiring β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.instInhabited : {α : Type u_1} → Inhabited (MeasurableSpace α)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqArg : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.Arg pu)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapLMonoidHom_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (f : (i : ι) → E i →L[𝕜] E i),
  PiTensorProduct.mapLMonoidHom f = PiTensorProduct.mapL f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ R : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R₀ ⟶ R) [CategoryTheory.Presheaf.IsLocallyInjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Functor Cᵒᵖ AddCommGrpCat} (φ : M₀.presheaf ⟶ A)
  [CategoryTheory.Presheaf.IsLocallyInjective J φ],
  CategoryTheory.Presheaf.IsSeparated J A →
    ∀ {Y : C} (r₀ r₀' : ↑(R₀.obj (Opposite.op Y))) (m₀ m₀' : ↑(M₀.obj (Opposite.op Y))),
      (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ =
          (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' →
        (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' →
          (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀) =
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀')
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).target = Prod.map Subtype.val id ⁻¹' e.target
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  K.homologyIsoSc' i j k hi hk = K.homologyIsoSc' i j k hi hk
-- Init.Data.Int.DivMod.Lemmas
Int.emod_two_eq : ∀ (x : ℤ), x % 2 = 0 ∨ x % 2 = 1
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.coe_basisRightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E) (hx : x ≠ 0), ⇑(o.basisRightAngleRotation x hx) = ![x, o.rightAngleRotation x]
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorUnit_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Grp C)).X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Init.Data.String.Basic
/-- Decodes an array of bytes that encode a string as [UTF-8](https://en.wikipedia.org/wiki/UTF-8) into
the corresponding string, or returns `none` if the array is not a valid UTF-8 encoding of a string.
 -/
String.fromUTF8? : ByteArray → Option String
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.map_coe_nhdsGE : ∀ (x : NNReal), Filter.map NNReal.toReal (nhdsWithin x (Set.Ici x)) = nhdsWithin (↑x) (Set.Ici ↑x)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_sum_of_identDistrib : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {s : Finset ι}
  {j : ι},
  (∀ (i : ι), Measurable (X i)) →
    ProbabilityTheory.iIndepFun X μ →
      (∀ i ∈ s, ∀ j ∈ s, ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) →
        j ∈ s → ∀ (t : ℝ), ProbabilityTheory.mgf (∑ i ∈ s, X i) μ t = ProbabilityTheory.mgf (X j) μ t ^ s.card
-- Lean.Server.FileWorker.SignatureHelp
/-- In a syntax stack, keep searching upwards, continuing with the parent of the current term.  -/
Lean.Server.FileWorker.SignatureHelp.SearchControl.continue : Lean.Server.FileWorker.SignatureHelp.SearchControl
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_pos : ∀ {α : Type u} [inst : Zero α] [inst_1 : LT α] {a : α}, 0 < ↑a ↔ 0 < a
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientQuotientEquivQuotient.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientAddGroup.quotientQuotientEquivQuotient N M h =
    (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h).toAddEquiv
      (QuotientAddGroup.map M (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.mk' N) ⋯) ⋯ ⋯
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instCoeOutAlgHom : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → CoeOut (𝒜 →ₐᵍ[R] ℬ) (A →ₐ[R] B)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffAt_arccos_iff : ∀ {x : ℝ} {n : WithTop ℕ∞}, ContDiffAt ℝ n Real.arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
-- Lean.Parser.Term
Lean.Parser.darrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.mk : ∀ {s : Substring.Raw},
  String.Pos.Raw.Valid s.str s.startPos → String.Pos.Raw.Valid s.str s.stopPos → s.startPos ≤ s.stopPos → s.Valid
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.counitInv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse)) =
    CategoryTheory.Functor.LaxMonoidal.ε e.functor
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, m.contains a = true
-- Mathlib.GroupTheory.Schreier
AddSubgroup.closure_add_image_add_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R),
  0 ∈ R → AddSubgroup.closure S = ⊤ → ↑(AddSubgroup.closure ((fun g => g + -↑(hR.toRightFun g)) '' (R + S))) + R = ⊤
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- The function `ContinuousLinearMap.mulLeftRight : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded
bilinear map.  -/
ContinuousLinearMap.mulLeftRight_isBoundedBilinear : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (𝕜' : Type u_5) [inst_1 : SeminormedRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'], IsBoundedBilinearMap 𝕜 fun p => ((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') p.1) p.2
-- Mathlib.Algebra.Regular.ULift
ULift.isAddRightRegular_down : ∀ {R : Type v} [inst : Add R] {a : ULift.{u, v} R}, IsAddRightRegular a.down ↔ IsAddRightRegular a
-- Mathlib.Topology.Algebra.Group.Basic
totallyDisconnectedSpace_iff_connectedComponent_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G],
  TotallyDisconnectedSpace G ↔ connectedComponent 1 = {1}
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.addConjugatesOfSet_subset_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, AddGroup.addConjugatesOfSet s ⊆ ↑(AddSubgroup.normalClosure s)
-- Lean.Meta.Tactic.Apply
/-- Apply the `n`-th constructor of the target type,
checking that it is an inductive type,
and that there are the expected number of constructors.
 -/
Lean.MVarId.nthConstructor : Lean.Name → ℕ → optParam (Option ℕ) none → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_toLex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsLeftRegular (toLex a) ↔ IsLeftRegular a
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_uIcc_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.uIcc i.succ j.succ = Set.uIcc i j
-- Mathlib.SetTheory.Cardinal.CountableCover
/-- If a set `t` is eventually covered by a countable family of sets, all with cardinality at
most `a`, then the cardinality of `t` is also bounded by `a`.
Superseded by `mk_le_of_countable_eventually_mem` which does not assume
that the indexing set lives in the same universe.  -/
Cardinal.mk_subtype_le_of_countable_eventually_mem_aux : ∀ {α ι : Type u} {a : Cardinal.{u}} [Countable ι] {f : ι → Set α} {l : Filter ι} [l.NeBot] {t : Set α},
  (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a
-- Mathlib.Topology.Algebra.Module.Basic
/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.

In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well.

This version is stated in terms of `Submodule.topologicalClosure`,
thus assumes that `M i`s are topological modules over `R`.
However, the statement is true without assuming continuity of the operations,
see `Submodule.closure_coe_iSup_map_single` above.  -/
Submodule.topologicalClosure_iSup_map_single : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : (i : ι) → TopologicalSpace (M i)] [inst_4 : DecidableEq ι]
  [inst_5 : ∀ (i : ι), ContinuousAdd (M i)] [inst_6 : ∀ (i : ι), ContinuousConstSMul R (M i)]
  (s : (i : ι) → Submodule R (M i)),
  (⨆ i, Submodule.map (LinearMap.single R M i) (s i)).topologicalClosure =
    Submodule.pi Set.univ fun i => (s i).topologicalClosure
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.support_binomial : ∀ {R : Type u} [inst : Semiring R] {k m : ℕ},
  k ≠ m →
    ∀ {x y : R},
      x ≠ 0 → y ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
UpgradedStandardBorel.mk : {α : Type u_1} →
  [toMeasurableSpace : MeasurableSpace α] →
    [toTopologicalSpace : TopologicalSpace α] →
      [toBorelSpace : BorelSpace α] → [toPolishSpace : PolishSpace α] → UpgradedStandardBorel α
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- The restriction of an equidecomposition as an equidecomposition.  -/
Equidecomp.restr : {X : Type u_1} → {G : Type u_2} → [inst : SMul G X] → Equidecomp X G → Set X → Equidecomp X G
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_empty : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus ∅ = Set.univ
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- Closed balls are bounded in the weak dual.  -/
WeakDual.isBounded_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x' : StrongDual 𝕜 E) (r : ℝ),
  Bornology.IsBounded (⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall x' r)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  Function.Injective ContinuousAffineEquiv.toAffineEquiv
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat'HAddPredOfNat : ∀ {n : ℕ}, Mathlib.Tactic.Ring.CSLiftVal n.toPNat' (n.pred + 1)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadLift_refl_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} [Pure m] (x : m α),
  Std.Internal.Do.wp (monadLift x) post epost = Std.Internal.Do.wp x post epost
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter'.eq_1 : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n],
  modularCyclotomicCharacter' L n =
    { toFun := modularCyclotomicCharacter.toFun n, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_toEnd_of_isNilpotent₂ : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsNilpotent L M] (x y : L), IsNilpotent ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFinitaryMapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α ↪ β}, (M.mapEmbedding f).Finitary
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^32 - 1` for natural numbers greater than or equal to `2^32`.
 -/
UInt32.ofNatTruncate : ℕ → UInt32
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.hasProd : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {x : β}
  [inst_1 : UniformSpace α], HasProdUniformly f g → HasProd (fun x_1 => f x_1 x) (g x)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.instMod : {R : Type u} → [inst : Field R] → Mod (Polynomial R)
-- Init.Data.Order.Lemmas
Std.total_of_refl_of_trichotomous : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] [Std.Trichotomous r], Std.Total r
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.lift_comp_of' : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] (f : AddMagma.FreeAddSemigroup α →ₙ+ β),
  AddMagma.FreeAddSemigroup.lift (f.comp AddMagma.FreeAddSemigroup.of) = f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) →
      ((t : Lean.Meta.Grind.Arith.CommRing.EqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.right_mem_support : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, G.Adj u v → v ∈ G.support
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Real part of a point of the unit disc.  -/
Complex.UnitClosedDisc.re : Complex.UnitClosedDisc → ℝ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_minKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {km kmm : α} (hkm : t.minKey? = some km), (t.modify k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `G : Cocone F ⥤ Cocone F'` reflects initial objects, it reflects colimit cocones.  -/
CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F : CategoryTheory.Functor J C} →
                  {F' : CategoryTheory.Functor K D} →
                    (G : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone F')) →
                      [CategoryTheory.Limits.ReflectsColimit
                            (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cocone F)) G] →
                        {c : CategoryTheory.Limits.Cocone F} →
                          CategoryTheory.Limits.IsColimit (G.obj c) → CategoryTheory.Limits.IsColimit c
-- Init.Data.List.Nat.Basic
List.length_filter_lt_length_iff_exists : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).length < l.length ↔ ∃ x ∈ l, ¬p x = true
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.add_comp : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B C : Rep.{w, u, v} k G} (f₁ f₂ : A ⟶ B)
  (g : B ⟶ C),
  CategoryTheory.CategoryStruct.comp (f₁ + f₂) g =
    CategoryTheory.CategoryStruct.comp f₁ g + CategoryTheory.CategoryStruct.comp f₂ g
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_succ_left_eq_erase_Ico : ∀ {a b : ℕ}, Finset.Ico a.succ b = (Finset.Ico a b).erase a
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_sInf : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (s : Set (Ideal S)), Ideal.comap f (sInf s) = ⨅ I ∈ s, Ideal.comap f I
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.unique_continuousLinearMapOfBilin : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) {v f : E},
  (∀ (w : E), inner 𝕜 f w = (B v) w) → f = (InnerProductSpace.continuousLinearMapOfBilin B) v
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extend_symm_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖)
  (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : F),
  (f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂).symm (e₂ x) = e₁ (f.symm x)
-- Mathlib.Analysis.Complex.Exponential
Real.abs_exp_sub_one_le : ∀ {x : ℝ}, |x| ≤ 1 → |Real.exp x - 1| ≤ 2 * |x|
-- Lean.Meta.Closure
Lean.Meta.Closure.instInhabitedToProcessElement : Inhabited Lean.Meta.Closure.ToProcessElement
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.instBEqRewriteLemma.beq : Mathlib.Tactic.LibraryRewrite.RewriteLemma → Mathlib.Tactic.LibraryRewrite.RewriteLemma → Bool
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : Colex α), ofColex (b +ᵥ a) = b +ᵥ ofColex a
-- Lean.DocString.Parser
/-- A parser that does nothing.
 -/
Lean.Doc.Parser.skipFn : Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.isAffineOpen_basicOpen : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ},
  f ∈ 𝒜 m → 0 < m → AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Proj.basicOpen 𝒜 f)