mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Regular.RegularSequence
/-- An alternate induction principle from `IsRegular.recIterModByRegular` where
we mod out by successive elements in both the module and the base ring. This is
useful for propagating certain properties of the initial `M`, e.g. faithfulness
or freeness, throughout the induction.  -/
RingTheory.Sequence.IsRegular.recIterModByRegularWithRing : {motive :
    (R : Type u) →
      [inst : CommRing R] →
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsRegular M rs → Sort u_7} →
  ((R : Type u) →
      [inst : CommRing R] →
        (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [inst_3 : Nontrivial M] → motive R M [] ⋯) →
    ({R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    (h1 : IsSMulRegular M r) →
                      (h2 :
                          RingTheory.Sequence.IsRegular (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
                        motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) h2 →
                          motive R M (r :: rs) ⋯) →
      {R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → (h : RingTheory.Sequence.IsRegular M rs) → motive R M rs h
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
/-- If one restricts a multivariate Gaussian measure indexed by a finite set `I` to
coordinates indexed by `J ⊆ I`, one obtains the multivariate Gaussian measure whose
covariance matrix is given by the corresponding submatrix.  -/
ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian : ∀ {ι : Type u_2} [inst : DecidableEq ι] {I J : Finset ι} {μ : EuclideanSpace ℝ ↥I} {S : Matrix ↥I ↥I ℝ},
  S.PosSemidef →
    ∀ (hJI : J ⊆ I),
      MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.restrict₂ hJI)) (ProbabilityTheory.multivariateGaussian μ S)
        (ProbabilityTheory.multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ)
          (S.submatrix (fun i => ⟨↑i, ⋯⟩) fun i => ⟨↑i, ⋯⟩))
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.monotone_retractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.retractClosure ≤ Q.retractClosure
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A pseudometric space induces a pseudoemetric space  -/
PseudoMetricSpace.toPseudoEMetricSpace : {α : Type u} → [PseudoMetricSpace α] → PseudoEMetricSpace α
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraidedObj_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C), (CategoryTheory.Center.ofBraidedObj X).fst = X
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.eq_1 : ∀ {α : Type u_1} [inst : LT α] (a : α), Order.IsPredPrelimit a = ∀ (b : α), ¬a ⋖ b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₁_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] (i : E.I₀),
  (CategoryTheory.PreZeroHypercover.pullback₁ f E).X i = CategoryTheory.Limits.pullback f (E.f i)
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- `NormedSpace.exp x` has explicit two-sided inverse `NormedSpace.exp (-x)`.  -/
NormedSpace.invertibleExpOfMemBall : {𝕂 : Type u_1} →
  {𝔸 : Type u_2} →
    [inst : NontriviallyNormedField 𝕂] →
      [inst_1 : NormedRing 𝔸] →
        [inst_2 : NormedAlgebra 𝕂 𝔸] →
          [CompleteSpace 𝔸] →
            [CharZero 𝕂] →
              {x : 𝔸} → x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius → Invertible (NormedSpace.exp x)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.kernel.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (a a_1 : X),
  a = a_1 → ∀ (a_2 a_3 : X), a_2 = a_3 → RKHS.kernel H a a_2 = RKHS.kernel H a_1 a_3
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_union_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε
-- Mathlib.Data.Rat.Lemmas
Rat.exists_eq_mul_div_num_and_eq_mul_div_den : ∀ (n : ℤ) {d : ℤ}, d ≠ 0 → ∃ c, n = c * (↑n / ↑d).num ∧ d = c * ↑(↑n / ↑d).den
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofHom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities], (CategoryTheory.MorphismProperty.RightFraction.ofHom W f).f = f
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- Suppose `f g : X ⟶ Y` where `X` is a reduced scheme and `Y` is a separated scheme.
Then `f = g` if `ι ≫ f = ι ≫ g` for some dominant `ι`.

Also see `ext_of_isDominant_of_isSeparated` for the general version over arbitrary bases.
 -/
AlgebraicGeometry.ext_of_isDominant : ∀ {W X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f g : X ⟶ Y} [Y.IsSeparated] (ι : W ⟶ X)
  [AlgebraicGeometry.IsDominant ι],
  CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g → f = g
-- Mathlib.RingTheory.Extension.Presentation.Basic
IsLocalization.Away.mvPolynomialQuotientEquiv.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  IsLocalization.Away.mvPolynomialQuotientEquiv S r = IsLocalization.Away.mvPolynomialQuotientEquiv S r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_filter_le_size : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool}, m.WF → (Std.HashMap.Raw.filter f m).size ≤ m.size
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.normalize_out : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : Associates α), normalize a.out = a.out
-- Mathlib.Algebra.CharP.Frobenius
/-- The Frobenius endomorphism commutes with any ring homomorphism.  -/
RingHom.frobenius_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (g : R →+* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p], g.comp (frobenius R p) = (frobenius S p).comp g
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The covariant functor `pt` from the category of locales to the category of
topological spaces, which sends a locale `L` to the topological space `PT L` of homomorphisms
from `L` to `Prop` and a locale homomorphism `f` to a continuous function between the spaces
of points.  -/
Locale.pt : CategoryTheory.Functor Locale TopCat
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.X_mul_pderiv_monomial : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ} {m : σ →₀ ℕ} {r : R},
  MvPolynomial.X i * (MvPolynomial.pderiv i) ((MvPolynomial.monomial m) r) = m i • (MvPolynomial.monomial m) r
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Associator for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Lax.OplaxTrans.associator : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H I : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) →
            (θ : G ⟶ H) →
              (ι : H ⟶ I) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅
                  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_comp_algebraMap : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R],
  MvPolynomial.constantCoeff.comp (algebraMap R (MvPolynomial σ R)) = RingHom.id R
-- Mathlib.SetTheory.ZFC.Class
Class.coe_empty : ↑∅ = ∅
-- Mathlib.RingTheory.Flat.Equalizer
AlgHom.tensorEqualizerEquiv_apply : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {A : Type u_4}
  {B : Type u_5} [inst_7 : CommRing A] [inst_8 : CommRing B] [inst_9 : Algebra R A] [inst_10 : Algebra R B]
  (f g : A →ₐ[R] B) [inst_11 : Module.Flat R T] (x : TensorProduct R T ↥(f.equalizer g)),
  (AlgHom.tensorEqualizerEquiv S T f g) x = (AlgHom.tensorEqualizer S T f g) x
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.iSup_biInf_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Frame α] {s : Set ι},
  s.Finite → ∀ {f : ι → ι' → α}, (∀ i ∈ s, Antitone (f i)) → ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.many1NoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Order.RelClasses
/-- The relation `r` is the nonstrict relation corresponding to the strict relation `s`.  -/
IsNonstrictStrictOrder.right_iff_left_not_left : ∀ {α : Type u_1} {r : semiOutParam (α → α → Prop)} {s : α → α → Prop} [self : IsNonstrictStrictOrder α r s] (a b : α),
  s a b ↔ r a b ∧ ¬r b a
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ici : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i),
  (Set.univ.pi fun i => Set.Ici (x i)) = Set.Ici x
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.isLocal_of_isMaximal_radical : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.radical.IsMaximal → I.IsLocal
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- an element in the index type  -/
CategoryTheory.SmallObject.FunctorObjIndex.i : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        {f : (i : I) → A i ⟶ B i} → {S X : C} → {πX : X ⟶ S} → CategoryTheory.SmallObject.FunctorObjIndex f πX → I
-- Mathlib.Algebra.Star.BigOperators
star_finsuppSum : ∀ {R : Type u_1} {ι : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : AddCommMonoid R] [inst_2 : StarAddMonoid R]
  (s : ι →₀ M) (f : ι → M → R), star (s.sum f) = s.sum fun i m => star f i m
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.mono : ∀ {α : Type u_1} {s : Set α} {D₁ D₂ : Set (Set α)} [inst : Preorder α],
  D₁ ⊆ D₂ → DirSupClosedOn D₂ s → DirSupClosedOn D₁ s
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapObjFunctorOppositeOpensCarrierTopIsSheafGrothendieckTopologyStructureSheaf : {R S : CommRingCat} →
  (f : R ⟶ S) →
    (p : PrimeSpectrum ↑R) →
      Algebra ↑R
        ↑(((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
                (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
            p)
-- Mathlib.Data.Sym.Sym2
Sym2.diagSet_compl_eq_fromRel_ne : ∀ {α : Type u_1}, Sym2.diagSetᶜ = Sym2.fromRel ⋯
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.ParserExtension.OLeanEntry.toEntry : Lean.Parser.ParserExtension.State →
  Lean.Parser.ParserExtension.OLeanEntry → Lean.ImportM Lean.Parser.ParserExtension.Entry
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The isomorphism `AddCircle T ≃ Ioc a (a + T)` whose inverse is the natural quotient map,
as an equivalence of measurable spaces.  -/
AddCircle.measurableEquivIoc : (T : ℝ) → [hT : Fact (0 < T)] → (a : ℝ) → AddCircle T ≃ᵐ ↑(Set.Ioc a (a + T))
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.RCond.eq_1 : ∀ {ι : Type u_2} (l : BoxIntegral.IntegrationParams) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  l.RCond r = (l.bRiemann = true → ∀ (x : ι → ℝ), r x = r 0)
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_intro_r : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop) (x y : l),
  Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.CompleteLattice.ofProp p) x) y =
    (p → Lean.Order.PartialOrder.rel x y)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.ringInverse_le_ringInverse : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  a ≤ b →
    autoParam (IsStrictlyPositive a) CStarAlgebra.ringInverse_le_ringInverse._auto_1 → Ring.inverse b ≤ Ring.inverse a
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure X}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (f : BoundedContinuousFunction X ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : X), f x ∂μs i) L) →
    ∀ (f : BoundedContinuousFunction X ℝ), Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given two finite disjoint sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` equals the
product of `f i` over `i ∈ s` times the product of `f i` over `i ∈ t`.  -/
finprod_mem_union : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  Disjoint s t →
    s.Finite → t.Finite → ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ioc_succ_top : ∀ {M : Type u_3} [inst : CommMonoid M] {a b : ℕ},
  a ≤ b → ∀ (f : ℕ → M), ∏ k ∈ Finset.Ioc a (b + 1), f k = (∏ k ∈ Finset.Ioc a b, f k) * f (b + 1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpIdIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Functor.mapGrpIdIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Grp.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapGrp.obj X).X) ⋯ ⋯) ⋯
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMapRingHom_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)),
  (LinearMap.prodMapRingHom R M M₂) f = f.1.prodMap f.2
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_sup_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α),
  (s.biUnion fun a => Finset.image (fun x => a ⊔ x) t) = s ⊻ t
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.mk.congr_simp : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
  (toLinearMap toLinearMap_1 : M →ₛₗ[σ] M₂) (e_toLinearMap : toLinearMap = toLinearMap_1) (invFun invFun_1 : M₂ → M)
  (e_invFun : invFun = invFun_1) (left_inv : Function.LeftInverse invFun toLinearMap.toFun)
  (right_inv : Function.RightInverse invFun toLinearMap.toFun),
  { toLinearMap := toLinearMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toLinearMap := toLinearMap_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_atTop_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → Filter.Tendsto (Real.logb b) Filter.atTop Filter.atBot
-- Mathlib.Analysis.Asymptotics.Defs
/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l`
(denoted as `u ~[l] v` in the `Asymptotics` namespace)
when `u x - v x = o(v x)` as `x` converges along `l`.  -/
Asymptotics.IsEquivalent : {α : Type u_1} → {E' : Type u_6} → [SeminormedAddCommGroup E'] → Filter α → (α → E') → (α → E') → Prop
-- Mathlib.Data.Num.Bitwise
SNum.instNeg : Neg SNum
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
in Cartan's formula, in the case where `f` has order zero at the origin.
 -/
ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_eq_zero : ∀ {f : ℂ → ℂ},
  meromorphicOrderAt f 0 = 0 →
    Real.circleAverage (fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖) 0 1 =
      ‖meromorphicTrailingCoeffAt f 0‖.posLog
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.subtype_linear : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [inst_4 : Nonempty ↥s], s.subtype.linear = s.direction.subtype
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_sup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
  Filter.Tendsto f (x₁ ⊔ x₂) y ↔ Filter.Tendsto f x₁ y ∧ Filter.Tendsto f x₂ y
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.next?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_one_or_self : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M) (a : α),
  s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a`.  -/
jacobiSym.mod_right : ∀ (a : ℤ) {b : ℕ}, Odd b → jacobiSym a b = jacobiSym a (b % (4 * a.natAbs))
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- The jump of `variationOnFromTo` on the right of a point is given by the distance between the
right limit and the value of the function.  -/
variationOnFromTo.rightLim_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_3} [inst_1 : PseudoMetricSpace E] [CompleteSpace E] {f : α → E}
  {a b : α},
  BoundedVariationOn f Set.univ →
    Function.rightLim (variationOnFromTo f Set.univ a) b =
      variationOnFromTo f Set.univ a b + dist (f b) (Function.rightLim f b)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In a canonically-ordered additive monoid, a sum bounds each of its terms.

See also `Finset.single_le_sum`.  -/
Finset.single_le_sum_of_canonicallyOrdered : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] {f : ι → M}
  {s : Finset ι} {i : ι}, i ∈ s → f i ≤ ∑ j ∈ s, f j
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBoundP?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut], (∃ x, t.upperBoundP? cut = some x) ↔ ∃ x ∈ t, cut x ≠ Ordering.gt
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr1Nil_lean : Coe Lean.Ident (Lean.TSyntax `rcasesPat)
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_of_sum_range_le : ∀ {f : ℕ → ℝ} {c : ℝ}, (∀ (n : ℕ), 0 ≤ f n) → (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → Summable f
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {A : Type u_1} [inst_1 : SeminormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A], ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf),
  hkf.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯) =
    CategoryTheory.CategoryStruct.comp S.toCycles (S.isoCyclesOfIsLimit hkf).inv
-- Mathlib.Algebra.BigOperators.Expect
/-- Average of a function over a finset. If the finset is empty, this is equal to zero.  -/
Finset.expect : {ι : Type u_1} → {M : Type u_4} → [inst : AddCommMonoid M] → [Module ℚ≥0 M] → Finset ι → (ι → M) → M
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
FirstOrder.Ring.genericPolyMap.eq_1 : ∀ {ι : Type u_1} {κ : Type u_2} (monoms : ι → Finset (κ →₀ ℕ)) (i : ι),
  FirstOrder.Ring.genericPolyMap monoms i =
    ∑ m ∈ (monoms i).attach, FreeCommRing.of (Sum.inl ⟨i, m⟩) * (↑m).prod fun j n => FreeCommRing.of (Sum.inr j) ^ n
-- Mathlib.GroupTheory.Sylow
Sylow.normal_of_normalizerCondition : ∀ {G : Type u} [inst : Group G],
  NormalizerCondition G → ∀ {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G), (↑P).Normal
-- Mathlib.Order.CompleteLattice.Basic
iInf_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β}, ⨅ x ∈ {b}, f x = f b
-- Mathlib.Data.Fintype.WithTopBot
instFintypeWithTop : {α : Type u_1} → [Fintype α] → Fintype (WithTop α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
NNReal.coe_real_pi : ↑NNReal.pi = Real.pi
-- Mathlib.Analysis.RCLike.Lemmas
FiniteDimensional.RCLike.properSpace_submodule : ∀ (K : Type u_1) {E : Type u_2} [inst : RCLike K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E]
  (S : Submodule K E) [FiniteDimensional K ↥S], ProperSpace ↥S
-- Mathlib.SetTheory.Cardinal.NatCard
/-- NB: `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_eq_zero_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Nat.card β = 0 → Nat.card α = 0
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.neZero' : ∀ {R : Type u_4} {ζ : R} [inst : CommRing R] [IsDomain R] {n : ℕ} [NeZero n], IsPrimitiveRoot ζ n → NeZero ↑n
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_indicatorConstLp : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s t : Set X} {μ : MeasureTheory.Measure X} [CompleteSpace E] {p : ENNReal},
  MeasurableSet s →
    ∀ (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) (e : E),
      ∫ (x : X) in s, ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = μ.real (t ∩ s) • e
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.degree_map_le : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  (Polynomial.map f p).degree ≤ p.degree
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filterMap f m) k =
    (Std.ExtDHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2
-- Init.Data.Vector.Lemmas
Vector.toList_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n}, (Vector.map f xs).toList = List.map f xs.toList