mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤),
  AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf =
    AlgebraicGeometry.Scheme.Cover.glueMorphisms (AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop 𝒜 f hf)
      (fun ri =>
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯)
          (AlgebraicGeometry.Proj.basicOpen 𝒜 ri.snd.fst).ι)
      ⋯
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J) (x : ↑(F.obj j)),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (-x)) (RingCat.Colimits.Prequotient.of j x).neg
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow : ∀ {E : Type u_2} [inst : SeminormedRing E] (a b c : ℝ) {f g : ℝ → E},
  (f =O[Filter.atTop] fun t => t ^ a) →
    (g =O[Filter.atTop] fun t => t ^ b) → a + b ≤ c → (f * g) =O[Filter.atTop] fun t => t ^ c
-- Mathlib.Algebra.Polynomial.Inductions
/-- An induction principle for polynomials, valued in Sort* instead of Prop.  -/
Polynomial.recOnHorner : {R : Type u} →
  [inst : Semiring R] →
    {M : Polynomial R → Sort u_1} →
      (p : Polynomial R) →
        M 0 →
          ((p : Polynomial R) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + Polynomial.C a)) →
            ((p : Polynomial R) → p ≠ 0 → M p → M (p * Polynomial.X)) → M p
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierCLM_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourier E F] (f : E), (FourierTransform.fourierCLM R E) f = FourierTransform.fourier f
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MkMor₂.mk : {m : Type → Type} → (Lean.Expr → m Mathlib.Tactic.BicategoryLike.Mor₂) → Mathlib.Tactic.BicategoryLike.MkMor₂ m
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.isCommRing : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Init.Data.List.Impl
/-- Alternates the lists in `xs` with the separator `sep`.

This is a tail-recursive version of `List.intercalate` used at runtime.

Examples:
* `List.intercalateTR sep [] = []`
* `List.intercalateTR sep [a] = a`
* `List.intercalateTR sep [a, b] = a ++ sep ++ b`
* `List.intercalateTR sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`
 -/
List.intercalateTR : {α : Type u_1} → List α → List (List α) → List α
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_perm_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] (k : α) (v : β k) {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.insertEntry k v l).Perm (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) l)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.MonoidalCategory.tensoringRight_ε : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalCategory.tensoringRight C) =
    (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} {le : LE β} {x : DecidableLE β} {f : α → β} {xs : List α} {h : xs ≠ []},
  List.maxIdxOn f xs h = List.minIdxOn f xs h
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.brecOn.go : {α : Type u} →
  {motive : Batteries.PairingHeapImp.Heap α → Sort u_1} →
    (t : Batteries.PairingHeapImp.Heap α) →
      ((t : Batteries.PairingHeapImp.Heap α) → Batteries.PairingHeapImp.Heap.below t → motive t) →
        motive t ×' Batteries.PairingHeapImp.Heap.below t
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A bilinear form `B` is **nonnegative** if for any `x` we have `0 ≤ B x x`.  -/
LinearMap.BilinForm.IsNonneg : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [LE R] → LinearMap.BilinForm R M → Prop
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.braiding_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C), (β_ G H).inv.hom.hom = (β_ G.X H.X).inv
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
/-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are sets of vertices such
that each pair is `ε`-uniform and `2 * ε`-dense, then a proportion of at least
`(1 - 2 * ε) * ε ^ 3` of the triples `(a, b, c) ∈ s × t × u` are triangles.  -/
SimpleGraph.triangle_counting' : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α},
  2 * ε ≤ ↑(G.edgeDensity s t) →
    G.IsUniform ε s t →
      2 * ε ≤ ↑(G.edgeDensity s u) →
        G.IsUniform ε s u →
          2 * ε ≤ ↑(G.edgeDensity t u) →
            G.IsUniform ε t u →
              (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤
                ↑{x ∈ s ×ˢ t ×ˢ u |
                      match x with
                      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}.card
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `(a, +∞)` and continuity at `a⁺`.  -/
MeasureTheory.integrableOn_Ioi_deriv_of_nonneg : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  ContinuousWithinAt g (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, 0 ≤ g' x) →
        Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- The walk `p` transferred to lie in `H`, given that `H` contains its edges.  -/
SimpleGraph.Walk.transfer : {V : Type u} →
  {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → (H : SimpleGraph V) → (∀ e ∈ p.edges, e ∈ H.edgeSet) → H.Walk u v
-- Mathlib.Computability.RecursiveIn
ComputableIn.sumInl : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {O : Set (ℕ →. ℕ)},
  ComputableIn O Sum.inl
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `A` is free as `R`-module.
For any subalgebra `S` of `B`, the centralizer of `1 ⊗ S ⊆ A ⊗ B` is `A ⊗ C_B(S)` where `C_B(S)` is
the centralizer of `S` in `B`.
 -/
Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R B) [Module.Free R A],
  Subalgebra.centralizer R ↑(Subalgebra.map Algebra.TensorProduct.includeRight S) =
    (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R ↑S).val).range
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz_refl : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) (hK1 hK2 : 0 < 1)
  (hA : AntilipschitzWith 1 ⇑(Equiv.refl X)) (hL : LipschitzWith 1 ⇑(Equiv.refl X)),
  Delone.DeloneSet.mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_of_isSlice : ∀ {ι : Type u_1} [Finite ι] {s : Set (ι → ℕ)}, IsSlice✝ s → IsSemilinearSet s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.resultType : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.Expr
-- Mathlib.Data.Set.Restrict
Set.range_domRestrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.range (s.domRestrict f) = f '' s
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- All `x : K` can be written as `n / d` or `d / n` with `n : R` and `d ∈ v.asIdealᶜ`.  -/
IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K] [inst_3 : Algebra R K]
  [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K),
  ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
-- Lean.Meta.Tactic.Subst
Lean.Meta.subst : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = false →
    ∀ {fallback : α},
      (t.alter k f).minKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.replicate.eq_1 : ∀ {α : Type u_1} (n : ℕ) (a : α), Multiset.replicate n a = ↑(List.replicate n a)
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.Raw.getD : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [Hashable α] → [LawfulBEq α] → Std.DHashMap.Raw α β → (a : α) → β a → β a
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_choose_prime_pow : ∀ {p n k : ℕ}, Nat.Prime p → k ≤ p ^ n → k ≠ 0 → ((p ^ n).choose k).factorization p = n - k.factorization p
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_closedBall_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} * Metric.closedBall 1 δ = Metric.closedBall x δ
-- Std.Http.Server
/-- Configuration of the server
 -/
Std.Http.Server.config : Std.Http.Server → Std.Http.Config
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : S →+* MvPolynomial σ T) (g : R →+* S) (φ : MvPolynomial σ R),
  (MvPolynomial.bind₂ f) ((MvPolynomial.map g) φ) = (MvPolynomial.bind₂ (f.comp g)) φ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.instEssSurjUnderToUnder : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T) [F.EssSurj], (CategoryTheory.StructuredArrow.toUnder X F).EssSurj
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.eval₂ : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
-- Mathlib.Algebra.Group.Irreducible.Lemmas
not_irreducible_pow : ∀ {M : Type u_2} [inst : Monoid M] {x : M} {n : ℕ}, n ≠ 1 → ¬Irreducible (x ^ n)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.coe_copy : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K)
  (f' : E → F) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_sub_right : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] {f : G → F} [μ.IsAddRightInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (t - g)) μ
-- Mathlib.Algebra.Polynomial.Coeff
/-- `Polynomial.sum` as a linear map.  -/
Polynomial.lsum : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R A] → [inst_4 : Module R M] → (ℕ → A →ₗ[R] M) → Polynomial A →ₗ[R] M
-- Mathlib.Order.Lattice
Monotone.of_le_map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  (∀ (x y : α), f x ⊔ f y ≤ f (x ⊔ y)) → Monotone f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_union_of_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ∏'[L] (x : β), 1 = 1
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mk : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] →
              {ρ : Representation A G W} →
                (toSubmodule : Submodule A W) →
                  (∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule → (ρ g) v ∈ toSubmodule) → Subrepresentation ρ
-- Mathlib.Topology.Inseparable
specializes_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), x ⤳ x
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
mul_mem_upperBounds_mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} {a b : M},
  a ∈ upperBounds s → b ∈ upperBounds t → a * b ∈ upperBounds (s * t)
-- Mathlib.Geometry.Manifold.SmoothApprox
Continuous.exists_contDiff_approx_and_eqOn : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {ε : E → ℝ} (n : ℕ∞),
  Continuous f →
    Continuous ε →
      (∀ (x : E), 0 < ε x) →
        ∀ {S U : Set E},
          IsClosed S →
            U ∈ nhdsSet S →
              ContDiffOn ℝ (↑n) f U →
                ∃ g,
                  ContDiff ℝ (↑n) g ∧
                    (∀ (x : E), dist (g x) (f x) < ε x) ∧ Set.EqOn g f S ∧ Function.support g ⊆ Function.support f
-- Mathlib.Order.Defs.Unbundled
Std.Asymm.irrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Asymm r], Std.Irrefl r
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.mk.injEq : ∀ (toBoolAlg : BoolAlg) [isFintype : Fintype ↑toBoolAlg] (toBoolAlg_1 : BoolAlg) (isFintype_1 : Fintype ↑toBoolAlg_1),
  ({ toBoolAlg := toBoolAlg, isFintype := isFintype } = { toBoolAlg := toBoolAlg_1, isFintype := isFintype_1 }) =
    (toBoolAlg = toBoolAlg_1 ∧ isFintype ≍ isFintype_1)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedCommRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'},
  (∀ i ∈ t, MDiffAt[s] (f i) z) → MDiffAt[s] (∏ i ∈ t, f i) z
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.corootForm_self_smul_root : ∀ {ι : 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) [inst_5 : Fintype ι]
  (i : ι), (P.CorootForm (P.coroot i)) (P.coroot i) • P.root i = 2 • P.CoPolarization (P.coroot i)
-- Mathlib.Order.Monotone.Monovary
StrictMono.trans_monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : PartialOrder ι], StrictMono f → Monovary g f → Monotone g
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.drop.match_1.splitter : (motive : Substring.Raw → ℕ → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : ℕ) →
      ((s : String) → (b e : String.Pos.Raw) → (n : ℕ) → motive { str := s, startPos := b, stopPos := e } n) →
        motive x x_1
-- Std.Data.ExtTreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtTreeMap.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → Option β × Std.ExtTreeMap α β cmp
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.comp_neg_int : ∀ {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : ℤ → E} {g : ℤ → F},
  f =O[Filter.cofinite] g → (fun n => f (-n)) =O[Filter.cofinite] fun n => g (-n)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.add_const : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableAdd M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => f x + c) μ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instModule : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → {S : NonUnitalSubalgebra R A} → Module R ↥S
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.get! a = t_1.get! a_1
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_le_iff : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] {r : NNReal} {A : Matrix m n α}, ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
-- Mathlib.Probability.Kernel.Category.SFinKer
/-- The underlying morphism.  -/
SFinKer.Hom.hom : {X Y : SFinKer} → X.Hom Y → ProbabilityTheory.Kernel X.carrier Y.carrier
-- Mathlib.Logic.Encodable.Basic
/-- If `α` and `β` are encodable, then so is their product.  -/
Encodable.Prod.encodable : {α : Type u_1} → {β : Type u_2} → [Encodable α] → [Encodable β] → Encodable (α × β)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const.instIsMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β}
  [hμβ : MeasureTheory.IsProbabilityMeasure μβ], ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.const α μβ)
-- Init.Data.List.Count
List.count_erase_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α},
  a ≠ b → ∀ {l : List α}, List.count a (l.erase b) = List.count a l
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C},
  CategoryTheory.CartesianMonoidalCategory.prodComparison (CategoryTheory.Functor.id C) A B =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instCompleteLattice.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  SaturatedSubmonoid.instCompleteLattice M =
    { toPartialOrder := inferInstance, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := Lattice.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (Submonoid.giSaturation M).liftCompleteLattice.toSupSet, isLUB_sSup := ⋯,
      toInfSet := inferInstance.toInfSet, isGLB_sInf := ⋯, toTop := inferInstance, le_top := ⋯,
      toOrderBot := (Submonoid.giSaturation M).liftCompleteLattice.toOrderBot }
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.of.sizeOf_spec : ∀ (carrier : Type u) [str : UniformSpace carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Group.Defs
npowRec.eq_1 : ∀ {M : Type u_1} [inst : One M] [inst_1 : Mul M] (x : M), npowRec 0 x = 1
-- Mathlib.Analysis.Complex.Exponential
Real.exp_multiset_sum : ∀ (s : Multiset ℝ), Real.exp s.sum = (Multiset.map Real.exp s).prod
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_apply : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : σ →₀ R), (Finsupp.weight w) f = f.sum fun i c => c • w i
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R 1 = Polynomial.X
-- Mathlib.Data.Nat.Cast.Basic
MonoidWithZeroHom.ext_nat : ∀ {A : Type u_3} [inst : MulZeroOneClass A] {f g : ℕ →*₀ A}, (∀ {n : ℕ}, 0 < n → f n = g n) → f = g
-- Mathlib.Computability.Primrec.List
/-- `List.drop` is primitive recursive.  -/
Primrec.list_drop : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ List.drop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α}
  {k : α} {h : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k h = ()
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_irreflexive : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.irreflexive ↔ Std.Irrefl fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instHomIsOverInvAsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] {f : X ⟶ Y} [inst_3 : CategoryTheory.IsIso f] [CategoryTheory.HomIsOver f S],
  CategoryTheory.HomIsOver (CategoryTheory.asIso f).inv S
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The map `S → T` when `S` is a non-unital star subalgebra contained in the non-unital star
algebra `T`.

This is the non-unital star subalgebra version of `Submodule.inclusion`, or
`NonUnitalSubalgebra.inclusion`  -/
NonUnitalStarSubalgebra.inclusion : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : StarRing A] → [inst_3 : Module R A] → {S T : NonUnitalStarSubalgebra R A} → S ≤ T → ↥S →⋆ₙₐ[R] ↥T
-- Mathlib.RingTheory.SurjectiveOnStalks
RingEquiv.surjectiveOnStalks : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.SurjectiveOnStalks
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ}, Γ = Δ ↔ ∀ (a : B), Γ.as.app a = Δ.as.app a