mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Coreflexive (crude) comonadicity theorem. If `F` has a right adjoint, `C` has and `F` preserves
coreflexive equalizers and `F` reflects isomorphisms, then `F` is comonadic.
 -/
CategoryTheory.Comonad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [CategoryTheory.Limits.HasCoreflexiveEqualizers C] →
                [F.ReflectsIsomorphisms] →
                  [CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F] → CategoryTheory.ComonadicLeftAdjoint F
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- The Euler product of a family of arithmetic functions. Defined as a `tprod`, but see
`tendsTo_eulerProduct_of_tendsTo` for the outward facing `eulerProduct` API.  -/
ArithmeticFunction.eulerProduct : {ι : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → (ι → ArithmeticFunction R) → ArithmeticFunction R
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W₁.HasOfPostcompProperty W₂], W₁.unop.HasOfPrecompProperty W₂.unop
-- Mathlib.NumberTheory.ModularForms.Petersson
/-- If `f, f'` are modular forms and `f'` is zero at infinity, then `petersson k f f'` has
exponentially rapid decay at infinity.  -/
UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] (f : F) {f' : F'},
  UpperHalfPlane.IsZeroAtImInfty ⇑f' →
    ∃ a > 0, UpperHalfPlane.petersson k ⇑f ⇑f' =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-a * τ.im)
-- Mathlib.Data.FP.Basic
FP.Float.sign' : [C : FP.FloatCfg] → FP.Float → Semiquot Bool
-- Lean.Meta.Tactic.Contradiction
/-- Close goal if `localDecl` is a "generalized disequality". Example:
```
h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
```
This kind of hypotheses is created when we generate conditional equations for match expressions.
 -/
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.processGenDiseq : Lean.MVarId → Lean.LocalDecl → Lean.MetaM Bool
-- Mathlib.Order.Filter.Map
Filter.comap_eval_neBot_iff' : ∀ {ι : Type u_6} {α : ι → Type u_7} {i : ι} {f : Filter (α i)},
  (Filter.comap (Function.eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.RingCat.Hom.mk.injEq : ∀ {R S : RingCat} (hom' hom'_1 : ↑R →+* ↑S), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.max!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.Equiv t₂ → t₁.max! = t₂.max!
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.of_isIso_comp_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f]
  [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.IsIso g
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_isStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  T.rlp.IsStableUnderBaseChange
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → (W.Equation P ↔ W.toAffine.Equation (P 0 / P 2) (P 1 / P 2))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Data.String.Defs
/-- `s.IsSuffix t` checks if the string `s` is a suffix of the string `t`.  -/
String.IsSuffix : String → String → Prop
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_toSubmonoid : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), (Subring.centralizer s).toSubmonoid = Submonoid.centralizer s
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.bddBelow_range_of_cofinite : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] {u : ι → α}
  {a : α} [IsCodirectedOrder α], Filter.Tendsto u Filter.cofinite (nhds a) → BddBelow (Set.range u)