mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.add_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddZeroClass P] (g₁ g₂ : M →+ N) (f : P →+ M), (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ofNat_mul' : ∀ {x : ℂ} {n : ℕ} [inst : n.AtLeastTwo],
  -Real.pi < OfNat.ofNat n * x.arg →
    OfNat.ofNat n * x.arg ≤ Real.pi → ∀ (y : ℂ), x ^ (OfNat.ofNat n * y) = (x ^ OfNat.ofNat n) ^ y
-- Mathlib.LinearAlgebra.Basis.Fin
/-- Let `b` be a basis for a submodule `N ≤ O`. If `y ∈ O` is linear independent of `N`
and `y` and `N` together span the whole of `O`, then there is a basis for `O`
whose basis vectors are given by `Fin.cons y b`.  -/
Module.Basis.mkFinConsOfLE : {R : Type u_3} →
  {M : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {n : ℕ} →
            {N O : Submodule R M} →
              (y : M) →
                y ∈ O →
                  Module.Basis (Fin n) R ↥N →
                    N ≤ O →
                      (∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) →
                        (∀ z ∈ O, ∃ c, z + c • y ∈ N) → Module.Basis (Fin (n + 1)) R ↥O
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph0_mul_continuum : Cardinal.aleph0 * Cardinal.continuum = Cardinal.continuum
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.mapMonoidHom_apply : ∀ {ι : 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)] (f : (i : ι) → s i →ₗ[R] s i),
  PiTensorProduct.mapMonoidHom f = PiTensorProduct.map f
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_subset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α} {s : Set α}, a ∈ s → a • t ⊆ s • t
-- Mathlib.GroupTheory.Index
AddSubgroup.index_smul : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A] (a : G)
  (S : AddSubgroup A), (a • S).index = S.index
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]! = m[k]!
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into a `Year` format.
 -/
Std.Time.Year.classify : ℕ → Option Std.Time.Year
-- Mathlib.Geometry.Manifold.VectorField.Pullback
instIsManifoldOfNatWithTopENatOfMinSmoothness_1 : ∀ {𝕜 : 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] [IsManifold I (minSmoothness 𝕜 1) M], IsManifold I 1 M
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterM m α → Sort u_3) →
      (it : Std.IterM m α) →
        (Unit → motive { internalState := { list := [] } }) →
          ((x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }) → motive it
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Filter.EventuallyEq.trans_isEquivalent : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {f g₁ g₂ : α → β},
  f =ᶠ[l] g₁ → Asymptotics.IsEquivalent l g₁ g₂ → Asymptotics.IsEquivalent l f g₂
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_nil : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α], m.WF → m.insertMany [] = m
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.neq_of_mem_ofStabilizer : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (a : α)
  {x : ↥(SubAddAction.ofStabilizer G a)}, ↑x ≠ a
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded URI userinfo component. Valid characters are `unreserved / sub-delims / ":"`.
 -/
Std.Http.URI.EncodedUserInfo : Type
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the sum of `f i` over `i ∈ s` is not equal to `0`, then there is some `x ∈ s`
such that `f x ≠ 0`.  -/
exists_ne_zero_of_finsum_mem_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
  ∑ᶠ (i : α) (_ : i ∈ s), f i ≠ 0 → ∃ x ∈ s, f x ≠ 0
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- An isometry between quadratic forms generated by `QuadraticForm.prod` can be constructed
from a pair of isometries between the left and right parts.  -/
QuadraticMap.IsometryEquiv.prod : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N₁ : Type u_5} →
        {N₂ : Type u_6} →
          {P : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M₁] →
                [inst_2 : AddCommMonoid M₂] →
                  [inst_3 : AddCommMonoid N₁] →
                    [inst_4 : AddCommMonoid N₂] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : Module R M₁] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module R N₁] →
                              [inst_9 : Module R N₂] →
                                [inst_10 : Module R P] →
                                  {Q₁ : QuadraticMap R M₁ P} →
                                    {Q₂ : QuadraticMap R M₂ P} →
                                      {Q₁' : QuadraticMap R N₁ P} →
                                        {Q₂' : QuadraticMap R N₂ P} →
                                          Q₁.IsometryEquiv Q₁' →
                                            Q₂.IsometryEquiv Q₂' → (Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂')
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `Localization.AtPrime.under_maximalIdeal`.

---

The unique maximal ideal of the localization at `I.primeCompl` lies over the ideal `I`.  -/
Localization.AtPrime.comap_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
  Ideal.under R (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
-- Mathlib.Order.WellFoundedSet
Set.IsWF.le_min_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty),
  a ≤ hs.min hn ↔ ∀ b ∈ s, a ≤ b
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.refl_toPartialEquiv : ∀ (X : Type u_1) (G : Type u_2) [inst : Monoid G] [inst_1 : MulAction G X],
  (Equidecomp.refl X G).toPartialEquiv = PartialEquiv.refl X
-- Mathlib.Analysis.Convex.Contractible
/-- A non-empty star convex set is a contractible space.  -/
StarConvex.contractibleSpace : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E} {x : E}, StarConvex ℝ x s → s.Nonempty → ContractibleSpace ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.ext₀_iff : ∀ {X : SSet} {f g : X.Path 0}, f = g ↔ f.vertex 0 = g.vertex 0
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.differentiableOn_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  DifferentiableOn ℝ (ProbabilityTheory.mgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.sup : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n}, φ.IsQF → ψ.IsQF → (φ ⊔ ψ).IsQF
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- If `n₁ ≥ n₂` and `K₁ ⊆ K₂`, `monoLM 𝕜` is the `𝕜`-linear inclusion of
`𝓓^{n₁}_{K₁}(E, F)` inside `𝓓^{n₂}_{K₂}(E, F)`. Otherwise, this is the zero map.

This is in fact continuous (see `monoCLM`). Furthermore:
* it is a topological embedding when `n₁ = n₂` and `K₁ ⊆ K₂` (not in Mathlib as of March 2026).
* it maps bounded sets to compact sets when `n₁ ≥ n₂ + 1` and `K₁ ⊆ K₂` (not in Mathlib as of
March 2026).

The parameters `n₁, n₂, K₁, K₂` are implicit as they can often be inferred from context, or
specified by a type ascription.
 -/
ContDiffMapSupportedIn.monoLM : (𝕜 : 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₁ n₂ : ℕ∞} →
                      {K₁ K₂ : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n₁ K₁ →ₗ[𝕜] ContDiffMapSupportedIn E F n₂ K₂
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.base.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f), s.base = s.π.app none
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- The coercion between numerator-denominator pairs happens componentwise.  -/
GenContFract.Pair.coeFn : {α : Type u_1} → {β : Type u_2} → [Coe α β] → GenContFract.Pair α → GenContFract.Pair β
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.below : {L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsExistential → Prop} →
      {n : ℕ} → {a : L.BoundedFormula α n} → a.IsExistential → Prop
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- Given such a diagram, then there is a natural morphism from the weak pullback of
`W ⟶ S` and `X ⟶ S` to the weak pullback of `Y ⟶ T` and `Z ⟶ T`.

```
W ⟶ Y
  ↘   ↘
  S ⟶ T
  ↗   ↗
X ⟶ Z
```
 -/
CategoryTheory.Limits.weakPullback.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z S T : C} →
      (f₁ : W ⟶ S) →
        (f₂ : X ⟶ S) →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f₁ f₂] →
            (g₁ : Y ⟶ T) →
              (g₂ : Z ⟶ T) →
                [inst_2 : CategoryTheory.Limits.HasWeakPullback g₁ g₂] →
                  (i₁ : W ⟶ Y) →
                    (i₂ : X ⟶ Z) →
                      (i₃ : S ⟶ T) →
                        CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁ →
                          CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂ →
                            (CategoryTheory.Limits.weakPullback f₁ f₂ ⟶ CategoryTheory.Limits.weakPullback g₁ g₂)
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.size : Lean.Grind.CommRing.Poly → ℕ
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskering_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c)
  {X Y : CategoryTheory.Bicategory.LeftLift f g} (η : X ⟶ Y),
  (CategoryTheory.Bicategory.LeftLift.whiskering h).map η =
    CategoryTheory.Bicategory.LeftLift.homMk
      (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.StructuredArrow.Hom.right η)) ⋯
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd.eq_1 : ∀ {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] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)),
  CategoryTheory.Functor.CommShift.isoAdd e₁ e₂ = CategoryTheory.Functor.CommShift.isoAdd' ⋯ e₁ e₂
-- Mathlib.Topology.MetricSpace.Isometry
/-- The right inverse of an isometry is an isometry.  -/
Isometry.right_inv : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {g : β → α},
  Isometry f → Function.RightInverse g f → Isometry g
-- Mathlib.Combinatorics.Graph.Simple
Graph.vertexSet_nontrivial_of_edgeSet_nonempty_of_loopless : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless], G.edgeSet.Nonempty → G.vertexSet.Nontrivial
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_anti_left_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {y : ι → ℝ}, AntitoneOn (fun x => dist x y) (Set.Iic y)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_three_lt_d9 : Real.log 3 < 1.0986122888
-- Init.Data.Order.MinMaxOn
_private.Init.Data.Order.MinMaxOn.0.maxOn.eq_1 : ∀ {β : Type u_1} {α : Sort u_2} [i : LE β] [inst : DecidableLE β] (f : α → β) (x y : α), maxOn f x y = minOn f x y
-- Mathlib.Order.SuccPred.LinearLocallyFinite
Countable.of_linearOrder_locallyFiniteOrder : ∀ {ι : Type u_1} [inst : LinearOrder ι] [LocallyFiniteOrder ι], Countable ι
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.tensorToSpan.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M),
  Submodule.tensorToSpan A p =
    TensorProduct.AlgebraTensorModule.lift
      { toFun := fun a => a • Submodule.inclusionSpan A p, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (pt : C) → ((CategoryTheory.Functor.const J).obj pt ⟶ F) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] [inst_2 : DecidableEq β]
  [inst_3 : InvolutiveInv β] (s : Finset α) (t : Finset β), (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_injective : ∀ {α : Type u_1} [inst : Encodable α], Function.Injective Encodable.encode
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The primitive character associated to a Dirichlet character.  -/
DirichletCharacter.primitiveCharacter : {R : Type u_1} →
  [inst : CommMonoidWithZero R] → {n : ℕ} → (χ : DirichletCharacter R n) → DirichletCharacter R χ.conductor
-- Mathlib.Algebra.Category.BoolRing
BoolRing.booleanRing : (self : BoolRing) → BooleanRing ↑self
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivisionCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α],
  MulOpposite.instDivisionCommMonoid = { toDivisionMonoid := MulOpposite.instDivisionMonoid, mul_comm := ⋯ }
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X),
  AlgebraicGeometry.Scheme.stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ⋯).hom
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → (∀ y ∈ s, g y = f y) → x ∈ s → ContinuousWithinAt g s x
-- Mathlib.Order.PropInstances
Prop.top_eq_true : ⊤ = True
-- Init.Meta.Defs
/-- Returns the number of hexadecimal digits.  -/
Lean.TSyntax.getHexNumSize : Lean.Syntax.HexNum → ℕ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtDHashMap.filter f m},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.filter f m) k h' = Std.ExtDHashMap.Const.get m k ⋯
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.η_toLinearMap : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k],
  (Representation.LinearizeMonoidal.η k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1})
-- Mathlib.Combinatorics.HalesJewett
/-- The combinatorial subspace corresponding to the identity embedding `(ι → α) → (ι → α)`.  -/
Combinatorics.Subspace.instInhabited : {α : Type u_6} → {ι : Type u_7} → Inhabited (Combinatorics.Subspace ι α ι)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.smul : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → SMul (AdicCompletion I R) (AdicCompletion I M)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc : ∀ {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]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.LaxMonoidal.ε G))
      (CategoryTheory.CategoryStruct.comp (adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) h
-- Lean.Environment
/-- Retrieves additional IR extension state for the interpreter.  -/
Lean.PersistentEnvExtension.getModuleIREntries : {α β σ : Type} → [Inhabited σ] → Lean.PersistentEnvExtension α β σ → Lean.Environment → Lean.ModuleIdx → Array α
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Candidate function for the tensor product of objects.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj : (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} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  D → D → D
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  (X_1 : C),
  (CategoryTheory.WithTerminal.equivComma.counitIso.inv.app X).left.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithTerminal.incl.obj X_1 with
      | CategoryTheory.WithTerminal.of x => X.left.obj x
      | CategoryTheory.WithTerminal.star => X.right)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.AlmostMono.mk.injEq : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} (line : Combinatorics.Line (Option α) ι)
  (color : κ) (has_color : ∀ (x : α), C (↑line (some x)) = color) (line_1 : Combinatorics.Line (Option α) ι)
  (color_1 : κ) (has_color_1 : ∀ (x : α), C (↑line_1 (some x)) = color_1),
  ({ line := line, color := color, has_color := has_color } =
      { line := line_1, color := color_1, has_color := has_color_1 }) =
    (line = line_1 ∧ color = color_1)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.isWF_support_evalCoeff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] (x : M), (Function.support (f.evalCoeff x)).IsWF
-- Mathlib.Tactic.FBinop
/-- For a given argument `x`, checks if there is a coercion from `fromS x` to `toS x`
if these expressions are type correct.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.hasCoeS : FBinopElab.SRec → FBinopElab.SRec → Lean.Expr → Lean.Elab.TermElabM Bool
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instModule : {𝕜 : Type u_2} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NormedField 𝕜] → [inst_5 : NormedSpace 𝕜 F] → [SMulCommClass ℝ 𝕜 F] → Module 𝕜 (SchwartzMap E F)
-- Batteries.Data.List.Lemmas
List.eraseIdx_idxOf_eq_erase : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), l.eraseIdx (List.idxOf a l) = l.erase a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
CategoryTheory.instCreatesLimitsOfShapeGrpMonForget₂Mon : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.Category.{u_2, w} J] →
          [CategoryTheory.Limits.HasLimitsOfShape J C] →
            CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.Grp.forget₂Mon C)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
0th face of a 2-simplex.  -/
SSet.Truncated.ev12₂ : {V : SSet.Truncated 2} →
  (φ : V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 })) →
    SSet.Truncated.ev1₂ φ ⟶ SSet.Truncated.ev2₂ φ
-- Mathlib.Analysis.Convex.BetweenList
List.Wbtw.map : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {l : List P},
  List.Wbtw R l → ∀ (f : P →ᵃ[R] P'), List.Wbtw R (List.map (⇑f) l)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.adic_surj : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type}
  (f : (ι → R) →ₗ[R] M), Function.Surjective ⇑f → Function.Surjective ⇑(AdicCompletion.map I f)
-- Lean.Environment
/-- Number of times each declaration has been unfolded by the kernel.  -/
Lean.Kernel.Diagnostics.unfoldCounter : Lean.Kernel.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- When `C` acts on the left on `D`, the functor
`curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ` is monoidal, where `D ⥤ D` has the
composition monoidal structure.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D).Monoidal
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.mk.sizeOf_spec : ∀ (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree),
  sizeOf { ctx := ctx, info := info, children := children } = 1 + sizeOf ctx + sizeOf info + sizeOf children