mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integral_continuousLinearMap_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ), ∫ (x : ℝ), L x ∂ProbabilityTheory.gaussianReal μ v = L μ
-- Init.Data.List.Control
List.foldlM_cons : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {b : β} {a : α}
  {l : List α},
  List.foldlM f b (a :: l) = do
    let init ← f b a
    List.foldlM f init l
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySum_smul : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (r : R) (f : MultilinearMap R N M₂), (r • f).currySum = r • f.currySum
-- Lean.Meta.Tactic.SolveByElim
/-- Transparency mode for calls to `apply`.  -/
Lean.Meta.SolveByElim.ApplyRulesConfig.transparency : Lean.Meta.SolveByElim.ApplyRulesConfig → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported : ∀ {ι : 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.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e
-- Mathlib.Order.UpperLower.Relative
isUpperSet_subtype_iff_isRelUpperSet : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {s : Set { x // P x }}, IsUpperSet s ↔ IsRelUpperSet (Subtype.val '' s) P
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The property that is satisfied by bifibrant objects, i.e. objects
that are both cofibrant and fibrant.
(This is only introduced in order to consider the full subcategory
`BifibrantObject`. Otherwise, the typeclasses `IsCofibrant` and
`IsFibrant` are preferred.)  -/
HomotopicalAlgebra.bifibrantObjects : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] →
      [CategoryTheory.Limits.HasInitial C] →
        [HomotopicalAlgebra.CategoryWithFibrations C] →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.ObjectProperty C
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.isLowerSet_preimage_coe : ∀ {α : Type u_1} [inst : LE α] {s t : Set α},
  IsUpperSet s → (IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.zpow₀_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 : ι) → GroupWithZero (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  (i : ι) (x : G i) (n : ℤ), ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧
-- Std.Data.ByteSlice
/-- Creates a new ByteSlice of a ByteArray
 -/
ByteSlice.ofByteArray : ByteArray → ByteSlice