mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for a multiplicative arithmetic function `f` with values in a
complete normed commutative ring `R`: if `‖f ·‖` is summable, then
`∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`.
This version is stated in the form of convergence of finite partial products.  -/
ArithmeticFunction.IsMultiplicative.eulerProduct : ∀ {R : Type u_1} [inst : NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R},
  f.IsMultiplicative →
    (Summable fun x => ‖f x‖) →
      Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ℕ), f n))
-- Init.System.IO
/-- Runs `act` in a separate `Task`, with priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Pure accesses to the
`Task` do not influence the impure `act`.

Unlike pure tasks created by `Task.spawn`, tasks created by this function will run even if the last
reference to the task is dropped. The `act` should explicitly check for cancellation via
`IO.checkCanceled` if it should be terminated or otherwise react to the last reference being
dropped.
 -/
BaseIO.asTask : {α : Type} → BaseIO α → optParam Task.Priority Task.Priority.default → BaseIO (Task α)
-- Mathlib.Tactic.Linter.DocString
/-- Extract all `declModifiers` from the input syntax. We later extract the `docstring` from it,
but we avoid extracting directly the `docComment` node, to skip `#adaptation_note`s.
 -/
Mathlib.Linter.getDeclModifiers : Lean.Syntax → Array Lean.Syntax
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.goals : Lean.Elab.Tactic.Grind.State → List Lean.Meta.Grind.Goal
-- Std.Data.ExtHashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtHashSet.getD : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → α → α
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- A locally compact right-uniform additive group is complete.  -/
IsRightUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace : ∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsRightUniformAddGroup G] [WeaklyLocallyCompactSpace G],
  CompleteSpace G
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂),
  (I.multicoforkEquivSigmaCofork.functor.map f).hom = f.hom
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yoneda_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ),
  (CategoryTheory.yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
-- Std.Data.DTreeMap.Internal.Model
/-- General tree-traversal function. Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.applyPartition : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      [inst : Ord α] →
        (k : α → Ordering) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (List ((a : α) × β a) →
                (c : Std.DTreeMap.Internal.Cell α β k) →
                  (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ) →
              δ
-- Mathlib.Algebra.Squarefree.Basic
isRadical_iff_squarefree_or_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x : R} [DecompositionMonoid R],
  IsRadical x ↔ Squarefree x ∨ x = 0
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_inter : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β},
  ContinuousWithinAt g t (f x) → ContinuousWithinAt f s x → ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib.Data.Set.Prod
Set.image_prodMk_subset_prod_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α}, a ∈ s → Prod.mk a '' t ⊆ s ×ˢ t
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember : Type
-- Init.Data.SInt.Basic
/-- Adds two word-sized signed integers, wrapping around on over- or underflow.  Usually accessed via
the `+` operator.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.add : ISize → ISize → ISize
-- Std.Http.Data.Request
Std.Http.Request.Builder.mk.inj : ∀ {line : Std.Http.Request.Head} {extensions : Std.Http.Extensions} {line_1 : Std.Http.Request.Head}
  {extensions_1 : Std.Http.Extensions},
  { line := line, extensions := extensions } = { line := line_1, extensions := extensions_1 } →
    line = line_1 ∧ extensions = extensions_1
-- Lean.MetavarContext
Lean.LocalInstance.mk.inj : ∀ {className : Lean.Name} {fvar : Lean.Expr} {className_1 : Lean.Name} {fvar_1 : Lean.Expr},
  { className := className, fvar := fvar } = { className := className_1, fvar := fvar_1 } →
    className = className_1 ∧ fvar = fvar_1
-- Init.System.IO
/-- Executes arbitrary side effects in a pure context. This a **dangerous** operation that can easily
undermine important assumptions about the meaning of Lean programs, and it should only be used with
great care and a thorough understanding of compiler internals, and even then only to implement
observationally pure operations.

This function is not a good way to convert a `BaseIO α` into an `α`. Instead, use
[`do`-notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation).

Because the resulting value is treated as a side-effect-free term, the compiler may re-order,
duplicate, or delete calls to this function. The side effect may even be hoisted into a constant,
causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
unsafeBaseIO : {α : Type} → BaseIO α → α
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.preimage_null : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → ∀ {s : Set β}, μb s = 0 → μa (f ⁻¹' s) = 0
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.wellPowered_of_isDetector : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] (G : C),
  CategoryTheory.IsDetector G → CategoryTheory.WellPowered.{v₁, v₁, u₁} C
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_le_diam : ∀ (s : Set ℝ), MeasureTheory.volume s ≤ Metric.ediam s
-- Mathlib.Topology.Algebra.Monoid
ContinuousAdd.to_continuousVAdd_op : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousVAdd Mᵃᵒᵖ M
-- Mathlib.Algebra.Group.Action.Sum
Sum.vadd_inl : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] (a : M) (b : α),
  a +ᵥ Sum.inl b = Sum.inl (a +ᵥ b)
-- Batteries.Data.String.Legacy
String.Pos.Raw.utf8GetAux.eq_def : ∀ (x : List Char) (x_1 x_2 : String.Pos.Raw),
  String.Pos.Raw.utf8GetAux x x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, x_3 => default
    | c :: cs, i, p => if i = p then c else String.Pos.Raw.utf8GetAux cs (i + c) p
-- Lean.Parser.Basic
Lean.Parser.instCoeStringParser : Coe String Lean.Parser.Parser
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedTerminationHints : Inhabited Lean.Elab.TerminationHints
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- An overring of a valuation ring is a valuation ring.  -/
ValuationSubring.ofLE : {K : Type u} → [inst : Field K] → (R : ValuationSubring K) → (S : Subring K) → R.toSubring ≤ S → ValuationSubring K
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Grind.CommRing.Mon.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Grind.CommRing.Mon → M Lean.Expr
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalHom.of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [Nontrivial S] [IsLocalRing R] (f : R →+* S),
  Function.Surjective ⇑f → IsLocalHom f
-- Lean.Parser.Tactic
Lean.Parser.Tactic.unknown.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnectParams.mk.inj : ∀ {uri uri_1 : Lean.Lsp.DocumentUri}, { uri := uri } = { uri := uri_1 } → uri = uri_1
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_tsub_tsub_cancel_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → a - c - (a - b) = b - c
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.forM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}}, t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Mathlib.Topology.Homeomorph.Defs
/-- If both `X` and `Y` have a unique element, then `X ≃ₜ Y`.  -/
Homeomorph.homeomorphOfUnique : (X : Type u_1) →
  (Y : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [Unique X] → [Unique Y] → X ≃ₜ Y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.diseq_to_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a b : α), a ≠ b → (a - b) * (a - b)⁻¹ = 1
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.pointed_zero : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ConvexCone.Pointed 0
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.root_sub_root_mem_of_pairingIn_pos : ∀ {ι : 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) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] {i j : ι} [IsDomain R],
  0 < P.pairingIn ℤ i j → i ≠ j → P.root i - P.root j ∈ Set.range ⇑P.root
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₂ X₂' : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (g' : R.obj X₂' ⟶ B.obj X₃) (γ : X₂' ⟶ X₂)
  (hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g') (A : w.CostructuredArrowDownwards g),
  (w.costructuredArrowDownwardsPrecomp g g' γ hγ).obj A =
    CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g' (CategoryTheory.CostructuredArrow.left A).right
      (CategoryTheory.CategoryStruct.comp γ (CategoryTheory.CostructuredArrow.left A).hom)
      (CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.CostructuredArrow.hom A)) ⋯
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.normSq_eq_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [cd : InnerProductSpace.Core 𝕜 F] {x : F}, InnerProductSpace.Core.normSq x = 0 ↔ x = 0
-- Mathlib.Topology.Category.TopCat.Limits.Basic
_private.Mathlib.Topology.Category.TopCat.Limits.Basic.0.termForget : Lean.ParserDescr
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.instGroup : {X : Type u_1} → [inst : TopologicalSpace X] → Group (X ≃ₜ X)
-- Init.Data.Nat.Basic
Nat.not_lt_of_le : ∀ {a b : ℕ}, a ≤ b → ¬b < a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_monomial_index : ∀ {R : Type u_1} [inst : Semiring R] {N : Type u_5} [inst_1 : AddCommMonoid N] {n : ℕ} {b : R} {h : ℕ → R → N},
  h n 0 = 0 → ((SkewPolynomial.monomial n) b).sum h = h n b
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.DTreeMap.Raw.maxKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Option α
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- At each step of the inductive construction, the cardinality bound `≤ #s ^ ℵ₀` holds.  -/
MeasurableSpace.cardinal_generateMeasurableRec_le : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{v}),
  Cardinal.mk ↑(MeasurableSpace.generateMeasurableRec s i) ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
-- Mathlib.Data.ZMod.QuotientGroup
/-- The sum of minimal periods over all orbits equals the index `[G:H]`.  -/
Subgroup.index_eq_sum_minimalPeriod : ∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G) [Finite (G ⧸ H)]
  [inst_2 : Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))],
  H.index = ∑ q, Function.minimalPeriod (fun x => g • x) q.out
-- Mathlib.Algebra.Vertex.HVertexOperator
/-- A heterogeneous `Γ`-vertex operator over a commutator ring `R` is an `R`-linear map from an
`R`-module `V` to `Γ`-Hahn series with coefficients in an `R`-module `W`.  -/
HVertexOperator : (Γ : Type u_5) →
  [PartialOrder Γ] →
    (R : Type u_6) →
      [inst : CommRing R] →
        (V : Type u_7) →
          (W : Type u_8) →
            [inst_1 : AddCommGroup V] → [Module R V] → [inst_3 : AddCommGroup W] → [Module R W] → Type (max u_7 u_8 u_5)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The difference of `log (1-z)⁻¹` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`.  -/
Complex.norm_log_one_sub_inv_add_logTaylor_neg_le : ∀ (n : ℕ) {z : ℂ},
  ‖z‖ < 1 → ‖Complex.log (1 - z)⁻¹ + Complex.logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given a functor `F : C ⥤ D`, this definition is part of the verification that
`Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom`
is universal, i.e. that  `F.op.lan : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂`
is the left Kan extension of `F ⋙ uliftYoneda : C ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂`
along `uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂`.  -/
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.extensionHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] →
            (Φ :
                CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension
                  (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂})) →
              CategoryTheory.Functor.LeftExtension.mk F.op.lan
                  (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶
                Φ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.essImage_yonedaMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaMon.essImage = fun F => (F.comp (CategoryTheory.forget MonCat)).IsRepresentable
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an object of `P.Under Q X` from a morphism `f : A ⟶ X` and a proof of `P f`.  -/
CategoryTheory.MorphismProperty.Under.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) → {X A : T} → (f : X ⟶ A) → P f → P.Under Q X
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.insertMany [] = t
-- Lean.Elab.BuiltinCommand
/-- Elaborate `#show_deprecated_modules`, displaying all deprecated modules.  -/
Lean.Elab.Command.elabShowDeprecatedModules : Lean.Elab.Command.CommandElab
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Convert the heap to an array in arbitrary order.  -/
Batteries.BinomialHeap.toArrayUnordered : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Array α
-- Init.Data.List.Nat.TakeDrop
List.set_eq_take_append_cons_drop : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α},
  l.set i a = if i < l.length then List.take i l ++ a :: List.drop (i + 1) l else l
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_inv_comp_iCocycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).inv (groupCohomology.iCocycles A 0) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f (groupCohomology.cochainsIso₀ A).inv
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Topology.Category.CompHausLike.Cartesian
/-- When the predicate `P` is preserved under taking type-theoretic products, that product is a
category-theoretic product in `CompHausLike P`.
 -/
CompHausLike.productIsLimit : {P : TopCat → Prop} →
  (X Y : CompHausLike P) →
    [inst : CompHausLike.HasProp P (↑X.toTop × ↑Y.toTop)] → CategoryTheory.Limits.IsLimit (X.productCone Y)
-- Lean.Elab.Term.TermElabM
/-- Convert unassigned universe level metavariables into parameters.
The new parameter names are fresh names of the form `u_i` with regard to `ctx.levelNames`, which is updated with the new names.  -/
Lean.Elab.Term.levelMVarToParam : Lean.Expr → (optParam (Lean.LMVarId → Bool) fun x => false) → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → (Std.DHashMap.Raw.Const.toList m).isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y X' : C}
  (s : X' ⟶ X) (hs : W s) (f : X' ⟶ Y) (X'_1 : C) (s_1 : X'_1 ⟶ X) (hs_1 : W s_1) (f_1 : X'_1 ⟶ Y),
  ({ X' := X', s := s, hs := hs, f := f } = { X' := X'_1, s := s_1, hs := hs_1, f := f_1 }) =
    (X' = X'_1 ∧ s ≍ s_1 ∧ f ≍ f_1)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The **correspondence theorem**, or lattice theorem,
or fourth isomorphism theorem for additive groups  -/
QuotientAddGroup.comapMk'OrderIso : {G : Type u} → [inst : AddGroup G] → (N : AddSubgroup G) → [hn : N.Normal] → AddSubgroup (G ⧸ N) ≃o { H // N ≤ H }
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The identity of the minimal pre-`1`-hypercover when `E` has pairwise pullbacks
is homotopic to itself.  -/
CategoryTheory.PreZeroHypercover.toPreOneHypercoverHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        [inst_1 : E.HasPullbacks] →
          CategoryTheory.PreOneHypercover.Homotopy (CategoryTheory.PreOneHypercover.Hom.id E.toPreOneHypercover)
            (CategoryTheory.PreOneHypercover.Hom.id E.toPreOneHypercover)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The `M`-equivariant functions from a monoid `M` to itself are exactly
right multiplications by elements of `M`. See also `RingEquiv.moduleEndSelf`.  -/
MulActionHom.End.equivMulOpposite : {M : Type u_2} → [inst : Monoid M] → (M →ₑ[id] M) ≃* Mᵐᵒᵖ
-- Mathlib.Algebra.Order.Archimedean.Basic
Units.instMulArchimedean : ∀ (M : Type u_5) [inst : CommMonoid M] [inst_1 : PartialOrder M] [MulArchimedean M], MulArchimedean Mˣ
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.expandIntValuePattern : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound.inj : ∀ {h h_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound h = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound h_1 → h = h_1
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : X' ⟶ F.partialRightAdjointObj Y)
  (g : X ⟶ X'),
  F.partialRightAdjointHomEquiv (CategoryTheory.CategoryStruct.comp g f) =
    CategoryTheory.CategoryStruct.comp (F.map g) (F.partialRightAdjointHomEquiv f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLE!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited (α × β)],
          Std.DTreeMap.Internal.Impl.Const.getEntryLE! k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryLE! k t₂
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_concat_zero : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (x.concat b).getLsbD 0 = b
-- Mathlib.Data.Ordering.Basic
/-- `o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on
`h : o₁ = .eq`.  -/
Ordering.dthen : (o : Ordering) → (o = Ordering.eq → Ordering) → Ordering
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂)[k]! = default
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csSup_iff' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
  BddAbove s → (a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b)
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_of_shell : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {ε C : ℝ}, 0 < ε → 0 ≤ C → ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) → ‖f‖ ≤ C
-- Init.Data.Nat.Fold
/-- Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f`
is applied to the current value and to the next natural number less than `n`, in increasing order.

This is a tail-recursive version of `Nat.fold` that's used at runtime.

Examples:
* `Nat.foldTR 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))`
* `Nat.foldTR 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]`
* `Nat.foldTR 0 (fun i _ xs => xs.push i) #[] = #[]`
 -/
Nat.foldTR : {α : Type u} → (n : ℕ) → ((i : ℕ) → i < n → α → α) → α → α
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_order_subst_right : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f : MvPowerSeries τ R} {φ : PowerSeries R},
  MvPowerSeries.constantCoeff f = 0 → PowerSeries.constantCoeff φ = 0 → f.order ≤ (PowerSeries.subst f φ).order
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)