mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
apply_le_nnnorm_cfcₙ_nnreal : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄,
  x ∈ quasispectrum NNReal a →
    autoParam (ContinuousOn f (quasispectrum NNReal a)) apply_le_nnnorm_cfcₙ_nnreal._auto_1 →
      autoParam (f 0 = 0) apply_le_nnnorm_cfcₙ_nnreal._auto_3 →
        autoParam (0 ≤ a) apply_le_nnnorm_cfcₙ_nnreal._auto_5 → f x ≤ ‖cfcₙ f a‖₊
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_prod : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι),
  s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => (f i).roots
-- Mathlib.Algebra.GradedMonoid
SetLike.GradedMul.mk : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Mul R] [inst_2 : Add ι] {A : ι → S},
  (∀ ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)) → SetLike.GradedMul A
-- Mathlib.Algebra.Group.Shrink
Shrink.instMul.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α], Shrink.instMul = (equivShrink α).symm.mul
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x y : X} (f : x ⟶ y),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).snd = S.snd.map f
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.ofSimplex_eq_subcomplex_mk : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  SSet.Subcomplex.ofSimplex x = { dim := n, simplex := x }.subcomplex
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.ε_app_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε F).app ((F.obj n).obj X) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor n).inv).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F n (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app X)
-- Mathlib.Data.Set.Function
Set.MapsTo.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ},
  Set.MapsTo g t p → Set.MapsTo f s t → Set.MapsTo (g ∘ f) s p
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.range_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  Set.range ContinuousAddMonoidHom.toContinuousMap = {f | f 0 = 0 ∧ ∀ (x y : A), f (x + y) = f x + f y}
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
/-- **Alias** of `IsGδ.setOfPred_liouville`. -/
IsGδ.setOf_liouville : IsGδ {x | Liouville x}
-- Batteries.Data.RunningStats
/-- Variance of running data stream (population variance).  -/
Batteries.RunningStats.variance : Batteries.RunningStats → Float
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instAlgebraSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : Field A] →
        [inst_1 : Field B] →
          [inst_2 : Field C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → Algebra ↥A⟮b⟯ ↥A⟮(algebraMap B C) b⟯