mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Dual
/-- Duality with respect to a general bilinear map can be expressed as duality using the
identity pairing.  -/
PointedCone.dual_eq_dual_id_image : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M), PointedCone.dual p s = PointedCone.dual LinearMap.id (⇑p '' s)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S),
  CategoryTheory.Sieve.ofArrows X f = CategoryTheory.Sieve.ofArrows X' f' →
    (Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful)
-- Batteries.Data.List.Basic
List.IsChain.below.nil : ∀ {α : Type u_1} {R : α → α → Prop} {motive : (a : List α) → List.IsChain R a → Prop}, List.IsChain.below ⋯
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C'.congr_simp : ∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : I → Bool),
      a = a_1 → Profinite.NobelingProof.C' C ho a = Profinite.NobelingProof.C' C_1 ⋯ a_1
-- Lean.Elab.Do.Basic
Lean.Elab.Do.expandNestedActions : {kind : Lean.SyntaxNodeKinds} → Lean.TSyntax kind → Lean.Elab.Do.DoElabM (Array Lean.DoElem × Lean.TSyntax kind)
-- Mathlib.RingTheory.Radical.NatInt
UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors : UniqueFactorizationMonoid.primeFactors = Nat.primeFactors
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinsetLeft.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (_i : β),
  (FirstOrder.Language.var (Sum.inr _i)).varFinsetLeft = ∅
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → DifferentiableAt 𝕜 f x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.ι_desc_assoc : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) (j : Fin (n + 2)) (hj : j ≠ i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) (CategoryTheory.CategoryStruct.comp hf.desc h) =
    CategoryTheory.CategoryStruct.comp (f j hj) h
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.splitter : {n : ℕ} →
  (motive : Fin (n + 1 + 1) → Sort u_1) →
    (x : Fin (n + 1 + 1)) →
      ((isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) →
        ((i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩) → motive x
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_neg : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S}
  (f : M →ₛₗ[σ] M₂) (x : M), f (-x) = -f x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.coconeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.colimit.coconeMorphism c = (CategoryTheory.Limits.colimit.isColimit F).descCoconeMorphism c
-- Mathlib.Topology.MetricSpace.Bounded
Metric.hasAntitoneBasis_cobounded_compl_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  (Bornology.cobounded α).HasAntitoneBasis fun r => (Metric.ball c r)ᶜ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instSingleton : {α : Type u_1} → [inst : TopologicalSpace α] → Singleton α (TopologicalSpace.Compacts α)
-- Mathlib.NumberTheory.Padics.PadicNumbers
instCommRingPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → CommRing ℚ_[p]
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical ring homomorphism interpreting an element of `R` as
a section of the structure sheaf.  -/
AlgebraicGeometry.StructureSheaf.toOpen : (R : Type u) →
  [inst : CommRing R] →
    (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
      CommRingCat.of R ⟶ (AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U)
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_True : Set.Ici True = {True}
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map self.m₃) = w₂₃
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop : AlgebraicGeometry.HasAffineProperty (CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme)
  fun X x f x_1 => AlgebraicGeometry.IsAffine X ∧ CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.appTop f)
-- Mathlib.Data.Set.Function
Set.mapsTo_union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f (s₁ ∪ s₂) t ↔ Set.MapsTo f s₁ t ∧ Set.MapsTo f s₂ t
-- Init.Control.MonadAttach
/-- This type class ensures that every monadic action `x : m α` can be recovered by stripping the
proof component from the subtypes returned by
`(MonadAttach.attach x) : m { a : α // MonadAttach.CanReturn x a }` . In other words,
the type class ensures that `Subtype.val <$> MonadAttach.attach x = x`.
 -/
WeaklyLawfulMonadAttach : (m : Type u → Type v) → [Monad m] → [MonadAttach m] → Prop
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.tendstoUniformlyOn_deriv_of_cthickening_subset : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U K : Set ℂ} {φ : Filter ι}
  {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E],
  TendstoLocallyUniformlyOn F f φ U →
    (∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) →
      ∀ {δ : ℝ},
        0 < δ →
          IsCompact K → IsOpen U → Metric.cthickening δ K ⊆ U → TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A morphism of LocallyRingedSpaces is an open immersion if it is an open immersion as a morphism
of SheafedSpaces
 -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion : {X Y : AlgebraicGeometry.LocallyRingedSpace} → (X ⟶ Y) → Prop
-- Mathlib.Data.Nat.Factors
Nat.mem_primeFactorsList : ∀ {n p : ℕ}, n ≠ 0 → (p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc.eq_1 : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0),
  SemiNormedGrp.explicitCokernelDesc w =
    (SemiNormedGrp.isColimitCokernelCocone f).desc (CategoryTheory.Limits.Cofork.ofπ g ⋯)
-- Lean.Meta.Hint
/-- Creates message data corresponding to a `HintSuggestions` collection and adds the corresponding info
leaf.
 -/
Lean.Meta.Hint.mkSuggestionsMessage : Array Lean.Meta.Hint.Suggestion → Lean.Syntax → Option String → Bool → Lean.CoreM Lean.MessageData
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given algebras $R \to S \to T$, the sequence
$H_1(L_{T/S}) \to T \otimes_S \Omega_{S/R} \to \Omega_{T/R}$
is exact.  -/
Algebra.H1Cotangent.exact_δ_mapBaseChange : ∀ (R : Type u₁) (S : Type u₂) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u₃)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T],
  Function.Exact ⇑(Algebra.H1Cotangent.δ R S T) ⇑(KaehlerDifferential.mapBaseChange R S T)
-- Init.Prelude
/-- Returns `true` if the environment contains a declaration with name `declName`  -/
Lean.Macro.hasDecl : Lean.Name → Lean.MacroM Bool
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported : ∀ {ι : 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 : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [K.IsStrictlySupported e] (i : ι), CategoryTheory.IsIso ((K.truncLE'ToRestriction e).f i)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderivWithin_add` -/
mvfderivWithin_fun_add : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g g' : M → F} {x : M},
  MDiffAt[s] g x → MDiffAt[s] g' x → UniqueMDiffAt[s] x → (d[s] fun i => g i + g' i) x = d[s] g x + d[s] g' x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α} {k k' fallback : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
      k ∈ l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKeyD k'
            fallback =
          k
-- Lean.Meta.Match.MatcherApp.Transform
Lean.Meta.MatcherApp.TransformAltFVars.mk.inj : ∀ {args fields overlaps discrEqs extraEqs args_1 fields_1 overlaps_1 discrEqs_1 extraEqs_1 : Array Lean.Expr},
  { args := args, fields := fields, overlaps := overlaps, discrEqs := discrEqs, extraEqs := extraEqs } =
      { args := args_1, fields := fields_1, overlaps := overlaps_1, discrEqs := discrEqs_1, extraEqs := extraEqs_1 } →
    args = args_1 ∧ fields = fields_1 ∧ overlaps = overlaps_1 ∧ discrEqs = discrEqs_1 ∧ extraEqs = extraEqs_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Augmented.stdSimplex_obj_left : ∀ (Δ : SimplexCategory), (SSet.Augmented.stdSimplex.obj Δ).left = SSet.stdSimplex.obj Δ
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {α β : F ⟶ G}, α.app = β.app → α = β
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_discreteTopology : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  [hL : DiscreteTopology ↥L] {e : F →ₗ[K] E},
  Continuous ⇑e → Function.Injective ⇑e → DiscreteTopology ↥(ZLattice.comap K L e)
-- Mathlib.Combinatorics.Enumerative.Composition
instDecidableEqComposition.decEq : {n : ℕ} → (x x_1 : Composition n) → Decidable (x = x_1)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).inradius = s.inradius
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.comul_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a b : A),
  CoalgebraStruct.comul (a * b) = CoalgebraStruct.comul a * CoalgebraStruct.comul b
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L),
  h.d (Int.negSucc 0) (Int.ofNat 0) =
    match Int.negSucc 0, Int.ofNat 0 with
    | Int.ofNat n, Int.ofNat m => L.d n m
    | Int.negSucc n, Int.negSucc m => K.d n m
    | Int.negSucc 0, Int.ofNat 0 => h.d₀
    | Int.ofNat a, Int.negSucc a_1 => 0
    | Int.negSucc a, Int.ofNat a_1 => 0
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_algEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f)
  {U : Type u_2} [inst_5 : CommRing U] (i : R →+* U) (x : U) (hx : Polynomial.eval₂ i x f = 0) (z : S),
  (h'.lift i x hx) ((h.algEquiv h') z) = (h.lift i x hx) z
-- Mathlib.RingTheory.FormalGroup.Basic
/-- The natural inclusion from formal group law into formal power series.  -/
FormalGroup.coeToPowerSeries : {R : Type u_1} → [inst : CommRing R] → Coe (FormalGroup R) (MvPowerSeries (Fin 2) R)
-- Mathlib.Order.Filter.CountableInter
eventually_countable_forall : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {p : α → ι → Prop},
  (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- An isometry between quadratic forms generated by `QuadraticMap.pi` can be constructed
from a pair of isometries between the left and right parts.  -/
QuadraticMap.IsometryEquiv.pi : {ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        {Nᵢ : ι → Type u_9} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
              [inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : (i : ι) → Module R (Mᵢ i)] →
                    [inst_5 : (i : ι) → Module R (Nᵢ i)] →
                      [inst_6 : Module R P] →
                        [inst_7 : Fintype ι] →
                          {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} →
                            {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} →
                              ((i : ι) → (Q i).IsometryEquiv (Q' i)) →
                                (QuadraticMap.pi Q).IsometryEquiv (QuadraticMap.pi Q')
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.localized'_ker_eq_ker_localizedMap : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {P : Type u_5}
  [inst_11 : AddCommMonoid P] [inst_12 : Module R P] {Q : Type u_6} [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q]
  [inst_15 : Module S Q] [inst_16 : IsScalarTower R S Q] (f' : P →ₗ[R] Q) [inst_17 : IsLocalizedModule p f']
  (g : M →ₗ[R] P),
  Submodule.localized' S p f g.ker =
    (LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g)).ker
-- Mathlib.Probability.UniformOn
/-- **Alias** of `ProbabilityTheory.isProbabilityMeasure_uniformOn`. -/
ProbabilityTheory.uniformOn_isProbabilityMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω},
  s.Finite → s.Nonempty → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Any subobject classifier `Ω` represents the subobjects functor `Subobject.presheaf`.  -/
CategoryTheory.Subobject.Classifier.representableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (𝒞 : CategoryTheory.Subobject.Classifier C) → (Subobject.presheaf C).RepresentableBy 𝒞.Ω
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.Raw.ofList l cmp).getKey? k' = some k
-- Init.Data.Fin.Lemmas
Fin.val_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), ↑(Fin.castAdd m i) = ↑i
-- Init.Data.String.PosRaw
String.instDecidableLtRaw : (p₁ p₂ : String.Pos.Raw) → Decidable (p₁ < p₂)
-- Mathlib.Order.SuccPred.Limit
/-- Recursion principle on a well-founded partial `SuccOrder`, separating out the case of a
minimal element.  -/
SuccOrder.limitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : SuccOrder α] →
          [WellFoundedLT α] →
            ((a : α) → IsMin a → motive a) →
              ((a : α) → ¬IsMax a → motive a → motive (Order.succ a)) →
                ((a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) → motive b
-- Mathlib.Algebra.Group.Action.Basic
/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`.  -/
MulAction.toPerm : {α : Type u_5} → {β : Type u_6} → [inst : Group α] → [MulAction α β] → α → Equiv.Perm β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k a : α} {v : β},
  Std.DHashMap.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Const.get! m a
-- Mathlib.Data.Finset.Image
Finset.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β}, b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b
-- Mathlib.ModelTheory.Graph
/-- The symbol representing the adjacency relation.  -/
FirstOrder.Language.adj : FirstOrder.Language.graph.Relations 2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- The composition of `cfcHom` with the natural embedding `C(s, R) → C(spectrum R a, R)`
whenever `spectrum R a ⊆ s`.

This is sometimes necessary in order to consider the same continuous functions applied to multiple
distinct elements, with the added constraint that `cfc` does not suffice. This can occur, for
example, if it is necessary to use uniqueness of this continuous functional calculus.  -/
cfcHomSuperset : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : Ring A] →
                  [inst_6 : StarRing A] →
                    [inst_7 : TopologicalSpace A] →
                      [inst_8 : Algebra R A] →
                        [instCFC : ContinuousFunctionalCalculus R A p] →
                          {a : A} → p a → {s : Set R} → spectrum R a ⊆ s → C(↑s, R) →⋆ₐ[R] A
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_add : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f₁ f₂ : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)),
  (f₁ + f₂) • g = f₁ • g + f₂ • g
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function for the zeros of `f * g` is less than or equal to the
sum of the logarithmic counting functions for the zeros of `f` and `g`, respectively.

Note: The statement proven here is found at the top of page 169 of [Lang: Introduction to Complex
Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) where it is written as
an inequality between functions. This could be interpreted as claiming that the inequality holds for
ALL values of `r`, which is not true. For a counterexample, take `f₁ : z → z` and `f₂ : z → z⁻¹`.
Then,

- `logCounting f₁ 0 = log`
- `logCounting f₂ 0 = 0`
- `logCounting (f₁ * f₂) 0 = 0`

But `log r` is negative for small `r`.
 -/
ValueDistribution.logCounting_mul_zero_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.logCounting (f₁ * f₂) 0 r ≤
              (ValueDistribution.logCounting f₁ 0 + ValueDistribution.logCounting f₂ 0) r
-- Mathlib.Data.Finset.Prod
Finset.offDiag_mono : ∀ {α : Type u_1}, Monotone Finset.offDiag
-- Mathlib.Order.KrullDimension
Order.coheight_coe_withBot : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.coheight ↑x = Order.coheight x
-- Init.Data.Nat.Lemmas
Nat.mul_right_comm : ∀ (n m k : ℕ), n * m * k = n * k * m
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsAddRightInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G],
  MeasureTheory.Measure.count.IsAddRightInvariant
-- Mathlib.Algebra.Squarefree.Basic
squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R] {r : R},
  (∃ x, Irreducible x) → (Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r)
-- Mathlib.Data.List.Permutation
List.foldr_permutationsAux2 : ∀ {α : Type u_1} (t : α) (ts : List α) (r L : List (List α)),
  List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L =
    List.flatMap (fun y => (List.permutationsAux2 t ts [] y id).2) L ++ r
-- Mathlib.Topology.UniformSpace.Basic
toTopologicalSpace_prod : ∀ {α : Type u_2} {β : Type u_3} [u : UniformSpace α] [v : UniformSpace β],
  instUniformSpaceProd.toTopologicalSpace = instTopologicalSpaceProd
-- ProofWidgets.Component.HtmlDisplay
/-- Display a value of type `Html` in the infoview.

The input can be a pure value
or a computation in any Lean metaprogramming monad
(e.g. `CommandElabM Html`).  -/
ProofWidgets.HtmlCommand.htmlCmd : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsStableUnderPostcompHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPostcomp (HomotopicalAlgebra.FibrantObject.homRel C)