mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_subset_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t : Set β}, s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.hom_ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} {φ ψ : a ⟶ b},
  CategoryTheory.Functor.Fiber.fiberInclusion.map φ = CategoryTheory.Functor.Fiber.fiberInclusion.map ψ → φ = ψ
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- The `0`-th successor of `a` is `a` itself.  -/
Std.PRange.LawfulUpwardEnumerable.succMany?_zero : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.PRange.LawfulUpwardEnumerable α] (a : α),
  Std.PRange.succMany? 0 a = some a
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.index_embedding : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)), c.index ((c.embedding i) j) = i
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.toInt16? : Lean.FuzzyMatching.Score✝ → Option Int16
-- Mathlib.Tactic.Linarith.Frontend
/-- Specify an oracle for identifying candidate contradictions.
`.simplexAlgorithmSparse`, `.simplexAlgorithmSparse`, and `.fourierMotzkin` are available.  -/
Mathlib.Tactic.Linarith.LinarithConfig.oracle : Mathlib.Tactic.Linarith.LinarithConfig → Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The component called by the `rw??` tactic  -/
Mathlib.Tactic.LibraryRewrite.LibraryRewriteComponent : ProofWidgets.Component SelectInsertParams
-- Mathlib.Data.Finset.Finsupp
/-- Finitely supported product of finsets.  -/
Finset.finsupp : {ι : Type u_1} → {α : Type u_2} → [inst : Zero α] → Finset ι → (ι → Finset α) → Finset (ι →₀ α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.read : Lean.Lsp.DocumentHighlightKind
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions.mk.inj : ∀ {documentSelector? documentSelector?_1 : Option Lean.Lsp.DocumentSelector},
  { documentSelector? := documentSelector? } = { documentSelector? := documentSelector?_1 } →
    documentSelector? = documentSelector?_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.strictMono_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), StrictMono ⇑f.symm
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.coev_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app (A ⟹ B))
      ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) =
    CategoryTheory.CategoryStruct.id (A ⟹ B)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_iff_forall_connectedComponent : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n ↔ ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable n
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂},
  autoParam Φ.HasLeftResolutions
      CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.hasLeftResolutions._autoParam →
    CategoryTheory.TwoSquare.GuitartExact
        (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).inv →
      Φ.IsLeftDerivabilityStructure
-- Mathlib.Data.Int.Bitwise
Int.bodd_add : ∀ (m n : ℤ), (m + n).bodd = (m.bodd ^^ n.bodd)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonTextDocumentSyncOptions.toJson : Lean.Lsp.TextDocumentSyncOptions → Lean.Json
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (x : R),
  (DoubleQuot.quotQuotEquivComm I J) ((DoubleQuot.quotQuotMk I J) x) = (DoubleQuot.quotQuotMk J I) x
-- Mathlib.Data.Set.PowersetCard
/-- A variant of `Set.powersetCard.nontrivial` that uses `Nat.card`.  -/
Set.powersetCard.nontrivial' : ∀ {α : Type u_1} {n : ℕ}, 0 < n → n < Nat.card α → Nontrivial ↑(Set.powersetCard α n)
-- Mathlib.Order.FixedPoints
OrderHom.le_prevFixed_iff : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) {y : ↑(Function.fixedPoints ⇑f)},
  y ≤ f.prevFixed x hx ↔ ↑y ≤ x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toOpens_inf : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G}, ↑(U ⊓ V) = ↑U ⊓ ↑V
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIso_ιTruncLE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ), QuasiIso (K.ιTruncLE n) ↔ K.IsLE n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.span_singleton_one : ∀ {A : Type u_3} [inst : Ring A] (I : Ideal A) [I.IsTwoSided], A ∙ 1 = ⊤
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α} {r' : α → β → Prop},
  SemicontinuousWithinAt r s x → SemicontinuousWithinAt r' s x → SemicontinuousWithinAt (r ⊔ r') s x
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : J.WEqualsLocallyBijective A]
  (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A)
  [inst_5 : CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A))
  [J.HasSheafCompose (CategoryTheory.forget A)],
  CategoryTheory.Epi ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).i.app f)
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.mapToSelf.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (xs : List ((_ : α) × α)) (a : (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs))
  (a_1 : (List.map Sigma.snd xs).Nodup),
  sizeOf (Plausible.InjectiveFunction.mapToSelf xs a a_1) = 1 + sizeOf xs + sizeOf a + sizeOf a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k k' : α},
  t.WF → (t.getKey? k = some k' ↔ ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), t.getKey k h = k')
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Icc : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R},
  0 ≤ b → Nat.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitAux_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)),
  (CategoryTheory.OverPresheafAux.counitAux F).hom =
    { app := fun X => TypeCat.ofHom (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop X)),
      naturality := ⋯ }
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isBasis_iff_empty_of_subset_loops : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, X ⊆ M.loops → (M.IsBasis I X ↔ I = ∅)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  (M₀ : PresheafOfModules R₀),
  (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationAdjunction α).unit.app M₀) =
    CategoryTheory.toSheafify J M₀.presheaf
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_eq_iff : ∀ {k : ℕ} {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size},
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst = k ↔
    k ≤ stackPos ∧
      String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k (stackPos + 1) ∧
        ∀ (k' : ℕ),
          k < k' →
            k' ≤ stackPos → ¬String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k' (stackPos + 1)
-- Mathlib.Algebra.GroupWithZero.Basic
pow_eq_zero_of_le : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {m n : ℕ}, m ≤ n → a ^ m = 0 → a ^ n = 0
-- Mathlib.Tactic.Explode.Datatypes
/-- How many `if`s (aka lambda-abstractions) this row is nested under.  -/
Mathlib.Explode.Entry.depth : Mathlib.Explode.Entry → ℕ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]` and `Πʳ (j : ι₂), [R₂ j, A₂ j]_[𝓕₂]`,
`RestrictedProduct.mapAlong` gives a function between them. The data needed is a
function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and functions `φ j : R₁ (f j) → R₂ j`
sending `A₁ (f j)` into `A₂ j` for an `𝓕₂`-large set of `j`'s.

See also `mapAlongMonoidHom`, `mapAlongAddMonoidHom` and `mapAlongRingHom` for variants.
 -/
RestrictedProduct.mapAlong : {ι₁ : Type u_3} →
  {ι₂ : Type u_4} →
    (R₁ : ι₁ → Type u_5) →
      (R₂ : ι₂ → Type u_6) →
        {𝓕₁ : Filter ι₁} →
          {𝓕₂ : Filter ι₂} →
            {A₁ : (i : ι₁) → Set (R₁ i)} →
              {A₂ : (i : ι₂) → Set (R₂ i)} →
                (f : ι₂ → ι₁) →
                  Filter.Tendsto f 𝓕₂ 𝓕₁ →
                    (φ : (j : ι₂) → R₁ (f j) → R₂ j) →
                      (∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)) →
                        RestrictedProduct (fun i => R₁ i) (fun i => A₁ i) 𝓕₁ →
                          RestrictedProduct (fun j => R₂ j) (fun j => A₂ j) 𝓕₂
-- Mathlib.Algebra.Algebra.StrictPositivity
IsUnit.isStrictlyPositive_star_right_conjugate_iff : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A] {u a : A},
  IsUnit u → (IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a)
-- Init.Data.Int.DivMod.Lemmas
Int.eq_zero_of_ediv_eq_zero : ∀ {d n : ℤ}, d ∣ n → n / d = 0 → n = 0
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.Iic_chainBotCoeff_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    Set.Iic (RootPairing.chainBotCoeff i j) = {k | P.root j - k • P.root i ∈ Set.range ⇑P.root}
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  hζ.integralPowerBasisOfPrimePow.gen = hζ.toInteger
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : Inhabited α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.le_tsub_iff_le_tsub : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable a → AddLECancellable c → a ≤ b → c ≤ b → (a ≤ b - c ↔ c ≤ b - a)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.base_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C}
  {f : Y ⟶ X} {S : J.Cover X} (I : (S.pullback f).Arrow), I.base.f = CategoryTheory.CategoryStruct.comp I.f f
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.id_onFunction : ∀ (L : FirstOrder.Language) (_n : ℕ) (a : L.Functions _n), (FirstOrder.Language.LHom.id L).onFunction a = id a
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If `minSmoothness 𝕜 m ≤ n` for some (finite) integer `m`, then one can
find `n' ∈ [minSmoothness 𝕜 m, n]` which is not `∞`: over `ℝ` or `ℂ`, just take `m`, and otherwise
just take `ω`. The interest of this technical lemma is that, if a function is `C^{n'}` at a point
for `n' ≠ ∞`, then it is `C^{n'}` on a neighborhood of the point (this property fails only
in `C^∞` smoothness, see `ContDiffWithinAt.contDiffOn`).  -/
exist_minSmoothness_le_ne_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {m : ℕ},
  minSmoothness 𝕜 ↑m ≤ n → ∃ n', minSmoothness 𝕜 ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ↑⊤
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedAddOfLipschitzAdd : ∀ {R : Type u_1} [inst : PseudoMetricSpace R] [inst_1 : AddMonoid R] [LipschitzAdd R], BoundedAdd R
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `lTensor A g : A ⊗ B →ₐ A ⊗ D` is the natural algebra morphism induced by `g : B →ₐ D`.  -/
Algebra.TensorProduct.lTensor : {R : Type uR} →
  {S : Type uS} →
    (A : Type uA) →
      {B : Type uB} →
        {D : Type uD} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring D] →
                              [inst_10 : Algebra R D] → (B →ₐ[R] D) → TensorProduct R A B →ₐ[S] TensorProduct R A D
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_eq_coverEntropy : ∀ {X : Type u_1} {F : Set X} [inst : UniformSpace X] (T : X → X),
  Set.MapsTo T F F → Dynamics.coverEntropyInf T F = Dynamics.coverEntropy T F
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.denote_map : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α}
  (target : Std.Sat.AIG.RefVec.MapTarget aig len) (idx : ℕ) (hidx : idx < len),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.map aig target).aig, ref := (Std.Sat.AIG.RefVec.map aig target).vec.get idx hidx }⟧ =
    ⟦assign, target.func aig (target.vec.get idx hidx)⟧
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.instInhabitedBiconeHomLeft : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    Inhabited (CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left)
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProdProj_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} {a : (F.obj A).obj},
  (CategoryTheory.ConcreteCategory.hom (F.map u)) a = CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X →
    ∀ (x : (F.obj X).obj),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.PreGaloisCategory.selfProdProj✝ u x))) a = x
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- The Riesz measure induced by a linear functional on `C_c(X, ℝ≥0)` is regular.  -/
NNRealRMK.rieszMeasure_regular : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal),
  (NNRealRMK.rieszMeasure Λ).Regular
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonCompletionItemCapabilities : Lean.FromJson Lean.Lsp.CompletionItemCapabilities
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.support_singularValues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), T.singularValues.support = Finset.range (Module.finrank 𝕜 ↥T.range)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.foldlM : {m : Type w → Type w'} →
  [Monad m] →
    {σ : Type w} →
      {α : Type u_1} →
        {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (σ → α → β → m σ) → σ → m σ
-- Init.Data.Option.Lemmas
Option.pbind_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  o.pbind f = none ↔ o = none ∨ ∃ a, ∃ (h : o = some a), f a h = none
-- Mathlib.MeasureTheory.Group.Pointwise
MeasurableSet.const_smul₀ : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Zero α] [inst_2 : MulActionWithZero G₀ α]
  [inst_3 : MeasurableSpace α] [MeasurableConstSMul G₀ α] [MeasurableSingletonClass α] {s : Set α},
  MeasurableSet s → ∀ (a : G₀), MeasurableSet (a • s)
-- Mathlib.CategoryTheory.Thin
/-- Construct a category instance from a `CategoryStruct`, using the fact that
hom spaces are subsingletons to prove the axioms.  -/
CategoryTheory.thin_category : {C : Type u₁} →
  [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] → [Quiver.IsThin C] → CategoryTheory.Category.{v₁, u₁} C
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_iff_subset_iUnion_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, Metric.closedBall y ↑ε
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.eq_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ {m : ℕ}, ↑m ≤ n → ∀ (x : E), p x m = iteratedFDeriv 𝕜 m f x
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- The trivial comonoid on the unit object is commutative.  -/
CategoryTheory.CommComon.instCommComonObjUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_lt_subst : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (x : Lean.Grind.Linarith.Var) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_lt_subst_cert x p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ < 0
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) (x : E), ↑f x = (someContDiffBumpBase E).toFun (f.rOut / f.rIn) (f.rIn⁻¹ • (x - c))
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_insert : ∀ (ctx : Nat.Internal.Linear.Context) (k : ℕ) (v : Nat.Internal.Linear.Var) (p : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx (Nat.Internal.Linear.Poly.insert k v p) =
    Nat.Internal.Linear.Poly.denote ctx p + k * Nat.Internal.Linear.Var.denote ctx v
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
/-- https://mathoverflow.net/questions/511862/transpose-symmetry-of-injectivity-of-linear-maps-over-semirings
asks whether this is still true without `IsCancelAdd R`.  -/
Matrix.linearIndependent_col_iff_row : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] {A : Matrix n n R} [IsCancelAdd R] [Finite n],
  LinearIndependent R A.col ↔ LinearIndependent R A.row
-- Batteries.Data.Array.Scan
Subarray.scanr_eq_scanr_extract : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Subarray α},
  Subarray.scanr f init as = Array.scanr f init (as.array.extract as.stop as.start)
-- Std.Time.DateTime
/-- The plain datetime component, evaluated lazily.
 -/
Std.Time.DateTime.date : Std.Time.DateTime → Thunk Std.Time.PlainDateTime
-- Mathlib.Analysis.Complex.Trigonometric
/-- The definition of `cosh` in terms of `exp`.  -/
Real.cosh_eq : ∀ (x : ℝ), Real.cosh x = (Real.exp x + Real.exp (-x)) / 2
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coneLeftOpOfCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J Cᵒᵖ} → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cone F.leftOp
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.instInhabited : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → Inhabited (CategoryTheory.Pseudofunctor B B)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_keys_iff_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α},
  k ∈ Std.Internal.List.keys l ↔ Std.Internal.List.containsKey k l = true
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- The canonical maps `F.obj j → F.ColimitType`.  -/
CategoryTheory.Functor.ιColimitType : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J (Type w₀)) → (j : J) → F.obj j → F.ColimitType
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_add_one`. -/
SimpleGraph.set_walk_length_succ_eq : ∀ {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ),
  {p | p.length = n + 1} = ⋃ w, ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' | p'.length = n}
-- Mathlib.Topology.Constructions
Continuous.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), Continuous (f i)) → Continuous (Pi.map f)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.map_iff_of_injective : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {k : ℕ} {ζ : M} {f : F}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N],
  Function.Injective ⇑f → (IsPrimitiveRoot (f ζ) k ↔ IsPrimitiveRoot ζ k)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.hom_ext₀ : ∀ {X : SSet} {f g : (SSet.boundary 0).toSSet ⟶ X}, f = g
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsSeparator (Opposite.op G) ↔ CategoryTheory.IsCoseparator G