mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.add : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} {s : Set X}
  [ContinuousAdd ε''] {f g : X → ε''},
  MeasureTheory.LocallyIntegrableOn f s μ →
    MeasureTheory.LocallyIntegrableOn g s μ → MeasureTheory.LocallyIntegrableOn (f + g) s μ
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The L-series of the von Mangoldt function restricted to the residue class `a` mod `q`
with `a` invertible in `ZMod q` is a linear combination of logarithmic derivatives of
L-functions of the Dirichlet characters mod `q` (on `re s > 1`).  -/
ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq : ∀ {q : ℕ} {a : ZMod q} [inst : NeZero q],
  IsUnit a →
    ∀ {s : ℂ},
      1 < s.re →
        LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt.residueClass a n)) s =
          -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_centralizer_iff : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {s : Set A} {z : A},
  z ∈ StarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_eq_one_iff : ∀ (x : ENNReal), x.toReal = 1 ↔ x = 1
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.IsTriangularizable.exists_hasEigenvalue : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [Nontrivial M]
  [LieModule.IsTriangularizable R L M] (x : L), ∃ φ, ((LieModule.toEnd R L M) x).HasEigenvalue φ
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.nonDependentFirst.sizeOf_spec : sizeOf Lean.Meta.ApplyNewGoals.nonDependentFirst = 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.StackEntry.expr.sizeOf_spec : ∀ (info : Lean.Meta.RefinedDiscrTree.ExprInfo),
  sizeOf (Lean.Meta.RefinedDiscrTree.StackEntry.expr info) = 1 + sizeOf info
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology map `S₁.homology ⟶ S₂.homology` induced by a morphism
`S₁ ⟶ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.homologyMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → [inst_2 : S₁.HasHomology] → [inst_3 : S₂.HasHomology] → S₁.homology ⟶ S₂.homology
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- A natural transformation between (lax) monoidal functors is monoidal if it satisfies
`ε F ≫ τ.app (𝟙_ C) = ε G` and `μ F X Y ≫ app (X ⊗ Y) = (app X ⊗ₘ app Y) ≫ μ G X Y`.  -/
CategoryTheory.NatTrans.IsMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F₁ F₂ : CategoryTheory.Functor C D} → (F₁ ⟶ F₂) → [F₁.LaxMonoidal] → [F₂.LaxMonoidal] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inl f g) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.empty : ∀ {α : Type u_1} (M : Matroid α), M.IsRkFinite ∅
-- Mathlib.RingTheory.Etale.Kaehler
/-- If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`.  -/
Algebra.Extension.tensorCotangent : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  {P : Algebra.Extension R S} →
                    {Q : Algebra.Extension R T} →
                      (f : P.Hom Q) →
                        [alg : Algebra P.Ring Q.Ring] →
                          (halg : algebraMap P.Ring Q.Ring = f.toRingHom) →
                            Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) →
                              TensorProduct S T P.Cotangent ≃ₗ[T] Q.Cotangent
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_lt_max_of_mul_lt_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] {a b c d : α} [MulLeftMono α] [MulRightMono α],
  a * b < c * d → min a b < max c d
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.primitiveRoots_one : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R], primitiveRoots 1 R = {1}
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lie_of : ∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] [inst_1 : DecidableEq ι] {i j : ι} (x : L i) (y : L j),
  ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = if hij : i = j then (DirectSum.of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
-- Mathlib.Data.List.Sym
List.mem_sym2_cons_iff : ∀ {α : Type u_1} {x : α} {xs : List α} {z : Sym2 α},
  z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
-- Init.Data.SInt.Bitwise
Int16.not_or_self : ∀ {a : Int16}, ~~~a ||| a = -1
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The type of natural transformations `shrinkYoneda.{w}.obj X ⟶ P`
with `X : C` and `P : Cᵒᵖ ⥤ Type w` is equivalent to `P.obj (op X)`.  -/
CategoryTheory.shrinkYonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {X : C} →
        {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
          (CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) ≃ P.obj (Opposite.op X)
-- Std.Http.Data.Response
/-- Inserts a typed extension value into the response being built.
 -/
Std.Http.Response.Builder.extension : {α : Type u_1} → Std.Http.Response.Builder → [TypeName α] → α → Std.Http.Response.Builder
-- Mathlib.Order.Closure
ClosureOperator.id_isClosed : ∀ (α : Type u_1) [inst : Preorder α] (x : α), (ClosureOperator.id α).IsClosed x = True
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The degree-sum formula for bipartite graphs, summing over the "right" part.

See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and
`SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges` for the version from the "left".  -/
SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges' : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.IsBipartiteWith ↑s ↑t → ∑ v ∈ t, G.degree v = G.edgeFinset.card
-- Std.Do.PostCond
Std.Do.PostShape.arg.injEq : ∀ (σ : Type u) (a : Std.Do.PostShape) (σ_1 : Type u) (a_1 : Std.Do.PostShape),
  (Std.Do.PostShape.arg σ a = Std.Do.PostShape.arg σ_1 a_1) = (σ = σ_1 ∧ a = a_1)
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- If `b` is an `R`-basis of `S` of cardinality `n`, then `normBound abv b` is an integer
such that for every `R`-integral element `a : S` with coordinates `≤ y`,
we have `Algebra.norm a ≤ normBound abv b * y ^ n`. (See also `norm_le` and `norm_lt`).  -/
ClassGroup.normBound : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [IsDomain S] →
          [inst_3 : Algebra R S] →
            AbsoluteValue R ℤ → {ι : Type u_5} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R S → ℤ
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The constant function with value `x : ℂ` as a modular form of weight 0 and any level.  -/
ModularForm.constℝ : {Γ : Subgroup (GL (Fin 2) ℝ)} → ℝ → [Γ.HasDetPlusMinusOne] → ModularForm Γ 0
-- Lean.Meta.Tactic.CasesOnStuckLHS
Lean.Meta.casesOnStuckLHS? : Lean.MVarId → Lean.MetaM (Option (Array Lean.MVarId))
-- Mathlib.Analysis.Convex.Basic
Monotone.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix.mk.sizeOf_spec : ∀ {n m : ℕ} (data : Array (Array ℚ)), sizeOf { data := data } = 1 + sizeOf data
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn'_eq : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n]
  [hl : Std.LawfulIteratorLoop α m n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : Std.IterM m β}
  {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)},
  forIn' it init f =
    Std.IterM.DefaultConsumers.forIn' (fun x x_1 f x_2 => monadLift x_2 >>= f) γ (fun x x_1 x_2 => True) it init
      it.IsPlausibleIndirectOutput ⋯ fun x1 x2 x3 => do
      let __do_lift ← f x1 x2 x3
      pure ⟨__do_lift, trivial⟩
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a right absorbing element for multiplication  -/
NonUnitalNonAssocRing.mul_zero : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a : α), a * 0 = 0
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_add_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (f : α → ENNReal),
  (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f
-- Aesop.Search.Queue
Aesop.LIFOQueue.instQueue : Aesop.Queue Aesop.LIFOQueue
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 g s x → DifferentiableWithinAt 𝕜 (f - g) s x
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_of_comm : ∀ {G : Type u_3} [hG : Group G], (∀ (a b : G), a * b = b * a) → Group.IsSolvable G
-- Mathlib.Order.SupClosed
InfClosed.preimage : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {s : Set α}
  [inst_2 : FunLike F β α] [InfHomClass F β α], InfClosed s → ∀ (f : F), InfClosed (⇑f ⁻¹' s)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v)))
  (x : F.Elementsᵒᵖ),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).functor.obj x =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.le_adjoinNegOne : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] (𝒢 : Subgroup (GL n R)),
  𝒢 ≤ 𝒢.adjoinNegOne
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- An open embedding of `X` into `Y`, with `X` nonempty, defines an open partial homeomorphism
whose source is all of `X`. The converse is also true; see
`OpenPartialHomeomorph.isOpenEmbedding`.  -/
Topology.IsOpenEmbedding.toOpenPartialHomeomorph : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (f : X → Y) → Topology.IsOpenEmbedding f → [Nonempty X] → OpenPartialHomeomorph X Y
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_bot_of_isLocalized₀_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_5 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M},
      (∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊥) → N = ⊥
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal : (M : Type u) → [Monoid M] → CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.prop_iterationFunctor_map_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (j : κ.ord.ToType),
  (CategoryTheory.SmallObject.succStruct I κ).prop
    ((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_rightUnitor : ∀ {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₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map U.rightUnitor.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U
          (CategoryTheory.Functor.id Y)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G Y).hom
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U))
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom)
-- Aesop.Forward.SlotIndex
Aesop.instDecidableEqSlotIndex.decEq : (x x_1 : Aesop.SlotIndex) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- The 1-cell dual bicategory `Bᵒᵖ`.

It is defined as follows.
* The objects of `Bᵒᵖ` correspond to objects of `B`.
* The morphisms `X ⟶ Y` in `Bᵒᵖ` are the morphisms `Y ⟶ X` in `B`.
* The 2-morphisms `f ⟶ g` in `Bᵒᵖ` are the 2-morphisms `f ⟶ g` in `B`. In other words, the
  directions of the 2-morphisms are preserved.
 -/
Bicategory.Opposite.bicategory : {B : Type u} → [CategoryTheory.Bicategory B] → CategoryTheory.Bicategory Bᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instLE : (ι : Type u_1) → LE (PreAbstractSimplicialComplex ι)
-- Init.GrindInstances.ToInt
Lean.Grind.instLTUInt64UintOfNatNat : Lean.Grind.ToInt.LT UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instOneTerm : {α : Type u_1} → One (FirstOrder.Language.presburger.Term α)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- A transfinite composition of shape `J` induces a transfinite composition
of shape `Set.Iic j` for any `j : J`.  -/
CategoryTheory.TransfiniteCompositionOfShape.iic : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (c : CategoryTheory.TransfiniteCompositionOfShape J f) →
                    (j : J) →
                      CategoryTheory.TransfiniteCompositionOfShape (↑(Set.Iic j)) (c.F.map (CategoryTheory.homOfLE ⋯))
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.inr_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  StrictMono ⇑(MonoidHom.inr α β)
-- Lean.Meta.Basic
/-- Given a monadic function `f` that takes a term and produces a new term,
lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
and then builds the lambda telescope term for the new term.
 -/
Lean.Meta.mapForallTelescope : (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Covering.Vitali
/-- The measurable **Vitali covering theorem**, filter version.

Assume one is given a family `t` of closed sets with nonempty interior, such that each `a ∈ t` is
included in a ball `B (x, r)` and covers a definite proportion of the ball `B (x, 3 r)` for a given
measure `μ` (think of the situation where `μ` is a doubling measure and `t` is a family of balls).
Consider a (possibly non-measurable) set `s` at which the family is fine, i.e., every point of `s`
belongs to arbitrarily small elements of `t`. Then one can extract from `t` a disjoint subfamily
that covers almost all `s`.

For more flexibility, we give a statement with a parameterized family of sets.
 -/
Vitali.exists_disjoint_covering_ae' : ∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α)
  (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α),
  (∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) →
    (∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)) →
      (∀ a ∈ t, (interior (B a)).Nonempty) →
        (∀ a ∈ t, IsClosed (B a)) →
          (∀ x ∈ s, ∃ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∃ a ∈ t, r a = ε ∧ c a = x) →
            ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
-- Mathlib.Topology.Category.TopCat.Limits.Konig
TopCat.partialSections.nonempty : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat)
  [CategoryTheory.IsCofilteredOrEmpty J] [h : ∀ (j : J), Nonempty ↑(F.obj j)] {G : Finset J}
  (H : Finset (TopCat.FiniteDiagramArrow✝ G)), (TopCat.partialSections F H).Nonempty
-- Lean.Meta.Check
Lean.Meta.checkProj : Lean.Name → ℕ → Lean.Expr → Lean.MetaM Unit
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray.congr_simp : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Roc α),
  r = r_1 → r.toArray = r_1.toArray
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.cosh_strictMonoOn : StrictMonoOn Real.cosh (Set.Ici 0)
-- Mathlib.Algebra.Polynomial.Sequence
/-- Make `S i` mean `S.elems' i`.  -/
Polynomial.Sequence.coeFun : {R : Type u_1} → [inst : Semiring R] → CoeFun (Polynomial.Sequence R) fun x => ℕ → Polynomial R
-- Lean.Declaration
Lean.InductiveVal.isRecEx : Lean.InductiveVal → Bool
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_apply : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁'),
  e.conj f = (↑e ∘ₛₗ f) ∘ₛₗ ↑e.symm
-- Mathlib.Algebra.Group.Action.Basic
AddAction.toFun_apply : ∀ {M : Type u_2} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (x : M) (y : α),
  (AddAction.toFun M α) y x = x +ᵥ y
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Restricting an open partial homeomorphism `e` to `e.source ∩ interior s`. We use the interior to
make sure that the restriction is well defined whatever the set s, since open partial homeomorphisms
are by definition defined on open sets. In applications where `s` is open, this coincides with the
restriction of partial equivalences.  -/
OpenPartialHomeomorph.restr : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → Set X → OpenPartialHomeomorph X Y
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rco_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + m → (m...n).toList.getD i fallback = fallback
-- Mathlib.NumberTheory.NumberField.CMField
/-- The kernel of `unitsMulComplexConjInv` is the subgroup of real units.
 -/
NumberField.IsCMField.unitsMulComplexConjInv_ker : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  (NumberField.IsCMField.unitsMulComplexConjInv K).ker = NumberField.IsCMField.realUnits K
-- Lean.Meta.Sym.SynthInstance
/-- Some modules in grind use builtin instances defined directly in core (e.g., `lia`).
Users may provide nonstandard instances that are definitionally equal to the ones in core.
Given a type, such as `HAdd Int Int Int`, this function returns the instance defined in
core.
 -/
Lean.Meta.Sym.getBuiltinInstance? : Lean.Expr → Option Lean.Expr
-- Batteries.Linter.UnnecessarySeqFocus
/-- Traverse the info tree down a given path.
Each `(n, i)` means that the array must have length `n` and we will descend into the `i`'th child.
 -/
Batteries.Linter.UnnecessarySeqFocus.getPath : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.sumElim_comp : ∀ {ι : Type u_1} {R : Type u_3} {S : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  {ι' : Type u_4} {x : ι → S} {y : ι' → A},
  AlgebraicIndependent R x → AlgebraicIndependent S y → AlgebraicIndependent R (Sum.elim y (⇑(algebraMap S A) ∘ x))
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vaddCommClass_left : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass M'] [inst_1 : VAdd M' β] [inst_2 : VAdd α β]
  [VAddCommClass M' α β] (S : AddSubmonoid M'), VAddCommClass (↥S) α β
-- Init.Data.String.Defs
String.utf8ByteSize_ofByteArray : ∀ {b : ByteArray} {h : b.IsValidUTF8}, { toByteArray := b, isValidUTF8 := h }.utf8ByteSize = b.size
-- Mathlib.Topology.Order
TopologicalSpace.not_indiscrete_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], ¬IndiscreteTopology α ↔ NontrivialTopology α
-- Mathlib.Topology.UniformSpace.Ascoli
/-- A version of the **Arzela-Ascoli theorem**.

Let `X, ι` be topological spaces, `𝔖` a covering of `X` by compact subsets, `α` a T2 uniform space,
`F : ι → (X → α)`, and `s` a subset of `ι`. Assume that:
* `F`, viewed as a function `ι → (X →ᵤ[𝔖] α)`, is a closed embedding (in other words, `ι`
  identifies to a closed subset of `X →ᵤ[𝔖] α` through `F`)
* `F '' s` is equicontinuous on each `K ∈ 𝔖`
* For all `x ∈ ⋃₀ 𝔖`, the image of `s` under `i ↦ F i x` is contained in some fixed compact subset.

Then `s` has compact closure in `ι`.  -/
ArzelaAscoli.isCompact_closure_of_isClosedEmbedding : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] [T2Space α] {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F) →
      ∀ {s : Set ι},
        (∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K) →
          (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) → IsCompact (closure s)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_zero_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (f : MvPolynomial σ R),
  (MvPolynomial.expand 0) f = MvPolynomial.C ((MvPolynomial.eval 1) f)