mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.EssentialFiniteness
/-- A ring hom is essentially of finite type if it is the composition of a localization map
and a ring hom of finite type. See `Algebra.EssFiniteType`.  -/
RingHom.EssFiniteType : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.RingTheory.Noetherian.Orzech
/-- Any Noetherian ring satisfies Orzech property.
See also `IsNoetherian.injective_of_surjective_of_submodule` and
`IsNoetherian.injective_of_surjective_of_injective`.  -/
IsNoetherianRing.orzechProperty : ∀ (R : Type u_1) [inst : Ring R] [IsNoetherianRing R], OrzechProperty R
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₂ =
    (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteAsIntModule : {α : Type u_1} → [Lean.Grind.CommRing α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Poly → α
-- Mathlib.Order.ModularLattice
/-- **Alias** of `covBy_sup_of_inf_covBy_of_inf_covBy_right`. -/
CovBy.sup_of_inf_of_inf_right : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The product `Π t : α, f t` of a family of topological modules is isomorphic
(both topologically and algebraically) to the space `f ⬝` when `α` only contains `⬝`.

This is `Equiv.piUnique` as a `ContinuousLinearEquiv`.
 -/
ContinuousLinearEquiv.piUnique : {α : Type u_9} →
  [inst : Unique α] →
    (R : Type u_10) →
      [inst_1 : Semiring R] →
        (f : α → Type u_11) →
          [inst_2 : (x : α) → AddCommMonoid (f x)] →
            [inst_3 : (x : α) → Module R (f x)] →
              [inst_4 : (x : α) → TopologicalSpace (f x)] → ((t : α) → f t) ≃L[R] f default
-- Lean.Structure
/-- Returns true if `constName` is the name of an inductive datatype
created using the `structure` or `class` commands.

These are inductive types for which structure information has been registered with `registerStructure`.
See also `Lean.getStructureInfo?`.
 -/
Lean.isStructure : Lean.Environment → Lean.Name → Bool
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
/-- A family of objects is "hom orthogonal" if
there is at most one morphism between distinct objects.

(In a category with zero morphisms, that must be the zero morphism.)  -/
CategoryTheory.HomOrthogonal : {C : Type u} → [CategoryTheory.Category.{v, u} C] → {ι : Type u_1} → (ι → C) → Prop
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (x : L) (i : ℕ),
  (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) =
    ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly.coeff i
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.mem_fundCocircuit : ∀ {α : Type u_1} (M : Matroid α) (e : α) (B : Set α), e ∈ M.fundCocircuit e B
-- Mathlib.Order.Antisymmetrization
toAntisymmetrization_le_toAntisymmetrization_iff : ∀ {α : Type u_1} {a b : α} [inst : Preorder α],
  toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a ≤ toAntisymmetrization (fun x1 x2 => x1 ≤ x2) b ↔ a ≤ b
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.nil.sizeOf_spec : sizeOf Lean.Meta.Grind.PendingSolverPropagationsData.nil✝ = 1
-- Mathlib.Order.Heyting.Basic
LE.le.disjoint_compl_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ b → Disjoint a bᶜ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {f : Option β → Option β},
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k' =
        if (k == k') = true then f (Std.DHashMap.Internal.Raw₀.Const.get? m k)
        else Std.DHashMap.Internal.Raw₀.Const.get? m k'
-- Std.Data.ByteSlice
instSliceableByteSliceNat_3 : Std.Roc.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.instIsRegularEpiOfNormalEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : CategoryTheory.NormalEpi f],
  CategoryTheory.IsRegularEpi f
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.mk'.sizeOf_spec : ∀ {α : Type v} [small : Std.Internal.Small α] [inst : SizeOf α] (inner : Std.Internal.ComputableSmall.Target α),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Topology.EMetricSpace.Defs
/-- Extended distance between two points  -/
EDist.edist : {α : Type u_2} → [self : EDist α] → α → α → ENNReal
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.instIsSplitMonoDiag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [inst_1 : CategoryTheory.Limits.HasBinaryProduct X X],
  CategoryTheory.IsSplitMono (CategoryTheory.Limits.diag X)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.coeff_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f pf s x → ∀ (v : Fin 0 → E), (pf 0) v = f x
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffOn_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E],
  UniqueDiffOn 𝕜 Set.univ
-- Std.Http.Data.URI.Config
/-- Maximum length of the query string, in bytes.
Raised from the previously hardcoded 1024 to 8192 to match `H1.Config.maxUriLength`
and allow real-world query strings.
 -/
Std.Http.URI.Config.maxQueryLength : Std.Http.URI.Config → ℕ
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- If all edge weights are non-negative, then the weight of any path is non-negative.  -/
Quiver.Path.weight_nonneg : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {w : {i j : V} → (i ⟶ j) → R},
  (∀ {i j : V} (e : i ⟶ j), 0 ≤ w e) → ∀ {i j : V} (p : Quiver.Path i j), 0 ≤ Quiver.Path.weight (fun {i j} => w) p
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instReprRingMode.repr : Mathlib.Tactic.RingNF.RingMode → ℕ → Std.Format
-- Mathlib.Topology.Order.ExtendFrom
continuousOn_uIcc_extendFrom_uIoo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {la lb : β} [RegularSpace β],
  ContinuousOn f (Set.uIoo a b) →
    Filter.Tendsto f (nhdsWithin a (Set.uIoo a b)) (nhds la) →
      Filter.Tendsto f (nhdsWithin b (Set.uIoo a b)) (nhds lb) →
        ContinuousOn (extendFrom (Set.uIoo a b) f) (Set.uIcc a b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α], Additive.ofMul ⊥ = ⊥
-- Mathlib.Data.Nat.Prime.Pow
Nat.Prime.pow_minFac : ∀ {p k : ℕ}, Nat.Prime p → k ≠ 0 → (p ^ k).minFac = p
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.map_id : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α), pkg.map pkg id = id
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.mk : {α : Type u} → α → Std.Rci α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.logDeriv_sin : logDeriv Complex.sin = Complex.cot
-- Init.Data.Vector.Basic
Vector.flatMap : {α : Type u_1} → {n : ℕ} → {β : Type u_2} → {m : ℕ} → Vector α n → (α → Vector β m) → Vector β (n * m)
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
/-- Implementation of `Mon.hasLimitsOfShape`:
the proposed cone over a functor `F : J ⥤ Mon C` is a limit cone.
 -/
CategoryTheory.Mon.limitConeIsLimit : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) →
              (hc : CategoryTheory.Limits.IsLimit c) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Mon.limitCone F c hc)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {X_1 Y : F.DescentData f} (φ : X_1 ⟶ Y) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor F sq sq₃).map φ).hom i = φ.hom i
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- If `forget C` reflects terminals and `ToType X` is a singleton, then `X` is terminal.  -/
CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
              (X : C) → Unique (CategoryTheory.ToType X) → CategoryTheory.Limits.IsTerminal X
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_is_cauchy : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  IsCauSeq norm (newton_seq_gen✝ hnorm)
-- Mathlib.Tactic.GCongr.Core
/-- The core of the `gcongr` tactic.  Parse a goal into the form `(f _ ... _) ∼ (f _ ... _)`,
look up any relevant `@[gcongr]` lemmas, try to apply them, recursively run the tactic itself on
"main" goals which are generated, and run the discharger on side goals which are generated. If there
is a user-provided template, first check that the template asks us to descend this far into the
match.  -/
Lean.MVarId.gcongr : Lean.MVarId → Option Bool → optParam ℕ 1000000 → Mathlib.Tactic.GCongr.GCongrM Bool
-- Mathlib.Algebra.Order.Field.Basic
_private.Mathlib.Algebra.Order.Field.Basic.0.exists_mul_right_lt₀ : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  a * b < c → ∃ b' > b, a * b' < c
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.select_add_select_not : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (P : ℕ → Prop) [hp : Fact (Nat.Prime p)] (x : WittVector p R),
  WittVector.select P x + WittVector.select (fun i => ¬P i) x = x
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Bundled graded (semi)ring homomorphisms. Use `GradedRingHom` for the namespace and other
identifiers, and `𝒜 →+*ᵍ ℬ` for the notation.  -/
GradedRingHom : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [Semiring A] → [Semiring B] → [SetLike σ A] → [SetLike τ B] → (ι → σ) → (ι → τ) → Type (max u_2 u_3)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If `f` is a continuous alternating map on `E`
and `m` is an element of `ι → E` such that one of the `m i` has norm `0`, then `f m` has norm `0`.

Note that we cannot drop the continuity assumption.
Indeed, let `ℝ₀` be a copy or `ℝ` with zero norm and indiscrete topology.
Then `f : (Unit → ℝ₀) → ℝ` given by `f x = x ()`
sends vector `1` with zero norm to number `1` with nonzero norm.  -/
AlternatingMap.norm_map_coord_zero : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] (f : E [⋀^ι]→ₗ[𝕜] F), Continuous ⇑f → ∀ {m : ι → E} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mapRingHom_apply : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] (f : K →+* L) (x : NumberField.RingOfIntegers K),
  ↑((NumberField.RingOfIntegers.mapRingHom f) x) = f ↑x
-- Mathlib.LinearAlgebra.CrossProduct
/-- The cross product of two vectors is perpendicular to the first vector.  -/
dot_self_cross : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), v ⬝ᵥ (crossProduct v) w = 0
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {n : ℕ} {a : α},
  p a = true → List.findIdxNth p (a :: xs) n = if n = 0 then 0 else List.findIdxNth p xs (n - 1) + 1
-- Mathlib.CategoryTheory.Limits.Types.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ Type*`, this is the inclusion `(F.obj (op j)).obj j ⟶ coend F`
for any `j : J`, which sends `x` to `Quot.mk _ ⟨j, x⟩`  -/
CategoryTheory.Limits.Types.coend.ι : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) →
      (j : J) → (F.obj (Opposite.op j)).obj j ⟶ CategoryTheory.Limits.Types.coend F
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : C} [inst_3 : CategoryTheory.AddMonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom)
      CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Free
/-- Embedding from magma to its free semigroup.  -/
Magma.AssocQuotient.of : {α : Type u} → [inst : Mul α] → α →ₙ* Magma.AssocQuotient α
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Monoid objects in `C` are "just" lax monoidal functors from the trivial monoidal category to `C`.
 -/
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C ≌ CategoryTheory.Mon C
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore : Lean.Expr →
  Lean.Meta.Grind.Arith.Linear.LinExpr →
    Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_union_inter`. -/
Set.diff_union_inter : ∀ {α : Type u_1} (s t : Set α), s \ t ∪ s ∩ t = s
-- Mathlib.Algebra.Ring.Parity
isUnit_two_iff_forall_even : ∀ {α : Type u_2} [inst : Semiring α], IsUnit 2 ↔ ∀ (a : α), Even a
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsUpperSet (f i j)) → IsUpperSet (⋃ i, ⋃ j, f i j)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin_apply : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k),
  (s.orderEmbOfFin h) i = (s.sort fun a b => a ≤ b)[i]
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_sConvexComb_right_le : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] (x : X)
  (f : Convexity.StdSimplex ℝ X), dist x (Convexity.sConvexComb f) ≤ Convexity.iConvexComb f (dist x)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.liftCLM_mk : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M]
  [inst_6 : Semiring S] [inst_7 : AddCommMonoid N] [inst_8 : Module S N] [inst_9 : TopologicalSpace N] {σ : R →+* S}
  (f : M →SL[σ] N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (x : M),
  (SeparationQuotient.liftCLM f hf) (SeparationQuotient.mk x) = f x
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G),
  ∫ (a : G), f a ∂MeasureTheory.Measure.comap (⇑φ) μ = MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂μ
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.RespectsIso],
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)) →
    P.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If `C` is `w`-locally small, any sieve induces a subfunctor of `shrinkYoneda.{w}.obj X`.  -/
CategoryTheory.Sieve.shrinkFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      {X : C} → CategoryTheory.Sieve X → CategoryTheory.Subfunctor (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.isBase_of_spanning : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → M.Spanning I → M.IsBase I
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Make a new heap containing `a`.  -/
Batteries.BinomialHeap.singleton : {α : Type u} → {le : α → α → Bool} → α → Batteries.BinomialHeap α le
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.instInhabitedFreeBicategory : (B : Type u) → [Inhabited B] → Inhabited (CategoryTheory.FreeBicategory B)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
isGLB_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  s.Nonempty → autoParam (BddBelow s) isGLB_csInf._auto_1 → IsGLB s (sInf s)
-- Mathlib.Data.Sym.Sym2
/-- One can use `attribute [local instance] Sym2.Rel.setoid` to temporarily
make `Quotient` functionality work for `α × α`.  -/
Sym2.Rel.setoid : (α : Type u) → Setoid (α × α)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_obj_X : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ)
  (K : CochainComplex C ℤ) (i : ℤ), ((CochainComplex.shiftFunctor C n).obj K).X i = K.X (i + n)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapIso_inv : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ),
  (groupCohomology.mapIso e e' he n).inv =
    groupCohomology.map (↑e) (Rep.ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.eq_2 : ∀ {α : Type u_1} (a : ℕ) (a_1 : Batteries.BinomialHeap.Imp.Heap α) (a_2 : α)
  (c s : Batteries.BinomialHeap.Imp.HeapNode α),
  Batteries.BinomialHeap.Imp.HeapNode.toHeap.go (Batteries.BinomialHeap.Imp.HeapNode.node a_2 c s) a a_1 =
    Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s (a - 1) (Batteries.BinomialHeap.Imp.Heap.cons (a - 1) a_2 c a_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertManyIfNewUnit_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit}, m.WF → m.insertManyIfNewUnit [] = m
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.filter_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
  f ≤ g → μ.FiniteAtFilter g → μ.FiniteAtFilter f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The left adjoint to `right`.  -/
CategoryTheory.Bicategory.LeftAdjoint.left : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → {right : b ⟶ a} → CategoryTheory.Bicategory.LeftAdjoint right → (a ⟶ b)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  FreeAddMonoid.map f =
    { toFun := fun l => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n₀ n₁ n₂ : ℤ) (z : CochainComplex.HomComplex.Cochain F G n₀),
  CochainComplex.HomComplex.δ n₁ n₂ (CochainComplex.HomComplex.δ n₀ n₁ z) = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `v` is a linearly independent family of vectors and the kernel of a linear map `f` is
disjoint with the submodule spanned by the vectors of `v`, then `f ∘ v` is a linearly independent
family of vectors. See also `LinearIndependent.map'` for a special case assuming `ker f = ⊥`.  -/
LinearIndependent.map : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M'] [inst_3 : Module R M] [inst_4 : Module R M'],
  LinearIndependent R v →
    ∀ {f : M →ₗ[R] M'}, Disjoint (Submodule.span R (Set.range v)) f.ker → LinearIndependent R (⇑f ∘ v)
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_neg_neg_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A * A⁻¹ * A⁻¹).card ≤ K ^ 2 * ↑A.card
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_inf_distrib_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α),
  s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.envExtensionsRef : IO.Ref (Array (Lean.EnvExtension Lean.EnvExtensionState))