mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If `G` preserves the coequalizer of `(f,g)`, then the coequalizer comparison map for `G` at `(f,g)`
is an isomorphism.
 -/
CategoryTheory.Limits.PreservesCoequalizer.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f g : X ⟶ Y) →
              [inst_2 : CategoryTheory.Limits.HasCoequalizer f g] →
                [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] →
                  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] →
                    CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ≅
                      G.obj (CategoryTheory.Limits.coequalizer f g)
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `leOnePart_le_one`.  -/
leOnePart_le_one' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_iff_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α], Order.succ a = b ↔ a ⋖ b
-- Mathlib.Algebra.Group.Equiv.Defs
AddHom.toAddEquiv_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (g : N →ₙ+ M)
  (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N), ⇑(f.toAddEquiv g h₁ h₂) = ⇑f
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → {P Q : CategoryTheory.Idempotents.Karoubi C} → Zero (P ⟶ Q)
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.closure_def : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : f.IsClosable), f.closure = Exists.choose hf
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- If `f : ℝⁿ → E` is a.e. continuous and bounded on a rectangular box `I`, then it is Box
integrable on `I` w.r.t. a locally finite measure `μ` with the same integral.  -/
MeasureTheory.AEContinuous.hasBoxIntegral : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [CompleteSpace E] {f : (ι → ℝ) → E} (μ : MeasureTheory.Measure (ι → ℝ))
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι},
  (∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C) →
    (∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x) →
      ∀ (l : BoxIntegral.IntegrationParams),
        BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
-- Mathlib.Data.Int.Cast.Lemmas
RingHom.ext_int : ∀ {R : Type u_5} [inst : NonAssocSemiring R] (f g : ℤ →+* R), f = g
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.succ_eq_iff_isMax`. -/
IsMax.succ_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α}, IsMax a → Order.succ a = a
-- Mathlib.Control.Traversable.Instances
List.id_traverse : ∀ {α : Type u_1} (xs : List α), List.traverse pure xs = pure xs
-- Mathlib.Data.Sum.Order
WithBot.orderIsoPUnitSumLex_bot : ∀ {α : Type u_1} [inst : LE α], WithBot.orderIsoPUnitSumLex ⊥ = toLex (Sum.inl PUnit.unit)
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_or : ∀ {a b c : UInt32}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFractionRel.trans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ z₃ : W.RightFraction X Y} [W.HasRightCalculusOfFractions],
  CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂ →
    CategoryTheory.MorphismProperty.RightFractionRel z₂ z₃ → CategoryTheory.MorphismProperty.RightFractionRel z₁ z₃
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.instLaxMonoidalSkeletonMapSkeleton : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [F.LaxMonoidal] → F.mapSkeleton.LaxMonoidal
-- Mathlib.Analysis.MellinTransform
/-- Compatibility with scalar multiplication by a normed field. For scalar multiplication by more
general rings assuming *a priori* that the Mellin transform is defined, see
`hasMellin_const_smul`.  -/
mellin_const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {𝕜 : Type u_2}
  [inst_2 : NormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜),
  mellin (fun t => c • f t) s = c • mellin f s
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mk.sizeOf_spec : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toPartialHomeomorph : PartialHomeomorph X Y) (open_source : IsOpen toPartialHomeomorph.source)
  (open_target : IsOpen toPartialHomeomorph.target),
  sizeOf { toPartialHomeomorph := toPartialHomeomorph, open_source := open_source, open_target := open_target } =
    1 + sizeOf toPartialHomeomorph + sizeOf open_source + sizeOf open_target
-- Init.Grind.Ring.Field
/-- Division is multiplication by the inverse.  -/
Lean.Grind.Field.div_eq_mul_inv : ∀ {α : Type u} [self : Lean.Grind.Field α] (a b : α), a / b = a * b⁻¹
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `div_le_iff₀` for a version with multiplication on the other side.  -/
div_le_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (b / c ≤ a ↔ b ≤ c * a)
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D)
  (F : CategoryTheory.Functor D E)
  [inst_7 : ∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F],
  (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- Indexed version of `exists_lt_of_csInf_lt`.
When `iInf f < a`, there is an element `i` such that `f i < a`.
 -/
exists_lt_of_ciInf_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {a : α} [Nonempty ι] {f : ι → α},
  iInf f < a → ∃ i, f i < a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.mkGeneratorNode? : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Meta.SynthInstance.GeneratorNode)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Sort u_2}
  (f : R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t),
  ValuativeRel.ValueGroupWithZero.lift f hf 0 = f 0 1
-- Init.Data.Array.Perm
List.perm_iff_toArray_perm : ∀ {α : Type u_1} {as bs : List α}, as.Perm bs ↔ as.toArray.Perm bs.toArray
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.symm_mapAlgEquiv : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (e : A ≃ₐ[R] B),
  (AddMonoidAlgebra.mapAlgEquiv R M e).symm = AddMonoidAlgebra.mapAlgEquiv R M e.symm
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  {i j : J} {xi : F.obj i} {xj : F.obj j},
  (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.LSeries_eq_mul_integral_aux : ∀ {f : ℕ → ℂ},
  f 0 = 0 →
    ∀ {r : ℝ},
      0 ≤ r →
        ∀ {s : ℂ},
          r < s.re →
            LSeriesSummable f s →
              ((fun n => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun n => ↑n ^ r) →
                LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
-- Mathlib.Data.Finset.Density
Finset.dens_le_one : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, s.dens ≤ 1
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.MonObj A]
  {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).map f).hom = A.map f
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.gc_saturation : ∀ (M : Type u_1) [inst : MulOneClass M], GaloisConnection Submonoid.saturation fun x => x.toSubmonoid
-- Mathlib.Data.Finset.Pi
Finset.pi_disjoint_of_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Type u_2} {s : Finset α} (t₁ t₂ : (a : α) → Finset (δ a)) {a : α},
  a ∈ s → Disjoint (t₁ a) (t₂ a) → Disjoint (s.pi t₁) (s.pi t₂)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.top_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊤ = ⊤
-- Lean.Elab.Command
Lean.Elab.Command.Context : Type
-- Init.Data.AC
Lean.Data.AC.sort.eq_1 : ∀ (xs : List ℕ), Lean.Data.AC.sort xs = Lean.Data.AC.sort.loop [] xs
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- Our function tends to zero at zero faster than any $P(x^{-1})$, $P∈ℝ[X]$, tends to infinity.  -/
expNegInvGlue.tendsto_polynomial_inv_mul_zero : ∀ (p : Polynomial ℝ), Filter.Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (nhds 0) (nhds 0)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial.eq_def : ∀ (n x : ℕ),
  n.ascFactorial x =
    match x with
    | 0 => 1
    | k.succ => (n + k) * n.ascFactorial k
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.colimitCoconeOfIsLUB_isColimit : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt),
  (Preorder.colimitCoconeOfIsLUB F h).isColimit = Preorder.isColimitOfIsLUB F (Preorder.coconeOfUpperBound F ⋯) h
-- Mathlib.Data.String.Basic
String.ltb_cons_addChar : ∀ (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : String.Pos.Raw),
  String.ltb { s := String.ofList (c :: cs₁), i := i₁ + c } { s := String.ofList (c :: cs₂), i := i₂ + c } =
    String.ltb { s := String.ofList cs₁, i := i₁ } { s := String.ofList cs₂, i := i₂ }
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsZeroOrMarkovKernel.eq_zero_or_isMarkovKernel' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [self : ProbabilityTheory.IsZeroOrMarkovKernel κ], κ = 0 ∨ ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a Heyting homomorphism preserves the bottom element.  -/
HeytingHom.map_bot' : ∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (self : HeytingHom α β),
  self.toFun ⊥ = ⊥
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.of_discrete : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [DiscreteTopology X] (f : X → Y), IsLocallyConstant f
-- Lean.Meta.LazyDiscrTree
/-- Lazy entries for root of trie.  -/
Lean.Meta.LazyDiscrTree.PreDiscrTree.tries : {α : Type} → Lean.Meta.LazyDiscrTree.PreDiscrTree α → Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.m.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] (j : ι), f.m j = CategoryTheory.Limits.Sigma.map (f.basicCell j)
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.exists_eq_add_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G), ∃ n, σ g = σ' g + S.inl n
-- Mathlib.Topology.Separation.Basic
R1Space.of_continuous_specializes_imp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : TopologicalSpace Y] {f : Y → X},
  Continuous f → (∀ (x y : Y), f x ⤳ f y → x ⤳ y) → R1Space Y
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- A natural transformation between functors `Karoubi C ⥤ D` is determined
by its value on objects coming from `C`.  -/
CategoryTheory.Idempotents.natTrans_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D]
  {F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (φ : F ⟶ G)
  (P : CategoryTheory.Idempotents.Karoubi C),
  φ.app P =
    CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
      (CategoryTheory.CategoryStruct.comp (φ.app { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ })
        (G.map P.decompId_p))
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.isAffineMap_fst : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {X : Type u_3}
  {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y],
  Convexity.IsAffineMap R Prod.fst
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_mul_eq_nnnorm_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E) {y : E}, ‖y‖₊ = 0 → ‖x * y‖₊ = ‖x‖₊
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_erase_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, (t.erase k).size ≤ t.size
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk : {B : Type u_1} → {F : Type u_4} → {E : B → Type u_5} → (proj : B) → E proj → Bundle.TotalSpace F E
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn.congr_simp : ∀ {a a_1 : ℕ} (e_a : a = a_1) (a1 : 1 < a) (n n_1 : ℕ), n = n_1 → Pell.yn a1 n = Pell.yn ⋯ n_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceBoolPred : Lean.Name → ℕ → (ℤ → ℤ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.eq_1 : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] (l : Filter α) (u v : α → E'),
  Asymptotics.IsEquivalent l u v = (u - v) =o[l] v
-- Mathlib.Data.List.Cycle
Cycle.coe_toMultiset : ∀ {α : Type u_1} (l : List α), (↑l).toMultiset = ↑l
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.ext_iff : ∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S}
  {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y}, x = y ↔ x.f = y.f
-- Mathlib.Algebra.Polynomial.Basic
/-- `Polynomial R` is the type of univariate polynomials over `R`,
denoted as `R[X]` within the `Polynomial` namespace.

Polynomials should be seen as (semi-)rings with the additional constructor `X`.
The embedding from `R` is called `C`.  -/
Polynomial.«term_[X]» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The trivial monoid object. We later show this is initial in `Mon C`.
 -/
CategoryTheory.Mon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon C
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.typesWith_inf : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ ψ : (L.withConstants α).Sentence),
  T.typesWith (φ ⊓ ψ) = T.typesWith φ ∩ T.typesWith ψ
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofErrorNameInfo : Lean.Elab.ErrorNameInfo → Lean.Elab.Info
-- Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
CategoryTheory.Functor.isColimitOfIsWellOrderContinuous.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J]
  (F : CategoryTheory.Functor J C) [inst_2 : F.IsWellOrderContinuous] (m : J) (hm : Order.IsSuccLimit m),
  F.isColimitOfIsWellOrderContinuous m hm = F.isColimitOfIsWellOrderContinuous m hm
-- Init.PropLemmas
forall_prop_decidable : {p : Prop} → (P : p → Prop) → [Decidable p] → [(h : p) → Decidable (P h)] → Decidable (∀ (h : p), P h)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.eq_3 : ∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (X Y : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C (X.tensor Y) x =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusionObj x) X Y).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X x) Y ≪≫
        CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y (X.normalizeObj x)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toBitVec = { toFin := n }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (f g : ContinuousMapZero X ℝ),
  (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
-- Init.Control.Lawful.Instances
ExceptT.run_monadMap : ∀ {n : Type u → Type u_1} {m : Type u → Type u_2} {ε α : Type u} [inst : MonadFunctorT n m]
  (f : {β : Type u} → n β → n β) (x : ExceptT ε m α), (monadMap f x).run = monadMap f x.run
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.Limits.cocone.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc hc_1 : CategoryTheory.Limits.IsColimit c), hc = hc_1 → PartOrdEmb.Limits.cocone hc = PartOrdEmb.Limits.cocone hc_1
-- Mathlib.Order.Preorder.Finite
Finset.exists_le_minimal : ∀ {α : Type u_2} [inst : Preorder α] {a : α} (s : Finset α), a ∈ s → ∃ b ≤ a, Minimal (fun x => x ∈ s) b
-- Mathlib.Data.Set.Finite.Lattice
/-- A finite union of sets which are all bounded above is still bounded above.  -/
Set.Finite.bddAbove_biUnion : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {I : Set β} {S : β → Set α},
  I.Finite → (BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono_ae : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b → f ≤ᵐ[μ] g → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.toEquiv_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  Function.Injective MeasurableEquiv.toEquiv
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceTo_le_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p₀.sliceTo q h ≤ p ↔ q ≤ String.Slice.Pos.ofSliceTo p
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_apply_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {a : A} {b : B}, e.symm b = a ↔ b = e a
-- Mathlib.Algebra.Group.End
AddAut.congr_apply : ∀ {G : Type u_3} [inst : AddGroup G] {H : Type u_7} [inst_1 : AddGroup H] (ϕ : G ≃+ H) (f : AddAut G),
  (AddAut.congr ϕ) f = ϕ.symm.trans (AddEquiv.trans f ϕ)
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.ssubset_or_eq`.

---

Set notation form of `LE.le.lt_or_eq` -/
HasSubset.Subset.ssubset_or_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ⊂ b ∨ a = b
-- Lean.Elab.Tactic.Config
/-- Given a hierarchical name `field`, returns the fully resolved field access, the base struct name, and the last projection function.
 -/
_private.Lean.Elab.Tactic.Config.0.Lean.Elab.Tactic.expandField : Lean.Name → Lean.Name → Lean.MetaM (Lean.Name × Lean.Name)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_inv_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso C D).inv.app X =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso X).inv
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.coconesEquiv_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Final.coconesEquiv F G).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun c =>
        CategoryTheory.Limits.Cocone.ext
          (CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.Cocone.whiskering F).comp CategoryTheory.Functor.Final.extendCocone).obj c).pt)
          ⋯)
      ⋯
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.snd_comp_inr : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], (OrderAddMonoidHom.snd α β).comp (OrderAddMonoidHom.inr α β) = OrderAddMonoidHom.id β
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int32
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
ContinuousAddEquiv.symm_apply_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) (x : M), e.symm (e x) = x