mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instIsLocalHomAtPrimeRingHomLocalRingHom : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {f : 𝒜 →+*ᵍ ℬ} {I : Ideal A} [inst_10 : I.IsPrime]
  {J : Ideal B} [inst_11 : J.IsPrime] {hIJ : I = Ideal.comap f J},
  IsLocalHom (HomogeneousLocalization.localRingHom f I J hIJ)
-- Lean.Util.ShareCommon
Lean.ShareCommon.objectFactory : ShareCommon.StateFactory
-- Mathlib.Topology.Neighborhoods
mem_closure_of_frequently_of_tendsto : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α},
  (∃ᶠ (x : α) in b, f x ∈ s) → Filter.Tendsto f b (nhds x) → x ∈ closure s
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.ext_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : AdicCompletion.AdicCauchySequence I M}, x = y ↔ ∀ (n : ℕ), ↑x n = ↑y n
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_ofNat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).untop₀ = OfNat.ofNat n
-- Mathlib.NumberTheory.PowModTotient
Nat.pow_totient_mod : ∀ {x k n : ℕ}, 1 < n → x.Coprime n → x ^ k % n = x ^ (k % n.totient) % n
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instCovariantClassHSMulLe : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K],
  CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.instNonemptyTotalOfIsFiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  [CategoryTheory.IsFiltered J] [∀ (j : J), CategoryTheory.IsFiltered (I j)],
  Nonempty (CategoryTheory.Limits.ColimitPresentation.Total P)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_mk_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S)
  (h₂ : S 0)
  (h₃ :
    ∀ (c : R) {x : M},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {x : L} {m : M},
      m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier)
  {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } ↔ x ∈ S
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → ContIntertwiningMap π₁ π₂ → V →L[R] W
-- Mathlib.Algebra.Algebra.Epi
/-- A heterogeneous variant of `TensorProduct.lid` when `R → A` is epi.  -/
TensorProduct.lid' : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          [Algebra.IsEpi R A] →
            (M : Type u_3) →
              [inst_4 : AddCommMonoid M] →
                [inst_5 : Module R M] → [inst_6 : Module A M] → [IsScalarTower R A M] → TensorProduct R A M ≃ₗ[A] M
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_sphere : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ),
  ⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.cache : {α β : Type} →
  {m : Type → Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Lean.MonadHashMapCacheAdapter α β m] → α → β → m Unit
-- Init.Data.Iterators.Basic
/-- The wrapped iterator.

In the wrapper, its finiteness is used as a termination measure.
 -/
Std.IterM.TerminationMeasures.Finite.it : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM.TerminationMeasures.Finite α m → Std.IterM m β
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLT! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (Sigma β)] → Std.ExtDTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_iff : ∀ (X : SSet) (d : ℕ), X.HasDimensionLT d ↔ ∀ (n : ℕ), d ≤ n → X.degenerate n = ⊤
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.MeasuredSets.edist_def : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s t : MeasureTheory.MeasuredSets μ),
  edist s t = μ (symmDiff ↑s ↑t)
-- Mathlib.Order.InitialSeg
PrincipalSeg.instCoeFunForall : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → CoeFun (PrincipalSeg r s) fun x => α → β
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoMod hp a (b - m • p) = toIcoMod hp a b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rcc_eq_add : ∀ {m n i fallback : ℕ}, i < n + 1 - m → (m...=n).toArray.getD i fallback = m + i
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.support_coeff`. -/
SkewMonoidAlgebra.support_toFinsupp : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (p : SkewMonoidAlgebra k G), p.coeff.support = p.support
-- Mathlib.Data.Nat.Sqrt
Nat.le_sqrt_of_eq_mul : ∀ {a b c : ℕ}, a = b * c → b ≤ a.sqrt ∨ c ≤ a.sqrt
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.size = 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m.insert k
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instSMulInt : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : Field R] → [inst_2 : IsOrderedRing R] → SMul ℤ (ArchimedeanClass R)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tprod_eq_tprodCoeff_one : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], ⇑(PiTensorProduct.tprod R) = PiTensorProduct.tprodCoeff R 1
-- Mathlib.Algebra.CubicDiscriminant
/-- The discriminant of a cubic polynomial.  -/
Cubic.discr : {R : Type u_5} → [Ring R] → Cubic R → R
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- `cyclotomic n ℤ` is the minimal polynomial of a primitive `n`-th root of unity `μ`.  -/
Polynomial.cyclotomic_eq_minpoly : ∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
  IsPrimitiveRoot μ n → 0 < n → ∀ [CharZero K], Polynomial.cyclotomic n ℤ = minpoly ℤ μ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mono_of_mono_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B)
  [h : CategoryTheory.Mono f.left], CategoryTheory.Mono f
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.zsmul_neg' : ∀ {G : Type u} [self : SubNegMonoid G] (n : ℕ) (a : G), Int.negSucc n • a = -(↑n.succ • a)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressReport.toJson : Lean.Lsp.WorkDoneProgressReport → Lean.Json
-- Std.Internal.Parsec.Basic
/-- Parsing succeeded, returning the new position `pos` and the parsed result `res`.
 -/
Std.Internal.Parsec.ParseResult.success : {α ι : Type} → ι → α → Std.Internal.Parsec.ParseResult α ι
-- Init.Data.Fin.Lemmas
/-- Proves a statement by cases on the underlying `Nat` value in a `Fin (n + 1)`.

The two cases are:
* `zero`, used when the value is of the form `(0 : Fin (n + 1))`
* `succ`, used when the value is of the form `(j : Fin n).succ`

The corresponding induction principle is `Fin.induction`.
 -/
Fin.cases : {n : ℕ} → {motive : Fin (n + 1) → Sort u_1} → motive 0 → ((i : Fin n) → motive i.succ) → (i : Fin (n + 1)) → motive i
-- Mathlib.Data.Fintype.Sets
Set.toFinset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Set α) [inst_1 : Fintype ↑s]
  [inst_2 : Fintype ↑(f '' s)], (f '' s).toFinset = Finset.image f s.toFinset
-- Mathlib.Algebra.Polynomial.Homogenize
/-- Given a polynomial `p` and a number `n ≥ natDegree p`,
returns a homogeneous bivariate polynomial `q` of degree `n` such that `q(x, 1) = p(x)`.

It is defined as `∑ k + l = n, a_k X_0^k X_1^l`, where `a_k` is the `k`th coefficient of `p`.  -/
Polynomial.homogenize : {R : Type u_1} → [inst : CommSemiring R] → Polynomial R → ℕ → MvPolynomial (Fin 2) R
-- Std.Http.Data.Headers.Name
/-- Converts the header name to title case (e.g., "Content-Type").

Note: some well-known headers have unconventional casing (e.g., "WWW-Authenticate"),
but since HTTP header names are case-insensitive, this always uses simple capitalization.
 -/
Std.Http.Header.Name.toCanonical : Std.Http.Header.Name → String
-- Mathlib.Data.Int.Log
/-- The least power of `b` such that `r ≤ b ^ log b r`.  -/
Int.clog : {R : Type u_1} → [inst : Semifield R] → [inst_1 : LinearOrder R] → [FloorSemiring R] → ℕ → R → ℤ
-- Batteries.Classes.Order
/-- Pull back a comparator by a function `f`, by applying the comparator to both arguments.  -/
Ordering.byKey : {α : Sort u_1} → {β : Sort u_2} → (α → β) → (β → β → Ordering) → α → α → Ordering
-- Mathlib.Algebra.Module.FinitePresentation
instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) [Module.FinitePresentation R M],
  IsLocalizedModule S (LocalizedModule.map S)
-- Init.Data.List.Count
List.countP_true : ∀ {α : Type u_1}, (List.countP fun x => true) = List.length
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- We have `[W, 0] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable.  -/
VectorField.mlieBracket_zero_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {W : (x : M) → TangentSpace I x},
  VectorField.mlieBracket I W 0 = 0
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.of_iso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom],
  p.IsStronglyCartesian f φ.hom
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_iInf_principal : ∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊇ x2) s → ∀ [Nonempty ι], (⨅ i, Filter.principal (s i)).HasBasis (fun x => True) s
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- Post-composition by a *fixed* continuous linear map as a continuous linear map for the pointwise
convergence topology.  -/
PointwiseConvergenceCLM.postcomp : {𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    {𝕜₃ : Type u_6} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    (E : Type u_7) →
                      {F : Type u_8} →
                        {G : Type u_10} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : TopologicalSpace E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : TopologicalSpace F] →
                                  [inst_8 : IsTopologicalAddGroup F] →
                                    [inst_9 : AddCommGroup G] →
                                      [inst_10 : TopologicalSpace G] →
                                        [inst_11 : IsTopologicalAddGroup G] →
                                          [inst_12 : Module 𝕜₁ E] →
                                            [inst_13 : Module 𝕜₂ F] →
                                              [inst_14 : Module 𝕜₃ G] →
                                                [inst_15 : ContinuousConstSMul 𝕜₂ F] →
                                                  [inst_16 : ContinuousConstSMul 𝕜₃ G] →
                                                    (F →SL[τ] G) → (E →SLₚₜ[σ] F) →SL[τ] E →SLₚₜ[ρ] G
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A `Subsemiring` containing -1 is a `Subring`.  -/
Subsemiring.toSubring : {R : Type u} → [inst : NonAssocRing R] → (s : Subsemiring R) → -1 ∈ s → Subring R
-- Lean.Syntax
Lean.isLitKind : Lean.SyntaxNodeKind → Bool
-- Mathlib.AlgebraicGeometry.Restrict
/-- For `f : R`, `D(f)` as an open subscheme of `Spec R` is isomorphic to `Spec R[1/f]`.  -/
AlgebraicGeometry.basicOpenIsoSpecAway : {R : CommRingCat} →
  (f : ↑R) → ↑(PrimeSpectrum.basicOpen f) ≅ AlgebraicGeometry.Spec (CommRingCat.of (Localization.Away f))
-- Init.Data.UInt.Lemmas
USize.lt_or_eq_of_le : ∀ {a b : USize}, a ≤ b → a < b ∨ a = b
-- Std.Http.Data.URI.Config
Std.Http.URI.Config.mk.sizeOf_spec : ∀
  (maxSchemeLength maxHostLength maxUserInfoLength maxSegmentLength maxQueryLength maxFragmentLength maxPathSegments
    maxTotalPathLength maxQueryParams : ℕ),
  sizeOf
      { maxSchemeLength := maxSchemeLength, maxHostLength := maxHostLength, maxUserInfoLength := maxUserInfoLength,
        maxSegmentLength := maxSegmentLength, maxQueryLength := maxQueryLength, maxFragmentLength := maxFragmentLength,
        maxPathSegments := maxPathSegments, maxTotalPathLength := maxTotalPathLength,
        maxQueryParams := maxQueryParams } =
    1 + sizeOf maxSchemeLength + sizeOf maxHostLength + sizeOf maxUserInfoLength + sizeOf maxSegmentLength +
              sizeOf maxQueryLength +
            sizeOf maxFragmentLength +
          sizeOf maxPathSegments +
        sizeOf maxTotalPathLength +
      sizeOf maxQueryParams
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk.injEq : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_16}
  {M₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  (toAddHom : M →ₙ+ M₂) (map_smul' : ∀ (m : R) (x : M), toAddHom.toFun (m • x) = σ m • toAddHom.toFun x)
  (toAddHom_1 : M →ₙ+ M₂) (map_smul'_1 : ∀ (m : R) (x : M), toAddHom_1.toFun (m • x) = σ m • toAddHom_1.toFun x),
  ({ toAddHom := toAddHom, map_smul' := map_smul' } = { toAddHom := toAddHom_1, map_smul' := map_smul'_1 }) =
    (toAddHom = toAddHom_1)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]), ↑(z1 * z2) = ↑z1 * ↑z2
-- Mathlib.Algebra.Group.Prod
MonoidHom.snd_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N) (g : M →* P), (MonoidHom.snd N P).comp (f.prod g) = g
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor_μ : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N)
  (m₁ m₂ : CategoryTheory.Discrete M),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.comap`.

---

A morphism of monoid objects induces a "restriction" or "comap" functor
between the categories of module objects.
 -/
CategoryTheory.Mod_.comap : {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.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                [inst_5 : CategoryTheory.MonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsMonHom f] →
                      CategoryTheory.Functor (CategoryTheory.Mod D B) (CategoryTheory.Mod D A)
-- Mathlib.NumberTheory.Divisors
Nat.divisors.eq_1 : ∀ (n : ℕ), n.divisors = {d ∈ Finset.Ico 1 (n + 1) | d ∣ n}
-- Mathlib.SetTheory.ZFC.Basic
/-- Indexed union of a family of ZFC sets. Uses `⋃` notation, scoped under the `ZFSet` namespace.  -/
ZFSet.iUnion : {α : Type u_1} → [Small.{u, u_1} α] → (α → ZFSet.{u}) → ZFSet.{u}
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_ofHom : ∀ {X Y : Type u} [inst : LinearOrder X] [inst_1 : LinearOrder Y] (f : X →o Y), LinOrd.Hom.hom (LinOrd.ofHom f) = f
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_le_mabs_of_le_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α],
  a ≤ 1 → b ≤ a → |a|ₘ ≤ |b|ₘ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.Mon_tensor_mul_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
-- Mathlib.Algebra.Order.Monovary
monovary_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → (Monovary f⁻¹ g ↔ Antivary f g)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedCnstrRHS.default : Lean.Meta.Grind.CnstrRHS
-- Init.Data.SInt.Basic
Int32.instOfNat : {n : ℕ} → OfNat Int32 n
-- Mathlib.Order.CompleteLattice.Basic
le_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α},
  (∀ (i : ι) (j : κ i), a ≤ f i j) → a ≤ ⨅ i, ⨅ j, f i j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).getKey? k = m₁.getKey? k
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η h)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The bundled group giving the filtered colimit of a diagram.  -/
GrpCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J GrpCat → GrpCat
-- Lean.Data.NameTrie
Lean.NamePart.str : String → Lean.NamePart
-- Batteries.Data.UInt
UInt16.lt_iff_toNat_lt_toNat : ∀ {x y : UInt16}, x < y ↔ x.toNat < y.toNat
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.moduleEndRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {X Y : C} → Module (CategoryTheory.End Y) (X ⟶ Y)
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairing_neg_one_neg_four_iff' : ∀ {ι : 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 j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N],
  IsSMulRegular R 2 → (P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_comp_assoc : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} (f : M₃ →ₛₗ[σ₃₁] M₁)
  [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂], ↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f = f
-- Init.SimpLemmas
forall_prop_congr_dom : ∀ {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → Prop), (∀ (a : p₁), q a) = ∀ (a : p₂), q ⋯
-- Lean.DocString.Parser
/-- The block's maximal directive size (that is, the greatest number of allowed colons).
 -/
Lean.Doc.Parser.BlockCtxt.maxDirective : Lean.Doc.Parser.BlockCtxt → Option ℕ
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_bind_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V),
  (AffineSpace.asymptoticNhds k V v).bind (AffineSpace.asymptoticNhds k P) = AffineSpace.asymptoticNhds k P v
-- Mathlib.Data.DFinsupp.Lex
/-- The less-than relation for the lexicographic ordering is decidable.  -/
DFinsupp.Lex.decidableLT : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : LinearOrder ι] → [inst_2 : (i : ι) → LinearOrder (α i)] → DecidableLT (Lex (Π₀ (i : ι), α i))