mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Notation
/-- `prio` is a builtin syntax category for priorities.
Priorities are used in many different attributes.
Higher numbers denote higher priority, and for example typeclass search will
try high priority instances before low priority.
In addition to literals like `37`, you can also use `low`, `mid`, `high`, as well as
add and subtract priorities.  -/
Lean.Parser.Category.prio : Lean.Parser.Category
-- Mathlib.Algebra.Group.Defs
/-- If all multiplications cancel on the right then every element is right-regular.  -/
IsRightRegular.all : ∀ {R : Type u_2} [inst : Mul R] [IsRightCancelMul R] (g : R), IsRightRegular g
-- Init.BinderPredicates
/-- The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`,
and similarly for other binary operators.
 -/
Lean.«term∃__,_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.proj_linear : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12}
  [inst_1 : (i : ι) → AddCommGroup (V i)] [inst_2 : (i : ι) → Module k (V i)] [inst_3 : (i : ι) → AddTorsor (V i) (P i)]
  (i : ι), (AffineMap.proj i).linear = LinearMap.proj i
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_append_left_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₁.Disjoint l
-- Mathlib.Order.CompleteLattice.Basic
Antitone.le_map_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {s : Set α} {f : α → β},
  Antitone f → ⨆ a ∈ s, f a ≤ f (sInf s)
-- Mathlib.Topology.Inseparable
IsOpen.stableUnderGeneralization : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → StableUnderGeneralization s
-- Lean.Environment
/-- Async access mode for environment extensions used in `EnvExtension.get/set/modifyState`.
When modified in concurrent contexts, extensions may need to switch to a different mode than the
default `mainOnly`, which will panic in such cases. The access mode is set at environment extension
registration time but can be overridden when calling the mentioned functions in order to weaken it
for specific accesses.

In all modes, the state stored into the `.olean` file for persistent environment extensions is the
result of `getState (asyncMode := .sync)` called on the main environment branch at the end of the
file, i.e. it encompasses all modifications on all branches except for `local` modifications for
which only the main branch is included.
 -/
Lean.EnvExtension.AsyncMode : Type
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousMul β],
  Asymptotics.SuperpolynomialDecay l k f →
    Asymptotics.SuperpolynomialDecay l k g → Asymptotics.SuperpolynomialDecay l k (f * g)
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of functors into a functor between the pi types.
 -/
CategoryTheory.Functor.pi : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          ((i : I) → CategoryTheory.Functor (C i) (D i)) → CategoryTheory.Functor ((i : I) → C i) ((i : I) → D i)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_right_of_le_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 0 < a → a ≤ 1 → m ≤ n → a ^ n ≤ a ^ m
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸}, DifferentiableWithinAt 𝕜 a s x → DifferentiableWithinAt 𝕜 b s x → DifferentiableWithinAt 𝕜 (a * b) s x
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.map_subtype_val_restriction : ∀ {α : Type u} {x : FreeCommRing α} (s : Set α) [inst : DecidablePred fun x => x ∈ s],
  x.IsSupported s → (FreeCommRing.map Subtype.val) ((FreeCommRing.restriction s) x) = x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.instDecidableConnected : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → Decidable G.Connected
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps.html : ProofWidgets.HtmlDisplayProps → ProofWidgets.Html
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The adjunction between n-truncation and the n-coskeleton.  -/
CategoryTheory.SimplicialObject.coskAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
        CategoryTheory.SimplicialObject.truncation n ⊣ CategoryTheory.SimplicialObject.Truncated.cosk n
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (n : ℕ), WittVector.init n = WittVector.select fun i => i < n
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modifyGet_EStateM_apply_eq : ∀ {σ α ε : Type} {post : α → σ → Prop} {epost : ε → σ → Prop} (f : σ → α × σ),
  Std.Internal.Do.wp (MonadStateOf.modifyGet f) post epost = fun s => post (f s).1 (f s).2
-- Mathlib.CategoryTheory.Core
/-- The core of a category is naturally included in the category.  -/
CategoryTheory.Core.inclusion : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.Core C) C
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The split mono `X.normalizedChainComplex R ⟶ X.chainComplex R`.  -/
SSet.fromNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → (X : SSet) → (R : C) → X.normalizedChainComplex R ⟶ X.chainComplex R
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.mem_ofFixingSubgroup_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {x : α},
  x ∈ SubMulAction.ofFixingSubgroup M s ↔ x ∉ s
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instSMulCommClass : ∀ {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul T R] [inst_1 : SMul T A] [inst_2 : SMul S R]
  [inst_3 : SMul S A] [SMulCommClass T S R] [SMulCommClass T S A], SMulCommClass T S (Unitization R A)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.equivIsoLimit_apply : ∀ {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} (i : r ≅ t)
  (P : CategoryTheory.Limits.IsLimit r), (CategoryTheory.Limits.IsLimit.equivIsoLimit i) P = P.ofIsoLimit i
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {l : List ((a : α) × β a)},
  (m.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) m l)
-- Mathlib.Topology.NhdsSet
nhdsSet_eq_bot_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {s : Set α}, nhdsSet s = ⊥ ↔ s = ∅
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.join_cons : ∀ {α : Type u} (a b : α) (s : Stream'.Seq α) (S : Stream'.Seq (Stream'.Seq1 α)),
  Stream'.Seq1.join ((a, Stream'.Seq.cons b s), S) = (a, (Stream'.Seq.cons (b, s) S).join)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.compl₁₂ : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {N' : Type u_6} [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup M'] [inst_3 : AddCommGroup N'] [inst_4 : CommRing R]
  [inst_5 : Module R M] [inst_6 : Module R M'] [inst_7 : Module R N] [inst_8 : Module R N'] (p : M →ₗ[R] N →ₗ[R] R)
  [p.IsPerfPair] (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N), (p.compl₁₂ ↑eM ↑eN).IsPerfPair
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `MonoidAlgebra.domCongr` as a `MonoidHom` from `MulAut`.  -/
MonoidAlgebra.domCongrAut : {R : Type u_1} →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Monoid M] → MulAut M →* MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A M
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 3rd object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
to `Fun(G³, A)` as a `k`-module.  -/
groupCohomology.cochainsIso₃ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (groupCohomology.inhomogeneousCochains A).X 3 ≅ ModuleCat.of k (G × G × G → ↑A)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Given a costructured arrow `S(Y) ⟶ X`, and an arrow `Y' ⟶ Y'`, we can construct a morphism of
costructured arrows given by `(S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X)`.  -/
CategoryTheory.CostructuredArrow.homMk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {Y' : C} →
            {S : CategoryTheory.Functor C D} →
              (f : CategoryTheory.CostructuredArrow S T) →
                (g : Y' ⟶ f.left) →
                  CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom) ⟶ f
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.neg : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x : WittVector p R), WittVector.mapFun (⇑f) (-x) = -WittVector.mapFun (⇑f) x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_string_iff : ∀ {pat : String} {s : String.Slice}, s.startsWith pat = true ↔ pat.toList <+: s.copy.toList
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- First candidate Day convolutions between objects.
Note that the name here is primed as in fact, we will use the other fields
in this class to produce convolutions with more controlled defeq properties.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions' : {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) →
                    CategoryTheory.MonoidalCategory.DayConvolution
                      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                            D).obj
                        d)
                      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                            D).obj
                        d')
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_of_exists_eq_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [T2Space α] [L.NeBot] [L.LeAtTop], (∃ b, f b = 0) → ∏'[L] (b : β), f b = 0
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_sum : ∀ {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [inst : AddCommMonoid β] {f : ι → α → β}
  (I : Finset ι), (UniformOnFun.ofFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (UniformOnFun.ofFun 𝔖) (f i)
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Noetherian.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [toEssentiallySmall : CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C],
  (∀ (X : C), CategoryTheory.IsNoetherianObject X) → CategoryTheory.Noetherian C
-- Mathlib.Data.Finset.SDiff
Finset.inter_sdiff_left_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∩ (t \ u) = t ∩ (s \ u)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingRight_def : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instIsDedekindFiniteAddMonoid : ∀ {α : Type u_1} [inst : AddZero α] [IsDedekindFiniteAddMonoid α], IsDedekindFiniteAddMonoid αᵃᵒᵖ
-- Lean.Elab.Command
/-- Registers a command elaborator for the given syntax node kind.

A command elaborator should have type `Lean.Elab.Command.CommandElab` (which is
`Lean.Syntax → Lean.Elab.Term.CommandElabM Unit`), i.e. should take syntax of the given syntax
node kind as a parameter and perform an action.

The `elab_rules` and `elab` commands should usually be preferred over using this attribute
directly.
 -/
Lean.Elab.Command.commandElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
functions. For an alternative version, convenient if the infinite sums are not already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_tsum_of_nonneg`.  -/
Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {A B : ℝ},
      0 ≤ A →
        0 ≤ B →
          (∀ (i : ι), 0 ≤ f i) →
            (∀ (i : ι), 0 ≤ g i) →
              HasSum (fun i => f i ^ p) (A ^ p) →
                HasSum (fun i => g i ^ q) (B ^ q) → ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Data.NNReal.Basic
NNReal.le_iInf_add_iInf : ∀ {ι : Sort u_3} {ι' : Sort u_4} [Nonempty ι] [Nonempty ι'] {f : ι → NNReal} {g : ι' → NNReal} {a : NNReal},
  (∀ (i : ι) (j : ι'), a ≤ f i + g j) → a ≤ (⨅ i, f i) + ⨅ j, g j
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Fin.castSucc.hcongr_2 : ∀ (n n' : ℕ), n = n' → ∀ (a : Fin n) (a' : Fin n'), a ≍ a' → a.castSucc ≍ a'.castSucc
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Run `k` on all pairs of body, bound variables that could possibly appear due to η-reduction  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.etaPossibilities : Lean.Expr →
  List Lean.FVarId →
    Bool →
      Lean.Meta.RefinedDiscrTree.LazyEntry →
        ReaderT Lean.Meta.RefinedDiscrTree.Context✝ Lean.MetaM
          (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_apply_prime : ∀ {p : ℕ}, Nat.Prime p → ArithmeticFunction.vonMangoldt p = Real.log ↑p
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_inv_app : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} (X : p.Fiber S),
  CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst.inv.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.Hom.Basic
OrderHom.piIso_symm_apply : ∀ {α : Type u_2} [inst : Preorder α] {ι : Type u_6} {π : ι → Type u_7} [inst_1 : (i : ι) → Preorder (π i)]
  (f : (i : ι) → α →o π i), (RelIso.symm OrderHom.piIso) f = OrderHom.pi f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.trans_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), (p.trans p.symm).Homotopic (Path.refl x₀)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.prod_map_comap_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ N) (g : M' →+ N') (S : AddSubmonoid N)
  (S' : AddSubmonoid N'),
  AddSubmonoid.comap (f.prodMap g) (S.prod S') = (AddSubmonoid.comap f S).prod (AddSubmonoid.comap g S')
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq : Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.out_lift_equiv : ∀ (a : Cardinal.{u}), Nonempty (Quotient.out (Cardinal.lift.{v, u} a) ≃ Quotient.out a)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- Constructor for points of Grothendieck topologies `J : GrothendieckTopology C`
that are given by a functor `p : N ⥤ C` from a cofiltered and initially small
category `N`.  -/
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          (p : CategoryTheory.Functor N C) →
            [CategoryTheory.InitiallySmall N] →
              {J : CategoryTheory.GrothendieckTopology C} →
                [CategoryTheory.IsCofiltered N] →
                  (∀ ⦃X : C⦄,
                      ∀ R ∈ J X,
                        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
                          ∃ Y g,
                            ∃ (_ : R.arrows g),
                              ∃ V q a,
                                CategoryTheory.CategoryStruct.comp a g =
                                  CategoryTheory.CategoryStruct.comp (p.map q) f) →
                    J.Point
-- Mathlib.Order.Antichain
isAntichain_iff_forall_not_lt : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α},
  IsAntichain (fun x1 x2 => x1 ≤ x2) s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬a < b
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function is 'meromorphic in normal form' at `x` if it vanishes around `x`
or if it can locally be written as `fun z ↦ (z - x) ^ n • g` where `g` is
analytic and does not vanish at `x`.  -/
MeromorphicNFAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C),
  (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).map η).app A).right =
    CategoryTheory.Functor.whiskerLeft (CategoryTheory.CosimplicialObject.Augmented.drop.obj A) η
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_map_homeomorph : ∀ {X : Type u_1} {Y : Type u_2} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace Y] [inst_3 : TopologicalSpace Y] [inst_4 : TopologicalSpace ε'']
  [inst_5 : ESeminormedAddMonoid ε''] [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → ε''}
  {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable f (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.LocallyIntegrable (f ∘ ⇑e) μ
-- Mathlib.Data.Sym.Sym2
Sym2.diagElem.congr_simp : ∀ {α : Type u_1} (z z_1 : Sym2 α) (e_z : z = z_1) (a : z.IsDiag), z.diagElem a = z_1.diagElem ⋯
-- Init.Data.SInt.Lemmas
Int64.ofInt_eq_ofNat : ∀ {n : ℕ}, Int64.ofInt ↑n = Int64.ofNat n
-- Mathlib.Order.Hom.Basic
/-- If `e` is an equivalence with monotone forward and inverse maps, then `e` is an
order isomorphism.  -/
Equiv.toOrderIso : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (e : α ≃ β) → Monotone ⇑e → Monotone ⇑e.symm → α ≃o β
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.pullbackFst_isLocalHom : ∀ {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) [IsLocalHom (CommRingCat.Hom.hom g)],
  IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.Limits.pullback.fst f g))
-- Init.Control.Lawful.Instances
ExceptT.run_liftWith : ∀ {m : Type u → Type u_1} {ε α : Type u} [inst : Monad m]
  (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m α),
  (liftWith f).run = Except.ok <$> f fun {β} x => x.run
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `CommRing` instance  -/
Lean.Meta.Grind.Arith.Linear.Struct.commRingInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.GroupTheory.Finiteness
instFGFreeMonoidOfFinite : ∀ (α : Type u_3) [Finite α], Monoid.FG (FreeMonoid α)
-- Mathlib.RingTheory.LocalRing.Module
Module.exists_basis_of_span_of_flat : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsLocalRing R]
  [Module.FinitePresentation R M] [Module.Flat R M] {ι : Type u} (v : ι → M),
  Submodule.span R (Set.range v) = ⊤ → ∃ κ a b, ∀ (i : κ), b i = v (a i)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₁_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1),
  (X.sc₁ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], Associates.out 0 = 0
-- Mathlib.Data.Vector.Basic
List.Vector.insertIdx_comm : ∀ {α : Type u_1} {n : ℕ} (a b : α) (i j : Fin (n + 1)),
  i ≤ j →
    ∀ (v : List.Vector α n),
      List.Vector.insertIdx b j.succ (List.Vector.insertIdx a i v) =
        List.Vector.insertIdx a i.castSucc (List.Vector.insertIdx b j v)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_inj : ∀ {c₁ c₂ : Cardinal.{u_1}}, c₁.ord = c₂.ord ↔ c₁ = c₂
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instMonoidHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], MonoidHomClass (α →*o β) α β
-- Mathlib.Tactic.MinImports
/-- `getAttrNames stx` extracts `attribute`s from `stx`.
It does not collect `simp`, `ext`, `to_additive`.
It should collect almost all other attributes, e.g., `fun_prop`.  -/
Mathlib.Command.MinImports.getAttrNames : Lean.Syntax → Lean.NameSet
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The arithmetic function associated to a Dirichlet character is multiplicative.  -/
DirichletCharacter.isMultiplicative_toArithmeticFunction : ∀ {N : ℕ} {R : Type u_1} [inst : CommMonoidWithZero R] (χ : DirichletCharacter R N),
  (toArithmeticFunction fun x => χ ↑x).IsMultiplicative
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_one_add' : ∀ {y : ℝ}, 1 + y ≠ 0 → ∀ (x : NNReal), x ^ (1 + y) = x * x ^ y
-- Mathlib.Algebra.CharP.Lemmas
neg_one_pow_expChar_pow : ∀ (R : Type u_1) [inst : Ring R] (p n : ℕ) [hR : ExpChar R p], (-1) ^ p ^ n = -1