mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsZariskiLocalAtSource : AlgebraicGeometry.IsZariskiLocalAtSource @AlgebraicGeometry.UniversallyOpen
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌈b / r⌉ - ⌈a / r⌉` multiples of `r` in `[a, b)`, if `a ≤ b`.  -/
Int.Ico_filter_dvd_card : ∀ (a b : ℤ) {r : ℤ}, 0 < r → ↑{x ∈ Finset.Ico a b | r ∣ x}.card = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0
-- Init.Meta.Defs
/-- Extracts the non-separator elements of a separated array.
 -/
Lean.Syntax.SepArray.getElems : {sep : String} → Lean.Syntax.SepArray sep → Array Lean.Syntax
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (c : C),
  (CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso G F L E c).hom.hom =
    CategoryTheory.CategoryStruct.id (G.obj (E.left.obj c))
-- Mathlib.Topology.Sheaves.Abelian
TopCat.Sheaf.instAbelian : {X : TopCat} →
  {C : Type v₁} →
    [inst : CategoryTheory.Category.{v₂, v₁} C] →
      [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] →
        [CategoryTheory.Abelian C] → CategoryTheory.Abelian (TopCat.Sheaf C X)
-- Lean.Meta.Closure
Lean.Meta.Closure.preprocess : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.class : Lean.Lsp.CompletionItemKind
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_inj : ∀ {α : Type u_1} {a b : α}, toBoolAlg a = toBoolAlg b ↔ a = b
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_iInf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_4} {x : α} {s : ι → TopologicalSpace.Closeds α},
  x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_v_fst_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      ((CochainComplex.mappingCocone.fst φ).f p₂) =
    α.v p₁ p₂ h₁₂
-- Init.GetElem
of_getElem?_eq_some : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem}
  [inst : GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)],
  c[i]? = some e → dom c i
-- Mathlib.Probability.Moments.MGFAnalytic
/-- The moment-generating function is analytic on the interior of the interval on which it is
defined.  -/
ProbabilityTheory.analyticOn_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOn ℝ (ProbabilityTheory.mgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.range_toSubring : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing R]
  [inst_3 : Nontrivial S] (f : R →+* S), (LocalSubring.range f).toSubring = (Subring.map f ⊤).copy (Set.range ⇑f) ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.markdown.sizeOf_spec : ∀ (markup : Lean.Lsp.MarkupContent), sizeOf (Lean.Lsp.InlayHintTooltip.markdown markup) = 1 + sizeOf markup
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.maximalIdeal_injective : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], Function.Injective fun w => w.maximalIdeal
-- Aesop.Tree.Data
Aesop.instNonemptyGoalData : ∀ {Rapp MVarCluster : Type} [Nonempty MVarCluster], Nonempty (Aesop.GoalData Rapp MVarCluster)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.DTreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The colimit cocone over any functor into a complete lattice.
 -/
CategoryTheory.Limits.CompleteLattice.colimitCocone : {α : Type u} →
  [inst : CompleteLattice α] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        (F : CategoryTheory.Functor J α) → CategoryTheory.Limits.ColimitCocone F
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.hasCoeToLinearEquiv : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N)
-- Mathlib.Data.Real.Sign
Real.sign_one : Real.sign 1 = 1
-- Mathlib.RingTheory.Support
Module.mem_support_iff_exists_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∈ Module.support R M ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
-- Mathlib.Algebra.BigOperators.Associated
Associates.prod_eq_one_iff : ∀ {M : Type u_2} [inst : CommMonoid M] {p : Multiset (Associates M)}, p.prod = 1 ↔ ∀ a ∈ p, a = 1
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.add_nsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddMonoid α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (x + n • c) = (-1) ^ n • f x
-- Mathlib.Logic.Function.Basic
Function.HasUncurry.mk : {α : Type u_5} → {β : outParam (Type u_6)} → {γ : outParam (Type u_7)} → (α → β → γ) → Function.HasUncurry α β γ
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.trans : ∀ {R : Type uR} {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A],
  Algebra.FiniteType R S → Algebra.FiniteType S A → Algebra.FiniteType R A
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- The projection from `ℝ` to a closed segment is smooth on the segment, in the manifold sense.  -/
contMDiffOn_projIcc : ∀ {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞},
  ContMDiffOn (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) n (Set.projIcc x y ⋯) (Set.Icc x y)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfMinpoly_gen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h : minpoly A pb.gen = minpoly A pb'.gen), (pb.equivOfMinpoly pb' h) pb.gen = pb'.gen
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ (c : ℝ) {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T (c • f) = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} (h : m.WF)
  {hc : k' ∈ Std.DHashMap.Raw.Const.modify m k f},
  (Std.DHashMap.Raw.Const.modify m k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
BialgEquiv.toHopfAlgIso_refl : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : HopfAlgebra R X],
  (BialgEquiv.refl R X).toHopfAlgIso = CategoryTheory.Iso.refl (HopfAlgCat.of R X)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.coconeOfRepresentable_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))),
  (CategoryTheory.Presheaf.coconeOfRepresentable P).pt = P
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s s' : Set ℝ}, IsMIntegralCurveOn γ v s → s' ⊆ s → IsMIntegralCurveOn γ v s'
-- Mathlib.Data.Nat.Log
Nat.clog_one_left : ∀ (n : ℕ), Nat.clog 1 n = 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodInverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') (f : CategoryTheory.CostructuredArrow S T × CategoryTheory.CostructuredArrow S' T'),
  (CategoryTheory.CostructuredArrow.prodInverse S S' T T').obj f =
    CategoryTheory.CostructuredArrow.mk (f.1.hom, f.2.hom)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}, p.IsPath → s(v, w) ∈ p.edges → w = p.penultimate
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_nsmul : ∀ {M N : AddCommGrpCat} (n : ℕ) (f : M ⟶ N), AddCommGrpCat.Hom.hom (n • f) = n • AddCommGrpCat.Hom.hom f
-- Mathlib.Topology.Covering.Basic
FiberBundle.isCoveringMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] {F : Type u_3} {E : X → Type u_4} [inst_1 : TopologicalSpace F]
  [DiscreteTopology F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : X) → TopologicalSpace (E x)]
  [FiberBundle F E], IsCoveringMap Bundle.TotalSpace.proj
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- A commuting family of symmetric linear maps on a finite-dimensional inner
product space is simultaneously diagonalizable.  -/
LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {ι : Type u_5} {T : ι → E →ₗ[𝕜] E},
  (∀ (i : ι), (T i).IsSymmetric) → Pairwise (Function.onFun Commute T) → ⨆ χ, ⨅ i, Module.End.eigenspace (T i) (χ i) = ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv =
    CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_apply_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (p : P₁), e.symm (e p) = p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.getElem_toList_eq : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Mathlib.Analysis.Normed.Operator.Basic
/-- A continuous linear map between seminormed spaces is bounded when the field is nontrivially
normed. The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
norm is then used to rescale any element into an element of norm in `[ε/C, ε]`, whose image has a
controlled norm. The norm control for the original element follows by rescaling.  -/
SemilinearMapClass.bound_of_continuous : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕), Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.isEmbedding_prodMap : ∀ {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList.eq_1 : ∀ {α : Type u_1}, FreeMonoid.toList = Equiv.refl (FreeMonoid α)
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.minFacHelper_3 : ∀ {n k k' : ℕ},
  k + 2 = k' → (n % k).beq 0 = false → Mathlib.Meta.NormNum.MinFacHelper n k → Mathlib.Meta.NormNum.MinFacHelper n k'
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n]
  [inst_6 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.map f it) = Std.IterM.foldM (fun d b => g d (f b)) init it
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- The Gelfand transform is an isometry when the algebra is a C⋆-algebra over `ℂ`.  -/
gelfandTransform_isometry : ∀ (A : Type u_1) [inst : CommCStarAlgebra A], Isometry ⇑(WeakDual.gelfandTransform ℂ A)
-- Batteries.Data.Random.MersenneTwister
_private.Batteries.Data.Random.MersenneTwister.0.Batteries.Random.MersenneTwister.Config.init.loop.eq_def : ∀ (cfg : Batteries.Random.MersenneTwister.Config) (w : BitVec cfg.wordSize) (v : Array (BitVec cfg.wordSize))
  (h : v.size ≤ cfg.stateSize),
  Batteries.Random.MersenneTwister.Config.init.loop✝ cfg w v h =
    if heq : v.size = cfg.stateSize then Vector.mk v heq
    else
      let v_1 := v.push w;
      have w_1 := cfg.initMult * (w ^^^ w >>> cfg.wordSize - 2) + ↑v_1.size;
      Batteries.Random.MersenneTwister.Config.init.loop✝ cfg w_1 v_1 ⋯
-- Mathlib.Analysis.BoxIntegral.Basic
/-- Quite often it is more natural to prove an estimate of the form `a * ε`, not `ε` in the RHS of
`BoxIntegral.hasIntegral_iff`, so we provide this auxiliary lemma.  -/
BoxIntegral.HasIntegral.of_mul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F}
  (a : ℝ),
  (∀ (ε : ℝ),
      0 < ε →
        ∃ r,
          (∀ (c : NNReal), l.RCond (r c)) ∧
            ∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I),
              l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ a * ε) →
    BoxIntegral.HasIntegral I l f vol y
-- Mathlib.Algebra.Group.Defs
SubtractionMonoid.toInvolutiveNeg : {G : Type u} → [self : SubtractionMonoid G] → InvolutiveNeg G
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Any.eq_2 : ∀ {α : Type u_1} (P : α → Prop) (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  Ordnode.Any P (Ordnode.node sz l x_1 r) = (Ordnode.Any P l ∨ P x_1 ∨ Ordnode.Any P r)
-- Mathlib.Algebra.BigOperators.WithTop
WithBot.coe_sum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNatClamp_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toFin = ⟨UInt16.size - 1, UInt16.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The coequalizer morphism in any colimit cocone is an epimorphism.  -/
CategoryTheory.Limits.epi_of_isColimit_cofork : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Cofork f g}
  (i : CategoryTheory.Limits.IsColimit c), CategoryTheory.Epi c.π
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  {inner inner_1 : Std.IterM m β}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Lean.Parser.Syntax
Lean.Parser.Command.notationItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.EssentiallySmall.of_functor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.LocallySmall.{w, v_1, u_1} C],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage →
    (∀ (Y : D), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x => Nonempty (F.obj x ≅ Y)) →
      CategoryTheory.EssentiallySmall.{w, v_1, u_1} C
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `final_comp` below.  -/
CategoryTheory.Functor.final_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Final] [G.IsEquivalence], (F.comp G).Final
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- `WithInitial.star` is initial.  -/
CategoryTheory.WithInitial.starInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.IsInitial CategoryTheory.WithInitial.star
-- Init.Data.Ord.Basic
instOrdChar : Ord Char
-- Mathlib.Topology.MetricSpace.Isometry
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
IsometryEquiv.Simps.apply : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → α → β
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `Iio b` and
nonnegative on `Ioo b c`. Then `f` attains its minimum on `Iio c` at `b`.  -/
isMinOn_Iio_of_deriv : ∀ {f : ℝ → ℝ} {b c : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Iio b) →
      DifferentiableOn ℝ f (Set.Ioo b c) →
        (∀ x ∈ Set.Iio b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Iio c) b
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instOrderedStructure : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M], L.OrderedStructure M
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.ext_iff : ∀ {α : Type u_2} {m m' : PseudoEMetricSpace α}, m = m' ↔ m.toEDist = m'.toEDist
-- Mathlib.Order.LatticeIntervals
Set.Ioc.codisjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a b : α} [inst_1 : Fact (a < b)] {x y : ↑(Set.Ioc a b)},
  Codisjoint x y ↔ ↑x ⊔ ↑y = b
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` depends only on `a` mod `b`.  -/
jacobiSym.mod_left' : ∀ {a₁ a₂ : ℤ} {b : ℕ}, a₁ % ↑b = a₂ % ↑b → jacobiSym a₁ b = jacobiSym a₂ b
-- Mathlib.Order.Heyting.Hom
HeytingHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] {f : HeytingHom α β}, f.toFun = ⇑f
-- Init.Data.List.Nat.Basic
List.getElem_eq_getElem_reverse : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.length), l[i] = l.reverse[l.length - 1 - i]
-- Mathlib.CategoryTheory.Abelian.Injective.Basic
/-- The preadditive Yoneda functor on `J` preserves colimits if `J` is injective.  -/
CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (J : C)
  [hP : CategoryTheory.Injective J],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)
-- Mathlib.Analysis.Seminorm
Seminorm.mem_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.closedBall x r ↔ p (y - x) ≤ r
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- A subobject of `src ⨯ tgt`, interpreted as a relation  -/
CategoryTheory.Dial.rel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (self : CategoryTheory.Dial C) → CategoryTheory.Subobject (self.src ⨯ self.tgt)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncGE.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'}
  [toIsRelIff : e.IsRelIff], (∀ {j : ι} {k' : ι'}, c'.Rel (e.f j) k' → ∃ k, e.f k = k') → e.IsTruncGE
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
exists_dist_lt_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x z : E} {δ ε : ℝ},
  0 < δ → 0 ≤ ε → dist x z < ε + δ → ∃ y, dist x y < δ ∧ dist y z ≤ ε
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If a group acts nontrivially, then the type is nontrivial  -/
MulAction.nontrivial_of_fixedPoints_ne_univ : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.fixedPoints G α ≠ Set.univ → Nontrivial α