mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- abstraction function for dependent sums  -/
MvQPF.Sigma.abs : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) →
      [inst : (α : A) → MvQPF (F α)] → ⦃α : TypeVec.{u} n⦄ → ↑(MvQPF.Sigma.P F) α → MvQPF.Sigma F α
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.termφ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyClass.sound : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.RightHomotopyRel f g →
    HomotopicalAlgebra.RightHomotopyClass.mk f = HomotopicalAlgebra.RightHomotopyClass.mk g
-- Batteries.Classes.Order
/-- Class for types where the ordering function is compatible with the `LE`.  -/
Std.LawfulLEOrd : (α : Type u_1) → [LE α] → [Ord α] → Prop
-- Mathlib.Data.Set.Prod
Set.decidableMemDiagonal : {α : Type u_1} → [h : DecidableEq α] → (x : α × α) → Decidable (x ∈ Set.diagonal α)
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
isStronglyTranscendental_iff_of_field : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R K] [FaithfulSMul R K]
  {x : K}, IsStronglyTranscendental R x ↔ Transcendental R x
-- Init.Grind.Lemmas
Lean.Grind.eq_congr' : ∀ {α : Sort u} {a₁ b₁ a₂ b₂ : α}, a₁ = b₂ → b₁ = a₂ → (a₁ = b₁) = (a₂ = b₂)
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
/-- The homomorphism from the units of a restricted product to the regular product of unit.  -/
RestrictedProduct.coeUnits : {ι : Type u_1} →
  {R : ι → Type u_2} →
    [inst : (i : ι) → Monoid (R i)] →
      {S : ι → Type u_3} →
        [inst_1 : (i : ι) → SetLike (S i) (R i)] →
          [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
            {B : (i : ι) → S i} →
              {𝓕 : Filter ι} → (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ →* (i : ι) → (R i)ˣ
-- Lean.Elab.BuiltinNotation
/-- Given an expression `e` that is the elaboration of `stx`, if `e` is a free variable, then return `k stx`.
Otherwise, return `(fun x => k x) e`
 -/
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.withLocalIdentFor : Lean.Term → Lean.Expr → (Lean.Term → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Group.Basic
zpow_sub : ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℤ), a ^ (m - n) = a ^ m * (a ^ n)⁻¹
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.mergeWith.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (mergeFn : α → β → β → β) (t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β)
  (ht₁ : t₁.Balanced),
  Std.DTreeMap.Internal.Impl.Const.mergeWith mergeFn t₁ t₂ ht₁ =
    Std.DTreeMap.Internal.Impl.foldl
      (fun t a b₂ =>
        (Std.DTreeMap.Internal.Impl.Const.alter a
            (fun x =>
              match x with
              | none => some b₂
              | some b₁ => some (mergeFn a b₁ b₂))
            t.impl ⋯).toBalancedTree)
      { impl := t₁, balanced_impl := ht₁ } t₂
-- Mathlib.Probability.Moments.Basic
ContinuousLinearEquiv.integral_comp_id_comm' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} (L : E ≃L[𝕜] F), ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toAlgEquiv_refl : ∀ {R : Type u_6} {A : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Star A],
  (StarAlgEquiv.refl R A).toAlgEquiv = AlgEquiv.refl
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The first of the two parallel morphisms of the fork diagram, induced by the first projection in
each pullback.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.firstMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type t} →
          [inst_1 : Small.{w, t} I] →
            (X : I → C) →
              (π : (i : I) → X i ⟶ B) →
                [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] →
                  CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X ⟶
                    CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.codRestrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {σ : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : SetLike σ N]
  [inst_3 : AddMemClass σ N] (f : M →ₙ+ N) (S : σ) (h : ∀ (x : M), f x ∈ S),
  f.codRestrict S h = { toFun := fun n => ⟨f n, ⋯⟩, map_add' := ⋯ }
-- Mathlib.Data.Sum.Basic
Sum.getLeft_eq_getLeft? : ∀ {α : Type u} {β : Type v} {x : α ⊕ β} (h₁ : x.isLeft = true) (h₂ : x.getLeft?.isSome = true),
  x.getLeft h₁ = x.getLeft?.get h₂
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_eq_zero : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M}, (∀ x ∈ l, x = 0) → l.sum = 0
-- Mathlib.GroupTheory.GroupAction.Defs
/-- `fixedBy m` is the set of elements fixed by `m`.  -/
AddAction.fixedBy : {M : Type u_1} → (α : Type u_3) → [inst : AddMonoid M] → [AddAction M α] → M → Set α
-- Lean.Elab.Do.PatternVar
_private.Lean.Elab.Do.PatternVar.0.Lean.Elab.Do.getLetRecDeclVars : Lean.TSyntax `Lean.Parser.Term.letRecDecl → Lean.Elab.TermElabM (Array Lean.Ident)
-- Init.MetaTypes
/-- A list of indices for which occurrences should not be rewritten.  -/
Lean.Meta.Occurrences.neg : List ℕ → Lean.Meta.Occurrences
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.brecOn.go : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {motive : (a a_1 : ι) → Monoid.CoprodI.NeWord M a a_1 → Sort u} →
        {a a_1 : ι} →
          (t : Monoid.CoprodI.NeWord M a a_1) →
            ((a a_2 : ι) → (t : Monoid.CoprodI.NeWord M a a_2) → Monoid.CoprodI.NeWord.below t → motive a a_2 t) →
              motive a a_1 t ×' Monoid.CoprodI.NeWord.below t
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive __do_lift
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} (𝕜 : Type u_3) [inst_3 : RCLike 𝕜] {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω}
  {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω 𝕜),
      Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_rii : ∀ {α : Type u_1} {xs : ListSlice α}, Std.Rii.Sliceable.mkSlice xs *...* = xs
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.lift_obj : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (F : V ⥤rq D) (v : V), (CategoryTheory.Cat.FreeRefl.lift F).obj (CategoryTheory.Cat.FreeRefl.mk v) = F.obj v
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instOne : {α : Type u_2} → {x : NonAssocSemiring α} → One (α →+* α)
-- Mathlib.Topology.Order.IsLUB
/-- This is an analogue of `Dense.continuous_sup` for functions taking values in a conditionally
complete linear order. The assumption of `BddAbove (range f)` is not needed in this theorem.  -/
Dense.ciSup' : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α]
  [ClosedIicTopology α] {f : γ → α} [inst_3 : TopologicalSpace γ] {S : Set γ},
  Dense S → Continuous f → ⨆ s, f ↑s = ⨆ i, f i
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_tmul : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x x' : E)
  (y y' : F), inner 𝕜 (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y'
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCoseparating_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C),
  P.op.IsCoseparating ↔ P.IsSeparating
-- Init.Data.Nat.Lemmas
Nat.le_succ_iff : ∀ {m n : ℕ}, m ≤ n.succ ↔ m ≤ n ∨ m = n.succ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.keysArray.isEmpty = t.isEmpty
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.lift_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f : { a // a ≠ 1 } → α)
  (h : ∀ (a b : { a // a ≠ 1 }), FiniteMulArchimedeanClass.mk ↑a ⋯ = FiniteMulArchimedeanClass.mk ↑b ⋯ → f a = f b)
  {a : M} (ha : a ≠ 1), FiniteMulArchimedeanClass.lift f h (FiniteMulArchimedeanClass.mk a ha) = f ⟨a, ha⟩
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.isIntertwining : ∀ {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} (f : ContIntertwiningMap π₁ π₂) (g : G) (v : V),
  f ((π₁ g) v) = (π₂ g) (f v)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_neg_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R (-v) ↔ LinearIndependent R v
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M),
  Submonoid.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (insert a s)` for
all `s` and `a ∉ s`.  -/
Finset.strictMono_iff_forall_lt_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
  StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM_eq_toArray_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n (Option γ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM f it).toArray =
    (Std.IterM.filterMapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toArray
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Implementation; see `CostructuredArrow.prodEquivalence`.  -/
CategoryTheory.CostructuredArrow.prodFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : CategoryTheory.Functor C D) →
                  (S' : CategoryTheory.Functor C' D') →
                    (T : D) →
                      (T' : D') →
                        CategoryTheory.Functor (CategoryTheory.CostructuredArrow (S.prod S') (T, T'))
                          (CategoryTheory.CostructuredArrow S T × CategoryTheory.CostructuredArrow S' T')
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.lift_uniq : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  (H' : Set.range ⇑g ⊆ Set.range ⇑f) (l : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp l f = g → l = AlgebraicGeometry.IsOpenImmersion.lift f g H'
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `FunLike.coe_sum`. -/
MultilinearMap.coe_sum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instFaithfulDecomposedDecomposedTo : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], (CategoryTheory.decomposedTo J).Faithful
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Transport evidence that a cone is a limit cone across an isomorphism of cones.  -/
CategoryTheory.Limits.IsLimit.ofIsoLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit r → (r ≅ t) → CategoryTheory.Limits.IsLimit t
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose (p ^ k * a) (p ^ k * b)` is congruent to `choose a b` modulo `p`.
Also see `choose_pow_mul_pow_mul_modEq_choose_nat` for the version with `MOD`.  -/
Choose.choose_pow_mul_pow_mul_modEq_choose : ∀ {k a b p : ℕ} [Fact (Nat.Prime p)], ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.mk.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {v v_1 : ι → E} (e_v : v = v_1) (hon : Orthonormal 𝕜 v)
  (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)), OrthonormalBasis.mk hon hsp = OrthonormalBasis.mk ⋯ ⋯
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.smallSchroder.match_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → (n = 0 → False) → motive n.succ) → motive x
-- Mathlib.Data.Prod.Basic
Prod.map_fst' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ),
  Prod.fst ∘ Prod.map f g = f ∘ Prod.fst
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsOpenEmbedding.functor_obj_injective : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  Function.Injective hf.functor.obj
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.forget.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.Cone.forget F =
    { obj := fun t => t.pt, map := fun {X Y} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional.sizeOf_spec : ∀ (name : Lean.Name) (s : Lean.Term),
  sizeOf (Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name s) = 1 + sizeOf name + sizeOf s
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_forget₂_TopCat_map : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopModuleCat R} (f : X ⟶ Y),
  TopCat.Hom.hom ((CategoryTheory.forget₂ (TopModuleCat R) TopCat).map f) = ↑(TopModuleCat.Hom.hom f)
-- Mathlib.Algebra.Group.Units.Basic
AddLeftCancelMonoid.eq_zero_of_add_right : ∀ {α : Type u} [inst : AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → a = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.counit_eq_toUnit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.ComonObj A],
  CategoryTheory.ComonObj.counit = CategoryTheory.SemiCartesianMonoidalCategory.toUnit A
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.cancellationTasks : Lean.Server.RequestCancellationToken → List (Lean.Server.ServerTask Unit)
-- Mathlib.Analysis.Normed.Order.Lattice
HasSolidNorm.mk : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α],
  (∀ ⦃x y : α⦄, |x| ≤ |y| → ‖x‖ ≤ ‖y‖) → HasSolidNorm α
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
/-- The (colimit) cocone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from
the colimit of `F ⋙ evaluation R X` for all `X`.  -/
PresheafOfModules.colimitCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
                  CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
                    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] →
              [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] →
                CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAddZeroClass : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → AddZeroClass (ι →₀ M)
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_radius_zero : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E],
  n ≠ 0 → ∀ (f : (Fin n → ℂ) → E) (c : Fin n → ℂ), (∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
/-- Constructor for IsOrdering that doesn't require `ne_top'`.  -/
RingPreordering.IsOrdering.mk' : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) [inst_1 : HasMemOrNegMem P],
  (∀ {x y : R}, x * y ∈ P.support → x ∈ P.support ∨ y ∈ P.support) → P.IsOrdering
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
/-- A ring homomorphism `f : R →+* A` is said to be integral
if every element `A` is integral with respect to the map `f`  -/
RingHom.IsIntegral : {R : Type u_1} → {A : Type u_3} → [inst : CommRing R] → [inst_1 : Ring A] → (R →+* A) → Prop
-- Init.Data.List.Lemmas
List.cons_inj_right : ∀ {α : Type u_1} (a : α) {l l' : List α}, a :: l = a :: l' ↔ l = l'
-- Mathlib.Order.Bounds.Basic
IsGLB.unique : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGLB s a → IsGLB s b → a = b
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.instIsBoundedSMul : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
  (S : Submodule R M) (𝕜 : Type u_4) [inst_3 : SeminormedCommRing 𝕜] [inst_4 : Module 𝕜 M] [IsBoundedSMul 𝕜 M]
  [inst_6 : SMul 𝕜 R] [inst_7 : IsScalarTower 𝕜 R M], IsBoundedSMul 𝕜 (M ⧸ S)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_natDegree : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.natDegree = f.natDegree - f.natTrailingDegree
-- Mathlib.CategoryTheory.Action.Monoidal
Action.associator_hom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y Z : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.V Y.V Z.V).hom
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_iSup_of_directed_le : ∀ {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} {Ω : Type u_4} {m : ι → MeasurableSpace Ω}
  {m' m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  (∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) →
    (∀ (i : ι), m i ≤ m0) →
      m' ≤ m0 → Directed (fun x1 x2 => x1 ≤ x2) m → ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
-- Mathlib.Topology.Closure
closure_iUnion_of_finite : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} [Finite ι] (f : ι → Set X),
  closure (⋃ i, f i) = ⋃ i, closure (f i)
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `g` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_fun_add_iff_meromorphicAt₁ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x → (MeromorphicAt (fun z => f z + g z) x ↔ MeromorphicAt g x)
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGT_eq_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos},
  s.posGT p h = q ↔ p < q.offset ∧ ∀ (q' : s.Pos), p < q'.offset → q ≤ q'
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given an additive quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the
restriction, `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
will take the value `∞` on any open set in the quotient!  -/
MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsAddRightInvariant],
      (MeasureTheory.Measure.map QuotientAddGroup.mk μ).AbsolutelyContinuous
        (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.prod : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {α' : Type u_1} {β' : Type u_2}
  [inst_2 : UniformSpace α'] [inst_3 : UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'},
  IsUniformEmbedding e₁ → IsUniformEmbedding e₂ → IsUniformEmbedding fun p => (e₁ p.1, e₂ p.2)
-- Mathlib.MeasureTheory.Group.FoelnerFilter
maxAddFoelner.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : AddGroup G]
  [inst_2 : AddAction G X],
  maxAddFoelner G μ =
    Filter.principal {s | MeasurableSet s ∧ μ s ≠ 0 ∧ μ s ≠ ⊤} ⊓
      ⨅ g, Filter.comap (fun s => μ (symmDiff (g +ᵥ s) s) / μ s) (nhds 0)
-- Init.Data.String.Basic
String.Pos.ofSliceTo_sliceTo : ∀ {s : String} {p₀ p : s.Pos} {h : p ≤ p₀}, String.Pos.ofSliceTo (p₀.sliceTo p h) = p
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.dvd_iff_le : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x y : O}, x ∣ y ↔ v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)
-- Lean.Meta.Basic
/-- If `true`, reduce terms such as `(fun x => t[x]) a` into `t[a]`  -/
Lean.Meta.Config.beta : Lean.Meta.Config → Bool
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- If `f : ℂ → ℂ` is meromorphic, then the Cartan kernel of integration is integrable as a function in
the two variables `α` and `β`.
 -/
ValueDistribution.Cartan.integrableOn_cartanKernel : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    MeasureTheory.IntegrableOn (fun p => ValueDistribution.Cartan.cartanKernel f R p.1 p.2)
      (Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volume