mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mk.inj : ∀ {α : Type u_6} {T : TopologicalSpace α} {σ : Type u_5} {F : Ctop α σ} {eq : F.toTopsp = T} {σ_1 : Type u_5}
  {F_1 : Ctop α σ_1} {eq_1 : F_1.toTopsp = T},
  { σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 } → σ = σ_1 ∧ F ≍ F_1
-- Mathlib.Data.Part
Part.toOption_eq_none : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], o.toOption = none ↔ ¬o.Dom
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (app : (X : C) → F.obj X ⟶ G.obj X) →
            autoParam
                (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                  CategoryTheory.CategoryStruct.comp (F.map f) (app Y) =
                    CategoryTheory.CategoryStruct.comp (app X) (G.map f))
                CategoryTheory.NatTrans.naturality._autoParam →
              CategoryTheory.NatTrans F G
-- Std.Data.HashMap.Lemmas
Std.HashMap.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ext_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Trident.ext._auto_1),
  (CategoryTheory.Limits.Trident.ext i w).hom = CategoryTheory.Limits.Trident.mkHom i.hom w
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.comap_prod_swap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel γ δ) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  ((ProbabilityTheory.Kernel.prodMkRight α η).prod (ProbabilityTheory.Kernel.prodMkLeft γ κ)).comap Prod.swap ⋯ =
    ((ProbabilityTheory.Kernel.prodMkRight γ κ).prod (ProbabilityTheory.Kernel.prodMkLeft α η)).map Prod.swap
-- Mathlib.Data.Set.Restrict
/-- Reverse of `Set.codRestrict_domRestrict`.  -/
Set.MapsTo.restrict_eq_codRestrict : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
  Set.MapsTo.restrict f s t h = Set.codRestrict (s.domRestrict f) t ⋯
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.ext_iff : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ},
  f = g ↔ f.toLinearMap = g.toLinearMap
-- Mathlib.Algebra.Polynomial.Cardinal
Polynomial.cardinalMk_le_max : ∀ {R : Type u} [inst : Semiring R], Cardinal.mk (Polynomial R) ≤ max (Cardinal.mk R) Cardinal.aleph0
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.truncate.eq_def : ∀ {F : PFunctor.{uA, uB}} (x : ℕ) (x_1 : PFunctor.Approx.CofixA F (x + 1)),
  PFunctor.Approx.truncate x_1 =
    match x, x_1 with
    | 0, PFunctor.Approx.CofixA.intro a a_1 => PFunctor.Approx.CofixA.continue
    | a.succ, PFunctor.Approx.CofixA.intro i f => PFunctor.Approx.CofixA.intro i (PFunctor.Approx.truncate ∘ f)
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.normSimpContext : Aesop.NormM.Context → Aesop.NormSimpContext
-- Mathlib.Topology.DiscreteQuotient
/-- **Alias** of `DiscreteQuotient.isClopen_setOfPred_rel`. -/
DiscreteQuotient.isClopen_setOf_rel : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x : X), IsClopen (Set.ofPred (S.toSetoid x))
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- `Completion.toCompletion` as an isometry equivalence onto the underlying completion.  -/
NumberField.InfinitePlace.Completion.isometryEquivCompletion : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → v.Completion ≃ᵢ (↑v).Completion
-- Mathlib.Algebra.Lie.Basic
/-- The inverse of a bijective morphism is a morphism.  -/
LieHom.inverse : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] →
            [inst_3 : LieRing L₂] →
              [inst_4 : LieAlgebra R L₂] →
                (f : L₁ →ₗ⁅R⁆ L₂) → (g : L₂ → L₁) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → L₂ →ₗ⁅R⁆ L₁
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool},
  (Std.ExtTreeSet.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
-- Mathlib.Analysis.Normed.Group.Defs
AddGroupNorm.toNormedAddCommGroup.eq_1 : ∀ {E : Type u_5} [inst : AddCommGroup E] (f : AddGroupNorm E),
  f.toNormedAddCommGroup =
    { toNorm := f.toNormedAddGroup.toNorm, toAddGroup := f.toNormedAddGroup.toAddGroup, add_comm := ⋯,
      toMetricSpace := f.toNormedAddGroup.toMetricSpace, dist_eq := ⋯ }
-- Init.Data.List.MinMaxIdx
List.getElem_get_maxIdxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : (List.maxIdxOn? f xs).isSome = true), xs[(List.maxIdxOn? f xs).get h] = List.maxOn f xs ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.ιPi_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right] (a : J.L),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I)
      (CategoryTheory.Limits.Pi.π I.left a) =
    CategoryTheory.Limits.Multiequalizer.ι I a
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.derivative'.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R],
  Polynomial.derivative' =
    { toFun := ⇑Polynomial.derivative, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
-- Init.Sym.Lemmas
Lean.Sym.and_eq_left : ∀ (a b : Prop), a = True → (a ∧ b) = b
-- Mathlib.Order.Interval.Set.Image
Monotone.image_Icc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  Monotone f → f '' Set.Icc a b ⊆ Set.Icc (f a) (f b)
-- Mathlib.Order.Hom.Lattice
LatticeHom.snd_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (x : α × β), LatticeHom.snd x = x.2
-- Mathlib.ModelTheory.Order
/-- The theory of dense linear orders without endpoints.  -/
FirstOrder.Language.dlo : (L : FirstOrder.Language) → [L.IsOrdered] → L.Theory
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The underlying map of `Proj ℬ ⟶ Proj 𝒜` on the level of sheafed spaces.  -/
AlgebraicGeometry.Proj.sheafedSpaceMap : {A B σ τ : Type u} →
  [inst : CommRing A] →
    [inst_1 : SetLike σ A] →
      [inst_2 : AddSubgroupClass σ A] →
        [inst_3 : CommRing B] →
          [inst_4 : SetLike τ B] →
            [inst_5 : AddSubgroupClass τ B] →
              {𝒜 : ℕ → σ} →
                {ℬ : ℕ → τ} →
                  [inst_6 : GradedRing 𝒜] →
                    [inst_7 : GradedRing ℬ] →
                      (f : 𝒜 →+*ᵍ ℬ) →
                        HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                          (AlgebraicGeometry.Proj.toSheafedSpace ℬ ⟶ AlgebraicGeometry.Proj.toSheafedSpace 𝒜)
-- Mathlib.Data.Matrix.Basic
RingHom.mapMatrix_apply : ∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] (f : α →+* β) (M : Matrix m m α), f.mapMatrix M = M.map ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsShortNF.a₂ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsShortNF], W.a₂ = 0
-- Lean.Parser.Command
Lean.Parser.Command.printSig.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.counit]
  (X : D), h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)
-- Lean.Expr
/-- Given `a b : Int`, returns `a - b`  -/
Lean.mkIntSub : Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_emptyWithCapacity : ∀ {α : Type u} {c : ℕ}, (Std.HashSet.Raw.emptyWithCapacity c).size = 0
-- Mathlib.CategoryTheory.ObjectProperty.Local
/-- Given `W : MorphismProperty C`, this is the property of `W`-colocal objects, i.e.
the objects `X` such that for any `g : Y ⟶ Z` such that `W g` holds, the postcomposition
with `g` gives a bijection `(X ⟶ Y) ≃ (X ⟶ Z)`.
(See the file `Mathlib/CategoryTheory/Localization/Bousfield.lean` for the "dual" construction
`ObjectProperty.isColocal : ObjectProperty C → MorphismProperty C`.)  -/
CategoryTheory.MorphismProperty.isColocal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.ObjectProperty C
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.mk.injEq : ∀ (toCacheableParserContext : Lean.Parser.CacheableParserContext) (parserName : Lean.Name) (pos : String.Pos.Raw)
  (toCacheableParserContext_1 : Lean.Parser.CacheableParserContext) (parserName_1 : Lean.Name) (pos_1 : String.Pos.Raw),
  ({ toCacheableParserContext := toCacheableParserContext, parserName := parserName, pos := pos } =
      { toCacheableParserContext := toCacheableParserContext_1, parserName := parserName_1, pos := pos_1 }) =
    (toCacheableParserContext = toCacheableParserContext_1 ∧ parserName = parserName_1 ∧ pos = pos_1)
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_mul_gcd_iff_dvd_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {m n k : α}, k ∣ m * gcd k n ↔ k ∣ m * n
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instCommMonoid : {R : Type u_2} →
  [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → CommMonoid ↑(Set.Ioc 0 1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ y ∉ t, 1 ≤ ∏ x ∈ s with g x = y, f x) → ∏ y ∈ t, ∏ x ∈ s with g x = y, f x ≤ ∏ x ∈ s, f x
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.coeff_weierstrassPExceptSeries : ∀ (L : PeriodPair) (l₀ x : ℂ) (i : ℕ),
  (L.weierstrassPExceptSeries l₀ x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i l
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.integral_cos_pow_pos : ∀ (n : ℕ), 0 < ∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ n
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The `n`-th cyclotomic polynomial with coefficients in `R`.  -/
Polynomial.cyclotomic : ℕ → (R : Type u_1) → [inst : Ring R] → Polynomial R
-- Init.Simproc
/-- Auxiliary attribute for builtin simplification procedures.
 -/
Lean.Parser.Attr.simprocBuiltinAttr : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.contains k = false
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).inverse =
    CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α.inv
-- Mathlib.Data.List.Defs
/-- `findM tac l` returns the first element of `l` on which `tac` succeeds, and
fails otherwise.  -/
List.findM : {α : Type u} → {m : Type u → Type v} → [Alternative m] → (α → m PUnit.{u + 1}) → List α → m α
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_apply : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β) (a : WithTop α),
  e.withTopCongr a = WithTop.map (⇑e) a
-- Init.Data.Rat.Lemmas
Rat.not_le : ∀ {a b : ℚ}, ¬a ≤ b ↔ b < a
-- Mathlib.Analysis.Convex.Mul
ConvexOn.smul_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F},
  ConvexOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is strictly convex, then for any point `a` the slope of the secant line of `f`
through `a` and `b` is strictly monotone with respect to `b`.  -/
StrictConvexOn.secant_strict_mono : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f →
    ∀ {a x y : 𝕜}, a ∈ s → x ∈ s → y ∈ s → x ≠ a → y ≠ a → x < y → (f x - f a) / (x - a) < (f y - f a) / (y - a)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ),
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q =
    CategoryTheory.Limits.limit.π (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f n₀)
      (Opposite.op q)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.card_torsion_le_of_isSMulRegular : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) (n : ℕ), n ≠ 0 → IsSMulRegular 𝕜 n → {x | n • x = 0}.encard ≤ ↑n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCompletionIdentifier.beq : Lean.Lsp.CompletionIdentifier → Lean.Lsp.CompletionIdentifier → Bool
-- Mathlib.Control.Basic
/-- A `CommApplicative` functor `m` is a (lawful) applicative functor which behaves identically on
`α × β` and `β × α`, so computations can occur in either order.  -/
CommApplicative : (m : Type u → Type v) → [Applicative m] → Prop
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq.induct_unfolding : ∀ (motive : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Prop),
  (∀ (x : Lean.Grind.AC.Var), motive (Lean.Grind.AC.Expr.var x) (Lean.Grind.AC.Seq.var x)) →
    (∀ (a b : Lean.Grind.AC.Expr), motive b b.toSeq → motive (a.op b) (a.toSeq' b.toSeq)) →
      ∀ (e : Lean.Grind.AC.Expr), motive e e.toSeq
-- Mathlib.Combinatorics.Digraph.Basic
/-- The empty digraph on a type `V` (denoted by `⊥`)
is the digraph such that no pairs of vertices are adjacent.
Note that `⊥` is called the empty digraph because it has no edges.
 -/
Digraph.emptyDigraph : (V : Type u_1) → Digraph V
-- Mathlib.CategoryTheory.Category.Cat.AsSmall
CategoryTheory.Cat.asSmallFunctor_obj : ∀ (C : CategoryTheory.Cat), CategoryTheory.Cat.asSmallFunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.AsSmall ↑C)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_toIocDiv_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b + toIocDiv hp a b • p = b
-- Mathlib.GroupTheory.Nilpotent
/-- Any descending central series for an additive group is bounded below by the lower
central series.  -/
AddSubgroup.descending_central_series_ge_lower : ∀ {G : Type u_1} [inst : AddGroup G] (H : ℕ → AddSubgroup G),
  AddSubgroup.IsDescendingCentralSeries H → ∀ (n : ℕ), ⊤.lowerCentralSeries n ≤ H n
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.hasSum_e2Summand_symmetricIco : ∀ (z : UpperHalfPlane),
  HasSum (fun x => EisensteinSeries.e2Summand x z)
    (2 * riemannZeta 2 -
      8 * ↑Real.pi ^ 2 *
        ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n)
    (SummationFilter.symmetricIco ℤ)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.bijective_leftHomotopyClassToHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y], Function.Bijective (HomotopicalAlgebra.leftHomotopyClassToHom L)
-- Mathlib.FieldTheory.Perfect
Function.Semiconj.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (ga : α → α) (gb : β → β),
  Function.Semiconj f ga gb = ∀ (x : α), f (ga x) = gb (f x)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGE? k = t₂.getKeyGE? k
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f) (F.obj.map g.op) =
    CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (CategoryTheory.CategoryStruct.comp (G.map g) f)
-- Mathlib.Data.Finset.Prod
/-- See also `Finset.sup_product_left`.  -/
Finset.product_biUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq γ] (s : Finset α) (t : Finset β)
  (f : α × β → Finset γ), (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The `positivity` extension which identifies expressions of the form `abv a`.
For performance reasons, we only attempt to apply this when `abv` is a variable.
If it is an explicit function, e.g. `|_|` or `‖_‖`, another extension should apply.  -/
IsAbsoluteValue.Mathlib.Meta.Positivity.evalAbv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tanh` is meromorphic.  -/
Complex.meromorphic_tanh : Meromorphic Complex.tanh
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `C` has colimits and `G` preserves colimits, then if `G` reflects isomorphisms then it reflects
colimits.
 -/
CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasColimitsOfSize.{w', w, v₁, u₁} C]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G
-- Mathlib.Algebra.MvPolynomial.Basic
IsRegular.monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {m : σ →₀ ℕ} {a : R},
  IsRegular a → IsRegular ((MvPolynomial.monomial m) a)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_dist_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y x' y' : α), dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'
-- Plausible.Sampleable
Plausible.Sum.SampleableExt : {α : Type u_1} →
  {β : Type u_2} → [Plausible.SampleableExt α] → [Plausible.SampleableExt β] → Plausible.SampleableExt (α ⊕ β)
-- Mathlib.RingTheory.PowerSeries.Trunc
_private.Mathlib.RingTheory.PowerSeries.Trunc.0.PowerSeries.truncAux : {R : Type u_1} → [inst : Semiring R] → ℕ → PowerSeries R → Polynomial R
-- Std.Data.ByteSlice
ByteSlice.instEmptyCollection : EmptyCollection ByteSlice
-- Mathlib.Algebra.Category.Grp.Adjunctions
CommMonCat.val_units_map_hom_apply : ∀ {X Y : CommMonCat} (f : X ⟶ Y) (u : (↑X)ˣ),
  ↑((CommGrpCat.Hom.hom (CommMonCat.units.map f)) u) = (CommMonCat.Hom.hom f) ↑u
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- The pushforward of `partialTraj κ a (a + 1)` along the the point at time `a + 1` is `κ a`.  -/
ProbabilityTheory.Kernel.map_partialTraj_succ_self : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ),
  ((ProbabilityTheory.Kernel.partialTraj κ a (a + 1)).map fun x => x ⟨a + 1, ⋯⟩) = κ a
-- Mathlib.NumberTheory.Transcendental.Liouville.Basic
Liouville.irrational : ∀ {x : ℝ}, Liouville x → Irrational x
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_univ : ∀ {α : Type u} {s : Set α} {l : Filter α}, s =ᶠ[l] Set.univ ↔ s ∈ l
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_le_index : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G),
  (interior U).Nonempty → MeasureTheory.Measure.haar.prehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.index ↑K ↑K₀)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis.contract_isBasis_sdiff_sdiff_of_subset`. -/
Matroid.IsBasis.contract_isBasis_diff_diff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → J ⊆ I → (M.contract J).IsBasis (I \ J) (X \ J)
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableOn_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R), DifferentiableOn 𝕜 (fun x => (Polynomial.aeval x) q) s
-- Mathlib.Condensed.Solid
/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^\solid`.  -/
Condensed.profiniteSolid : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor Profinite (CondensedMod R)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Filter the elements of a tree satisfying a predicate.

```
filter (fun x ↦ x < 3) {1, 2, 4} = {1, 2}
filter (fun x ↦ x > 5) {1, 2, 4} = ∅
```  -/
Ordnode.filter : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Ordnode α → Ordnode α
-- Mathlib.Topology.Order.LeftRightLim
/-- An antitone function is continuous to the right at a point if and only if its right limit
coincides with the value of the function.  -/
Antitone.continuousWithinAt_Ioi_iff_rightLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x