mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_indicator_const : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} [CompleteSpace E] (e : E) ⦃s : Set X⦄,
  MeasurableSet s → ∫ (x : X), s.indicator (fun x => e) x ∂μ = μ.real s • e
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₃] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {F₀₃ : CategoryTheory.Functor C₀ C₃} {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁}
  {G₃₂ : CategoryTheory.Functor C₃ C₂} {G₂₀ : CategoryTheory.Functor C₂ C₀} {G₃₀ : CategoryTheory.Functor C₃ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₀₃ : F₀₃ ⊣ G₃₀)
  (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) (τ₀₂₃ : G₃₀ ⟶ G₃₂.comp G₂₀),
  CategoryTheory.CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃)
        (adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃)) =
    (CategoryTheory.conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (CategoryTheory.CategoryStruct.comp τ₀₂₃
        (CategoryTheory.CategoryStruct.comp (G₃₂.whiskerLeft τ₀₁₂) (G₃₂.associator G₂₁ G₁₀).inv))
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g₁ g₂ : G →L[𝕜] H),
  TensorProduct.mapL f (g₁ + g₂) = TensorProduct.mapL f g₁ + TensorProduct.mapL f g₂
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_diagonal : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α] [inst_4 : Module R β]
  [inst_5 : DecidableEq n] (A : Matrix l m α) (b : n → β),
  Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) =
    Matrix.blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the right is constant,
expressed as a subtraction involving a `weightedVSubOfPoint` expression.  -/
Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ b : P),
  ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)
-- Mathlib.Topology.Algebra.Valued.WithVal
NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [inst_1 : Field K] (v : Valuation K Γ₀)
  (R : Type u_4) [inst_2 : CommRing R] [inst_3 : Algebra R K] [IsIntegralClosure R ℤ K],
  IsIntegralClosure R ℤ (WithVal v)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.hom_inv_id_eval_assoc : ∀ {C : Type u_1} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.GradedObject J C}
  (e : X ≅ Y) (j : J) {Z : C} (h : X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom j) (CategoryTheory.CategoryStruct.comp (e.inv j) h) = h
-- Mathlib.Topology.Inseparable
specializes_of_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x = y → x ⤳ y
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points is `C^n`.  -/
ContDiffAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G} {n : WithTop ℕ∞} (x : E),
  ContDiffAt 𝕜 n g (f x) → ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (g ∘ f) x
-- Mathlib.Topology.Category.TopCat.Basic
/-- The discrete topology on any type.  -/
TopCat.discrete : CategoryTheory.Functor (Type u) TopCat
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_injective : ∀ {α : Type u_1}, Function.Injective Multiset.powerset
-- Init.Data.Array.Attach
Array.unattach_flatten : ∀ {α : Type u_1} {p : α → Prop} {xs : Array (Array { x // p x })},
  xs.flatten.unattach = (Array.map Array.unattach xs).flatten
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] (u : M₀ˣ), ↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = ↑u⁻¹
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.zpow_left₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → ∀ (m : ℤ), Commute (a ^ m) b
-- Mathlib.Algebra.Order.Hom.TypeTags
Additive.instUniqueOrderAddMonoidIso : {G : Type u_1} →
  {H : Type u_2} →
    [inst : CommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : CommMonoid H] → [inst_3 : PartialOrder H] → [Unique (G ≃*o H)] → Unique (Additive G ≃+o Additive H)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed {s | (s ∩ F).Nonempty}
-- Mathlib.Algebra.Order.Kleene
/-- Pullback an `IdemSemiring` instance along an injective function.  -/
Function.Injective.idemSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : IdemSemiring α] →
      [inst_1 : LE β] →
        [inst_2 : LT β] →
          [inst_3 : Zero β] →
            [inst_4 : One β] →
              [inst_5 : Add β] →
                [inst_6 : Mul β] →
                  [inst_7 : Pow β ℕ] →
                    [inst_8 : SMul ℕ β] →
                      [inst_9 : NatCast β] →
                        [inst_10 : Max β] →
                          [inst_11 : Bot β] →
                            (f : β → α) →
                              Function.Injective f →
                                (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) →
                                  (∀ {x y : β}, f x < f y ↔ x < y) →
                                    f 0 = 0 →
                                      f 1 = 1 →
                                        (∀ (x y : β), f (x + y) = f x + f y) →
                                          (∀ (x y : β), f (x * y) = f x * f y) →
                                            (∀ (n : ℕ) (x : β), f (n • x) = n • f x) →
                                              (∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                (∀ (n : ℕ), f ↑n = ↑n) →
                                                  (∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) → f ⊥ = ⊥ → IdemSemiring β
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_mod : ∀ {a b : UInt8}, (a % b).toBitVec = a.toBitVec % b.toBitVec
-- Init.Data.UInt.Lemmas
UInt64.ofNat_size : UInt64.ofNat UInt64.size = 0
-- Mathlib.Topology.Algebra.GroupWithZero
continuousOn_zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  (m : ℤ), ContinuousOn (fun x => x ^ m) {0}ᶜ
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.pathCast.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] {x x' y y' : X} {p q : Path x y} (F : p.Homotopy q) (hx : x' = x)
  (hy : y' = y), F.pathCast hx hy = F
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `f'` and `f₁'` are two derivatives of `f` within `s` at `x`, then they are equal on the
tangent cone to `s` at `x`  -/
HasFDerivWithinAt.unique_on : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' f₁' : E →L[𝕜] F} {x : E} {s : Set E} [T2Space F],
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f₁' s x → Set.EqOn (⇑f') (⇑f₁') (tangentConeAt 𝕜 s x)
-- Init.Data.UInt.Bitwise
UInt32.ofNat_shiftLeft : ∀ (a b : ℕ), b < 32 → UInt32.ofNat (a <<< b) = UInt32.ofNat a <<< UInt32.ofNat b
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.HomotopyClass.eq_homotopyClass : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet}
  (x : SSet.RelativeMorphism.HomotopyClass A B φ), ∃ f, f.homotopyClass = x
-- Mathlib.Algebra.GradedMonoid
Mul.gMul : (ι : Type u_1) → {R : Type u_2} → [inst : Add ι] → [Mul R] → GradedMonoid.GMul fun x => R
-- Std.Async.System
Std.Async.System.instInhabitedSystemUser.default : Std.Async.System.SystemUser
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_pair : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (a b : Projectivization K V), Projectivization.IsCollinear {a, b}
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_natCast_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.lpNorm (fun x => ↑n * f x) p μ = ↑n * MeasureTheory.lpNorm f p μ
-- Mathlib.Probability.Distributions.TwoValued
/-- If a random variable is ae equal to `0` or `1`, then its conditional variance is the product of
the conditional probabilities that it's equal to `0` and that it's equal to `1`.  -/
ProbabilityTheory.condVar_of_ae_eq_zero_or_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
  m ≤ m₀ →
    ∀ {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
      AEMeasurable X μ →
        (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → ProbabilityTheory.condVar m X μ =ᵐ[μ] μ[X | m] * μ[1 - X | m]
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸], ContDiff 𝕜 n fun p => p.1 * p.2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The measurable **Besicovitch covering theorem**.

Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at
`x`, with arbitrarily small radii. Then there exists a disjoint covering of almost all `s` by
admissible closed balls centered at some points of `s`.

This version requires the underlying measure to be s-finite, and the space to have the
Besicovitch covering property (which is satisfied for instance by finite-dimensional
normed real vector spaces).
It expresses the conclusion in a slightly awkward form (with a subset of `α × ℝ`) coming from the
proof technique.

For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`.
 -/
Besicovitch.exists_disjoint_closedBall_covering_ae_aux : ∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  (f : α → Set ℝ) (s : Set α),
  (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
    ∃ t,
      t.Countable ∧
        (∀ p ∈ t, p.1 ∈ s) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem_nhdsWithin : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s t : Set M} {x : M},
  (∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ nhdsWithin x t → P f s x → P f t x) →
    ChartedSpace.LiftPropWithinAt P g s x → s ∈ nhdsWithin x t → ChartedSpace.LiftPropWithinAt P g t x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_disjUnion : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (h : Disjoint s₁ s₂),
  ∑ x ∈ s₁.disjUnion s₂ h, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeFunctorFunctorCategoryOfHasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  [W.IsStableUnderCobaseChange] (J : Type u'') [inst_2 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.Limits.HasPushouts C], (W.functorCategory J).IsStableUnderCobaseChange
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.hasCoequalizers_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Limits.HasCoequalizers Cᵒᵖ
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atBot_curry : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {p : α × β → Prop},
  (∀ᶠ (x : α × β) in Filter.atBot, p x) → ∀ᶠ (k : α) in Filter.atBot, ∀ᶠ (l : β) in Filter.atBot, p (k, l)
-- Mathlib.GroupTheory.Index
/-- An additive subgroup has index two if and only if there exists `a` such that
for all `b`, exactly one of `a + b` and `b` belong to `H`.  -/
AddSubgroup.index_eq_two_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (a + b ∈ H) (b ∈ H)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.id_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.ContainsIdentities] [inst_2 : Wᵣ.ContainsIdentities] (c : C),
  (CategoryTheory.Span.id c).r = CategoryTheory.CategoryStruct.id c
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.intValuation_eq_of_coe : ∀ {K : Type u_2} [inst : Field K] (P : Polynomial K),
  (Polynomial.idealX K).intValuation P = (PowerSeries.idealX K).intValuation ↑P
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.adjoinIntegral_eq_one_of_isUnit : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [IsDomain A] (x : K) (hx : IsIntegral A x),
  IsUnit (FractionalIdeal.adjoinIntegral (nonZeroDivisors A) x hx) →
    FractionalIdeal.adjoinIntegral (nonZeroDivisors A) x hx = 1
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.comap_id : ∀ {α : Type u_2} [inst : TopologicalSpace α],
  TopologicalSpace.Opens.comap (ContinuousMap.id α) = FrameHom.id (TopologicalSpace.Opens α)
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_univ_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] [inst_2 : Fintype α] (t : Finset α),
  Finset.univ.addEnergy t = Fintype.card α * t.card ^ 2
-- Mathlib.Topology.Algebra.Monoid
le_nhds_add : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] (a b : M),
  nhds a + nhds b ≤ nhds (a + b)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_eq_zero_iff_of_nonpos : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, f i ≤ 0) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
-- Init.Data.String.Decode
String.utf8EncodeChar_eq_cons_cons_cons_cons : ∀ {c : Char},
  c.utf8Size = 4 →
    String.utf8EncodeChar c =
      [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
        (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- The image of a bounded set under a Lipschitz map is bounded.  -/
LipschitzWith.isBounded_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {s : Set α}, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_append_right_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₁
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.sound : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op),
  g +ᵥ ⇑(QuotientAddGroup.mk' N) ⁻¹' U = ⇑(QuotientAddGroup.mk' N) ⁻¹' U
-- Std.Time.Zoned.Database.Basic
/-- Converts a `TZif.TZifV2` structure to a `ZoneRules` structure, extending transitions beyond
the last stored entry using the POSIX TZ footer string when present.
 -/
Std.Time.TimeZone.convertTZifV2 : Std.Time.TimeZone.TZif.TZifV2 → String → Except String Std.Time.TimeZone.ZoneRules
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_center : ∀ (R : Type u) [inst : NonUnitalNonAssocSemiring R], ↑(NonUnitalSubsemiring.center R) = Set.center R
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.instGroupWithZero : {G₀ : Type u_2} → [GroupWithZero G₀] → GroupWithZero (ConjAct G₀)
-- Mathlib.GroupTheory.Nilpotent
/-- The upper central series of an additive group is an ascending central series.  -/
AddSubgroup.upperCentralSeries_isAscendingCentralSeries : ∀ (G : Type u_1) [inst : AddGroup G], AddSubgroup.IsAscendingCentralSeries (AddSubgroup.upperCentralSeries G)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Finset.measurable_restrict_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] (s : Finset α) {f : α → γ},
  Measurable f → Measurable (s.restrict f)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.FiniteType.finite_cell`.

---

`cell C n` is finite for every `n`.  -/
Topology.CWComplex.FiniteType.finite_cell : ∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteType C] (n : ℕ), Finite (Topology.RelCWComplex.cell C n)
-- Lean.Parser.Command
Lean.Parser.Term.quot.formatter : Lean.PrettyPrinter.Formatter
-- Std.Http.Data.URI.Basic
Std.Http.URI.Port.value.injEq : ∀ (port port_1 : UInt16), (Std.Http.URI.Port.value port = Std.Http.URI.Port.value port_1) = (port = port_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_def_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Save `e.ematchDiagSource` in `c` if it is not `.other`.
This is used to implement `grind.ematch.diagnostics`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.saveSource : Lean.Meta.Grind.EMatch.Choice → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Util.Superscript
Mathlib.Tactic.superscriptTerm.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.lt_sup_iff_notMem : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Submodule R M}
  {a : M}, I < I ⊔ R ∙ a ↔ a ∉ I
-- Mathlib.Topology.Algebra.Support
tsupport_add : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass α] (f g : X → α),
  (tsupport fun x => f x + g x) ⊆ tsupport f ∪ tsupport g
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₐc[R] B} (h₀ : ∀ (x y : A), f (x + y) = f x + f y)
  (h₁ :
    ∀ (m : R) (x : A),
      { toFun := ⇑f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₀ }.toFun x)
  (h₂ : CoalgebraStruct.counit ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } = CoalgebraStruct.counit)
  (h₃ :
    TensorProduct.map { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ }
          { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } ∘ₗ
        CoalgebraStruct.comul =
      CoalgebraStruct.comul ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ })
  (h₄ : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1)
  (h₅ :
    ∀ (x y : A),
      { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) =
        { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x *
          { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y),
  { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄,
      map_mul' := h₅ } =
    f
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_opow : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
-- Lean.Meta.Tactic.Grind.Extension
/-- A constraint of the form `depth lhs < n`. The `lhs` is one of the bound variables.
The depth is computed in constant time using the `approxDepth` field attached to expressions.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.depthLt : ℕ → ℕ → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_finset_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ},
  0 ≤ r → (s.sup p).closedBall x r = s.inf fun i => (p i).closedBall x r
-- Mathlib.Analysis.Normed.Group.Basic
enorm_pos : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedAddMonoid E] {a : E}, 0 < ‖a‖ₑ ↔ a ≠ 0
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = ⇑(DoubleQuot.quotQuotEquivQuotSup I J).symm
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eval₂AlgHom_apply : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b)
  (p : Polynomial A), (Polynomial.eval₂AlgHom f b hf) p = Polynomial.eval₂ (↑f) b p
-- Mathlib.Algebra.Order.Module.Defs
instPosSMulStrictMonoIntOfIsOrderedAddMonoid : ∀ {G : Type u_3} [inst : PartialOrder G] [inst_1 : AddCommGroup G] [IsOrderedAddMonoid G], PosSMulStrictMono ℤ G
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builderOption.sizeOf_spec : ∀ (o : Aesop.Frontend.BuilderOption), sizeOf (Aesop.Frontend.Feature.builderOption o) = 1 + sizeOf o
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (x y : M₁),
  (B x) y = ⇑(b.repr x) ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec ⇑(b.repr y)
-- Mathlib.Order.Filter.Pointwise
Filter.mul_neBot_iff : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, (f * g).NeBot ↔ f.NeBot ∧ g.NeBot