mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.PrimeCounting
/-- `primesBelow n` is the set of primes less than `n` as a `Finset`.  -/
Nat.primesBelow : ℕ → Finset ℕ
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
AntitoneOn.integrableOn_of_measure_ne_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E},
  AntitoneOn f s →
    ∀ {a b : X}, IsLeast s a → IsGreatest s b → μ s ≠ ⊤ → MeasurableSet s → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Algebra.Group.Commute.Defs
/-- Any element commutes with itself.  -/
Commute.refl : ∀ {S : Type u_3} [inst : Mul S] (a : S), Commute a a
-- Mathlib.NumberTheory.SmoothNumbers
/-- `factoredNumbers s`, for a finite set `s` of natural numbers, is the set of positive natural
numbers all of whose prime factors are in `s`.  -/
Nat.factoredNumbers : Finset ℕ → Set ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineHom.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) →
    AlgebraicGeometry.IsAffineHom f
-- Mathlib.SetTheory.Lists
Lists'.ofList.eq_def : ∀ {α : Type u_1} (x : List (Lists α)),
  Lists'.ofList x =
    match x with
    | [] => Lists'.nil
    | a :: l => Lists'.cons a (Lists'.ofList l)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M]
  [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M]
  (v w : MeasureTheory.VectorMeasure α M) [Countable β] {f : β → Set α},
  (∀ (b : β), MeasurableSet (f b)) →
    (∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)) → v.restrict (⋃ b, f b) ≤ w.restrict (⋃ b, f b)
-- Mathlib.Algebra.Order.Quantale
/-- Multiplication is distributive over join in a quantale  -/
IsQuantale.sSup_mul_distrib : ∀ {α : Type u_1} {inst : Semigroup α} {inst_1 : CompleteLattice α} [self : IsQuantale α] (s : Set α) (y : α),
  sSup s * y = ⨆ x ∈ s, x * y
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.star_apply : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (A : F →WOT[𝕜] F) (x : F), (star A) x = (star A.toCLM) x
-- Mathlib.RingTheory.LocalIso
/-- Local isomorphisms are stable under composition.  -/
Algebra.IsLocalIso.trans : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommSemiring T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] [Algebra.IsLocalIso R S]
  [Algebra.IsLocalIso S T], Algebra.IsLocalIso R T
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isGLB_l : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α}, IsGLB {b | a ≤ u b} (l a)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.div` -/
TendstoUniformly.fun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l →
    TendstoUniformly f' g' l → TendstoUniformly (fun i i_1 => f i i_1 / f' i i_1) (fun i => g i / g' i) l
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.trans : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b c : R} [IsCancelAdd R], A.IsDetpBalanced a b → A.IsDetpBalanced b c → A.IsDetpBalanced a c
-- Std.Http.Protocol.H1.Reader
/-- Parse fixed-length body bytes, tracking the number of bytes remaining.
 -/
Std.Http.Protocol.H1.Reader.BodyState.fixed : ℕ → Std.Http.Protocol.H1.Reader.BodyState
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.finite_setOfPred_addOrderOf_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ},
  0 < n → {u | addOrderOf u = n}.Finite
-- Init.Data.List.Lemmas
List.mem_of_mem_head? : ∀ {α : Type u_1} {l : List α} {a : α}, a ∈ l.head? → a ∈ l
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
`g : W ≅ Z` induces an isomorphism `coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z`.  -/
CategoryTheory.Limits.coprod.mapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] →
        [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z] → (W ≅ Y) → (X ≅ Z) → (W ⨿ X ≅ Y ⨿ Z)
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Given a finite index subgroup `S ≤ G`, this is a natural isomorphism between the `Ind_S^G` and
`Coind_G^S` functors `Rep k S ⥤ Rep k G`.  -/
Rep.indCoindNatIso : (k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] → Rep.indFunctor k S.subtype ≅ Rep.coindFunctor k S.subtype
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_bijective_of_comp_eq_id_right : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P) (g : P →ₗ[R] N),
  g ∘ₗ f = LinearMap.id → Function.Bijective ⇑(dualTensorHom R M P) → Function.Bijective ⇑(dualTensorHom R M N)
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_norm' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {K : NNReal},
  AntilipschitzWith K f → f 1 = 1 → ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Raw.Const.get? (t.insertIfNew k v) a =
        if cmp k a = Ordering.eq ∧ k ∉ t then some v else Std.DTreeMap.Raw.Const.get? t a
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
SSet.N.toSemiSimplexCategory_obj : ∀ (X : SSet) [inst : X.Nonsingular] (s : X.N), (SSet.N.toSemiSimplexCategory X).obj s = { len := s.dim }
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_Ioo_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X},
  a < b →
    autoParam (Order.IsSuccPrelimit b) map_coe_Ioo_atTop._auto_1 →
      Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.sub_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x y : G i), ⟦⟨i, x⟩⟧ - ⟦⟨i, y⟩⟧ = ⟦⟨i, x - y⟩⟧
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α] (n : ℕ)
  (lhs : aig.RefVec w) (rhs : aig.RefVec n) (pow : ℕ),
  sizeOf { n := n, lhs := lhs, rhs := rhs, pow := pow } = 1 + sizeOf n + sizeOf lhs + sizeOf rhs + sizeOf pow
-- Mathlib.Order.Filter.SmallSets
Filter.eventually_smallSets' : ∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop},
  (∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s) → ((∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, p s)
-- Mathlib.Algebra.Divisibility.Basic
dvd_pow : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → ∀ {n : ℕ}, n ≠ 0 → a ∣ b ^ n
-- Mathlib.GroupTheory.Sylow
Sylow.normal_of_all_max_subgroups_normal : ∀ {G : Type u} [inst : Group G] [Finite G],
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) →
    ∀ {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G), (↑P).Normal
-- Init.Data.Ord.Basic
instInhabitedOrdering.default : Ordering
-- Mathlib.RingTheory.Trace.Basic
trace_eq_sum_roots : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : Type u_6}
  [inst_3 : Field F] [inst_4 : Algebra K F] [FiniteDimensional K L] {x : L},
  (Polynomial.map (algebraMap K F) (minpoly K x)).Splits →
    (algebraMap K F) ((Algebra.trace K L) x) = Module.finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_coe : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Preprocessor.mk.injEq : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase) (transform : Lean.Expr → Lean.MetaM (List Lean.Expr))
  (toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform_1 : Lean.Expr → Lean.MetaM (List Lean.Expr)),
  ({ toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 }) =
    (toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products of measurable spaces are symmetric.  -/
MeasurableEquiv.prodComm : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → α × β ≃ᵐ β × α
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- As we are using chain complexes indexed by `ℕ`, we shall need the relation
`c` such `c m n` if and only if `n+1=m`.  -/
AlgebraicTopology.DoldKan.c : ComplexShape ℕ
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableWithinAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {s : Set E} {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  DifferentiableWithinAt 𝕜 c s x → DifferentiableWithinAt 𝕜 u s x → DifferentiableWithinAt 𝕜 (fun y => (c y) (u y)) s x
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the inverse of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the first projection is
the morphism `Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism
`s ↦ s ⊗ₜ[R] 1`.
 -/
AlgebraicGeometry.pullbackSpecIso_inv_fst : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
-- Init.Data.List.MinMaxIdx
List.left_le_maxIdxOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : xs ≠ []), List.maxIdxOn f xs h ≤ List.maxIdxOn f (xs ++ ys) ⋯
-- Mathlib.Algebra.Order.Group.PosPart
negPart_eq_ite : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a⁻ = if a ≤ 0 then -a else 0
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
/-- Turn a `CNF.Clause PosFin` into the representation used by the LRAT checker.
 -/
Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' : {n : ℕ} →
  Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
    Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.ne_bot : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α}, s.Intersecting → a ∈ s → a ≠ ⊥
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), f.symm.symm = f
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
/-- If `F` is dense, the left Kan extension of `F` along `F` is isomorphic to the identity.  -/
CategoryTheory.Functor.IsDense.leftKanExtensionIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [inst_2 : F.IsDense] → F.leftKanExtension F ≅ CategoryTheory.Functor.id D
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.instTrans : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Trans Std.DTreeMap.Raw.Equiv Std.DTreeMap.Raw.Equiv Std.DTreeMap.Raw.Equiv
-- Mathlib.Topology.Continuous
Dense.denseRange_val : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, Dense s → DenseRange Subtype.val
-- Mathlib.Data.Set.Piecewise
Set.injective_piecewise_iff : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] {f g : α → β},
  Function.Injective (s.piecewise f g) ↔ Set.InjOn f s ∧ Set.InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
-- Mathlib.Algebra.Prime.Lemmas
Prime.pow_dvd_of_dvd_mul_right : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M},
  Prime p → ∀ (n : ℕ), ¬p ∣ b → p ^ n ∣ a * b → p ^ n ∣ a
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurryRight_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  (f : MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) (m : (i : Fin n.succ) → M i),
  f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.mk : Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Nil.noConfusionType : Sort v✝ → EPost⟨⟩ → EPost⟨⟩ → Sort v✝
-- Mathlib.Data.Int.GCD
Nat.xgcdAux_fst : ∀ (x y : ℕ) (s t s' t' : ℤ), (x.xgcdAux s t y s' t').1 = x.gcd y
-- Lean.Parser.Term
Lean.Parser.Term.basicFun.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.CoprodI
/-- A relation on the free monoid on alphabet `Σ i, M i`,
relating `⟨i, 1⟩` with `1` and `⟨i, x⟩ * ⟨i, y⟩` with `⟨i, x * y⟩`.  -/
Monoid.CoprodI.Rel : {ι : Type u_1} →
  (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → FreeMonoid ((i : ι) × M i) → FreeMonoid ((i : ι) × M i) → Prop
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid have a multiplication and multiplicative identity.  -/
Units.instMulOneClass : {α : Type u} → [inst : Monoid α] → MulOneClass αˣ
-- Mathlib.GroupTheory.OrderOfElement
zpowersEquivZPowers_apply : ∀ {G : Type u_1} [inst : Group G] {x y : G} [inst_1 : Finite G] (h : orderOf x = orderOf y) (n : ℕ),
  (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
-- Mathlib.Algebra.Order.Group.Defs
neg_le_neg : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α}, a ≤ b → -b ≤ -a
-- Mathlib.Topology.UniformSpace.OfFun
/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring.  -/
UniformSpace.ofFun : {X : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] →
      [inst_1 : PartialOrder M] →
        (d : X → X → M) →
          (∀ (x : X), d x x = 0) →
            (∀ (x y : X), d x y = d y x) →
              (∀ (x y z : X), d x z ≤ d x y + d y z) → (∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) → UniformSpace X
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `PreservesCofilteredLimitsOfSize.{w', w} F` means that `F` sends all limit cones over any
cofiltered diagram `J ⥤ C` to limit cones, where `J : Type w` with `[Category.{w'} J]`.  -/
CategoryTheory.Limits.PreservesCofilteredLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Data.List.Sort
List.perm_insertionSort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (l : List α), (List.insertionSort r l).Perm l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.PrepareRenameParams
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The special case of the first simplicial identity  -/
SimplexCategory.δ_comp_δ_self_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {Z : SimplexCategory} (h : { len := n + 1 + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) h) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) h)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
`TangentSpace`. Version in terms of the one-variable derivatives.  -/
mfderiv_prod_eq_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M × M' → M''} {p : M × M'} {v : TangentSpace (I.prod I') p},
  MDiffAt f p → (mfderiv% f p) v = ((mfderiv% fun z => f (z, p.2)) p.1) v.1 + ((mfderiv% fun z => f (p.1, z)) p.2) v.2
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_mul : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α},
  (s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Order.SuccPred
Order.covBy_iff_add_one_eq : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  x ⋖ y ↔ x + 1 = y
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [K.IsStrictlySupported e] (i : ι), CategoryTheory.IsIso ((K.restrictionToTruncGE' e).f i)
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.shortExact_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.ShortExact ↔ S.unop.ShortExact
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom_id : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), (Algebra.Generators.Hom.id P).toAlgHom = AlgHom.id R P.Ring
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.le_def : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L), K ≤ K' ↔ ↑K ⊆ ↑K'
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.adapt_EST_bind : ∀ {ε₁ ε₂ α β : Type} (f : ε₁ → ε₂) (ma : EIO ε₁ α) (g : α → EIO ε₁ β),
  EIO.adapt f (EST.bind ma g) = EST.bind (EIO.adapt f ma) fun a => EIO.adapt f (g a)
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.map_exp : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {B : Type u_2} {F : Type u_3} [inst_2 : Ring B]
  [inst_3 : FunLike F A B] [RingHomClass F A B] [inst_5 : Module ℚ B] {a : A},
  IsNilpotent a → ∀ (f : F), f (IsNilpotent.exp a) = IsNilpotent.exp (f a)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_undef : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ¬MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ → ProbabilityTheory.mgf X μ t = 0
-- Mathlib.Algebra.GroupWithZero.Action.Prod
/-- A `DistribMulAction` by a product monoid is equivalent to
commuting `DistribMulAction`s by the factors.  -/
DistribMulAction.prodEquiv : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_3) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          [inst_2 : AddMonoid α] →
            DistribMulAction (M × N) α ≃
              (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller_sModEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ},
  (Ideal.Quotient.mk I) y = (Perfection.coeff (R ⧸ I) p n) x →
    (Perfection.teichmuller p I) x ≡ y ^ p ^ n [SMOD I ^ (n + 1)]
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The structure maps to `S` as a natural transformation.  -/
AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        [inst_1 : 𝒰.LocallyDirected] → 𝒰.functorOfLocallyDirected ⟶ (CategoryTheory.Functor.const 𝒰.I₀).obj X
-- Mathlib.Order.Ideal
/-- Given a starting point, and a countable family of cofinal sets,
this is an increasing sequence that intersects each cofinal set.  -/
Order.sequenceOfCofinals : {P : Type u_1} → [inst : Preorder P] → P → {ι : Type u_2} → [Encodable ι] → (ι → Order.Cofinal P) → ℕ → P
-- Std.Sat.AIG.CNF
/-- Project the auxiliary variable assignment out of a CNF assignment
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectRightAssign : (ℕ → Bool) → ℕ → Bool
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_le_mk : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedCancelAddMonoid M] {m m' : M}
  {s s' : ℕ+}, DivisibleHull.mk m s ≤ DivisibleHull.mk m' s' ↔ ↑s' • m ≤ ↑s • m'
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Constant whose import failed.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.const : Lean.Meta.RefinedDiscrTree.ImportFailure✝ → Lean.Name
-- Init.Data.Vector.Range
Vector.zipIdx_singleton : ∀ {α : Type u_1} {x : α} {k : ℕ}, #v[x].zipIdx k = #v[(x, k)]
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mem_inf : ∀ {M : Type u_1} [inst : Add M] {p p' : AddSubsemigroup M} {x : M}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'