mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.isNilpotent_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {P : MvPolynomial σ R},
  IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (MvPolynomial.coeff i P)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (fallback : (a : α) × β a) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getEntryD k fallback =
    match compare k k' with
    | Ordering.lt => l.getEntryD k fallback
    | Ordering.gt => r.getEntryD k fallback
    | Ordering.eq => ⟨k', v⟩
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- `x ^ k = o(exp(b * x))` as `x → ∞` for any integer `k` and positive `b`.  -/
isLittleO_zpow_exp_pos_mul_atTop : ∀ (k : ℤ) {b : ℝ}, 0 < b → (fun x => x ^ k) =o[Filter.atTop] fun x => Real.exp (b * x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∉ t → t.get? a = none
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the monomial `a*X^d` is infinite if `a = 0` and `degree d` otherwise.  -/
MvPowerSeries.order_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {d : σ →₀ ℕ} {a : R} [inst_1 : Decidable (a = 0)],
  ((MvPowerSeries.monomial d) a).order = if a = 0 then ⊤ else ↑(Finsupp.degree d)
-- Std.Data.Internal.List.Associative
Std.Internal.List.assoc_induction : ∀ {α : Type u} {β : α → Type v} {motive : List ((a : α) × β a) → Prop},
  motive [] →
    (∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tail → motive (⟨k, v⟩ :: tail)) →
      ∀ (t : List ((a : α) × β a)), motive t
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {β : Type u_10} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {f : Ω → β}
  {g : Ω → γ}, ProbabilityTheory.Kernel.IndepFun f g κ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_subset_iff : ∀ {α : Type u_2} [inst : Mul α] {s t u : Set α}, s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u
-- Mathlib.Topology.Algebra.Ring.Compact
/-- Compact Hausdorff Artinian (commutative) rings are finite. This is not an instance, as it would
apply to every `Finite` goal, causing slowly failing typeclass search in some cases.  -/
IsArtinianRing.finite_of_compactSpace_of_t2Space : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsArtinianRing R], Finite R
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.homRel.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.FreeGroupoid.homRel C ((Quiver.FreeGroupoid.of C).map (CategoryTheory.CategoryStruct.comp f g))
    (CategoryTheory.CategoryStruct.comp ((Quiver.FreeGroupoid.of C).map f) ((Quiver.FreeGroupoid.of C).map g))
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- The convergent of `GenContFract.of v` at step `n - 1` is exactly `v` if the
`IntFractPair.stream` of the corresponding continued fraction terminated at step `n`.  -/
GenContFract.of_correctness_of_nth_stream_eq_none : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K],
  GenContFract.IntFractPair.stream v n = none → v = (GenContFract.of v).convs (n - 1)
-- Mathlib.Data.ZMod.QuotientRing
Int.quotientSpanNatEquivZMod_comp_castRingHom : ∀ (n : ℕ),
  (↑(Int.quotientSpanNatEquivZMod n).symm).comp (Int.castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})
-- Mathlib.Data.W.Constructions
WType.toNat.eq_1 : ∀ (f : WType.Natβ WType.Natα.zero → WType WType.Natβ), (WType.mk WType.Natα.zero f).toNat = 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_smul : ∀ {R : Type u_1} {S : Type u_4} [inst : Semiring R] [inst_1 : Monoid S] {M : Type u_6} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N₂ : Type u_9} [inst_5 : TopologicalSpace N₂]
  [inst_6 : AddCommMonoid N₂] [inst_7 : Module R N₂] {N₃ : Type u_10} [inst_8 : TopologicalSpace N₃]
  [inst_9 : AddCommMonoid N₃] [inst_10 : Module R N₃] [inst_11 : DistribMulAction S N₃] [inst_12 : SMulCommClass R S N₃]
  [inst_13 : ContinuousConstSMul S N₃] [inst_14 : DistribMulAction S N₂] [inst_15 : ContinuousConstSMul S N₂]
  [inst_16 : SMulCommClass R S N₂] [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂),
  hₗ ∘SL (c • fₗ) = c • hₗ ∘SL fₗ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toArray_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.keys.toArray = m.keysArray
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_3 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m n n' : M),
  CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X)
    ((CategoryTheory.shiftFunctor C n').obj ((CategoryTheory.shiftFunctor C n).obj Y))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The canonical morphism from `R` to the pushforward of its restriction to `Over x`.  -/
SheafOfModules.pushforwardOver : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (x : C) → R ⟶ ((CategoryTheory.Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)
-- Mathlib.LinearAlgebra.Span.Basic
/-- See also `Submodule.span_preimage_eq`.  -/
Submodule.span_preimage_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  (f : M →ₛₗ[σ₁₂] M₂) (s : Set M₂), Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuousOn_sin : ∀ {s : Set ℝ}, ContinuousOn Real.sin s
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.not_and_or_eq : ∀ (p q : Prop), (¬(p ∧ q)) = (¬p ∨ ¬q)
-- Mathlib.Data.Part
Part.bind_defined : ∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} (h : f.Dom), (g (f.get h)).Dom → (f.bind g).Dom
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hasForgetToRing : (R : Type u) → [inst : CommRing R] → CategoryTheory.HasForget₂ (AlgCat R) RingCat
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_smul : ∀ {S : Type u_2} {R : Type u} {M : Type v} [inst : SMul S R] [inst_1 : SMul S M] (s : S) (x : TrivSqZeroExt R M),
  (s • x).fst = s • x.fst
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.skipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {h : A.PairingCore} →
      {α : Type v} →
        [inst : PartialOrder α] →
          (rank : h.ι → α) →
            (∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y) → h.WeakRankFunction α
-- Mathlib.Analysis.LConvolution
MeasureTheory.mlconvolution.eq_1 : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] (f g : G → ENNReal)
  (μ : MeasureTheory.Measure G) (x : G), MeasureTheory.mlconvolution f g μ x = ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
le_pow_sup : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : SemilatticeSup M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ},
  a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n
-- Mathlib.Data.Set.Image
/-- The image of `range some` under `Option.elim b f` equals `range f`.  -/
Option.image_elim_range_some_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (b : β), (fun o => o.elim b f) '' Set.range some = Set.range f
-- Mathlib.SetTheory.Cardinal.NatCard
/-- If `f` is an embedding, then `Nat.card α ≤ Nat.card β`. We must also assume
`Nat.card β = 0 → Nat.card α = 0` since `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_le_of_embedding' : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), (Nat.card β = 0 → Nat.card α = 0) → Nat.card α ≤ Nat.card β
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SizeOf 𝕜] [inst_10 : SizeOf V]
  [inst_11 : SizeOf V₂] [inst_12 : SizeOf P] [inst_13 : SizeOf P₂] (toAffineMap : P →ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), ‖toAffineMap.linear x‖ = ‖x‖),
  sizeOf { toAffineMap := toAffineMap, norm_map := norm_map } = 1 + sizeOf toAffineMap
-- Mathlib.Topology.Continuous
/-- Lean's elaborator has trouble elaborating applications of lemmas that state that the composition of
two functions satisfy some property at a point, like `ContinuousAt.comp` / `ContDiffAt.comp` and
`ContMDiffWithinAt.comp`. The reason is that a lemma like this looks like
`ContinuousAt g (f x) → ContinuousAt f x → ContinuousAt (g ∘ f) x`.
Since Lean's elaborator elaborates the arguments from left-to-right, when you write `hg.comp hf`,
the elaborator will try to figure out *both* `f` and `g` from the type of `hg`. It tries to figure
out `f` just from the point where `g` is continuous. For example, if `hg : ContinuousAt g (a, x)`
then the elaborator will assign `f` to the function `Prod.mk a`, since in that case `f x = (a, x)`.
This is undesirable in most cases where `f` is not a variable. There are some ways to work around
this, for example by giving `f` explicitly, or to force Lean to elaborate `hf` before elaborating
`hg`, but this is annoying.
Another better solution is to reformulate composition lemmas to have the following shape
`ContinuousAt g y → ContinuousAt f x → f x = y → ContinuousAt (g ∘ f) x`.
This is even useful if the proof of `f x = y` is `rfl`.
The reason that this works better is because the type of `hg` doesn't mention `f`.
Only after elaborating the two `ContinuousAt` arguments, Lean will try to unify `f x` with `y`,
which is often easy after having chosen the correct functions for `f` and `g`.
Here is an example that shows the difference:
```
example [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} (f : X → X → Y)
    (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
    ContinuousAt (fun x ↦ f x x) x₀ :=
  -- hf.comp (continuousAt_id.prod continuousAt_id) -- type mismatch
  -- hf.comp_of_eq (continuousAt_id.prod continuousAt_id) rfl -- works
```
 -/
LibraryNote.comp_of_eq_lemmas : Batteries.Util.LibraryNote
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.eq_ite : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [inst_5 : DecidableEq ι] {i j : ι} (v : G i) (w : G j),
      inner 𝕜 ((V i) v) ((V j) w) = if i = j then inner 𝕜 ((V i) v) ((V j) w) else 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `none`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.Raw.getEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option ((a : α) × β a)
-- Mathlib.Computability.Reduce
toNat_manyOneEquiv : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {p : Set α}, ManyOneEquiv (toNat p) p
-- Mathlib.Probability.Process.Filtration
MeasureTheory.SigmaFiniteFiltration.SigmaFinite : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {inst : Preorder ι} {μ : MeasureTheory.Measure Ω}
  {f : MeasureTheory.Filtration ι m} [self : MeasureTheory.SigmaFiniteFiltration μ f] (i : ι),
  MeasureTheory.SigmaFinite (μ.trim ⋯)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_bot_of_card_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H], Nat.card ↥H ≤ 1 → H = ⊥
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.type_toPSet : ∀ (o : Ordinal.{u_1}), o.toPSet.Type = o.ToType
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iio_disjoint_Ioi_of_le : ∀ {α : Type v} [inst : Preorder α] {a b : α}, b ≤ a → Disjoint (Set.Iio b) (Set.Ioi a)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppLid_apply_apply : ∀ (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ),
  ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The `IsUniformAddGroup` structure on `PowerSeries` of a `IsUniformAddGroup`  -/
PowerSeries.WithPiTopology.instIsUniformAddGroup : ∀ (R : Type u_1) [inst : UniformSpace R] [inst_1 : AddGroup R] [IsUniformAddGroup R], IsUniformAddGroup (PowerSeries R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
  [X.IsCoskeletal n], CategoryTheory.IsIso ((CategoryTheory.SimplicialObject.coskAdj n).unit.app X)
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.instHasImagesType : CategoryTheory.Limits.HasImages (Type u)
-- Mathlib.Data.EReal.Basic
EReal.eq_top_iff_forall_lt : ∀ (x : EReal), x = ⊤ ↔ ∀ (y : ℝ), ↑y < x
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_dvd_iff' : ∀ {u : PrimeMultiset} {n : ℕ+}, u.prod ∣ n ↔ u ≤ n.factorMultiset
-- Mathlib.Algebra.Category.CommBialgCat
/-- The underlying type.  -/
CommBialgCat.carrier : {R : Type u} → [inst : CommRing R] → CommBialgCat R → Type v
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimApp : Array Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The trivial restriction-closed groupoid is indeed `ClosedUnderRestriction`.  -/
closedUnderRestriction_idRestrGroupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H], ClosedUnderRestriction idRestrGroupoid
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.lastDart_mem_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), p.lastDart hnil ∈ p.darts
-- Mathlib.Algebra.Group.Even
isSquare_iff_exists_mul_self : ∀ {α : Type u_2} [inst : Mul α] (a : α), IsSquare a ↔ ∃ r, a = r * r
-- Mathlib.RingTheory.DividedPowers.Basic
/-- The divided power structure on an ideal `I` of a commutative ring `A`.  -/
DividedPowers : {A : Type u_1} → [inst : CommSemiring A] → Ideal A → Type u_1
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilteriUnion_neBot : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I), (BoxIntegral.IntegrationParams.toFilteriUnion I π₀).NeBot
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.image_Iic_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  MonotoneOn f (Set.Iic b) → f '' Set.Iic b ⊆ Set.Iic (f b)
-- Mathlib.Order.WellFounded
Function.argminOn_le : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LinearOrder β] [inst_1 : WellFoundedLT β] (s : Set α) {a : α}
  (ha : a ∈ s), f (Function.argminOn f s ⋯) ≤ f a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasHomology],
  h.homologyIso = S.rightHomologyIso.symm ≪≫ h.rightHomologyIso
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_id : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x =
    CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.eq_zero_iff : ∀ {M : Type u_1} [inst : MonoidWithZero M] {a b : M}, Associated a b → (a = 0 ↔ b = 0)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (property : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' property
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.extract : Lean.Parser.SyntaxStack → ℕ → ℕ → Array Lean.Syntax
-- Mathlib.Topology.Maps.OpenQuotient
isQuotientMap_of_isOpenQuotientMap_of_isInducing : ∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace C] [inst_3 : TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D),
  g ∘ p = q ∘ f →
    Topology.IsInducing f →
      Function.Surjective p →
        IsOpenQuotientMap q → Topology.IsEmbedding g → q ⁻¹' q '' Set.range f ⊆ Set.range f → Topology.IsQuotientMap p
-- Mathlib.Order.Minimal
minimalFor_eq_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] {f : ι → α} {i j : ι}, MinimalFor (fun x => x = j) f i ↔ i = j
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] (i j : ι) [IsDomain R] [P.IsReduced],
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
-- Lean.Language.Basic
Lean.Language.SnapshotTreeTransform.mk.sizeOf_spec : ∀ (addTrailing : Substring.Raw), sizeOf { addTrailing := addTrailing } = 1 + sizeOf addTrailing
-- Lean.Elab.Declaration
Lean.Elab.Command.elabDeclaration : Lean.Elab.Command.CommandElab
-- Mathlib.NumberTheory.Multiplicity
dvd_geom_sum₂_iff_of_dvd_sub : ∀ {R : Type u_1} {n : ℕ} [inst : CommRing R] {x y p : R},
  p ∣ x - y → (p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1))
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital seminormed commutative ring is also a non-unital
seminormed commutative ring, with the restriction of the norm.  -/
NonUnitalSubalgebra.nonUnitalSeminormedCommRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} →
      [inst_1 : NonUnitalSeminormedCommRing E] →
        [inst_2 : Module 𝕜 E] → (s : NonUnitalSubalgebra 𝕜 E) → NonUnitalSeminormedCommRing ↥s
-- Mathlib.CategoryTheory.Simple
/-- An object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero.  -/
CategoryTheory.Simple : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Prop
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.instPartialOrder : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] → (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → PartialOrder (ProjectiveSpectrum 𝒜)
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.projZeroRingHom.congr_simp : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜], GradedRing.projZeroRingHom 𝒜 = GradedRing.projZeroRingHom 𝒜
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `cthickening_cthickening`.  -/
Metric.cthickening_cthickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ ε : ℝ},
  0 ≤ ε → 0 ≤ δ → ∀ (s : Set α), Metric.cthickening ε (Metric.cthickening δ s) ⊆ Metric.cthickening (ε + δ) s
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.arity : Lean.Meta.SparseCasesOnInfo → ℕ
-- Init.SimpLemmas
or_false : ∀ (p : Prop), (p ∨ False) = p
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanModuleQuery : Lean.ToJson Lean.Lsp.LeanModuleQuery
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_J : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).J = 𝒰.I₀
-- Mathlib.Data.List.ChainOfFn
List.isChain_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} {r : α → α → Prop},
  List.IsChain r (List.ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
-- Mathlib.Tactic.ProdAssoc
/-- The iterated product corresponding to a `ProdTree`.  -/
Lean.Expr.ProdTree.getType : Lean.Expr.ProdTree → Lean.Expr