mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdjoinRoot
/-- Ring homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`.  -/
AdjoinRoot.mk : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → Polynomial R →+* AdjoinRoot f
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas.mk : Lean.PHashMap Lean.Meta.AuxLemmaKey (Lean.Name × List Lean.Name) → Lean.Meta.AuxLemmas
-- Mathlib.NumberTheory.FLT.Three
/-- If `p : 𝓞 K` is a prime that divides both `S.a + S.b` and `S.a + η * S.b`, then `p`
is associated with `λ`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K},
  Prime p →
    p ∣
        FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
          FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
      p ∣
          FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
            ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
        Associated p (hζ.toInteger - 1)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg_eq_neg : ∀ {M : Type u_1} [inst : AddGroup M] (S : AddSubmonoid M) (x : ↥S.leftNeg), ↑(S.fromLeftNeg x) = -↑x
-- Mathlib.Algebra.Group.Invertible.Basic
invertibleEquivOfLeftInverse_apply : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : FunLike F R S] [inst_3 : MonoidHomClass F R S] [inst_4 : FunLike G S R] [inst_5 : MonoidHomClass G S R]
  (f : F) (g : G) (r : R) (h : Function.LeftInverse ⇑g ⇑f) (x : Invertible (f r)),
  (invertibleEquivOfLeftInverse f g r h) x = Invertible.ofLeftInverse (⇑f) g r h
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.lhsPrec : Lean.Parser.ParserCacheEntry → ℕ
-- Mathlib.Algebra.Ring.Defs
NonAssocCommRing.toNonAssocCommSemiring : {α : Type u} → [self : NonAssocCommRing α] → NonAssocCommSemiring α
-- Mathlib.Data.List.Perm.Lattice
List.Perm.dropSlice_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α} (n m : ℕ),
  xs.Perm ys → ys.Nodup → (List.dropSlice n m xs).Perm (ys ∩ List.dropSlice n m xs)
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isInt_le_false : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ},
  Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (b' < a') = true → ¬a ≤ b
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionLiteralSupportValueSet
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_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.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], (K.shortComplexTruncLE e).f = K.ιTruncLE e
-- Mathlib.Data.Nat.Factorization.Induction
/-- Given `P 0`, `P 1`, and `P (p ^ n)` for positive prime powers, and a way to extend `P a` and
`P b` to `P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers.  -/
Nat.recOnPosPrimePosCoprime : {motive : ℕ → Sort u_1} →
  ((p n : ℕ) → Nat.Prime p → 0 < n → motive (p ^ n)) →
    motive 0 →
      motive 1 → ((a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)) → (a : ℕ) → motive a
-- Mathlib.Order.Minimal
MaximalFor.minimalFor_of_strictAntiOn_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {Q : ι → Prop} {f : ι → α}
  {g : α → β} {i : ι}, StrictAntiOn g (f '' Set.ofPred Q) → MaximalFor Q (g ∘ f) i → MinimalFor Q f i
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_neg : ∀ {d : ℤ} (x : ℤ√d), (-x).norm = x.norm
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.instModuleEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} → [inst_2 : Semiring R] → [CategoryTheory.Linear R C] → (X : C) → Module R (CategoryTheory.End X)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mul_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedCommMonoidWithZero α] [inst_1 : LinearOrderedCommMonoidWithZero β]
  (f g : α →*₀o β) (a : α), (f * g) a = f a * g a
-- Mathlib.Util.AtomM.Recurse
/-- A basically empty simp context, passed to the `simp` traversal in `AtomM.onSubexpressions`.
 -/
Mathlib.Tactic.AtomM.Recurse.Context.ctx : Mathlib.Tactic.AtomM.Recurse.Context → Lean.Meta.Simp.Context
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.inter : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s' : Set (Set Ω)} (s₂ : Set (Set Ω))
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ → ProbabilityTheory.Kernel.IndepSets (s₁ ∩ s₂) s' κ μ
-- Init.Data.List.Scan.Lemmas
List.scanr_append : ∀ {α : Type u_1} {β : Type u_2} {b : β} {f : α → β → β} (l₁ l₂ : List α),
  List.scanr f b (l₁ ++ l₂) = List.scanr f (List.foldr f b l₂) l₁ ++ (List.scanr f b l₂).tail
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isOpenEmbedding_iff_isIso_comp : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f],
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {x : OptionT m α} {h : PUnit.{u + 1} → OptionT m α}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)⦄ MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_smul_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F) (c : ℝ) (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.setToL1S (fun s => c • T s) f = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Lean.Meta.Structure
/-- Instantiates the default value given by the default value function `defaultFn`.
- `defaultFn` is the default value function returned by `Lean.getEffectiveDefaultFnForField?` or `Lean.getDefaultFnForField?`.
- `levels?` is the list of levels to use, and otherwise the levels are inferred.
- `params` is the list of structure parameters. These are assumed to be correct for the given levels.
- `fieldVal?` is a function for getting fields for values, if they exist.

If successful, returns a set of fields used and the resulting default value.
Success is expected. Callers should do metacontext backtracking themselves if needed.
 -/
Lean.Meta.instantiateStructDefaultValueFn? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadError m] →
        [MonadLiftT Lean.MetaM m] →
          [MonadControlT Lean.MetaM m] →
            Lean.Name →
              Option (List Lean.Level) →
                Array Lean.Expr → (Lean.Name → m (Option Lean.Expr)) → m (Option (Lean.NameSet × Lean.Expr))
-- Mathlib.Analysis.Seminorm
/-- Balls at the origin are balanced.  -/
balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, Balanced 𝕜 (Metric.ball 0 r)
-- Init.PropLemmas
Decidable.not_forall : ∀ {α : Sort u_1} {p : α → Prop} [Decidable (∃ x, ¬p x)] [(x : α) → Decidable (p x)], (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.modularCharacterFun_map_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G], MeasureTheory.Measure.modularCharacterFun 1 = 1
-- Lean.Elab.DocString
/-- Elaborates a sequence of blocks into a module doc snippet.  -/
Lean.Doc.elabModSnippet : Lean.DeclarationRange → Lean.TSyntaxArray `block → ℕ → Lean.Doc.DocM Lean.VersoModuleDocs.Snippet
-- Mathlib.Analysis.Convex.Between
affineSegment_const_vsub_image : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y p : P),
  (fun x => p -ᵥ x) '' affineSegment R x y = affineSegment R (p -ᵥ x) (p -ᵥ y)
-- Aesop.Rule
Aesop.defaultSimpRulePriority : ℤ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_ne_C : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (a : R), Polynomial.X ≠ Polynomial.C a
-- Mathlib.CategoryTheory.Adjunction.Whiskering
/-- Given an adjunction `F ⊣ G`, this provides the natural adjunction
`(whiskeringLeft _ _ C).obj G ⊣ (whiskeringLeft _ _ C).obj F`.  -/
CategoryTheory.Adjunction.whiskerLeft : (C : Type u_1) →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {F : CategoryTheory.Functor D E} →
              {G : CategoryTheory.Functor E D} →
                (F ⊣ G) →
                  ((CategoryTheory.Functor.whiskeringLeft E D C).obj G ⊣
                    (CategoryTheory.Functor.whiskeringLeft D E C).obj F)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I) (X : C) {Z : C} (h : G.obj (I.obj (H.obj (F.obj X))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).unit.app X) h =
    CategoryTheory.CategoryStruct.comp (adj₁.unit.app X)
      (CategoryTheory.CategoryStruct.comp (G.map (adj₂.unit.app (F.obj X))) h)
-- Mathlib.Data.List.PeriodicityLemma
List.HasPeriod.eq_1 : ∀ {α : Type u_1} (w : List α) (p : ℕ), w.HasPeriod p = (w <+: List.take p w ++ w)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquiv_functor : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)),
  (CategoryTheory.Over.ConstructProducts.conesEquiv B F).functor =
    CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F
-- Mathlib.RingTheory.Artinian.Module
/-- The quotient of a commutative Artinian ring by its nilradical is isomorphic to
a finite product of fields, namely the quotients by the maximal ideals.  -/
IsArtinianRing.quotNilradicalEquivPi : (R : Type u_1) →
  [inst : CommRing R] → [IsArtinianRing R] → (R ⧸ nilradical R) ≃ₐ[R] (I : MaximalSpectrum R) → R ⧸ I.asIdeal
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap_basicOpen : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S) (x : R),
  AlgebraicGeometry.StructureSheaf.comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) ⋯ =
    IsLocalization.map
      (↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj (Opposite.op (PrimeSpectrum.basicOpen (f x))))) f ⋯
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.sdiff_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α}, a ∈ L → b ∈ L → a \ b ∈ L
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictTarget_source : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target),
  (f.restrictTarget U hU hU').source = (f.symm.restrictSource U hU hU').target
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.mk.injEq : ∀ (hoverInfo : Lean.Server.Completion.HoverInfo) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.CompletionInfo)
  (hoverInfo_1 : Lean.Server.Completion.HoverInfo) (ctx_1 : Lean.Elab.ContextInfo) (info_1 : Lean.Elab.CompletionInfo),
  ({ hoverInfo := hoverInfo, ctx := ctx, info := info } = { hoverInfo := hoverInfo_1, ctx := ctx_1, info := info_1 }) =
    (hoverInfo = hoverInfo_1 ∧ ctx = ctx_1 ∧ info = info_1)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.G2.eq_1 : ∀ (z : UpperHalfPlane),
  EisensteinSeries.G2 z = ∑'[SummationFilter.symmetricIcc ℤ] (m : ℤ), EisensteinSeries.e2Summand m z
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierSMul` is a function space on which the Fourier transform is homogeneous.  -/
FourierSMul : (R : Type u_5) → (E : Type u_6) → (F : outParam (Type u_7)) → [SMul R E] → [SMul R F] → [FourierTransform E F] → Prop
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_lt_ofENat : ∀ {m : ℕ} [inst : m.AtLeastTwo] {n : ℕ∞}, OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
-- Mathlib.Order.Interval.Set.OrdConnectedLinear
Set.Nonempty.eq_Icc_iff_nat : ∀ {I : Set ℕ},
  I.Nonempty → BddAbove I → (I = Set.Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Set.Ioo x y) I → y ≤ x + 1)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- All dynamical balls of a minimal dynamical cover of `F` intersect `F`. This lemma is the key
to relate Bowen-Dinaburg's definition of topological entropy with covers and their definition
of topological entropy with nets.  -/
Dynamics.nonempty_inter_of_coverMincard : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ} [U.IsSymm] {s : Finset X},
  Dynamics.IsDynCoverOf T F U n ↑s →
    ↑s.card = Dynamics.coverMincard T F U n → ∀ x ∈ s, (F ∩ UniformSpace.ball x (Dynamics.dynEntourage T U n)).Nonempty
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ne_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {χ : MulChar R R'},
  χ ≠ 1 ↔ ∃ a, χ ↑a ≠ 1
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.of_val : ∀ {M : Type u_1} (a : ArchimedeanOrder M), ArchimedeanOrder.of (ArchimedeanOrder.val a) = a
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integrable_comp_smul_iff : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  (f : E → F) {R : ℝ}, R ≠ 0 → (MeasureTheory.Integrable (fun x => f (R • x)) μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A zero functor preserves limits.  -/
CategoryTheory.Functor.preservesLimitsOfSize_of_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.IsZero G → CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.FormallyUnramified.iff_map_maximalIdeal_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [inst_5 : IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S],
  Algebra.FormallyUnramified R S ↔
    Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) ∧
      Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S
-- Init.Data.UInt.Basic
/-- Converts a `Fin UInt32.size` into the corresponding `UInt32`.  -/
UInt32.ofFin : Fin UInt32.size → UInt32
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_dirac' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
  [inst_2 : MeasurableSpace α] (f : α → E) (a : α),
  MeasureTheory.StronglyMeasurable f → ∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.inv.hom₃ e.hom.hom₃ = CategoryTheory.CategoryStruct.id B.obj₃
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toLawfulOrderLT : ∀ {α : Type u} [self : Std.PreorderPackage α], Std.LawfulOrderLT α
-- Mathlib.Tactic.Linarith.Datatypes
/-- A linear expression is a list of pairs of variable indices and coefficients,
representing the sum of the products of each coefficient with its corresponding variable.

Some functions on `Linexp` assume that `n : Nat` occurs at most once as the first element of a pair,
and that the list is sorted in decreasing order of the first argument.
This is not enforced by the type but the operations here preserve it.
 -/
Mathlib.Tactic.Linarith.Linexp : Type
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edges_mapLe_eq_edges : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.mapLe h p).edges = p.edges
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compRightAlgHom_apply : ∀ (R : Type u_2) [inst : CommSemiring R] (A : Type u_3) [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsTopologicalSemiring A] {α : Type u_5} {β : Type u_6} [inst_5 : TopologicalSpace α]
  [inst_6 : TopologicalSpace β] (f : C(α, β)) (g : C(β, A)), (ContinuousMap.compRightAlgHom R A f) g = g.comp f
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsBigO` over a `Homeomorph`.  -/
Homeomorph.isBigO_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F},
  f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (e.symm b)] (g ∘ ⇑e)
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_pos_iff : ∀ (n : Int32), 0 < n.toNatClampNeg ↔ 0 < n
-- Mathlib.Algebra.DirectSum.Internal
/-- The canonical ring isomorphism between `⨁ i, A i` and `R`  -/
DirectSum.coeRingHom : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : Semiring R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubmonoidClass σ R] →
              (A : ι → σ) →
                [inst_4 : AddMonoid ι] → [inst_5 : SetLike.GradedMonoid A] → (DirectSum ι fun i => ↥(A i)) →+* R
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData_H_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ),
  ↑(CochainComplex.HomComplex.leftHomologyData K L n).H = CochainComplex.HomComplex.CohomologyClass K L n
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_neg : ∀ (a : UInt16), (-a).toUInt8 = -a.toUInt8
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv_left₀`. -/
Monovary.inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → Monovary f g → Antivary f⁻¹ g
-- Mathlib.SetTheory.Ordinal.Exponential
/-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and
`w < b ^ u`.

We special case `log 0 x = log 1 x = 0`, as well as `log b 0 = 0`.  -/
Ordinal.log : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_apply_coe : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : σ →₀ ℕ), m.toWithBotSyn ↑a = ↑(m.toSyn a)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instEpiAppColonπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C), CategoryTheory.Epi ((Φ.colonπ Ψ).app X)
-- Mathlib.Order.Antisymmetrization
lt_of_antisymmRel_of_lt : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b < c → a < c
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddCommGrpCat.Hom.mk.injEq : ∀ {A B : AddCommGrpCat} (hom' hom'_1 : ↑A →+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Topology.UniformSpace.Basic
nhdset_of_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {d : SetRel α α} (s : SetRel α α),
  d ∈ uniformity α → ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.zero : ∀ {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O fun x => 0
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.liftQSpanSingleton_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {R₂ : Type u_3}
  {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M)
  (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M), (Submodule.liftQSpanSingleton x f h) (Submodule.Quotient.mk y) = f y
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.lintegral_join_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} (f : α → ENNReal) (m : MeasureTheory.Measure (MeasureTheory.Measure α)),
  ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f x ∂μ ∂m
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_induction : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (p : α → Prop),
  (∀ (a b : α), p a → p b → p (a * b)) → p 1 → (∀ x ∈ s, p x) → p (s.noncommProd comm)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn.visit.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [inst : Monad m] (f : α → σ → m (ForInStep σ)) (a : σ),
  RBTree.RBNode.forIn.visit f RBTree.RBNode.nil a = pure (ForInStep.yield a)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.list_prod_zpow' : ∀ {α : Type u_1} [inst : CommGroupWithZero α] {r : ℤ} {l : List α},
  Mathlib.Tactic.FieldSimp.zpow' l.prod r = (List.map (fun x => Mathlib.Tactic.FieldSimp.zpow' x r) l).prod
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_sliceTo_eq_false_iff : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos
-- Mathlib.Data.List.SplitBy
List.nil_notMem_splitBy : ∀ {α : Type u_1} (r : α → α → Bool) (l : List α), [] ∉ List.splitBy r l
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version for two elements of `ℝ≥0` and real exponents.  -/
NNReal.rpow_arith_mean_le_arith_mean2_rpow : ∀ (w₁ w₂ z₁ z₂ : NNReal), w₁ + w₂ = 1 → ∀ {p : ℝ}, 1 ≤ p → (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.DSimproc : Type
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.support_toPartitionOfUnity_subset : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι),
  Function.support ⇑(f.toPartitionOfUnity i) ⊆ Function.support ⇑(f i)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.toLp_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : α × β), (WithLp.toLp p x).snd = x.2
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodProdProdComm_toEquiv : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'],
  ↑(MulEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'