mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Build a `R[M]`-linear map from a `R`-linear map and evidence that it is `M`-equivariant.  -/
MonoidAlgebra.equivariantOfLinearOfComm : {R : Type u_1} →
  {M : Type u_7} →
    [inst : Monoid M] →
      [inst_1 : CommSemiring R] →
        {V : Type u_10} →
          {W : Type u_11} →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module R V] →
                [inst_4 : Module (MonoidAlgebra R M) V] →
                  [IsScalarTower R (MonoidAlgebra R M) V] →
                    [inst_6 : AddCommMonoid W] →
                      [inst_7 : Module R W] →
                        [inst_8 : Module (MonoidAlgebra R M) W] →
                          [IsScalarTower R (MonoidAlgebra R M) W] →
                            (f : V →ₗ[R] W) →
                              (∀ (g : M) (v : V), f (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • f v) →
                                V →ₗ[MonoidAlgebra R M] W
-- Init.MetaTypes
/-- Maximum number of library suggestions to use. If `none`, uses the default limit.
Only relevant when `suggestions` is `true`.
 -/
Lean.Meta.Simp.Config.maxSuggestions : Lean.Meta.Simp.Config → Option ℕ
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_le_iff : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)},
  p₁.prod p₂ ≤ q ↔ Submodule.map (LinearMap.inl R M M₂) p₁ ≤ q ∧ Submodule.map (LinearMap.inr R M M₂) p₂ ≤ q
-- Mathlib.Algebra.Order.Star.Basic
/-- **Alias** of the reverse direction of `IsSelfAdjoint.iff_of_le`. -/
IsSelfAdjoint.of_le : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {a b : R},
  a ≤ b → IsSelfAdjoint b → IsSelfAdjoint a
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.rightInverse.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f f_1 : E →L[R] F} (e_f : f = f_1) (h : f.HasRightInverse), h.rightInverse = ⋯.rightInverse
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instNonemptyShiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.Nonempty], (P.shiftClosure A).Nonempty
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey!_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false →
        (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey! =
          if compare t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasStrictDerivAt.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasStrictDerivAt f f' x → ∀ (n : ℕ), HasStrictDerivAt (fun x => f x ^ n) (↑n * f x ^ (n - 1) * f') x
-- Mathlib.Algebra.Ring.Ext
NonAssocRing.toNonUnitalNonAssocring_injective : ∀ {R : Type u}, Function.Injective (@NonAssocRing.toNonUnitalNonAssocRing R)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k))
  (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.alter k f t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      match f none with
      | none =>
        { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some v =>
        {
          impl :=
            Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
          balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl =>
      match h : compare k k' with
      | Ordering.lt =>
        match Std.DTreeMap.Internal.Impl.alter k f l' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.gt =>
        match Std.DTreeMap.Internal.Impl.alter k f r' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.eq =>
        match f (some (cast ⋯ v')) with
        | none => { impl := l'.glue r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
        | some v =>
          { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {U V : N} (f : U ⟶ V),
  (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor p).map f =
    CategoryTheory.CategoryOfElements.homMk
      ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).elementsMk (p.obj U)
        (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.id (p.obj U))))
      ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).elementsMk (p.obj V)
        (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.id (p.obj V))))
      (p.map f) ⋯
-- Std.Async.Basic
/-- Converts `AsyncTask` into `Async`.
 -/
Std.Async.Async.ofAsyncTask : {α : Type} → Std.Async.AsyncTask α → Std.Async.Async α
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} (i i_1 : ↥b.support),
  i = i_1 →
    ∀ (a a_1 : ↥b.support ⊕ ι),
      a = a_1 →
        ∀ (a_2 a_3 : ↥b.support ⊕ ι),
          a_2 = a_3 → RootPairing.GeckConstruction.h i a a_2 = RootPairing.GeckConstruction.h i_1 a_1 a_3
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.alter m k f) k = f (Std.DHashMap.Const.get? m k)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a),
  MvPowerSeries.substAlgHom ha = MvPowerSeries.aeval ⋯
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  (∀ b ∈ s, f b ≤ g b) → s.sup f ≤ s.sup g
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.subtype.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M),
  p.subtype = { toFun := Subtype.val, map_vadd' := ⋯ }
-- Mathlib.Computability.DFA
/-- A language is regular if and only if it is defined by a DFA with finite states.

This is more general than using the definition of `Language.IsRegular` directly, as the state type
`σ` is universe-polymorphic.
 -/
Language.isRegular_iff : ∀ {T : Type u} {L : Language T}, L.IsRegular ↔ ∃ σ x M, M.accepts = L
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.exists_vadd_eq : ∀ (M : Type u_1) {α : Type u_3} [inst : VAdd M α] [AddAction.IsPretransitive M α] (x y : α), ∃ m, m +ᵥ x = y
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Init.Data.List.Nat.Sublist
List.suffix_map_iff_of_injective : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → β},
  Function.Injective f → (List.map f l₁ <:+ List.map f l₂ ↔ l₁ <:+ l₂)
-- Mathlib.Algebra.Ring.BooleanRing
/-- Every generalized Boolean algebra has the structure of a nonunital commutative ring with the
following data:

* `a + b` unfolds to `a ∆ b` (symmetric difference)
* `a * b` unfolds to `a ⊓ b`
* `-a` unfolds to `a`
* `0` unfolds to `⊥`
 -/
GeneralizedBooleanAlgebra.toNonUnitalCommRing : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → NonUnitalCommRing α
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_functorPushforward_post : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {X : C} (U : CategoryTheory.Over X) (S : CategoryTheory.Sieve U),
  (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.post F).obj U))
      (CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.post F) S) =
    CategoryTheory.Sieve.functorPushforward F ((CategoryTheory.Sieve.overEquiv U) S)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (1, 2)`) .  -/
Real.exists_measure_rpow_eq_integral_rpowIntegrand₁₂ : ∀ {p : ℝ},
  p ∈ Set.Ioo 1 2 →
    ∃ μ,
      ∀ x ∈ Set.Ici 0,
        MeasureTheory.IntegrableOn (fun t => p.rpowIntegrand₁₂ t x) (Set.Ioi 0) μ ∧
          x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₁₂ t x ∂μ
-- Mathlib.Algebra.RingQuot
RingQuot.zero_quot : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), { toQuot := Quot.mk (RingQuot.Rel r) 0 } = 0
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.RightRigidCategory.rightDual : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.RightRigidCategory C] → (X : C) → CategoryTheory.HasRightDual X
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.isEmpty = true → (t.insert k).min? = some k
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.containsₘ_eq_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.containsₘ a = Std.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Algebra.Category.ModuleCat.Stalk
/-- (Implementation). The module structure on `AddCommGrpCat.FilteredColimits.colimit`.  -/
CategoryTheory.Limits.filteredColimitsModule : {C : Type u_1} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.IsFiltered C] →
      (R : CategoryTheory.Functor C RingCat) →
        (M : CategoryTheory.Functor C Ab) →
          [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)] →
            (∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
                (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
                  (CategoryTheory.ConcreteCategory.hom (R.map f)) r •
                    (CategoryTheory.ConcreteCategory.hom (M.map f)) m) →
              Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M)
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.ext : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] {C₁ C₂ : ProperCone R E},
  (∀ (x : E), x ∈ C₁ ↔ x ∈ C₂) → C₁ = C₂
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Alias** of `MonoidHom.domRestrictHomKerEquiv_symm_coe_apply`. -/
MonoidHom.restrictHomKerEquiv_symm_coe_apply : ∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal]
  (f : G ⧸ H →* A) (g : G), ↑((MonoidHom.domRestrictHomKerEquiv A H).symm f) g = f ↑g
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsGalois X],
  MulAction.IsPretransitive (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 x_4 : x ⟶ x_1) (Γ : x_3 ⟶ x_4) (η : x_1 ⟶ x_2) (a : B),
  (CategoryTheory.Bicategory.whiskerRight Γ η).as.app a = CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (η.app a)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.point_mem_closedInterior_face_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [Nontrivial k] [ZeroLEOneClass k] {n : ℕ}
  (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {j : Fin (n + 1)},
  s.points j ∈ (s.face h).closedInterior ↔ j ∈ fs
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap'_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (a : α),
  (P.colimitsClosure J).IsClosedUnderColimitsOfShape (J a)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.fiberwise_left : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α}
  {f : α × β → E} {g : α × β → F} {l' : Filter β},
  f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun x => f (x, b)) =O[l] fun x => g (x, b)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofEquivFun_repr_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι), ((Module.Basis.ofEquivFun e).repr x) i = e x i
-- Mathlib.CategoryTheory.Localization.StructuredArrow
_private.Mathlib.CategoryTheory.Localization.StructuredArrow.0.CategoryTheory.Localization.induction_structuredArrow' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X : C}
  (P : CategoryTheory.StructuredArrow (W.Q.obj X) W.Q → Prop),
  P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (W.Q.obj X))) →
    (∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
        P (CategoryTheory.StructuredArrow.mk φ) →
          P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (W.Q.map f)))) →
      (∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
          P (CategoryTheory.StructuredArrow.mk φ) →
            P
              (CategoryTheory.StructuredArrow.mk
                (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Localization.isoOfHom W.Q W w hw).inv))) →
        ∀ (g : CategoryTheory.StructuredArrow (W.Q.obj X) W.Q), P g
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_le_rootMultiplicity_of_dvd : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R},
  q ≠ 0 → p ∣ q → ∀ (x : R), Polynomial.rootMultiplicity x p ≤ Polynomial.rootMultiplicity x q
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabTParserMacroAux : Lean.Term → Lean.Term → Lean.Term → Lean.Elab.TermElabM Lean.Syntax
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.outParam.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.PatternArgKind.outParam = 1
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a multiplication-invariant pseudodistance.  -/
SeminormedCommGroup.ofMulDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : CommGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y) → SeminormedCommGroup E
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.grp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (self : CategoryTheory.CommGrp C) → CategoryTheory.GrpObj self.X
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk.sizeOf_spec : ∀ (cells : Finset (ℕ × ℕ)) (isLowerSet : IsLowerSet ↑cells),
  sizeOf { cells := cells, isLowerSet := isLowerSet } = 1 + sizeOf cells
-- Mathlib.NumberTheory.Divisors
_private.Mathlib.NumberTheory.Divisors.0.Int.termNegNatCast : Lean.ParserDescr
-- Mathlib.Data.Set.Finite.Basic
/-- The identity map, bundled as an equivalence between the subtypes of `s : Set α` and of
`h.toFinset : Finset α`, where `h` is a proof of finiteness of `s`.  -/
Set.Finite.subtypeEquivToFinset : {α : Type u} → {s : Set α} → (hs : s.Finite) → { x // x ∈ s } ≃ ↥hs.toFinset
-- Mathlib.Order.UpperLower.CompleteLattice
upperSetIsoLowerSet_symm_apply : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), (RelIso.symm upperSetIsoLowerSet) s = s.compl
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.comap_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.comap (⇑e) Filter.atTop = Filter.atTop
-- Mathlib.CategoryTheory.Widesubcategory
/-- `InducedWideCategory D F P`, where `F : C → D`, is a typeclass synonym for `C`,
which provides a category structure so that the morphisms `X ⟶ Y` are the morphisms
in `D` from `F X` to `F Y` which satisfy a property `P : MorphismProperty D` that is multiplicative.
 -/
CategoryTheory.InducedWideCategory : {C : Type u₁} →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      (C → D) → (_P : CategoryTheory.MorphismProperty D) → [_P.IsMultiplicative] → Type u₁
-- Init.Data.Array.Lemmas
Array.any_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (Array.replicate n a).any f = if n = 0 then false else f a
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), - -a = a
-- Mathlib.Data.Multiset.Fintype
Multiset.cast_symm_apply_snd : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (h : s = t) (x : t.ToType),
  ((Multiset.cast h).symm x).snd = Fin.cast ⋯ x.snd
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_symm : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ),
  (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm
-- Init.Data.List.Lemmas
List.append_left_eq_self : ∀ {α : Type u_1} {xs ys : List α}, xs ++ ys = ys ↔ xs = []
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensor_ext : ∀ {R : Type u} [inst : CommSemiring R] {M₁ M₂ M₃ : SemimoduleCat R}
  {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃},
  (∀ (m : ↑M₁) (n : ↑M₂), (SemimoduleCat.Hom.hom f) (m ⊗ₜ[R] n) = (SemimoduleCat.Hom.hom g) (m ⊗ₜ[R] n)) → f = g
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
/-- A morphism property stable under associator isomorphisms of a monoidal category.  -/
CategoryTheory.MorphismProperty.IsStableUnderAssociator : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.mapOfMeasurable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (f : β → γ) (hf : Measurable f),
  κ.mapOfMeasurable f hf = { toFun := fun a => MeasureTheory.Measure.map f (κ a), measurable' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.map_rightSection : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : CategoryTheory.IsSplitCoequalizer f g π)
  (F : CategoryTheory.Functor C D), (q.map F).rightSection = F.map q.rightSection
-- Mathlib.Order.Lattice
/-- The infimum is the *greatest* lower bound  -/
SemilatticeInf.le_inf : ∀ {α : Type u} [self : SemilatticeInf α] (a b c : α), a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c
-- Mathlib.LinearAlgebra.Pi
/-- A bilinear map into `Fin n.succ → M₃` can be built out of a map into `M₃` and a map into
`Fin n → M₃`  -/
LinearMap.vecCons₂ : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M₃] →
                      {n : ℕ} → (M →ₗ[R] M₂ →ₗ[R] M₃) → (M →ₗ[R] M₂ →ₗ[R] Fin n → M₃) → M →ₗ[R] M₂ →ₗ[R] Fin n.succ → M₃
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instMonoidWithZero : {α : Type u_1} → [MonoidWithZero α] → MonoidWithZero (Lex α)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toList_rco_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...n).toList[i]?.isNone = true) = ((n - m).toNat ≤ i)
-- Mathlib.Order.Interval.Basic
/-- The nonempty closed intervals in an order.

We define intervals by the pair of endpoints `fst`, `snd`. To convert intervals to the set of
elements between these endpoints, use the coercion `NonemptyInterval α → Set α`.  -/
NonemptyInterval : (α : Type u_6) → [LE α] → Type u_6
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : G.Adj u' v'),
  h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`.  -/
EuclideanDomain.gcdB : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_reverse`. -/
List.SortedLT.of_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedLT → l.SortedGT