mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Attributes
Lean.ParametricAttribute.ext : {α : Type} →
  Lean.ParametricAttribute α →
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α)
-- Init.Data.SInt.Basic
instSubInt64 : Sub Int64
-- Mathlib.Data.ENat.Lattice
ENat.add_iInf : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, a + iInf f = ⨅ b, a + f b
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.lhs : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.TernaryInput → aig.Ref
-- Mathlib.Data.List.Fold
List.foldl_cons_nil : ∀ {α : Type u_1} {l : List α}, List.foldl (flip List.cons) [] l = l.reverse
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeLeftRingHom_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (a : A), Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1
-- Init.Data.Sum.Basic
/-- Checks whether a sum is the right injection `inr` and, if so, retrieves its contents.  -/
Sum.getRight? : {α : Type u_1} → {β : Type u_2} → α ⊕ β → Option β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoPushout_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp inr h.isoPushout.hom = CategoryTheory.Limits.pushout.inr f g
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesTypes.isEagerSplit : Lean.Meta.Grind.CasesTypes → Lean.Name → Bool
-- Std.Sat.AIG.CachedGatesLemmas
/-- Encoding of XOR as boolean expression in AIG form.
 -/
_private.Std.Sat.AIG.CachedGatesLemmas.0.Std.Sat.AIG.xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_eq_insertMany! : ∀ {α : Type u} {β : Type v} {x : Ord α} {l : List (α × β)} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t.Balanced),
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l h) = ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter! m₂) k =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.get? m₁ k else none
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded URI component with a compile-time proof that it contains only valid encoded characters.
This provides type-safe URI encoding without runtime validation.

The invariant guarantees that the string contains only unreserved characters (alphanumeric, hyphen, period,
underscore, tilde) and percent signs (for escape sequences).
 -/
Std.Http.URI.EncodedString : (UInt8 → Bool) → Type
-- Init.Data.Nat.Basic
Nat.beq.eq_def : ∀ (x x_1 : ℕ),
  x.beq x_1 =
    match x, x_1 with
    | Nat.zero, Nat.zero => true
    | Nat.zero, n.succ => false
    | n.succ, Nat.zero => false
    | n.succ, m.succ => n.beq m
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.mk : {G : Type u_1} →
  [inst : CategoryTheory.Groupoid G] →
    (quiverGenerators : Quiver (IsFreeGroupoid.Generators G)) →
      (of :
          {a b : IsFreeGroupoid.Generators G} →
            (a ⟶ b) →
              ((have this := a;
                this) ⟶
                b)) →
        (∀ {X : Type v} [inst_1 : Group X] (f : Quiver.Labelling (IsFreeGroupoid.Generators G) X),
            ∃! F, ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (of g) = f g) →
          IsFreeGroupoid G
-- Mathlib.Data.Int.Bitwise
Int.shiftRight_negSucc : ∀ (m n : ℕ), Int.negSucc m >>> ↑n = Int.negSucc (m >>> n)
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.eqToHom_comp_homOfLE_assoc : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c) {Z : X} (h : c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hbc) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) h
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.projection_equiv_id_iff_isNoetherian : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} (hST : IsCompl S T), S.projection T hST ≈ LinearMap.id ↔ IsNoetherian K ↥T
-- Mathlib.Order.SupClosed
SupClosed.insert_lowerBounds : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α} {a : α}, SupClosed s → a ∈ lowerBounds s → SupClosed (insert a s)
-- Mathlib.Algebra.Group.Conj
IsAddConj.refl : ∀ {α : Type u} [inst : AddMonoid α] (a : α), IsAddConj a a
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- `seminormFromConst_seq c f x` is antitone.  -/
seminormFromConst_seq_antitone : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → ∀ (x : R), Antitone (seminormFromConst_seq c f x)
-- Mathlib.Order.Types.Defs
OrderType.type_le_type : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β] (h : α ↪o β), OrderType.type α ≤ OrderType.type β
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Obj.mk : Option Lean.Expr → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.toIsometryClass : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂],
  IsometryClass 𝓕 E E₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instVAdd.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instVAdd = { vadd := fun a s => { carrier := (fun x => a +ᵥ x) '' ↑s, lower' := ⋯ } }
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The category of pointed Galois objects is cofiltered.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instIsCofilteredOrEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Given an open partial homeomorphism `e` from a space `α` into `H`, if its source covers the
whole space `α`, then the induced charted space structure on `α` is `HasGroupoid G` for any
structure groupoid `G` which is closed under restrictions.  -/
OpenPartialHomeomorph.singleton_hasGroupoid : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : OpenPartialHomeomorph α H)
  (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G], HasGroupoid α G
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.quotientMeasure_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [Countable G] {s t : Set α} [MeasureTheory.SMulInvariantMeasure G α μ]
  [MeasurableConstSMul G α],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s) =
        MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict t)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_eq_iInf' : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α), m.trim s = ⨅ t, m ↑t
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.fromSpecResidueField_apply : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X) (s : ↥(AlgebraicGeometry.Spec (X.residueField x))),
  (X.fromSpecResidueField x) s = x
-- Std.Internal.UV.System
/-- Gets the title of the current process.
 -/
Std.Internal.UV.System.getProcessTitle : IO String
-- Mathlib.Data.WSeq.Defs
/-- Get the list of indexes of elements of `s` satisfying `p`  -/
Stream'.WSeq.findIndexes : {α : Type u} → (p : α → Prop) → [DecidablePred p] → Stream'.WSeq α → Stream'.WSeq ℕ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rco : ∀ {m n i : ℕ}, (m...n).toList[i]? = if i < n - m then some (m + i) else none
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  MeasurableSet s → ((∀ᵐ (z : α × β) ∂μ.prod ν, z ∈ s) ↔ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) ∈ s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_lt : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α},
  Measurable f → Measurable g → MeasurableSet {a | f a < g a}
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCycle_rotate`. -/
SimpleGraph.Walk.IsCycle.rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  c.IsCycle → (c.rotate u hu).IsCycle
-- Mathlib.GroupTheory.Complement
AddSubgroup.vadd_leftQuotientEquiv : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {F : Type u_2} [inst_1 : AddGroup F] [inst_2 : AddAction F G]
  [inst_3 : AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H),
  f +ᵥ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv (f +ᵥ q))
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_one_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨1, SSet.horn₃₂.desc.multicofork_π_one._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 1).inv f₁) h
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_inj : ∀ {a b : Ordinal.{u}}, a.gamma = b.gamma ↔ a = b
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.mono_left : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, s ⊆ t → IsCofinalFor t u → IsCofinalFor s u
-- Lean.Meta.Tactic.Grind.Types
/-- Solver extension, can only be generated by `registerSolverExtension` that allocates a unique index
for this extension into each goal's extension state's array.
 -/
Lean.Meta.Grind.SolverExtension : Type → Type
-- Init.Data.SInt.Bitwise
Int16.shiftLeft_or : ∀ {a b c : Int16}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Init.PropLemmas
Decidable.of_not_imp : ∀ {a b : Prop} [Decidable a], ¬(a → b) → a
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.comp.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.ToPartrec.Cont) (a_2 : Turing.ToPartrec.Code) (a_3 : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.comp a a_1 = Turing.ToPartrec.Cont.comp a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodEquiv_symm_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H)
  (q : (G ⧸ A) × H ⧸ B), (QuotientAddGroup.prodEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1st 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 1 ≅ ModuleCat.of k (G → ↑A)
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X], MeasureTheory.Measure.support 0 = ∅
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The derivation relative to the morphism of commutative rings `φ'.app X` induced by
a derivation relative to a morphism of presheaves of commutative rings.  -/
PresheafOfModules.Derivation'.app : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
        {φ' : S' ⟶ R} → M.Derivation' φ' → (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.neg_prod_neg : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Ring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : IsTopologicalAddGroup M₂] [inst_8 : AddCommGroup M₃] [inst_9 : Module R M₃] [inst_10 : TopologicalSpace M₃]
  [inst_11 : IsTopologicalAddGroup M₃] (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃),
  (-f).prod (-g) = -f.prod g
-- Mathlib.Analysis.Complex.Basic
RCLike.re_tsum : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜},
  Summable f L → RCLike.re (∑'[L] (a : α), f a) = ∑'[L] (a : α), RCLike.re (f a)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.fix.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : Turing.PartrecToTM2.Cont'} {a_2 : Turing.ToPartrec.Code}
  {a_3 : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.Cont'.fix a a_1 = Turing.PartrecToTM2.Cont'.fix a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Util.AddRelatedDecl
/-- Re-implementation of the inner loop of `Lean.Linter.tacticCheckInstances` for use on
declarations synthesized by Mathlib attributes (`@[simps]`, `@[reassoc]`, `@[elementwise]`, ...).
Returns the list of semireducible non-instance definitions that `Meta.check declType .default`
had to unfold but `Meta.check declType .implicit` would not, or `none` if `declType` already
passes the `.implicit` check.  -/
_private.Mathlib.Util.AddRelatedDecl.0.Mathlib.Tactic.checkImplicitTransparency : Lean.Expr → Lean.MetaM (Option (List Lean.Name))
-- Mathlib.Data.Set.Insert
/-- **Alias** of `Set.ofPred_eq_eq_singleton`. -/
Set.setOf_eq_eq_singleton : ∀ {α : Type u_1} {a : α}, {n | n = a} = {a}
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any natural number
`n` and any real numbers `b` and `c` such that `b` is positive.  -/
Real.tendsto_mul_exp_add_div_pow_atTop : ∀ (b c : ℝ) (n : ℕ), 0 < b → Filter.Tendsto (fun x => (b * Real.exp x + c) / x ^ n) Filter.atTop Filter.atTop
-- Mathlib.Data.ZMod.IntUnitsPower
ZMod.natCast_smul_units : ∀ (n : ℕ) (au : Additive ℤˣ), ↑n • au = n • au
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p]
  (x : K), (IsPerfectClosure.equiv i j p) (i x) = j x
-- Init.Grind.Ring.Basic
/-- `PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.

The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.

The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
instances for general finite fields via `FiniteField.pow_card`.
 -/
Lean.Grind.PowIdentity : (α : Type u) → [Lean.Grind.CommSemiring α] → outParam ℕ → Prop
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- The real-valued function sending `x ∈ R` to the limit of `(f (x * c^n))/((f c)^n)`.  -/
seminormFromConst' : {R : Type u_1} → [inst : CommRing R] → R → RingSeminorm R → R → ℝ
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `c ↦ c ⊙ₗ d` as a functor.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight : (C : Type u_1) →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] → D → CategoryTheory.Functor C D
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.nnnorm_le_of_forall_inner_le : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A] {M : CStarMatrix m n A}
  {C : NNReal},
  (∀ (v : WithCStarModule A (m → A)) (w : WithCStarModule A (n → A)),
      ‖inner A w ((CStarMatrix.toCLM M) v)‖₊ ≤ C * ‖v‖₊ * ‖w‖₊) →
    ‖M‖₊ ≤ C
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.div : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : Div β],
  Function.Periodic f c → Function.Periodic g c → Function.Periodic (f / g) c
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallHom.equiv_shift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {W : CategoryTheory.MorphismProperty C} {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] [inst_5 : W.IsCompatibleWithShift M] (L : CategoryTheory.Functor C D)
  [inst_6 : L.IsLocalization W] [inst_7 : L.CommShift M] {X Y : C}
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : CategoryTheory.Localization.SmallHom W X Y)
  (a : M)
  [inst_9 :
    CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X)
      ((CategoryTheory.shiftFunctor C a).obj Y)],
  (CategoryTheory.Localization.SmallHom.equiv W L) (f.shift a) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L a).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Localization.SmallHom.equiv W L) f))
        ((CategoryTheory.Functor.commShiftIso L a).inv.app Y))
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_of_tendsto_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} {a : α} {s : Set α} {l : Filter β},
  Filter.Tendsto f (nhds a) l → Filter.Tendsto f (nhdsWithin a s) l
-- Init.Data.List.Impl
/-- Replaces the element at the given index, if it exists, with the result of applying `f` to it.

This is a tail-recursive version of `List.modify`.

Examples:
* `[1, 2, 3].modifyTR 0 (· * 10) = [10, 2, 3]`
* `[1, 2, 3].modifyTR 2 (· * 10) = [1, 2, 30]`
* `[1, 2, 3].modifyTR 3 (· * 10) = [1, 2, 3]`
 -/
List.modifyTR : {α : Type u_1} → List α → ℕ → (α → α) → List α
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.eq_of_mem_of_mem : ∀ {ι : Type u_1} {I J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ},
  J₁ ∈ π → J₂ ∈ π → x ∈ J₁ → x ∈ J₂ → J₁ = J₂
-- Mathlib.Algebra.Ring.Opposite
NonUnitalRingHom.fromOpposite_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)), ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
-- Aesop.Forward.SlotIndex
Aesop.instHashableSlotIndex.hash : Aesop.SlotIndex → UInt64
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {x : R},
  IsSMulRegular R x → x ∈ Ring.jacobson R → ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R
-- Mathlib.MeasureTheory.Integral.CircleTransform
/-- The derivative of `circleTransform` w.r.t. `w`.  -/
Complex.circleTransformDeriv : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ℝ → ℂ → ℂ → (ℂ → E) → ℝ → E
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instInfOpenSubgroup : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → Min (OpenSubgroup G)
-- Mathlib.Tactic.NormNum.Result
/-- The result of `norm_num` running on an expression `x` of type `α`.
Untyped version of `Result`.  -/
Mathlib.Meta.NormNum.Result' : Type
-- Mathlib.Order.Lattice.Congruence
LatticeCon.toSetoid : {α : Type u_2} → [inst : Lattice α] → LatticeCon α → Setoid α
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.addAutoBoundImplicits.go : Array Lean.Expr → Option String.Pos.Raw → List Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.smul_apply : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)] (c : 𝕜) (x : PiLp p β) (i : ι),
  (c • x).ofLp i = c • x.ofLp i
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetBind.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α}, a • ∅ = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero.  -/
ENNReal.tendsto_tsum_compl_atTop_zero : ∀ {α : Type u_4} {f : α → ENNReal},
  ∑' (x : α), f x ≠ ⊤ → Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ext_iff : ∀ {X Y : AddCommGrpCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.mk.sizeOf_spec : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} (marks : Array Bool) (hmarks : marks.size = aig.decls.size)
  (inv : Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks hmarks),
  sizeOf { marks := marks, hmarks := hmarks, inv := inv } = 1 + sizeOf marks + sizeOf hmarks
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The (topological) closure of a non-unital subring of a non-unital topological ring is
itself a non-unital subring.  -/
NonUnitalSubring.topologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalRing R] → [IsSemitopologicalRing R] → NonUnitalSubring R → NonUnitalSubring R
-- Init.Omega.IntList
/-- Implementation of `*` on `IntList`.  -/
Lean.Omega.IntList.mul : Lean.Omega.IntList → Lean.Omega.IntList → Lean.Omega.IntList