mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t₁ t₂ : Finset β}
  [inst_2 : DecidableEq β], s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
-- Mathlib.Algebra.Group.Defs
Monoid.toSemigroup : {M : Type u} → [self : Monoid M] → Semigroup M
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddZeroClass.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddZeroClass α],
  Shrink.instAddZeroClass = (equivShrink α).symm.addZeroClass
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_isGLB : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : Preorder α]
  [InfConvergenceClass α] {f : ι → α} {a : α},
  Monotone f → IsGLB (Set.range f) a → Filter.Tendsto f Filter.atBot (nhds a)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- The star algebra homomorphism underlying an instance of the continuous functional calculus;
a version for continuous functions on the spectrum.

In this case, the user must supply the fact that `a` satisfies the predicate `p`, for otherwise it
may be the case that no star algebra homomorphism exists. For instance if `R := ℝ` and `a` is an
element whose spectrum (in `ℂ`) is disjoint from `ℝ`, then `spectrum ℝ a = ∅` and so there can be
no star algebra homomorphism between these spaces.

While `ContinuousFunctionalCalculus` is stated in terms of these homomorphisms, in practice the
user should instead prefer `cfc` over `cfcHom`.
 -/
cfcHom : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : TopologicalSpace A] →
                  [inst_6 : Ring A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : Algebra R A] →
                        [instCFC : ContinuousFunctionalCalculus R A p] → {a : A} → p a → C(↑(spectrum R a), R) →⋆ₐ[R] A
-- Mathlib.Order.Hom.Lattice
LatticeHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  {g : LatticeHom β γ} {f₁ f₂ : LatticeHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Data.Finmap
Finmap.instSDiff : {α : Type u} → {β : α → Type v} → [DecidableEq α] → SDiff (Finmap β)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubMulAction.ofFixingSubgroup.append.congr_simp : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x x_1 : Fin n ↪ ↥(SubMulAction.ofFixingSubgroup M s)),
  x = x_1 → SubMulAction.ofFixingSubgroup.append x = SubMulAction.ofFixingSubgroup.append x_1
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup.measurable_sup_const : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Max M} [self : MeasurableSup M] (c : M), Measurable fun x => x ⊔ c
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_multiplicative : ∀ {α : Type u}, Cardinal.mk (Multiplicative α) = Cardinal.mk α
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Mon D)),
  CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.obj F =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F
-- Mathlib.Analysis.Convex.Function
convexOn_iff_pairwise_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β},
  ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceLErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size),
  (Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr).size = l.size + 1 + r.size
-- Mathlib.Tactic.DeriveTraversable
/-- similar to `traverseConstructor` but for `Functor`  -/
Mathlib.Deriving.Traversable.mapConstructor : Lean.Name →
  Lean.Name →
    Lean.Expr →
      Lean.Expr → Lean.Expr → List Lean.Expr → List (Bool × Lean.Expr) → Lean.MVarId → Lean.Elab.TermElabM Unit
-- Lean.Util.Trace
Lean.trace.profiler : Lean.Option Bool
-- Mathlib.MeasureTheory.Measure.Regular
/-- For an outer regular measure, the measure of a set is the infimum of the measures of open sets
containing it.  -/
Set.measure_eq_iInf_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α)
  [μ.OuterRegular], μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U
-- Mathlib.Topology.Sets.Closeds
/-- The equivalence `IrreducibleCloseds α ≃ { x : Set α // IsClosed x ∧ IsIrreducible x }` is an
order isomorphism.  -/
TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' : (α : Type u_2) →
  [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α ≃o { x // IsClosed x ∧ IsIrreducible x }
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_inter_conull : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ tᶜ = 0 → μ (s ∩ t) = μ s
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAt_add_const_iff`. -/
HasDerivAt.add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt f f' x → HasDerivAt (fun x => f x + c) f' x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_nhds_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (U : OpenSubgroup G), ↑U ∈ nhds 1
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioi_pred_eq_Ici_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Set.Ioi (Order.pred a) = Set.Ici a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_coe_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {f : α → NNReal}, (Continuous fun a => ↑(f a)) ↔ Continuous f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr_eq_discr' : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), QuadraticForm.discr (Pi.basisFun R n) Q = Q.discr'
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceNe : Lean.Meta.Simp.Simproc
-- Mathlib.Data.ENat.Lattice
ENat.add_iSup : ∀ {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞), a + ⨆ i, f i = ⨆ i, a + f i
-- Aesop.Frontend.Saturate
Aesop.ElabM.runForwardElab : {α : Type} → Lean.MVarId → Aesop.ElabM α → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Polynomial.Div
/-- `modByMonic`, denoted as `p  %ₘ q`, gives the remainder of `p` by a monic polynomial `q`.  -/
Polynomial.«term_%ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c < max a b → Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (min a c)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_4 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (op : Std.Tactic.BVDecide.BVBinOp)
  (lhs rhs : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.bin op rhs) =
    op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.covers : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X),
  x ∈ Set.range ⇑(𝒰.f (𝒰.idx x))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof : Type
-- Init.Data.SInt.Basic
instDivISize : Div ISize
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_linear : ∀ {R : Type u} {a b : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X + Polynomial.C b).degree = 1
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.hom_ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S} {f g : a ⟶ b},
  (HasFibers.ι S).map f = (HasFibers.ι S).map g → f = g
-- Mathlib.Data.List.Cycle
List.nextOr.eq_2 : ∀ {α : Type u_1} [inst : DecidableEq α] (x x_1 head : α), [head].nextOr x x_1 = x_1
-- Std.Http.Data.URI.Config
/-- Maximum length of the URI scheme component (e.g. `https`), in bytes.
The scheme grammar requires at least one leading ALPHA; the remaining budget is
`max(0, maxSchemeLength - 1)` additional characters.
 -/
Std.Http.URI.Config.maxSchemeLength : Std.Http.URI.Config → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β}, Std.DTreeMap.Raw.Const.get (t.insert k v) k ⋯ = v
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism (in `Type`) between
morphisms from the colimit object to a specified object `W`,
and cocones with cone point `W`.
 -/
CategoryTheory.Limits.colimit.homIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            (W : C) → ULift.{u₁, v} (CategoryTheory.Limits.colimit F ⟶ W) ≅ F.cocones.obj W
-- Mathlib.Data.Num.ZNum
ZNum.ofInt'_neg : ∀ (n : ℤ), ZNum.ofInt' (-n) = -ZNum.ofInt' n
-- Mathlib.MeasureTheory.Function.L2Space
/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
equal to the inner product of the constant `c` and the integral of `f` over `s`.  -/
MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {s : Set α} [CompleteSpace E]
  [inst_4 : NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) (f : ↥(MeasureTheory.Lp E 2 μ)),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs c) f = inner 𝕜 c (∫ (x : α) in s, ↑↑f x ∂μ)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- A map from `Πʳ i, [R i, A i] × Πʳ i, [R' i, A' i]` is continuous
*iff* its restriction to each `Πʳ i, [R i, A i]_[𝓟 S] × Πʳ i, [R' i, A' i]_[𝓟 S]`
(with `S` cofinite) is continuous.

This is the key result for continuity of multiplication and addition.  -/
RestrictedProduct.continuous_dom_prod : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {R' : ι → Type u_3} {A' : (i : ι) → Set (R' i)} [inst_1 : (i : ι) → TopologicalSpace (R' i)],
      (∀ (i : ι), IsOpen (A' i)) →
        ∀ {X : Type u_4} [inst_2 : TopologicalSpace X]
          {f :
            RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite ×
                RestrictedProduct (fun i => R' i) (fun i => A' i) Filter.cofinite →
              X},
          Continuous f ↔
            ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S),
              Continuous (f ∘ Prod.map (RestrictedProduct.inclusion R A hS) (RestrictedProduct.inclusion R' A' hS))
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Result.mk.sizeOf_spec : ∀ (proof : Lean.Expr), sizeOf { proof := proof } = 1 + sizeOf proof
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_mod_two_pow : ∀ {a b n : ℕ}, (a &&& b) % 2 ^ n = a % 2 ^ n &&& b % 2 ^ n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.IsStrongLimit.aleph0_le : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → Cardinal.aleph0 ≤ c
-- Mathlib.Topology.Order
IsOpen.mono : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α}, IsOpen s → t₁ ≤ t₂ → IsOpen s
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.tsum_coe_ne_top : ∀ {α : Type u_1} (p : PMF α), ∑' (a : α), p a ≠ ⊤
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.extensions : Lean.Meta.Grind.Params → Lean.Meta.Grind.ExtensionStateArray
-- Aesop.Search.SearchM
Aesop.NormSimpContext.configStx? : Aesop.NormSimpContext → Option Lean.Term
-- Lean.Elab.Tactic.Basic
/-- Like `evalTacticAt`, but without restoring the goal list or pruning solved goals.
Useful when these tasks are already being done in an outer loop.
 -/
Lean.Elab.Tactic.evalTacticAtRaw : Lean.Syntax → Lean.MVarId → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A closed subset of a countably compact set is countably compact.  -/
IsCountablyCompact.of_isClosed_subset : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A B : Set E},
  IsCountablyCompact A → IsClosed B → B ⊆ A → IsCountablyCompact B
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.disjoint_compl_right_iff : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : α}, Heyting.IsRegular b → (Disjoint a bᶜ ↔ a ≤ b)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Comonad C} →
      (toNatTrans : CategoryTheory.NatTrans M.toFunctor N.toFunctor) →
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X)
            CategoryTheory.ComonadHom.app_ε._autoParam →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
                  CategoryTheory.CategoryStruct.comp (M.δ.app X)
                    (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X))))
              CategoryTheory.ComonadHom.app_δ._autoParam →
            CategoryTheory.ComonadHom M N
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE.instHasHomology : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i' : ι'), (K.truncGE e).HasHomology i'
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_id' : ∀ {R : Type u_1} [inst : CommSemiring R], PrimeSpectrum.BasicConstructibleSetData.map (RingHom.id R) = id
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.directive.sizeOf_spec : sizeOf Lean.Elab.DocElabKind.directive = 1
-- Mathlib.Order.PiLex
/-- The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order.  -/
Pi.«termΠₗ_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_left_zero : ∀ {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (x : E), LineDeriv.lineDerivOp 0 x = 0
-- Mathlib.Topology.NhdsKer
nhdsKer_subset_nhdsKer_iff_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, nhdsKer s ⊆ nhdsKer t ↔ nhdsSet s ≤ nhdsSet t
-- Mathlib.CategoryTheory.Functor.Currying
/-- The object level part of the currying functor. (See `curry` for the functorial version.)
 -/
CategoryTheory.Functor.curryObj : {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] →
            CategoryTheory.Functor (C × D) E → CategoryTheory.Functor C (CategoryTheory.Functor D E)
-- Mathlib.Data.Finset.Defs
Finset.coe_coeEmb : ∀ {α : Type u_1}, ⇑Finset.coeEmb = SetLike.coe
-- Lean.Parser.Types
Lean.Parser.ParserState.mk : Lean.Parser.SyntaxStack →
  ℕ →
    String.Pos.Raw →
      Lean.Parser.ParserCache →
        Option Lean.Parser.Error →
          Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error) → Lean.Parser.ParserState
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_pos_imp_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R]
  [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R], 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
-- Mathlib.Data.Finsupp.Multiset
Finsupp.sum_toMultiset : ∀ {α : Type u_1} [inst : AddCommMonoid α] (f : α →₀ ℕ), (Finsupp.toMultiset f).sum = f.sum fun a n => n • a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keysArray_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).keysArray = t.keysArray
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIocDiv_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIocDiv hp a b • p = toIocMod hp a b
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.isColoop_iff_sdiff_closure`. -/
Matroid.isColoop_iff_diff_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_inj : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v.restrict x = v.restrict y ↔ v x = v y
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The associator in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.Bicategory.associator : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : CategoryTheory.Bicategory.Adj B} →
      (α : a ⟶ b) →
        (β : b ⟶ c) →
          (γ : c ⟶ d) →
            CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β) γ ≅
              CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp β γ)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.counit.comp_app_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{max u v, u} C],
  (CategoryTheory.Cat.FreeRefl.quotientFunctor C).comp
      (CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of C)).toFunctor =
    CategoryTheory.pathComposition C
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_eq_map : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : DistribSMul M V] [inst_4 : SMulCommClass M k V] (a : M) (s : AffineSubspace k V),
  a • s = AffineSubspace.map (DistribSMul.toLinearMap k V a).toAffineMap s
-- Init.Omega.LinearCombo
/-- The `i`-th coordinate function.  -/
Lean.Omega.LinearCombo.coordinate : ℕ → Lean.Omega.LinearCombo
-- Mathlib.Topology.Path
Path.coe_reparam : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval}
  (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1), ⇑(γ.reparam f hfcont hf₀ hf₁) = ⇑γ ∘ f
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.uniqueRingEquiv_apply : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : Subsingleton M]
  (a : AddMonoidAlgebra R M), (AddMonoidAlgebra.uniqueRingEquiv M) a = a.coeff 0
-- Mathlib.FieldTheory.Minpoly.Basic
/-- Given any `f : B →ₐ[A] B'` and any `x : L`, the minimal polynomial of `x` vanishes at `f x`.  -/
minpoly.aeval_algHom : ∀ (A : Type u_1) {B : Type u_2} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Ring B']
  [inst_3 : Algebra A B] [inst_4 : Algebra A B'] (f : B →ₐ[A] B') (x : B), (Polynomial.aeval (f x)) (minpoly A x) = 0
-- Mathlib.Data.Rat.Floor
Rat.round_cast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : ℚ),
  round ↑x = round x
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α], b ≤ a → Order.pred b < a
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.id_tensorHom_id : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R) (N : SemimoduleCat R),
  SemimoduleCat.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) =
    CategoryTheory.CategoryStruct.id (SemimoduleCat.of R (TensorProduct R ↑M ↑N))
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₃_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ₃.natDegree ≤ 4
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instNontrivial : ∀ (p : ENNReal) (V : Type u_4) [Nontrivial V], Nontrivial (WithLp p V)
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.mem_singleton_apply_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i},
  a ∈ f.singleton i ↔ a = f i
-- Mathlib.Data.Prod.Basic
Prod.snd_comp_mk : ∀ {α : Type u_1} {β : Type u_2} (x : α), Prod.snd ∘ Prod.mk x = id
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurable_iSup : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [SecondCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → Measurable τ
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.isUnit_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (f : M ≃ₗ[R] M') (v : Module.Basis ι R M) (v' : Module.Basis ι R M'), IsUnit ((LinearMap.toMatrix v v') ↑f).det
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.SurjectiveOnStalks
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instIsMultiplicativeSchemeQuasiCompact : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.QuasiCompact
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.castSucc (Finset.Ioo i j) = Finset.Ioo i.castSucc j.castSucc
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.HasExactColimitsOfShape.mk : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim → CategoryTheory.HasExactColimitsOfShape J C
-- Mathlib.Data.Fin.VecNotation
/-- `vecHead v` gives the first entry of the vector `v`  -/
Matrix.vecHead : {α : Type u} → {n : ℕ} → (Fin n.succ → α) → α
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_integral_norm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, a ≤ b → ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ ∫ (x : ℝ) in a..b, ‖f x‖ ∂μ
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_injective : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] (i : ι),
  Function.Injective (Pi.mulSingle i)