mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function is locally integrable on a compact set, then it is integrable on that set.  -/
MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.LocallyIntegrableOn f s μ → IsCompact s → MeasureTheory.IntegrableOn f s μ
-- Lean.Structure
Lean.StructureResolutionOrderConflict.mk.sizeOf_spec : ∀ (isDirectParent : Bool) (badParent : Lean.Name) (conflicts : Array (Bool × Lean.Name)),
  sizeOf { isDirectParent := isDirectParent, badParent := badParent, conflicts := conflicts } =
    1 + sizeOf isDirectParent + sizeOf badParent + sizeOf conflicts
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : DecidableLE α] [inst_2 : OrderTop α] (s : Finset α) (a : α),
  s.truncatedSup a = if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.codisjoint_mrange_inl_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Codisjoint (MonoidHom.mrange Monoid.Coprod.inl) (MonoidHom.mrange Monoid.Coprod.inr)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctorRev_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  (F.toProfunctorRev.map f).app X_1 = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_symm_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : r₁ ⟶ r₂),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l₂).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂).symm
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r₁).hom
            (CategoryTheory.CategoryStruct.comp α (CategoryTheory.Bicategory.leftUnitor r₂).inv)))
        (CategoryTheory.Bicategory.rightUnitor l₁).hom)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : CategoryTheory.Limits.HasImage f.hom]
  [inst_2 : CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.id f)],
  CategoryTheory.Limits.image.map (CategoryTheory.CategoryStruct.id f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
closedAbsConvexHull_min : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s t : Set E},
  s ⊆ t → AbsConvex 𝕜 t → IsClosed t → (closedAbsConvexHull 𝕜) s ⊆ t
-- Lean.DocString.Parser
/-- Skip whitespace for name and arguments. If the argument is `none`,
it's in a single-line context and whitespace may only be the space
character. If it's `some N`, then newlines are allowed, but `N` is the
minimum indentation column.
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.nameArgWhitespace : Option ℕ → Lean.Parser.ParserFn
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_cons : ∀ {G : Type u_7} [inst : AddCommGroup G] (a : G) (l : List G), (a :: l).alternatingSum = a - l.alternatingSum
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorHomImpl_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂),
  (CategoryTheory.Dial.tensorHomImpl f g).f = CategoryTheory.Limits.prod.map f.f g.f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mdifferentiableWithinAt_iff : ∀ {𝕜 : 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'] {f f₁ : M → M'} {x : M} {s : Set M},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → (MDiffAt[s] f x ↔ MDiffAt[s] f₁ x)
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of groups. For a diagram explaining the variables,
see the module docstring.  -/
MonoidHom.injective_of_surjective_of_injective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8}
  {N₄ : Type u_9} [inst : Group M₁] [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group M₄] [inst_4 : Group N₁]
  [inst_5 : Group N₂] [inst_6 : Group N₃] [inst_7 : Group N₄] (f₁ : M₁ →* M₂) (f₂ : M₂ →* M₃) (f₃ : M₃ →* M₄)
  (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (g₃ : N₃ →* N₄) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃) (i₄ : M₄ →* N₄),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        Function.MulExact ⇑f₁ ⇑f₂ →
          Function.MulExact ⇑f₂ ⇑f₃ →
            Function.MulExact ⇑g₁ ⇑g₂ →
              Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Injective ⇑i₄ → Function.Injective ⇑i₃
-- Mathlib.NumberTheory.PrimeCounting
Nat.mem_primesBelow : ∀ {k n : ℕ}, n ∈ k.primesBelow ↔ n < k ∧ Nat.Prime n
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.collectLevelParamsInInductive : List Lean.InductiveType → Array Lean.Name
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.extremePoints_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E}, IsExtreme 𝕜 A B → Set.extremePoints 𝕜 B = B ∩ Set.extremePoints 𝕜 A
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instMonad : Monad WithZero
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The `Spec` functor into the category of affine schemes.  -/
AlgebraicGeometry.AffineScheme.Spec : CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.AffineScheme
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.mk.inj : ∀ {seen : Lean.NameMap (Array Lean.Name)} {axioms : Lean.NameSet} {seen_1 : Lean.NameMap (Array Lean.Name)}
  {axioms_1 : Lean.NameSet},
  { seen := seen, axioms := axioms } = { seen := seen_1, axioms := axioms_1 } → seen = seen_1 ∧ axioms = axioms_1
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_of_isPrincipal_mul_opow`. -/
Ordinal.principal_add_of_principal_mul_opow : ∀ {b o : Ordinal.{u}},
  1 < b → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (b ^ o) → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Lean.Parser.Basic
Lean.Parser.longestMatchMkResult : ℕ → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_pprod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α}
  {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β},
  la.HasBasis pa sa →
    lb.HasBasis pb sb → (la ×ˢ lb).HasBasis (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.disjoint_splitCenterBox : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) {s t : Set ι}, s ≠ t → Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.mapsto_domChart_source_codChart_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), Set.MapsTo f h.domChart.source h.codChart.source
-- Init.Data.UInt.Lemmas
UInt16.add_sub_cancel : ∀ (a b : UInt16), a + b - b = a
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_symm_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] (x : M),
  Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)) =
    nhdsWithin x s
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- In a locally path connected space, each path component is a closed set.  -/
IsClosed.pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X), IsClosed (pathComponent x)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulForwardPatternModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat]
  [toLawfulForwardPattern : String.Slice.Pattern.LawfulForwardPattern pat],
  (∀ {s : String.Slice} (pos : s.Pos),
      String.Slice.Pattern.ForwardPattern.skipPrefix? pat s = some pos ↔
        String.Slice.Pattern.Model.IsLongestMatch pat pos) →
    String.Slice.Pattern.Model.LawfulForwardPatternModel pat
-- Mathlib.Order.Hom.Set
/-- Order isomorphism between `univ : Set α` and `α`.  -/
OrderIso.Set.univ : {α : Type u_1} → [inst : Preorder α] → ↑Set.univ ≃o α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.uniqueUpToIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t), (P.uniqueUpToIso Q).hom = Q.liftConeMorphism s
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.codeAction? : Lean.Lsp.TextDocumentClientCapabilities → Option Lean.Lsp.CodeActionClientCapabilities
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.op_unop : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.MorphismProperty Cᵒᵖ), P.unop.op = P
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the isomorphisms `hF : eA.functor ⋙ e'.functor ≅ F`,
`hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor` and the datum of
an isomorphism `η : G ⋙ F ≅ eB.functor`.  -/
AlgebraicTopology.DoldKan.Compatibility.τ₁ : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  {eB : B ≌ B'} →
                    {e' : A' ≌ B'} →
                      {F : CategoryTheory.Functor A B'} →
                        (eA.functor.comp e'.functor ≅ F) →
                          {G : CategoryTheory.Functor B A} →
                            (eB.functor.comp e'.inverse ≅ G.comp eA.functor) →
                              (G.comp F ≅ eB.functor) → (eB.functor.comp (e'.inverse.comp e'.functor) ≅ eB.functor)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The open immersion `Spec Γ(𝒪ₓ/I, U) ⟶ Spec Γ(𝒪ₓ/I, V)` if `U ≤ V`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) → {U V : ↑X.affineOpens} → U ≤ V → (I.glueDataObj U ⟶ I.glueDataObj V)
-- Mathlib.Algebra.Order.Ring.Pow
/-- **Bernoulli's inequality** reformulated to estimate `a^n`.  -/
one_add_mul_sub_le_pow : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R},
  -1 ≤ a → ∀ (n : ℕ), 1 + ↑n * (a - 1) ≤ a ^ n
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.instLaplacian : {E : Type u_5} →
  {F : Type u_8} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          [inst_3 : InnerProductSpace ℝ E] → [FiniteDimensional ℝ E] → Laplacian (SchwartzMap E F) (SchwartzMap E F)
-- Mathlib.Topology.Compactness.LocallyCompact
instWeaklyLocallyCompactSpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [WeaklyLocallyCompactSpace X]
  [WeaklyLocallyCompactSpace Y], WeaklyLocallyCompactSpace (X × Y)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.superposeAC?.go.eq_def : ∀ (s₁ s₂ : Lean.Grind.AC.Seq) (r₁ c r₂ : Option Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.superposeAC?.go✝ s₁ s₂ r₁ c r₂ =
    match s₁, s₂ with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y =>
      if (x == y) = true then
        Lean.Grind.AC.Seq.superposeAC?.mkResult✝ (Lean.Grind.AC.rev✝ r₁) (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ c x))
          (Lean.Grind.AC.rev✝ r₂)
      else
        Lean.Grind.AC.Seq.superposeAC?.mkResult✝ (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ r₁ x)) (Lean.Grind.AC.rev✝ c)
          (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ r₂ y))
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s₂ =>
      if (x == y) = true then
        Lean.Grind.AC.Seq.superposeAC?.mkResult✝ (Lean.Grind.AC.rev✝ r₁) (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ c x))
          (Lean.Grind.AC.app✝ (Lean.Grind.AC.rev✝ r₂) s₂)
      else
        if x < y then
          Lean.Grind.AC.Seq.superposeAC?.mkResult✝ (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ r₁ x))
            (Lean.Grind.AC.rev✝ c) (Lean.Grind.AC.app✝ (Lean.Grind.AC.rev✝ r₂) (Lean.Grind.AC.Seq.cons y s₂))
        else Lean.Grind.AC.Seq.superposeAC?.go✝ (Lean.Grind.AC.Seq.var x) s₂ r₁ c (Lean.Grind.AC.push✝ r₂ y)
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.var y =>
      if (x == y) = true then
        Lean.Grind.AC.Seq.superposeAC?.mkResult✝ (Lean.Grind.AC.app✝ (Lean.Grind.AC.rev✝ r₁) s₁)
          (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ c x)) (Lean.Grind.AC.rev✝ r₂)
      else
        if x < y then Lean.Grind.AC.Seq.superposeAC?.go✝ s₁ (Lean.Grind.AC.Seq.var y) (Lean.Grind.AC.push✝ r₁ x) c r₂
        else
          Lean.Grind.AC.Seq.superposeAC?.mkResult✝
            (Lean.Grind.AC.app✝ (Lean.Grind.AC.rev✝ r₁) (Lean.Grind.AC.Seq.cons x s₁)) (Lean.Grind.AC.rev✝ c)
            (Lean.Grind.AC.rev✝ (Lean.Grind.AC.push✝ r₂ y))
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.cons y s₂ =>
      if (x == y) = true then Lean.Grind.AC.Seq.superposeAC?.go✝ s₁ s₂ r₁ (Lean.Grind.AC.push✝ c x) r₂
      else
        if x < y then
          Lean.Grind.AC.Seq.superposeAC?.go✝ s₁ (Lean.Grind.AC.Seq.cons y s₂) (Lean.Grind.AC.push✝ r₁ x) c r₂
        else Lean.Grind.AC.Seq.superposeAC?.go✝ (Lean.Grind.AC.Seq.cons x s₁) s₂ r₁ c (Lean.Grind.AC.push✝ r₂ y)
-- Mathlib.Algebra.Order.Ring.Abs
abs_pow_sub_pow_le : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : LinearOrder α] (a b : α) (n : ℕ) [IsOrderedRing α],
  |a ^ n - b ^ n| ≤ |a - b| * ↑n * max |a| |b| ^ (n - 1)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integral_gaussian_complex_Ioi : ∀ {b : ℂ}, 0 < b.re → ∫ (x : ℝ) in Set.Ioi 0, Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2) / 2
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextEditBatch : Lean.ToJson Lean.Lsp.TextEditBatch
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_mem_support_of_nonzero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.natTrailingDegree ∈ p.support
-- Init.Data.Ord.Vector
Vector.instOrd : {α : Type u_1} → {n : ℕ} → [Ord α] → Ord (Vector α n)
-- Lean.ImportingFlag
/-- We say Lean is "initializing" when it is executing `builtin_initialize` declarations or importing modules.
Recall that Lean executes `initialize` declarations while importing modules.
 -/
Lean.initializing : BaseIO Bool
-- Std.Http.Data.Body.Any
Std.Http.Body.Any.mk.injEq : ∀ (recv : Std.Async.Async (Option Std.Http.Chunk)) (close : Std.Async.Async Unit) (isClosed : Std.Async.Async Bool)
  (recvSelector : Std.Async.Selector (Option Std.Http.Chunk))
  (tryRecv : Std.Async.Async (Option (Option Std.Http.Chunk)))
  (getKnownSize : Std.Async.Async (Option Std.Http.Body.Length))
  (setKnownSize : Option Std.Http.Body.Length → Std.Async.Async Unit) (recv_1 : Std.Async.Async (Option Std.Http.Chunk))
  (close_1 : Std.Async.Async Unit) (isClosed_1 : Std.Async.Async Bool)
  (recvSelector_1 : Std.Async.Selector (Option Std.Http.Chunk))
  (tryRecv_1 : Std.Async.Async (Option (Option Std.Http.Chunk)))
  (getKnownSize_1 : Std.Async.Async (Option Std.Http.Body.Length))
  (setKnownSize_1 : Option Std.Http.Body.Length → Std.Async.Async Unit),
  ({ recv := recv, close := close, isClosed := isClosed, recvSelector := recvSelector, tryRecv := tryRecv,
        getKnownSize := getKnownSize, setKnownSize := setKnownSize } =
      { recv := recv_1, close := close_1, isClosed := isClosed_1, recvSelector := recvSelector_1, tryRecv := tryRecv_1,
        getKnownSize := getKnownSize_1, setKnownSize := setKnownSize_1 }) =
    (recv = recv_1 ∧
      close = close_1 ∧
        isClosed = isClosed_1 ∧
          recvSelector = recvSelector_1 ∧
            tryRecv = tryRecv_1 ∧ getKnownSize = getKnownSize_1 ∧ setKnownSize = setKnownSize_1)
-- Init.WF
/-- Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the
context of a termination proof inside `if-then-else` with the condition.
 -/
ite_eq_dite : ∀ {P : Prop} {α : Sort u_1} {a b : α} [inst : Decidable P],
  (if P then a else b) = if h : P then binderNameHint h () a else binderNameHint h () b
-- Mathlib.RepresentationTheory.Equiv
Representation.diagonalOneEquivLeftRegular_symm_apply_single : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Monoid G] (g : G) (r : k),
  (Representation.diagonalOneEquivLeftRegular k G).symm (MonoidAlgebra.single g r) =
    MonoidAlgebra.single (uniqueElim g) r
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ),
  0 ≤ r → r • j = r.toNNReal • j
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a function on the values from right to left (in decreasing order).  -/
RBTree.RBMap.foldr : {α : Type u} → {β : Type v} → {σ : Type w} → {cmp : α → α → Ordering} → (α → β → σ → σ) → σ → RBTree.RBMap α β cmp → σ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.X_eq_iff : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ y₁ x₂ y₂ : F} {h₁ : W.Nonsingular x₁ y₁}
  {h₂ : W.Nonsingular x₂ y₂},
  x₁ = x₂ ↔
    WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ = WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ ∨
      WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ = -WeierstrassCurve.Affine.Point.some x₂ y₂ h₂
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.Iso.isMatching_map : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {M : G.Subgraph} (f : G ≃g G'),
  (SimpleGraph.Subgraph.map f.toHom M).IsMatching ↔ M.IsMatching
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecls.mk : Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl → Mathlib.Meta.FunProp.FunPropDecls
-- Lean.Parser.Command
Lean.Parser.Command.version.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_pos_of_nextCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.nextCoeff ≠ 0 → 0 < p.natDegree
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocessOutParam.preprocessArgs : Array ℕ → Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_restrict_left : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (g : Y.PartialMap Z),
  (f.restrict U hU hU').comp g =
    (f.comp g).restrict
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor f.domain.ι).obj
          ((TopologicalSpace.Opens.map f.hom.base).obj g.domain) ⊓
        U)
      ⋯ ⋯
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.finite_setOfPred_absNorm_le₀ : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm ↑I ≤ n}.Finite
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_3.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Turing.TM0to1.Λ' Γ Λ → Sort u_3) (a : Γ) (q : Λ)
  (h_1 : (q : Λ) → motive (Turing.TM0to1.Λ'.normal q))
  (h_2 : (d : Turing.Dir) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q))
  (h_3 : (a : Γ) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q)),
  (match Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q with
    | Turing.TM0to1.Λ'.normal q => h_1 q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q => h_2 d q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q => h_3 a q) =
    h_3 a q
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.comp_homeomorph_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {E' : Type u_3}
  [inst_2 : TopologicalSpace E'] (g : E' ≃ₜ E), IsCoveringMap (f ∘ ⇑g) ↔ IsCoveringMap f
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z),
  (e.transOpenPartialHomeomorph f').source = ⇑e ⁻¹' f'.source
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_stableUnderComposition : RingHom.StableUnderComposition @RingHom.FiniteType
-- Mathlib.Data.ZMod.Basic
ZMod.coe_unitOfCoprime : ∀ {n : ℕ} (x : ℕ) (h : x.Coprime n), ↑(ZMod.unitOfCoprime x h) = ↑x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instLeast? : Std.PRange.Least? Int16
-- Init.Data.String.Substring
/-- Retains only the longest prefix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's end position towards its start position.
 -/
Substring.Raw.takeWhile : Substring.Raw → (Char → Bool) → Substring.Raw
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlEval.mk : {α : Type u} → (α → Lean.Elab.Command.CommandElabM ProofWidgets.Html) → ProofWidgets.HtmlEval α