mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.eval_at_1 : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ), Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.hasPushouts_symmetry_of_hasPushoutsAlong : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {S X Y : C} {f : S ⟶ X}
  [CategoryTheory.Limits.HasPushoutsAlong f] {g : S ⟶ Y}, CategoryTheory.Limits.HasPushout f g
-- Batteries.Classes.RatCast
/-- Canonical homomorphism from `Rat` to a division ring `K`.
This is just the bare function in order to aid in creating instances of `DivisionRing`.  -/
Rat.cast : {K : Type u} → [RatCast K] → ℚ → K
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm2 : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_one_right_of_dvd : ∀ {R : Type u} [inst : CommRing R] {x y : R}, x ∣ y → IsCoprime x (y + 1)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_apply_ae : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
      ∀ {t : Set α}, MeasurableSet t → (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balance_sz_dual : ∀ {α : Type u_1} {l r : Ordnode α},
  ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
      ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
    (∃ l', Ordnode.Raised l' r.dual.size ∧ Ordnode.BalancedSz l' l.dual.size) ∨
      ∃ r', Ordnode.Raised l.dual.size r' ∧ Ordnode.BalancedSz r.dual.size r'
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instPow.eq_1 : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α],
  NonemptyInterval.instPow = { pow := fun s n => { toProd := s.toProd ^ n, fst_le_snd := ⋯ } }
-- Mathlib.Algebra.Group.Irreducible.Lemmas
AddEquiv.addIrreducible_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] {x : M}
  [inst_2 : EquivLike F M N] [AddEquivClass F M N] (f : F), AddIrreducible (f x) ↔ AddIrreducible x
-- Init.Notation
/-- `a >>> b` computes `a` shifted to the right by `b` places.
The meaning of this notation is type-dependent.
* On `Nat` and fixed width unsigned types like `UInt8`,
  this is equivalent to `a / 2 ^ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>>>` in identifiers is `shiftRight`. -/
«term_>>>_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
cyclotomic_comp_X_add_one_isEisensteinAt : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ((Polynomial.cyclotomic p ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (ℤ ∙ ↑p)
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendEquiv.eq_1 : ∀ {α : Type u_1} (m n : ℕ),
  Fin.appendEquiv m n =
    { toFun := fun fg => Fin.append fg.1 fg.2,
      invFun := fun f => (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i)), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGE n).map f) =
    CategoryTheory.CategoryStruct.comp f ((t.truncGEπ n).app Y)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- A restatement of `prod_ite_eq` with the equality test reversed.  -/
Finsupp.prod_ite_eq' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : DecidableEq α]
  (f : α →₀ M) (a : α) (b : α → M → N),
  (f.prod fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.get? a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => none
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      bif k == a then some v else Std.DHashMap.Internal.AssocList.get? a es
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.CastMode.noConfusionType : Sort v✝ → Mathlib.Tactic.DepRewrite.CastMode → Mathlib.Tactic.DepRewrite.CastMode → Sort v✝
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.comp_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {n : WithTop ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) (x : M), (f.comp g) x = f (g x)
-- Mathlib.Data.List.Defs
/-- The last element of a list, with the default if list empty  -/
List.getLastI : {α : Type u_1} → [Inhabited α] → List α → α
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerTerm_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), PadicInt.mahlerTerm 1 n = mahler n
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.isoMk_inv_out : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget),
  (CategoryTheory.EnrichedFunctor.isoMk h).inv.out = h.inv
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  (Std.DTreeMap.filterMap f t).size = t.size ↔
    ∀ (k : α) (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Const.get t k h)).isSome = true
-- Init.Data.List.Erase
List.erase_eq_iff : ∀ {α : Type u_1} [inst : BEq α] {l' : List α} [LawfulBEq α] {a : α} {l : List α},
  l.erase a = l' ↔ a ∉ l ∧ l = l' ∨ ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂
-- Mathlib.Data.Nat.Choose.Factorization
/-- Modified version of `emultiplicity_le_emultiplicity_of_dvd_right`
but for factorization.  -/
Nat.factorization_le_factorization_of_dvd_right : ∀ {a b c : ℕ}, b ∣ c → b ≠ 0 → c ≠ 0 → b.factorization a ≤ c.factorization a
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- A presheaf `P` is a sheaf for the Grothendieck topology `J` iff for every covering sieve
`S` of `J`, the natural cone associated to `P` and `S` is a limit cone.  -/
CategoryTheory.Presheaf.isSheaf_iff_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J P ↔
    ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op))
-- Std.Do.SPred.DerivedLaws
ULift.down_dite : ∀ {α : Type u_1} {φ : Prop} [inst : Decidable φ] (t : φ → α) (e : ¬φ → α),
  (if h : φ then { down := t h } else { down := e h }).down = if h : φ then t h else e h
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f : A₀.a ⟶ A₁.a)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam)
  (f_1 : A₀.a ⟶ A₁.a)
  (h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f_1) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f_1)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam),
  ({ f := f, h := h } = { f := f_1, h := h_1 }) = (f = f_1)
-- Mathlib.Data.Nat.Prime.Basic
/-- If `p` is prime,
and `a` doesn't divide `p^k`, but `a` does divide `p^(k+1)`
then `a = p^(k+1)`.
 -/
Nat.eq_prime_pow_of_dvd_least_prime_pow : ∀ {a p k : ℕ}, Nat.Prime p → ¬a ∣ p ^ k → a ∣ p ^ (k + 1) → a = p ^ (k + 1)
-- Mathlib.Data.List.OfFn
List.get_ofFn : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (List.ofFn f).length), (List.ofFn f).get i = f (Fin.cast ⋯ i)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on a quantale are similar to the Heyting
operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ᵣ z ↔ y * x ≤ z` or alternatively `x ⇨ₗ y = sSup { z | x * z ≤ y }`.
 -/
Quantale.rightMulResiduation : {α : Type u_1} → [Semigroup α] → [CompleteLattice α] → α → α → α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).getKey! k = k
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `t` and a subset `s` of `t`, the product of `f i` over `i ∈ s`
times the product of `f i` over `t \ s` equals the product of `f i` over `i ∈ t`.  -/
finprod_mem_mul_sdiff : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t → t.Finite → (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.ringInst : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Expr
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- A variant of `IsValuativeTopology.mem_nhds_iff` using subtraction.  -/
IsValuativeTopology.mem_nhds_iff' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  {s : Set R} {x : R}, s ∈ nhds x ↔ ∃ γ, {z | (ValuativeRel.valuation R) (z - x) < ↑γ} ⊆ s
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The category of functors `WithInitial C ⥤ D` is equivalent to the category
`Comma (const C) (𝟭 (C ⥤ D))`.  -/
CategoryTheory.WithInitial.equivComma : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.WithInitial C) D ≌
          CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s t : Set α),
  ↑(lowerClosure s) + t = ↑(lowerClosure (s + t))
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpUniqueProd_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique α] (a : β), (LinearIsometryEquiv.withLpUniqueProd p 𝕜 α β).symm a = WithLp.toLp p (default, a)
-- Mathlib.CategoryTheory.Enriched.Opposite
CategoryTheory.forgetEnrichmentOppositeEquivalence_functor : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] (C : Type u) [inst_3 : CategoryTheory.EnrichedCategory V C],
  (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).functor =
    CategoryTheory.forgetEnrichmentOppositeEquivalence.functor V C
-- Init.Data.SInt.Lemmas
UInt16.toInt16_sub : ∀ (a b : UInt16), (a - b).toInt16 = a.toInt16 - b.toInt16
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} (p : P) {f : P ≃ᵃⁱ[ℝ] P},
  f s.center = s.center → AffineSubspace.map (↑f.toAffineEquiv) (s.orthRadius p) = s.orthRadius (f p)
-- Mathlib.Data.ENat.Basic
ENat.sub_sub_cancel : ∀ {a b : ℕ∞}, a ≠ ⊤ → b ≤ a → a - (a - b) = b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_inv`. -/
Equiv.Perm.SameCycle.of_inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f⁻¹.SameCycle x y → f.SameCycle x y
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_ne_eq_erase : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  DFinsupp.filter (fun x => x ≠ i) f = DFinsupp.erase i f
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.mk.sizeOf_spec : ∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toZeroHom : ZeroHom α β) (map_one' : toZeroHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y),
  sizeOf { toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } = 1 + sizeOf toZeroHom + sizeOf map_one'
-- Mathlib.Order.MinMax
/-- For elements `a` and `b` of a linear order, either `max a b = a` and `b ≤ a`,
or `max a b = b` and `a < b`.
Use cases on this lemma to automate linarith in inequalities  -/
max_cases : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b
-- Mathlib.RingTheory.Artinian.Ring
/-- [Stacks Tag 00J8](https://stacks.math.columbia.edu/tag/00J8) -/
IsArtinianRing.isNilpotent_jacobson_bot : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing R], IsNilpotent ⊥.jacobson
-- Mathlib.Topology.MetricSpace.Algebra
lipschitz_with_lipschitz_const_mul : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [inst_2 : LipschitzMul β] (p q : β × β),
  dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q
-- Mathlib.Data.NNReal.Defs
/-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`.  -/
Mathlib.Meta.Positivity.evalNNRealtoReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.mk.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (obj : C → D → Type w)
  (map : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj X Y' ⟶ obj X' Y))
  (map_id :
    autoParam
      (∀ (X : C) (Y : D),
        map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
          CategoryTheory.CategoryStruct.id (obj X Y))
      CategoryTheory.ProfunctorCore.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
        map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
          CategoryTheory.CategoryStruct.comp (map f g') (map f' g))
      CategoryTheory.ProfunctorCore.map_comp._autoParam),
  sizeOf { obj := obj, map := map, map_id := map_id, map_comp := map_comp } = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R),
  W'.negAddY P Q * (P 2 * Q 2) ^ 3 =
    (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) *
        (W'.addX P Q * (P 2 * Q 2) ^ 2 - P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) +
      P 1 * Q 2 ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3
-- Mathlib.Analysis.Normed.Group.Uniform
ZeroHomClass.bound_of_antilipschitz : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal},
  AntilipschitzWith K ⇑f → ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
-- Std.Http.Data.Headers.Basic
/-- The `Content-Length` header, representing the size of the message body in bytes.
Parses only valid natural number values.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-8.6-2
 -/
Std.Http.Header.ContentLength : Type
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGE! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_zero : ∀ {T : Type w} [inst : CommRing T] (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S],
  Polynomial.aroots 0 S = 0
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_intCast_le_one`.

---

The `v`-adic absolute value of an integer is `≤ 1`.  -/
NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℤ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.mvarId : Lean.Elab.Term.MVarErrorInfo → Lean.MVarId
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_eq_getElem_data : ∀ {a : ByteArray} {i : ℕ} {h : i < a.size}, a[i] = a.data[i]
-- Mathlib.Data.Multiset.MapFold
Multiset.induction_on_multiset_quot : ∀ {α : Type u_1} {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)),
  (∀ (s : Multiset α), p (Multiset.map (Quot.mk r) s)) → p s
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
derivWithin_comp_add_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (x + a)) s x = derivWithin f (a +ᵥ s) (x + a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.mkToIntVar : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
_private.Mathlib.Analysis.Complex.ValueDistribution.Cartan.0.ValueDistribution.logCounting_add_log_trailingCoeff_eq_circleAverage_add_logCounting_top : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    R ≠ 0 →
      ∀ (a : ℂ),
        ValueDistribution.logCounting f (↑a) R + Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖ =
          Real.circleAverage (fun x => Real.log ‖f x - a‖) 0 R + ValueDistribution.logCounting f ⊤ R
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- Special case of `submodule.liftQ` when `p` is the span of `x`. In this case, the condition on
`f` simply becomes vanishing at `x`.  -/
Submodule.liftQSpanSingleton : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {R₂ : Type u_3} →
            {M₂ : Type u_4} →
              [inst_3 : Ring R₂] →
                [inst_4 : AddCommGroup M₂] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} → (x : M) → (f : M →ₛₗ[τ₁₂] M₂) → f x = 0 → M ⧸ R ∙ x →ₛₗ[τ₁₂] M₂
-- Mathlib.CategoryTheory.Comma.Arrow
/-- **Alias** of `CategoryTheory.Arrow.w`. -/
CategoryTheory.Arrow.Hom.w : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g.hom =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X.PartialMap Y) (e_f : f = f_1) (U U_1 : X.Opens) (e_U : U = U_1)
  (hU : Dense ↑U) (hU' : U ≤ f.domain), f.restrict U hU hU' = f_1.restrict U_1 ⋯ ⋯
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult : Type
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instModuleQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Semiring S] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module S M] → (c : ModuleCon S M) → Module S (ModuleCon.Quotient M c)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D)
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C],
  CategoryTheory.HasExactColimitsOfShape J D
-- Lean.Parser.Basic
Lean.Parser.withResultOfInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.Order.Category.LinOrd
LinOrd.ofHom_comp : ∀ {X Y Z : Type u} [inst : LinearOrder X] [inst_1 : LinearOrder Y] [inst_2 : LinearOrder Z] (f : X →o Y) (g : Y →o Z),
  LinOrd.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (LinOrd.ofHom f) (LinOrd.ofHom g)
-- Std.Time.Date.Unit.Month
/-- Proves that every value provided by a clipDay is a valid day in a year.
 -/
Std.Time.Month.Ordinal.valid_clipDay : ∀ {leap : Bool} {month : Std.Time.Month.Ordinal} {day : Std.Time.Day.Ordinal},
  Std.Time.Month.Ordinal.Valid leap month (Std.Time.Month.Ordinal.clipDay leap month day)
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_atTop_of_Ioo_subset : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  s ⊆ Set.Iio b →
    (∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsSuccPrelimit b) map_coe_atTop_of_Ioo_subset._auto_1 →
        Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_or_lt_of_sub_lt_sub : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b c d : α},
  a - d < b - c → a < b ∨ c < d
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedCancelAddMonoid` under an injective map.  -/
Function.Injective.isOrderedCancelAddMonoid : ∀ {α : Type u} {β : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : Preorder β] (f : β → α),
  (∀ (x y : β), f (x + y) = f x + f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → IsOrderedCancelAddMonoid β
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- A Dyck word is a list of `DyckStep`s with as many `U`s as `D`s and with every prefix having
at least as many `U`s as `D`s.  -/
DyckWord : Type
-- Init.Data.Order.Ord
Std.OrientedCmp.isGE_eq_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp a b).isGE = (cmp b a).isLE
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).contains a = false