mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `Semiring` instance along a surjective function.  -/
Function.Surjective.semiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : Pow S ℕ] →
                    [inst_6 : NatCast S] →
                      [inst_7 : Semiring R] →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : R), f (x + y) = f x + f y) →
                              (∀ (x y : R), f (x * y) = f x * f y) →
                                (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                  (∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) → (∀ (n : ℕ), f ↑n = ↑n) → Semiring S
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.zero_testAgainstNN : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω],
  MeasureTheory.FiniteMeasure.testAgainstNN 0 = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile pat = pos ↔
    ¬String.Slice.Pattern.Model.RevMatchesAt pat pos ∨ String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos pos
-- Mathlib.Probability.Distributions.Gaussian.CharFun
ProbabilityTheory.gaussian_charFunDual_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : NormedSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure μ] {m : E} {f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ},
  f.toBilinForm.IsPosSemidef →
    (∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (↑(L m) * Complex.I - ↑((f L) L) / 2)) →
      m = ∫ (x : E), x ∂μ ∧ f = ProbabilityTheory.covarianceBilinDual μ
-- Init.Prelude
/-- **The axiom of choice**. `Nonempty α` is a proof that `α` has an element,
but the element itself is erased. The axiom `choice` supplies a particular
element of `α` given only this proof.

The textbook axiom of choice normally makes a family of choices all at once,
but that is implied from this formulation, because if `α : ι → Type` is a
family of types and `h : ∀ i, Nonempty (α i)` is a proof that they are all
nonempty, then `fun i => Classical.choice (h i) : ∀ i, α i` is a family of
chosen elements. This is actually a bit stronger than the ZFC choice axiom;
this is sometimes called "[global choice](https://en.wikipedia.org/wiki/Axiom_of_global_choice)".

In Lean, we use the axiom of choice to derive the law of excluded middle
(see `Classical.em`), so it will often show up in axiom listings where you
may not expect. You can use `#print axioms my_thm` to find out if a given
theorem depends on this or other axioms.

This axiom can be used to construct "data", but obviously there is no algorithm
to compute it, so Lean will require you to mark any definition that would
involve executing `Classical.choice` or other axioms as `noncomputable`, and
will not produce any executable code for such definitions.
 -/
Classical.choice : {α : Sort u} → Nonempty α → α
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly concave function `f` and positive weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` are all equal
(and in fact all equal to their center of mass w.r.t. `w`).  -/
StrictConcaveOn.map_sum_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.ext : ∀ {n : ℕ} {x y : OrderedFinpartition n}, x.length = y.length → x.partSize ≍ y.partSize → x.emb ≍ y.emb → x = y
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap_eq_swapTR.go : ∀ (α : Type u_1) (xs : List α) (i j : ℕ) (acc : Array α),
  List.swapTR.go (acc.toList ++ xs) xs i j acc = acc.toList ++ xs.swap i j
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsZeroApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsZeroApply (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_eq_zero_of_pos_iff : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜],
  0 < p → ∀ {x : 𝕜}, 0 < x → (↑x = 0 ↔ ∃ n, n • p = x)
-- Mathlib.SetTheory.Ordinal.Basic
/-- `Quotient.inductionOn₂` specialized to ordinals.

Not to be confused with well-founded induction `WellFoundedLT.induction`.  -/
Ordinal.inductionOn₂ : ∀ {motive : Ordinal.{u_1} → Ordinal.{u_2} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}),
  (∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop)
      [inst_1 : IsWellOrder β s], motive (Ordinal.type r) (Ordinal.type s)) →
    motive o₁ o₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_sub_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ a c → ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..c, f x ∂μ = ∫ (x : ℝ) in c..b, f x ∂μ
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.discriminant_mul_discriminantEquiv_apply : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (z : UpperHalfPlane),
  ModularForm.discriminant z * (CuspForm.discriminantEquiv f) z = f z
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- The univariate `X : R⟦X⟧` can be substituted in power series

This lemma is added because `simp` doesn't find it from `HasSubst.X`.  -/
PowerSeries.HasSubst.X' : ∀ {R : Type u_2} [inst : CommRing R], PowerSeries.HasSubst PowerSeries.X
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_subset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- The canonical maps `P.obj (op (p.obj U)) ⟶ (ofIsCofiltered p hp).presheafFiber.obj P`
that are part of the colimit cocone `presheafFiberOfIsCofilteredCocone`.  -/
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          (p : CategoryTheory.Functor N C) →
            [inst_3 : CategoryTheory.InitiallySmall N] →
              {J : CategoryTheory.GrothendieckTopology C} →
                [inst_4 : CategoryTheory.IsCofiltered N] →
                  (hp :
                      ∀ ⦃X : C⦄,
                        ∀ R ∈ J X,
                          ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
                            ∃ Y g,
                              ∃ (_ : R.arrows g),
                                ∃ V q a,
                                  CategoryTheory.CategoryStruct.comp a g =
                                    CategoryTheory.CategoryStruct.comp (p.map q) f) →
                    {A : Type u''} →
                      [inst_5 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (U : N) →
                            (P : CategoryTheory.Functor Cᵒᵖ A) →
                              P.obj (Opposite.op (p.obj U)) ⟶
                                (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.ediv_eq_zero_of_lt_abs : ∀ {a b : ℤ}, 0 ≤ a → a < |b| → a / b = 0
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom))
        (CategoryTheory.ChosenPullbacksAlong.fst S.hom T.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom)
-- Mathlib.GroupTheory.Focal
Subgroup.focalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G),
  H.focalSubgroup = Subgroup.closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
-- Batteries.Data.List.Perm
List.Subperm.count_le : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α}, l₁.Subperm l₂ → ∀ (a : α), List.count a l₁ ≤ List.count a l₂
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_uIoc : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.uIoc i j = Set.uIoc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.CategoryTheory.Comma.Basic
/-- A natural transformation `R₁ ⟶ R₂` induces a functor `Comma L R₁ ⥤ Comma L R₂`.  -/
CategoryTheory.Comma.mapRight : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              {R₁ R₂ : CategoryTheory.Functor B T} →
                (R₂ ⟶ R₁) → CategoryTheory.Functor (CategoryTheory.Comma L R₂) (CategoryTheory.Comma L R₁)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty,
it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨅ i, f i`.  -/
Real.iInf_nonneg : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ iInf f
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.refl.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G),
  GroupExtension.Equiv.refl S = { toMulEquiv := MulEquiv.refl E, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntUInt64UintOfNatNat : Lean.Grind.ToInt UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.Data.Finset.Lattice.Fold
map_finset_inf : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
  [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β] [inst_4 : FunLike F α β] [InfTopHomClass F α β] (f : F)
  (s : Finset ι) (g : ι → α), f (s.inf g) = s.inf (⇑f ∘ g)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_prod_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' : Type u_14}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_15} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} (f : M → M' × N'), MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.comap_bracket_incl : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  {I₁ I₂ : LieIdeal R L}, ⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.image_ofSnowflaking_closedEBall`. -/
Metric.Snowflaking.image_ofSnowflaking_emetricClosedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking '' Metric.closedEBall x d =
    Metric.closedEBall (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
/-- A simplicial set is finite if it has finitely many nondegenerate simplices.  -/
SSet.Finite : SSet → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.sin` is complex analytic.  -/
Complex.analyticAt_sin : ∀ {x : ℂ}, AnalyticAt ℂ Complex.sin x
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_of_tendsto_atBot : ∀ {x : ℝ*} (r : ℝ), Filter.Germ.Tendsto x Filter.atBot → x < ↑r
-- Std.Async.Basic
/-- Block until the `ETask` in `x` finishes and returns its value. Propagates any error encountered
during execution.
 -/
Std.Async.ETask.block : {ε α : Type} → Std.Async.ETask ε α → EIO ε α
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.get! : Lean.Parser.SyntaxStack → ℕ → Lean.Syntax
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.principal_units_le_units : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.principalUnitGroup ≤ A.unitGroup
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity from scaled pairwise positive distance. Backward of
`similar_iff_exists_pos_pairwise_dist_eq`.  -/
Similar.of_exists_pos_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, 0 < r ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.continuous_totalSpaceMk : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  (x : B), Continuous (Bundle.TotalSpace.mk x)
-- Init.Data.Array.Attach
Array.countP_attachWith : ∀ {α : Type u_1} {p : α → Prop} {q : α → Bool} {xs : Array α} {H : ∀ a ∈ xs, p a},
  Array.countP (fun a => q ↑a) (xs.attachWith p H) = Array.countP q xs
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.context.injEq : ∀ (i : Lean.Elab.PartialContextInfo) (t : Lean.Elab.InfoTree) (i_1 : Lean.Elab.PartialContextInfo)
  (t_1 : Lean.Elab.InfoTree),
  (Lean.Elab.InfoTree.context i t = Lean.Elab.InfoTree.context i_1 t_1) = (i = i_1 ∧ t = t_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α) (n : ℕ), ↑(s ^ n) = ↑s ^ n
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
(mulVecᵣ_eq _ _).symm
```
 -/
Matrix.mulVecᵣ_eq : ∀ {l m : ℕ} {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α),
  A.mulVecᵣ v = A.mulVec v
-- Mathlib.Data.EReal.Operations
/-- For any extended real number `x` which is not `⊥`, the sum of `x` and `⊤` is equal to `⊤`.  -/
EReal.add_top_of_ne_bot : ∀ {x : EReal}, x ≠ ⊥ → x + ⊤ = ⊤
-- Init.Data.UInt.Lemmas
UInt32.mod_eq_of_lt : ∀ {a b : UInt32}, a < b → a % b = a
-- Init.Control.Lawful.Basic
pure_unit_seqLeft : ∀ {f : Type → Type u_1} [inst : Applicative f] [LawfulApplicative f] (x : f Unit), pure () <* x = x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.iInf_le_lintegral : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  (f : α → ENNReal), ⨅ x, f x ≤ ∫⁻ (x : α), f x ∂μ
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * 2^-n`, then the distance from
`f 0` to the limit of `f` is bounded above by `2 * C`.  -/
edist_le_of_edist_le_geometric_two_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α},
  (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ 2 * C
-- Init.Data.Range.Basic
Std.Legacy.Range.«term[:_]» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.isClosedImmersion_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.SurjectiveOnStalks f ∧ Topology.IsClosedEmbedding ⇑f
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.FiniteRel : {α β : Type w} →
  (m : Type w → Type w') →
    [inst : Std.Iterator α m β] → [Std.Iterators.Finite α m] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd.mk : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Add M],
  autoParam (∀ (c : M), Measurable fun x => c + x) MeasurableAdd.measurable_const_add._autoParam →
    autoParam (∀ (c : M), Measurable fun x => x + c) MeasurableAdd.measurable_add_const._autoParam → MeasurableAdd M
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic value of an integer `z ≠ 0` is its `p`-adic value as a rational.  -/
padicValRat.of_nat : ∀ {p n : ℕ}, padicValRat p ↑n = ↑(padicValNat p n)
-- Mathlib.Algebra.Module.SpanRank
/-- The span of the generators equals the submodule.  -/
Submodule.span_generators : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  Submodule.span R p.generators = p
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_inv_cancel_left'` for a stronger version.  -/
ENNReal.mul_inv_cancel_left : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * (a⁻¹ * b) = b
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens : ∀ {X : AlgebraicGeometry.Scheme}, QuasiSeparatedSpace ↥X ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_set_normalizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G} {g : G},
  g ∈ AddSubgroup.normalizer S ↔ ∀ (h : G), h ∈ S ↔ g + h + -g ∈ S
-- Mathlib.Tactic.Ring.Common
/-- A proof that the original expression is equal to the normalized result.  -/
Mathlib.Tactic.Ring.Common.Result.proof : {u : Lean.Level} →
  {α : Q(Type u)} →
    {E : Q(«$α») → Type u_1} → {e : Q(«$α»)} → (self : Mathlib.Tactic.Ring.Common.Result E e) → Q(«$e» = unknown_1)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Given an adjunction `F ⊣ G`, the functor that associates to an algebra over `F` a
coalgebra over `G` defined via adjunction applied to the structure map.  -/
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ⊣ G) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Algebra F) (CategoryTheory.Endofunctor.Coalgebra G)
-- Mathlib.Algebra.Ring.Action.Invariant
IsInvariantSubring.toMulSemiringAction : (M : Type u_1) →
  {R : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : Ring R] →
        [inst_2 : MulSemiringAction M R] → (S : Subring R) → [IsInvariantSubring M S] → MulSemiringAction M ↥S
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.binaryProductLimitCone_cone_π_app_left : ∀ (G H : AddCommGrpCat),
  (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } =
    AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_sumInr : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q' : M'}, mfderiv% Sum.inr q' = ContinuousLinearMap.id 𝕜 (TangentSpace I q')
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : SizeOf R] (toSubsemiring : Subsemiring R)
  (eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0),
  sizeOf { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
    1 + sizeOf toSubsemiring
-- Mathlib.Algebra.Module.Torsion.Free
smul_ne_zero_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r • m ≠ 0 ↔ r ≠ 0 ∧ m ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `BraidedCategory` instance on `Center C`.  -/
CategoryTheory.Center.braiding : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : CategoryTheory.Center C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X
-- Mathlib.Data.List.Pi
List.Pi.nil.congr_simp : ∀ {ι : Type u_1} (α : ι → Sort u_3) (i : ι) (a : i ∈ []), List.Pi.nil α i a = List.Pi.nil α i a
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_inter_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iio a ∩ Set.Ioi b = Set.Ioo b a
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- Upper bound for the summand `|c * z + d| ^ (-k)`, as a product of a function of `z` and a
function of `c, d`.  -/
EisensteinSeries.summand_bound : ∀ (z : UpperHalfPlane) {k : ℝ},
  0 ≤ k → ∀ (x : Fin 2 → ℤ), ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ EisensteinSeries.r z ^ (-k) * ‖x‖ ^ (-k)
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.AEStronglyMeasurable.integral_condKernel : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E],
  MeasureTheory.AEStronglyMeasurable f ρ →
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
-- Lean.Parser.Types
Lean.Parser.instBEqError.beq : Lean.Parser.Error → Lean.Parser.Error → Bool
-- Mathlib.GroupTheory.PresentedGroup
/-- The canonical map from the free group on `α` to a presented group with generators `x : α`,
where `x` is mapped to its equivalence class under the given set of relations `rels`  -/
PresentedGroup.mk : {α : Type u_1} → (rels : Set (FreeGroup α)) → FreeGroup α →* PresentedGroup rels
-- Init.Data.Bool
Bool.bne_self_left : ∀ (a b : Bool), (a != (a != b)) = b
-- Mathlib.Logic.Equiv.Prod
Equiv.punitProd_apply : ∀ (α : Type u_9) (a : PUnit.{u_10 + 1} × α), (Equiv.punitProd α) a = a.2
-- Init.Data.SInt.Lemmas
ISize.ofNat_toNatClampNeg : ∀ (x : ISize), 0 ≤ x → ISize.ofNat x.toNatClampNeg = x