mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsPreprimitive.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] [toIsPretransitive : MulAction.IsPretransitive G X],
  (∀ {B : Set X}, MulAction.IsBlock G B → MulAction.IsTrivialBlock B) → MulAction.IsPreprimitive G X
-- Mathlib.Topology.Spectral.Hom
SpectralMap.coe_comp_continuousMap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β), ⇑f ∘ ⇑g = ⇑↑f ∘ ⇑↑g
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_f' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsRelIff] {i : ι} {i' : ι'}
  (hi : e.f i = i'),
  (HomologicalComplex.restrictionMap φ e).f i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (φ.f i') (L.restrictionXIso e hi).inv)
-- Mathlib.Util.Notation3
/-- A fold variable, use the fold state (do not reverse the array).  -/
Mathlib.Notation3.BoundValueType.foldr : Mathlib.Notation3.BoundValueType
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.CommGrpCat.Hom.mk.sizeOf_spec : ∀ {A B : CommGrpCat} (hom' : ↑A →* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_vadd_eball`. -/
EMetric.preimage_vadd_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), (fun x => c +ᵥ x) ⁻¹' Metric.eball x r = Metric.eball (-c +ᵥ x) r
-- Mathlib.Data.Set.Prod
Set.prod_inter_prod : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
-- Mathlib.LinearAlgebra.LinearPMap
/-- Projection to the first coordinate as a `LinearPMap`  -/
LinearPMap.fst : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} →
            [inst_3 : AddCommGroup F] → [inst_4 : Module R F] → Submodule R E → Submodule R F → E × F →ₗ.[R] E
-- Mathlib.Data.Set.Function
Set.RightInvOn.surjOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.RightInvOn f' f t → Set.MapsTo f' t s → Set.SurjOn f s t
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Ioi : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b : M), (fun x => x + a) '' Set.Ioi b = Set.Ioi (b + a)
-- Aesop.Search.Main
Aesop.finishIfProven : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Bool
-- Mathlib.Probability.Distributions.Pareto
/-- The pdf of the Pareto distribution, as a function valued in `ℝ≥0∞`.  -/
ProbabilityTheory.paretoPDF : ℝ → ℝ → ℝ → ENNReal
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_exp : Measurable Real.exp
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- The structure containing the data of a functorial factorization of morphisms as
a surjective map followed by an injective map in a concrete category.  -/
CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] → [CategoryTheory.ConcreteCategory C FC] → Type (max u v)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_neg : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Ring R] (v : AbsoluteValue R S)
  (x : WithAbs v), (-x).ofAbs = -x.ofAbs
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.hasColimits : CategoryTheory.Limits.HasColimits AlgebraicGeometry.AffineScheme
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- The natural maps `Xᵢ ⟶ Uᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (self : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) →
          self.functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.alter₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {f : Option (β a) → Option (β a)},
  m.WF → (↑(Std.DHashMap.Internal.Raw₀.alter ⟨m, h⟩ a f)).WF
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it' it : Std.Iter α},
  it'.IsPlausibleSuccessorOf it ↔
    ∃ a,
      it.internalState.next = some a ∧
        a < it.internalState.upperBound ∧
          Std.PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
-- Std.Async.Process
Std.IO.Process.PId.mk.inj : ∀ {toUInt64 toUInt64_1 : UInt64}, { toUInt64 := toUInt64 } = { toUInt64 := toUInt64_1 } → toUInt64 = toUInt64_1
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.mk : Array Lean.Expr → Lean.LocalContext → Lean.LocalInstances → Option Lean.Expr → Lean.Elab.Term.FunBinders.State
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_right_mem_zero : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {i : ι} [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜] {a b : A},
  b ∈ 𝒜 0 → ↑(((DirectSum.decompose 𝒜) (a * b)) i) = ↑(((DirectSum.decompose 𝒜) a) i) * b
-- Mathlib.MeasureTheory.Measure.Map
/-- The pushforward of a measure as a linear map. It is defined to be `0` if `f` is not
a measurable function.  -/
MeasureTheory.Measure.mapₗ : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → (α → β) → MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure β
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = { toSupHom := f.copy f' h, map_bot' := ⋯ }
-- Std.Http.Data.Headers.Basic
/-- Parses a `Host` header value.
 -/
Std.Http.Header.Host.parse : Std.Http.Header.Value → Option Std.Http.Header.Host
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild : Lean.Expr →
  ℕ → (Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)) → Lean.Meta.Sym.M✝ Lean.Expr
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α σ : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  (Std.Do.wp (MonadLift.monadLift x)).apply Q = fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)
-- Std.Sync.Mutex
/-- Creates a new `BaseMutex`.  -/
Std.BaseMutex.new : BaseIO Std.BaseMutex
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationLeftAdjoint_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (d : D) (t : C),
  ((CategoryTheory.evaluationLeftAdjoint D c).obj d).obj t = ∐ fun x => d
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension : Type → Type → Type
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits, then `F : C ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.instHomotopyLike : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop}, ContinuousMap.HomotopyLike (f₀.HomotopyWith f₁ P) f₀ f₁
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {ι' : Type u_5}
  {g : ι' → ι},
  Function.Injective g → ProbabilityTheory.Kernel.iIndep m κ μ → ProbabilityTheory.Kernel.iIndep (m ∘ g) κ μ
-- Mathlib.GroupTheory.OrderOfElement
exists_orderOf_eq_prime_pow_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)],
  (∃ k, orderOf x = p ^ k) ↔ ∃ m, x ^ p ^ m = 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousSub : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G],
  ContinuousSub (SeparationQuotient G)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective : ∀ {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]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)],
  CategoryTheory.Presheaf.IsLocallySurjective J f₂
-- Mathlib.Topology.Instances.RealVectorSpace
/-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear.  -/
map_real_smul : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {F : Type u_2} [inst_4 : AddCommGroup F] [inst_5 : Module ℝ F] [inst_6 : TopologicalSpace F] [ContinuousSMul ℝ F]
  [T2Space F] {G : Type u_3} [inst_9 : FunLike G E F] [AddMonoidHomClass G E F] (f : G),
  Continuous ⇑f → ∀ (c : ℝ) (x : E), f (c • x) = c • f x
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.even_card_of_char_two : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F], ringChar F = 2 → Fintype.card F % 2 = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The universal morphism from the profinite completion to `P`.  -/
ProfiniteGrp.ProfiniteCompletion.lift : {G : GrpCat} →
  {P : ProfiniteGrp.{u}} → (G ⟶ GrpCat.of ↑P.toProfinite.toTop) → (ProfiniteGrp.ProfiniteCompletion.completion G ⟶ P)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.truncGE a ⟶ t.truncGE b` when `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE : {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) → (a b : ℤ) → a ≤ b → (t.truncGE a ⟶ t.truncGE b)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.instFromJsonOptions.fromJson : Lean.Json → Except String Lean.Lsp.DeleteFile.Options
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestImpl.eval : Lean.TSyntax `tactic →
  Lean.Elab.Tactic.SavedState →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Try.TryTactic) →
      Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_smul_top_le : ∀ (R : Type u_1) [inst : Ring R] (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Ring.jacobson R • ⊤ ≤ Module.jacobson R M
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction.parseAdd : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- When `M` is a `B`-module in `D` and `f : A ⟶ B` is a morphism of internal
monoid objects, `M` inherits an `A`-module structure via
"restriction of scalars", i.e `γ[A, M] = f ⊵ₗ M ≫ γ[B, M]`.  -/
CategoryTheory.Mod.scalarRestriction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                [inst_5 : CategoryTheory.MonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsMonHom f] → (M : D) → [CategoryTheory.ModObj B M] → CategoryTheory.ModObj A M
-- Mathlib.FieldTheory.Galois.Profinite
finGaloisGroupMap.map_id : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L : (FiniteGaloisIntermediateField k K)ᵒᵖ),
  finGaloisGroupMap (CategoryTheory.CategoryStruct.id L) =
    CategoryTheory.CategoryStruct.id (Opposite.unop L).finGaloisGroup
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.le_log_of_opow_le : ∀ {b x c : Ordinal.{u_1}}, 1 < b → b ^ c ≤ x → c ≤ Ordinal.log b x
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.Category.assoc' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y),
  CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g) f
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapComp_inv_app : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↑Z),
  (TopologicalSpace.Opens.mapComp f g).inv.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_snd_assoc : ∀ (X : SSet) {Z : SSet} (h : SSet.stdSimplex.obj { len := 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (SSet.stdSimplex.obj { len := 1 })) h) =
    CategoryTheory.CategoryStruct.comp (SSet.const (SSet.stdSimplex.obj₀Equiv.symm 0)) h
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.failedAssign : Lean.Meta.Simp.DischargeResult
-- Mathlib.Data.List.Rotate
List.mem_cyclicPermutations_iff : ∀ {α : Type u} {l l' : List α}, l ∈ l'.cyclicPermutations ↔ l ~r l'
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ext : ∀ {X Y : CommMonCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableWithinAt_section_of_subsingleton : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {u : Set B}
  {x : B} [Subsingleton F], MDiffAt[u] (T% s) x
-- Lean.Meta.Tactic.Grind.LawfulEqCmp
_private.Lean.Meta.Tactic.Grind.LawfulEqCmp.0.Lean.Meta.Grind.getLawfulEqCmpThm?.go? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- A different version of the (C) → (T) implication of the portmanteau theorem:
If the set of measures is tight, a `limsup` inequality for compact sets implies weak convergence.  -/
MeasureTheory.tendsto_of_forall_isCompact_of_isTightMeasureSet : ∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  MeasureTheory.IsTightMeasureSet (Set.range (MeasureTheory.ProbabilityMeasure.toMeasure ∘ μs)) →
    (∀ (F : Set Ω), IsCompact F → Filter.limsup (fun x => (μs x) F) L ≤ μ F) → Filter.Tendsto μs L (nhds μ)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) AlgebraicGeometry.Scheme.Spec
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- If `t` is a weak limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such
that `h ≫ f = k ≫ g`, then we get `l : W ⟶ t.pt`, which satisfies `l ≫ fst t = h`
and `l ≫ snd t = k`, see `IsWeakLimit.lift_fst` and `IsWeakLimit.lift_snd`.  -/
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsWeakLimit t →
              {W : C} →
                (h : W ⟶ X) →
                  (k : W ⟶ Y) →
                    CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g → (W ⟶ t.pt)
-- Mathlib.Order.OrderDual
OrderDual.instPartialOrder : (α : Type u_2) → [PartialOrder α] → PartialOrder αᵒᵈ
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
unitsEquivNeZero_apply_coe : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀ˣ), ↑(unitsEquivNeZero a) = ↑a
-- Mathlib.RingTheory.Valuation.Basic
Valuation.coe_mk : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (f : R →*₀ Γ₀)
  (h : ∀ (x y : R), (↑f).toFun (x + y) ≤ max ((↑f).toFun x) ((↑f).toFun y)),
  ⇑{ toMonoidWithZeroHom := f, map_add_le_max' := h } = ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Given embeddings `f : G ↪g G'` and `g : H ↪g H'`, returns an embedding from `G ⊕g H` to
`G' ⊕g H'` that applies `f` to the left component and `g` to the right component.  -/
SimpleGraph.Embedding.sum : {V : Type u_3} →
  {V' : Type u_4} →
    {W : Type u_5} →
      {W' : Type u_6} →
        {G : SimpleGraph V} →
          {H : SimpleGraph W} → {G' : SimpleGraph V'} → {H' : SimpleGraph W'} → G ↪g G' → H ↪g H' → G ⊕g H ↪g G' ⊕g H'
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.validateUTF8.go.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = false → motive false) → (x = true → motive true) → motive x
-- Mathlib.Algebra.Star.Basic
/-- Typeclass for a trivial star operation. This is mostly meant for `ℝ`.
 -/
TrivialStar : (R : Type u) → [Star R] → Prop
-- Mathlib.MeasureTheory.Measure.Count
Unique.count_eq_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Unique α],
  MeasureTheory.Measure.count = MeasureTheory.Measure.dirac default
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tendsto_atTop_zero_of_summable : ∀ {f : ℕ → NNReal}, Summable f → Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.Control.Monad.Writer
WriterT.run_pass : ∀ {M : Type u → Type v} {α ω : Type u} [inst : Monad M] (cmd : WriterT ω M (α × (ω → ω))),
  (pass cmd).run =
    (fun x =>
        match x with
        | ((a, f), w) => (a, f w)) <$>
      cmd.run
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_symm_C_C : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (r : R),
  (MvPolynomial.sumRingEquiv R S₁ S₂).symm (MvPolynomial.C (MvPolynomial.C r)) = MvPolynomial.C r
-- Init.Data.Array.Basic
/-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.   -/
Array.toListImpl : {α : Type u} → Array α → List α
-- Mathlib.Data.ENNReal.Inv
ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow : ∀ {y : ENNReal}, 1 < y → y ≠ ⊤ → Set.Ioo 0 ⊤ = ⋃ n, Set.Ico (y ^ n) (y ^ (n + 1))
-- Mathlib.Data.Multiset.Filter
/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a multiset to its
image under `f`.  -/
Multiset.mapEmbedding : {α : Type u_1} → {β : Type v} → (α ↪ β) → Multiset α ↪o Multiset β
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Non-unital seminormed ring structure on the product of two non-unital seminormed rings,
using the sup norm.  -/
Prod.nonUnitalSeminormedRing : {α : Type u_2} →
  {β : Type u_3} → [NonUnitalSeminormedRing α] → [NonUnitalSeminormedRing β] → NonUnitalSeminormedRing (α × β)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instReprOrigin.repr : Lean.Meta.Origin → ℕ → Std.Format
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.id : ∀ {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧}, ProbabilityTheory.HasLaw id μ μ
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.UniformEquicontinuous.mono : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {H H' : Set (β → α)},
  H.UniformEquicontinuous → H' ⊆ H → H'.UniformEquicontinuous
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.star_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : StarAddMonoid β] [inst_4 : ContinuousStar β] (f : CompactlySupportedContinuousMap α β) (x : α),
  (star f) x = star (f x)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_univ : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.vanishingIdeal ∅ = ⊤
-- Std.Http.Data.Status
Std.Http.Status.multipleChoices.sizeOf_spec : sizeOf Std.Http.Status.multipleChoices = 1
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_inv : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s : Set M),
  sSup s⁻¹ = (sInf s)⁻¹
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
Converts a path in the quiver `single_obj α` into a list of elements of type `a`.
 -/
Quiver.SingleObj.pathToList : {α : Type u_1} → {x : Quiver.SingleObj α} → Quiver.Path (Quiver.SingleObj.star α) x → List α
-- Mathlib.Data.Fintype.Prod
instFintypeProd : (α : Type u_4) → (β : Type u_5) → [Fintype α] → [Fintype β] → Fintype (α × β)
-- Mathlib.Topology.Algebra.Support
hasCompactMulSupport_iff_eventuallyEq : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β},
  HasCompactMulSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 1
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The congruence on `HomologicalComplex V c` given by the existence of a homotopy.
 -/
homotopic : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → (c : ComplexShape ι) → HomRel (HomologicalComplex V c)
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Cardinal.mk_biUnion_le_of_le`. -/
Cardinal.mk_iUnion_Ordinal_le_of_le : ∀ {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}},
  o.card ≤ c →
    Cardinal.aleph0 ≤ c →
      ∀ (A : Ordinal.{u_1} → Set β), (∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_le_pow : ∀ (n k : ℕ), n.choose k ≤ n ^ k