mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
/-- Given an ideal `I` of a commutative ring `R`, we say that a polynomial `f : R[X]`
is *Distinguished at `I`* if `f` is monic and `IsWeaklyEisensteinAt I`.
i.e. `f` is of the form `xⁿ + a₁xⁿ⁻¹ + ⋯ + aₙ` with `aᵢ ∈ I` for all `i`.
 -/
Polynomial.IsDistinguishedAt : {R : Type u_1} → [inst : CommRing R] → Polynomial R → Ideal R → Prop
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.ext : ∀ {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X}, @Diffeology.IsPlot X d₁ = @Diffeology.IsPlot X d₂ → d₁ = d₂
-- Mathlib.Data.Finset.DenselyOrdered
Finset.exists_between : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] {s t : Finset α},
  s.Nonempty → t.Nonempty → (∀ x ∈ s, ∀ y ∈ t, x < y) → ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk''_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (S : CategoryTheory.StrictPseudofunctorPreCore B C) {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.StrictPseudofunctor.mk'' S).map a = S.map a
-- Mathlib.Data.Set.Piecewise
Set.apply_piecewise : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort u_8} (h : (i : α) → δ i → δ' i) {x : α},
  h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.linear_equivMapOfInjective : ∀ {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁] [inst_2 : NormedSpace 𝕜 V₁] [inst_3 : PseudoMetricSpace P₁]
  [inst_4 : NormedAddTorsor V₁ P₁] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [inst_9 : Nonempty ↥E]
  (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ),
  (E.equivMapOfInjective φ hφ).linear =
    (Submodule.equivMapOfInjective φ.linear ⋯ E.direction).trans
      (LinearEquiv.ofEq (Submodule.map φ.linear E.direction) (AffineSubspace.map φ E).direction ⋯)
-- Mathlib.Order.Antichain
/-- **Alias** of `IsAntichain.eq_setOfPred_maximal`.

---

If `t` is an antichain shadowing and including the set of maximal elements of `s`,
then `t` *is* the set of maximal elements of `s`.  -/
IsAntichain.eq_setOf_maximal : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) t →
    (∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t) →
      (∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b) → {x | Maximal (fun x => x ∈ s) x} = t
-- Mathlib.Algebra.Group.Action.Basic
MulAction.toPerm_symm_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (a : α) (x : β),
  (Equiv.symm (MulAction.toPerm a)) x = a⁻¹ • x
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unone_coe : ∀ {α : Type u} {x : α} (hx : ↑x ≠ 1), WithOne.unone hx = x
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.is_basis_iff_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) {v : ι → M},
  LinearIndependent R v ∧ Submodule.span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)
-- Mathlib.Algebra.Homology.Augment
/-- The truncation of an `ℕ`-indexed cochain complex,
deleting the object at `0` and shifting everything else down.
 -/
CochainComplex.truncate : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      CategoryTheory.Functor (CochainComplex V ℕ) (CochainComplex V ℕ)
-- Mathlib.CategoryTheory.Category.Basic
/-- The identity morphism on an object.  -/
CategoryTheory.CategoryStruct.id : {obj : Type u} → [self : CategoryTheory.CategoryStruct.{v, u} obj] → (X : obj) → X ⟶ X
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.sum.eq_1 : ∀ (L : FirstOrder.Language) (L' : FirstOrder.Language),
  L.sum L' =
    { Functions := fun n => L.Functions n ⊕ L'.Functions n, Relations := fun n => L.Relations n ⊕ L'.Relations n }
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckTypeAscription : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instFieldCarrierFunctionField : (X : AlgebraicGeometry.Scheme) → [inst : AlgebraicGeometry.IsIntegral X] → Field ↑X.functionField
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
/-- Given `X : TopCat`, this is the bijection between `0`-simplices
of the singular simplicial set of `X` and `X`.  -/
TopCat.toSSetObj₀Equiv : {X : TopCat} → (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 }) ≃ ↑X
-- Mathlib.Algebra.Polynomial.Basis
/-- The monomials form a basis on `R[X]`. To get the rank of a polynomial ring,
use this and `Basis.mk_eq_rank`.  -/
Polynomial.basisMonomials : (R : Type u) → [inst : Semiring R] → Module.Basis ℕ R (Polynomial R)
-- Std.Http.Data.Request
Std.Http.Request.instReprHead.repr : Std.Http.Request.Head → ℕ → Std.Format
-- Aesop.Tree.Data
Aesop.MVarCluster.mk : Aesop.MVarClusterData Aesop.Goal Aesop.Rapp → Aesop.MVarCluster
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For each set `B` in the submodule basis on `A`, there is another basis element `B'` such
that the set-theoretic product `B' * B'` is in `B`.  -/
RingSubgroupsBasis.mul : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
  RingSubgroupsBasis B → ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.foldrM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.foldrM f init t₁ = Std.DTreeMap.Raw.foldrM f init t₂
-- Std.Data.TreeMap.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.TreeMap.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zero_rpow_nonneg : ∀ (x : ℝ), 0 ≤ 0 ^ x
-- Mathlib.Tactic.Convert
Convert.ExpensiveConfig.mk : Congr!.Config → Convert.ExpensiveConfig
-- Init.Data.Vector.Lemmas
Vector.append_eq_replicate_iff : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {a : α},
  xs ++ ys = Vector.replicate (n + m) a ↔ xs = Vector.replicate n a ∧ ys = Vector.replicate m a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
ModuleCat.restrictScalarsComp'.congr_simp : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f),
  ModuleCat.restrictScalarsComp' f g gf hgf = ModuleCat.restrictScalarsComp' f g gf hgf
-- Lean.Expr
Lean.mkApp3 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.mk.sizeOf_spec : ∀ (message? since? : Option String),
  sizeOf { message? := message?, since? := since? } = 1 + sizeOf message? + sizeOf since?
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.negRev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.tail_nil : ∀ {α : Type u}, Stream'.Seq.nil.tail = Stream'.Seq.nil
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom.default : Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Set.ofPred.eq_1 : ∀ {α : Type u} (p : α → Prop), Set.ofPred p = p
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.map_hexagon_reverse : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                (CategoryTheory.MonoidalCategoryStruct.tensorObj
                  ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
                  ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))).app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                  ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)))
-- Mathlib.Algebra.Order.Pi
Function.extend_le_one : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : One γ] [inst_1 : LE γ] {f : α → β} {g : α → γ} {e : β → γ},
  g ≤ 1 → e ≤ 1 → Function.extend f g e ≤ 1
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.isSeparator : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {ι : Type w} {S : ι → A},
  (CategoryTheory.ObjectProperty.ofObj S).IsSeparating →
    ∀
      [inst_3 :
        CategoryTheory.Limits.HasCoproduct fun x =>
          match x with
          | (X, i) => CategoryTheory.Presheaf.freeYoneda X (S i)]
      [CategoryTheory.Limits.HasZeroMorphisms A],
      CategoryTheory.IsSeparator
        (∐ fun x =>
          match x with
          | (X, i) => CategoryTheory.Presheaf.freeYoneda X (S i))
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.logHomeomorph_symm : ENNReal.logHomeomorph.symm = EReal.expHomeomorph
-- Mathlib.Order.Atoms
Pi.isAtomic : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → PartialOrder (π i)] [inst_1 : (i : ι) → OrderBot (π i)]
  [∀ (i : ι), IsAtomic (π i)], IsAtomic ((i : ι) → π i)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- Implementation detail:
the morphism level of `pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U`
 -/
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      {V W : CategoryTheory.Pairwise ι} →
        (V ⟶ W) →
          (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U V ⟶
            TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U W)
-- Mathlib.Data.List.Sublists
List.sublists_singleton : ∀ {α : Type u} (a : α), [a].sublists = [[], [a]]
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.Denumerable.lower.match_1.splitter : (motive : List ℕ → ℕ → Sort u_1) →
  (x : List ℕ) →
    (x_1 : ℕ) → ((x : ℕ) → motive [] x) → ((m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n) → motive x x_1
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.mk.sizeOf_spec : ∀ (visited : Std.HashSet UInt64) (found : Lean.FVarIdSet),
  sizeOf { visited := visited, found := found } = 1 + sizeOf visited + sizeOf found
-- Init.Data.SInt.Bitwise
Int8.toBitVec_xor : ∀ (a b : Int8), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit.eq_1 : ∀ {α : Type u_1} (f : α → α) (x : α),
  Function.periodicOrbit f x = ↑(List.map (fun n => f^[n] x) (List.range (Function.minimalPeriod f x)))
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.leftCosetEquivAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α),
  AddSubgroup.leftCosetEquivAddSubgroup g =
    { toFun := fun x => ⟨-g + ↑x, ⋯⟩, invFun := fun x => ⟨g + ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Basic
/-- Update the type of the given metavariable. This function assumes the new type is
definitionally equal to the current one  -/
Lean.MVarId.setType : Lean.MVarId → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Data.Seq.Parallel
Computation.parallel_empty : ∀ {α : Type u} (S : Stream'.WSeq (Computation α)), S.head.Promises none → Computation.parallel S = Computation.empty α
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_uInt8ToNat : ∀ (n : UInt8), UInt32.ofNatLT n.toNat ⋯ = n.toUInt32
-- Mathlib.Topology.Maps.Basic
IsOpenMap.of_inverse : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f' : Y → X},
  Continuous f' → Function.LeftInverse f f' → Function.RightInverse f f' → IsOpenMap f
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension at `Y` when
`E.coconeAt Y` is a colimit cocone.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.LeftExtension F → D → Type (max (max (max u_1 v_2) u_4) v_4)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.abs_moebius_le_one : ∀ {n : ℕ}, |ArithmeticFunction.moebius n| ≤ 1
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.distinguished_cocone_triangle₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₁] {Y Z : C} (b : Y ⟶ Z),
  P Y →
    P Z →
      ∃ X,
        ∃ (_ : P X),
          ∃ a c,
            CategoryTheory.Pretriangulated.Triangle.mk a b c ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Cancellation of a telescoping product.  -/
List.prod_range_div : ∀ {G : Type u_7} [inst : CommGroup G] (n : ℕ) (f : ℕ → G),
  (List.map (fun k => f (k + 1) / f k) (List.range n)).prod = f n / f 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_ric : ∀ {n i : ℕ}, (*...=n).toList[i]! = if i ≤ n then i else 0
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_comp_mulHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
  { toFun := ⇑g ∘ ⇑f, map_mul' := ⋯ } = (↑g).comp ↑f
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousVAdd.finite_stabilizer' : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T] [ProperlyDiscontinuousVAdd Γ T] (x : T),
  {γ | γ +ᵥ x = x}.Finite
-- Lean.Data.Lsp.Basic
/-- A human-readable string describing the actual change.
The string is rendered prominent in the user interface.  -/
Lean.Lsp.ChangeAnnotation.label : Lean.Lsp.ChangeAnnotation → String
-- Mathlib.Data.FunLike.Module
/-- A `FunLike` type with scalar multiplication that satisfies `(m • f) x = m • f x`, `0 x = 0`,
`(f + g) x = f x + g x` is a `DistribMulAction` if `β` is a `DistribMulAction`.  -/
FunLike.distribMulAction : {M : Type u_1} →
  {F : Type u_3} →
    {α : Type u_4} →
      {β : Type u_5} →
        [i : FunLike F α β] →
          [inst : Monoid M] →
            [inst_1 : AddMonoid β] →
              [inst_2 : AddMonoid F] →
                [inst_3 : DistribMulAction M β] →
                  [inst_4 : SMul M F] →
                    [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply M F α β] → DistribMulAction M F
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.EReal.eventually_atTop_exists_nat_between : ∀ {a b : EReal}, a < b → 0 ≤ b → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, a * ↑n ≤ ↑m ∧ ↑m ≤ b * ↑n
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e₁` and `e₂` are congruent modulo the equivalence classes in `enodes`.  -/
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.isCongruent : Lean.Meta.Grind.ENodeMap → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Laplacian for functions on real inner product spaces, with respect to a set `s`. Use `open
InnerProductSpace` to access the notation `Δ[s]` for `InnerProductSpace.LaplacianWithin`.
 -/
InnerProductSpace.«termΔ[_]_» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- In a finite-dimensional vector space over `ℝ`, the series `∑ x, ‖f x‖` is unconditionally
summable if and only if the series `∑ x, f x` is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite-dimensional spaces.  -/
summable_norm_iff : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f : α → E}, (Summable fun x => ‖f x‖) ↔ Summable f
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.eq_one' : ∀ {G : Type u_1} [inst : Monoid G] [IsMulTorsionFree G] {a : G}, IsOfFinOrder a → a = 1
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.trans_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (e₁ : M ≃+ N)
  (e₂ : N ≃+ P) (m : M), (e₁.trans e₂) m = e₂ (e₁ m)
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder ℤ
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Monoid R] →
              [inst_5 : DistribMulAction R A] → [StarModule R A] → DistribMulAction R ↥(selfAdjoint A)
-- Mathlib.Topology.Defs.Filter
/-- A set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.  -/
nhds : {X : Type u_3} → [TopologicalSpace X] → X → Filter X
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.associator_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y Z : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.f =
    (CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst Z.fst).inv
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The equivalence between the type associated to `multiequalizer (S.index P)` and `Meq P S`.  -/
CategoryTheory.Meq.equiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  [∀ {X : C} (S : J.Cover X),
                        CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
                          (CategoryTheory.forget D)] →
                    {X : C} →
                      (P : CategoryTheory.Functor Cᵒᵖ D) →
                        (S : J.Cover X) →
                          [inst_5 : CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                            CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer (S.index P)) ≃
                              CategoryTheory.Meq P S
-- Std.Time.Format
/-- The europeanDate format, which follows the pattern `dd-MM-uuuu`.
 -/
Std.Time.Formats.europeanDate : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.Data.Num.ZNum
ZNum.cast_mul : ∀ {α : Type u_1} [inst : NonAssocRing α] (m n : ZNum), ↑(m * n) = ↑m * ↑n
-- Mathlib.Topology.Order.LiminfLimsup
BoundedLENhdsClass.isBounded_le_nhds : ∀ {α : Type u_7} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : BoundedLENhdsClass α] (a : α),
  Filter.IsBounded (fun x1 x2 => x1 ≤ x2) (nhds a)
-- Mathlib.AlgebraicGeometry.Stalk
/-- [Stacks Tag 01J7](https://stacks.math.columbia.edu/tag/01J7) -/
AlgebraicGeometry.Scheme.range_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X}, Set.range ⇑(X.fromSpecStalk x) = {y | y ⤳ x}
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.instIsCoatomicSubmodule : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], IsCoatomic (Submodule R M)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of finitely many `C^k` connections is a `C^k` connection.  -/
CovariantDerivative.ContMDiffCovariantDerivative.finiteAffineCombination : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] {ι : Type u_7} {s : Finset ι} (cov : ι → CovariantDerivative I F V) {f : ι → M → 𝕜}
  (hf : ∑ i ∈ s, f i = 1) {n : WithTop ℕ∞},
  (∀ i ∈ s, ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n (f i)) →
    (∀ i ∈ s, (cov i).ContMDiffCovariantDerivative n) →
      (CovariantDerivative.finiteAffineCombination cov hf).ContMDiffCovariantDerivative n