mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.IO
_private.Init.System.IO.0.IO.Process.Child.mk.inj : ∀ {cfg : IO.Process.StdioConfig} {stdin : cfg.stdin.toHandleType} {stdout : cfg.stdout.toHandleType}
  {stderr : cfg.stderr.toHandleType} {stdin_1 : cfg.stdin.toHandleType} {stdout_1 : cfg.stdout.toHandleType}
  {stderr_1 : cfg.stderr.toHandleType},
  { stdin := stdin, stdout := stdout, stderr := stderr } =
      { stdin := stdin_1, stdout := stdout_1, stderr := stderr_1 } →
    stdin = stdin_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_apply_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIocDiv hp a (a + p) = 0
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_eq_sum : ∀ {α : Type u_3} {β : Type u_6} [inst : AddCommMonoid β] (s : Finset α) (f : α → β), s.noncommSum f ⋯ = s.sum f
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lintegral_eq_of_lmarginal_eq : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [inst_3 : Fintype δ] (s : Finset δ)
  {f g : ((i : δ) → X i) → ENNReal},
  Measurable f →
    Measurable g →
      ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ →
        ∫⁻ (x : (i : δ) → X i), f x ∂MeasureTheory.Measure.pi μ =
          ∫⁻ (x : (i : δ) → X i), g x ∂MeasureTheory.Measure.pi μ
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.success.inj : ∀ {mvarsToCheckType instMVars mvarsToCheckType_1 instMVars_1 : Array Lean.MVarId},
  Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType instMVars =
      Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType_1 instMVars_1 →
    mvarsToCheckType = mvarsToCheckType_1 ∧ instMVars = instMVars_1
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.exists_affineOpenCover_presentation : ∀ {X : AlgebraicGeometry.Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M],
  ∃ 𝒰, ∀ (i : 𝒰.I₀), Nonempty (SheafOfModules.Presentation (M.restrict (𝒰.f i)))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.Hom.hom_pow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [inst_3 : CategoryTheory.IsCommMonObj N.X]
  (f : M ⟶ N) (n : ℕ), (f ^ n).hom = f.hom ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ 4 = W.preΨ₄
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.ωUnit_coe : ∀ (p : ℕ), ↑(LucasLehmer.ωUnit p) = LucasLehmer.X.ω
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, sep, ...as]` is split at the `sep` element equal to `a`,
the result is the concatenation of `splitOnP` called on `xs` and `as`  -/
List.splitOn_append_cons_of_beq : ∀ {α : Type u_1} [inst : BEq α] {a : α} (xs as : List α) {sep : α},
  (sep == a) = true → List.splitOn a (xs ++ sep :: as) = List.splitOn a xs ++ List.splitOn a as
-- Mathlib.CategoryTheory.Yoneda
/-- Extensionality via Coyoneda. The typical usage would be
```
-- Goal is `X ≅ Y`
apply Coyoneda.ext
-- Goals are now functions `(X ⟶ Z) → (Y ⟶ Z)`, `(Y ⟶ Z) → (X ⟶ Z)`, and the fact that these
-- functions are inverses and natural in `Z`.
```
 -/
CategoryTheory.Coyoneda.ext : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X Y : C) →
      (p : {Z : C} → (X ⟶ Z) → (Y ⟶ Z)) →
        (q : {Z : C} → (Y ⟶ Z) → (X ⟶ Z)) →
          (∀ {Z : C} (f : X ⟶ Z), q (p f) = f) →
            (∀ {Z : C} (f : Y ⟶ Z), p (q f) = f) →
              (∀ {Z Z' : C} (f : Y ⟶ Z) (g : Z ⟶ Z'),
                  q (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (q f) g) →
                (X ≅ Y)
-- Mathlib.MeasureTheory.Group.LIntegral
/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative
function `f` is 0 iff `f` is 0.  -/
MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : TopologicalSpace G]
  [inst_2 : AddGroup G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.Regular] [NeZero μ]
  {f : G → ENNReal}, Continuous f → (∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Mono S.v₀₁.τ₃
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck}
  (base : X.base ⟶ Y.base) (fiber : X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber) (base_1 : X.base ⟶ Y.base)
  (fiber_1 : X.fiber ⟶ (F.map base_1.op.toLoc).toFunctor.obj Y.fiber),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A} {f : Polynomial A}
  {h : PowerSeries A},
  g.IsWeierstrassFactorization f h → f.natDegree = ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_v₁₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.v₁₂ = CategoryTheory.ShortComplex.opMap S.v₁₂
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.pos_eq_rawEndPos : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → (it.i = it.s.rawEndPos ↔ r = [])
-- Mathlib.Topology.Order.Basic
Dense.topology_eq_generateFrom : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α},
  Dense s → inst = TopologicalSpace.generateFrom (Set.Ioi '' s ∪ Set.Iio '' s)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `locallyLipschitz_neg_iff`. -/
LocallyLipschitz.neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz f → LocallyLipschitz (-f)
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.dense_preimage_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → ∀ {s : Set Y}, Dense (f ⁻¹' s) ↔ Dense s
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Nanosecond.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toNanoseconds : Std.Time.WallTime → Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.sectionOfCone c)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.associator_naturality : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂) (f₃ : X₃.Hom Y₃),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- The radius of a formal multilinear series is the largest `r` such that the sum `Σ ‖pₙ‖ ‖y‖ⁿ`
converges for all `‖y‖ < r`. This implies that `Σ pₙ yⁿ` converges for all `‖y‖ < r`, but these
definitions are *not* equivalent in general.  -/
FormalMultilinearSeries.radius : {𝕜 : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → FormalMultilinearSeries 𝕜 E F → ENNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- A `reflexivePair` composed with a functor is isomorphic to the `reflexivePair` obtained by
applying the functor at each map.  -/
CategoryTheory.Limits.reflexivePair.compRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A B : C} →
          (f g : A ⟶ B) →
            (s : B ⟶ A) →
              (sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B) →
                (sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B) →
                  (F : CategoryTheory.Functor C D) →
                    (CategoryTheory.Limits.reflexivePair f g s sl sr).comp F ≅
                      CategoryTheory.Limits.reflexivePair (F.map f) (F.map g) (F.map s) ⋯ ⋯
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.typed.inj : ∀ {ref : Lean.Syntax} {a : Lean.Elab.Tactic.RCases.RCasesPatt} {a_1 : Lean.Term} {ref_1 : Lean.Syntax}
  {a_2 : Lean.Elab.Tactic.RCases.RCasesPatt} {a_3 : Lean.Term},
  Lean.Elab.Tactic.RCases.RCasesPatt.typed ref a a_1 = Lean.Elab.Tactic.RCases.RCasesPatt.typed ref_1 a_2 a_3 →
    ref = ref_1 ∧ a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsSpanning.mk : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, (∀ (a : G), a ∈ M ∨ -a ∈ M) → M.IsSpanning
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- The complex closed unit disc, denoted as `𝕔𝔻` within the Complex namespace  -/
Complex.UnitDisc.term𝕔𝔻 : Lean.ParserDescr
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_le_of_le_mul : ∀ {a b c : ℤ}, 0 < c → a ≤ b * c → a.tdiv c ≤ b + if 0 ≤ a then 0 else 1
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRight_map_app_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : CategoryTheory.Functor D E} (τ : X ⟶ Y)
  (F : CategoryTheory.Functor C D) (c : C),
  (((CategoryTheory.Functor.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommRingCat.Hom.mk.inj : ∀ {R S : CommRingCat} {hom' hom'_1 : ↑R →+* ↑S}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.self : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α) (a : α),
  variationOnFromTo f s a a = 0
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.map_comp : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (self.map X Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z))
      (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z))
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.orderBot : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.InitialMonoClass C] → {X : C} → OrderBot (CategoryTheory.Subobject X)
-- Init.Grind.AC
Lean.Grind.AC.Seq.beq' : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Init.Data.Array.Bootstrap
Array.foldrM_eq_reverse_foldlM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α},
  Array.foldrM f init xs = List.foldlM (fun x y => f y x) init xs.toList.reverse
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_add_single : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι)
  (f : Π₀ (i : ι), β i), (DFinsupp.erase i f + fun₀ | i => f i) = f
-- Std.Do.WP.Monad
Std.Do.WPMonad.toWP : {m : Type u → Type v} →
  {ps : outParam Std.Do.PostShape} → {inst : Monad m} → [self : Std.Do.WPMonad m ps] → Std.Do.WP m ps
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_powerset_insert : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∉ s →
      ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
        ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t + ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)
-- Mathlib.Order.CountableDenseLinearOrder
/-- Given an ideal which intersects `definedAtLeft β a`, pick `b : β` such that
some partial function in the ideal maps `a` to `b`.  -/
Order.PartialIso.funOfIdeal : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] →
        [inst_2 : DenselyOrdered β] →
          [inst_3 : NoMinOrder β] →
            [inst_4 : NoMaxOrder β] →
              [inst_5 : Nonempty β] →
                (a : α) →
                  (I : Order.Ideal (Order.PartialIso α β)) →
                    (∃ f ∈ Order.PartialIso.definedAtLeft β a, f ∈ I) → { b // ∃ f ∈ I, (a, b) ∈ ↑f }
-- Mathlib.Data.Finset.Sups
Finset.coe_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Finset α), ↑s.compls = compl '' ↑s
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V W : (TopologicalSpace.Opens ↥↑U)ᵒᵖ} (i : V ⟶ W),
  (↑U).presheaf.map i = X.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).map i.unop).op
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₂.contains k = true → (m₁.inter m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} (c : β), Filter.EventuallyConst (fun x => c) l
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularMono.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (Z : C) →
          (left right : Y ⟶ Z) →
            (w :
                autoParam (CategoryTheory.CategoryStruct.comp f left = CategoryTheory.CategoryStruct.comp f right)
                  CategoryTheory.RegularMono.w._autoParam) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w) → CategoryTheory.RegularMono f
-- Mathlib.Condensed.Module
instAbelianCondensedMod : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Abelian (CondensedMod R)
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, this is the functor sending a `G`-representation `A` to the
`G ⧸ S`-representation it induces on `A_S`.  -/
Rep.quotientToCoinvariantsFunctor : (k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) → [inst_2 : S.Normal] → CategoryTheory.Functor (Rep.{w, u, v} k G) (Rep.{w, u, v} k (G ⧸ S))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.of_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.map f p).IsCycle → p.IsCycle
-- Aesop.Builder.NormSimp
_private.Aesop.Builder.NormSimp.0.Aesop.getSimpEntriesFromPropConst : Lean.Name → Lean.MetaM (Array Lean.Meta.SimpEntry)
-- Mathlib.SetTheory.ZFC.PSet
PSet.instLE : LE PSet.{u_1}
-- Mathlib.RingTheory.FreeRing
/-- The ring homomorphism `FreeRing α →+* R` induced from a map `α → R`.  -/
FreeRing.lift : {α : Type u} → {R : Type v} → [inst : Ring R] → (α → R) ≃ (FreeRing α →+* R)
-- Mathlib.Data.Real.Basic
CauSeq.Completion.ofRat_rat : ∀ {abv : ℚ → ℚ} [inst : IsAbsoluteValue abv] (q : ℚ), CauSeq.Completion.ofRat q = ↑q
-- Lean.Compiler.InitAttr
/-- Registers an initialization procedure. Initialization procedures are run in files that import the
file they are defined in.

This attribute comes in two kinds: Without arguments, the tagged declaration should have type
`IO Unit` and are simply run during initialization. With a declaration name as a argument, the
tagged declaration should be an opaque constant and the provided declaration name an action in `IO`
that returns a value of the type of the tagged declaration. Such initialization procedures store
the resulting value and make it accessible through the tagged declaration.

The `initialize` command should usually be preferred over using this attribute directly.
 -/
Lean.regularInitAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.toLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryLaxFunctor B C → CategoryTheory.LaxFunctor B C
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_singleton : ∀ {X : Type u} [inst : PseudoMetricSpace X] (δ : ℝ) (x : X), Metric.thickening δ {x} = Metric.ball x δ
-- Init.Prelude
/-- Decides whether two 32-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt32.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt32) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt32) = 7 by decide`
 -/
UInt32.decEq : (a b : UInt32) → Decidable (a = b)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.elemExponent_le_of_pow_mem : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] {a : L} {n : ℕ},
  a ^ ringExpChar K ^ n ∈ (algebraMap K L).range → IsPurelyInseparable.elemExponent K a ≤ n
-- Mathlib.Topology.CompactOpen
/-- Currying as a homeomorphism between the function spaces `C(X × Y, Z)` and `C(X, C(Y, Z))`.  -/
Homeomorph.curry : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            [LocallyCompactSpace X] → [LocallyCompactSpace Y] → C(X × Y, Z) ≃ₜ C(X, C(Y, Z))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.id : ∀ (K : Type u_2) [inst : Field K], IsUnramifiedAtInfinitePlaces K K
-- Mathlib.Topology.Constructions
continuous_pi_iff : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i}, Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_comp_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] (f : ι → ι') (x : ι' → K), Height.logHeight (x ∘ f) ≤ Height.logHeight x
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_opens : ∀ {α : Type u} [t : TopologicalSpace α], TopologicalSpace.IsTopologicalBasis {U | IsOpen U}
-- Mathlib.Combinatorics.Tiling.Tile
/-- The points in the prototile. Use the coercion to `Set X`, or `∈` on the `Prototile`, rather
than using `carrier` directly. The coercion cannot use `SetLike` because it does not satisfy
`coe_injective`.  -/
DiscreteTiling.Prototile.carrier : {G : Type u_1} → {X : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Prototile G X → Set X
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_le_addOrderOf : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M},
  0 < addOrderOf m → ∀ (a : α), AddAction.period m a ≤ addOrderOf m
-- Mathlib.Order.Category.BoolAlg
BoolAlg.dualEquiv_inverse : BoolAlg.dualEquiv.inverse = BoolAlg.dual
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.apply_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂), e (e.symm c) = c
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'OfInv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) (a : m → R) (a_1 : n), (Matrix.toLin'OfInv hMM' hM'M) a a_1 = (Matrix.toLin' M') a a_1
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- If one restricts the finite-dimensional distribution of the real Brownian motion over a finset
`J` to a smaller finset `I`, one obtains the finite-dimensional distribution of
the real Brownian motion over `I`.  -/
ProbabilityTheory.BrownianReal.measurePreserving_restrict_projectiveFamily : ∀ {I J : Finset NNReal} (hIJ : I ⊆ J),
  MeasureTheory.MeasurePreserving (Finset.restrict₂ hIJ) (ProbabilityTheory.BrownianReal.projectiveFamily J)
    (ProbabilityTheory.BrownianReal.projectiveFamily I)
-- Mathlib.AlgebraicTopology.CechNerve
/-- Given an object `X : C`, the Čech nerve of the hom to the terminal object `X ⟶ ⊤_ C` is
naturally isomorphic to a simplicial object sending `⦋n⦌` to `Xⁿ⁺¹` (when `C` is `G-Set`, this is
`EG`, the universal cover of the classifying space of `G`).  -/
CategoryTheory.CechNerveTerminalFrom.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] →
        (X : C) →
          (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).cechNerve ≅
            CategoryTheory.cechNerveTerminalFrom X
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- Returns `some c` if the current ring has a nonzero characteristic `c`.  -/
Lean.Meta.Grind.Arith.CommRing.nonzeroChar? : {m : Type → Type} → [Monad m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m (Option ℕ)
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.instSub : {α : Type u_1} → [Sub α] → [Bot α] → Sub (WithTop α)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Access the second component of an element of `YonedaCollection F X`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        {X : C} →
          (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) →
            F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst))
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_div_iff_mul_le : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ 0 → b ≠ ⊤ ∨ c ≠ ⊤ → (a ≤ c / b ↔ a * b ≤ c)
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_of_pos : ∀ {x : EReal}, 0 < x → ⊥ * x = ⊥
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_iSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), LowerSemicontinuous (f i)) → LowerSemicontinuous fun x' => ⨆ i, f i x'