mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.grothendieckTopology.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsStableUnderBaseChange] [inst_2 : P.HasPullbacks], P.grothendieckTopology = P.coverage.toGrothendieck
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.le_iff_derivFamily : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → ∀ {a : Ordinal.{u}}, (∀ (i : ι), f i a ≤ a) ↔ ∃ o, Ordinal.derivFamily f o = a
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.range_toContinuousMultilinearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N],
  Set.range ContinuousAlternatingMap.toContinuousMultilinearMap =
    {f | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0}
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- Not `@[simp]` since it already reduces to `carrier = carrier`.  -/
AlgebraicGeometry.SheafedSpace.mk_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier)
  (h : presheaf.IsSheaf), ↑{ carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier
-- Aesop.Forward.LevelIndex
Aesop.instInhabitedLevelIndex.default : Aesop.LevelIndex
-- Mathlib.Algebra.Order.Group.PosPart
mabs_div_eq_leOnePart_sq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a : α), |a|ₘ / a = a⁻ᵐ ^ 2
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMonObjObjEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y : Cᵒᵖ},
  CategoryTheory.shrinkYonedaMonObjObjEquiv = Shrink.mulEquiv
-- Mathlib.NumberTheory.Pell
/-- Construct a solution from `x`, `y` and a proof that the equation is satisfied.  -/
Pell.Solution₁.mk : {d : ℤ} → (x y : ℤ) → x ^ 2 - d * y ^ 2 = 1 → Pell.Solution₁ d
-- Lean.Data.KVMap
Lean.KVMap.subset : Lean.KVMap → Lean.KVMap → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- This is a more general but less convenient version of `rpow_le_rpow_of_exponent_ge`.
This version allows `x = 0`, so it explicitly forbids `x = y = 0`, `z ≠ 0`.  -/
Real.rpow_le_rpow_of_exponent_ge_of_imp : ∀ {x y z : ℝ}, 0 ≤ x → x ≤ 1 → z ≤ y → (x = 0 → y = 0 → z = 0) → x ^ y ≤ x ^ z
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.type : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.Expr
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- A function is continuous on a set if and only if its composition with an open partial
homeomorphism on the right is continuous on the corresponding set.  -/
OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y},
  s ⊆ e.target → (ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s))
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- Let `G` act on a space `X` and `A : Set X`. We say `f : X → X` is a decomposition on `A`
as witnessed by some `S : Finset G` if for all `a ∈ A`, the value `f a` can be obtained
by applying some element of `S` to `a` instead.

More familiarly, the restriction of `f` to `A` is the result of partitioning `A` into finitely many
pieces, then applying a single element of `G` to each piece.  -/
Equidecomp.IsDecompOn : {X : Type u_1} → {G : Type u_2} → [SMul G X] → (X → X) → Set X → Finset G → Prop
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space with bounded variation on an
interval is differentiable almost everywhere in this interval. This one differs from
`LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem` by using `DifferentiableAt` instead of
`DifferentiableWithinAt` in its conclusion.  -/
BoundedVariationOn.ae_differentiableAt_of_mem_uIcc : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} {a b : ℝ},
  BoundedVariationOn f (Set.uIcc a b) → ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → DifferentiableAt ℝ f x
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.biSup_fromEdgeSet_singleton_eq : ∀ {V : Type u_1} (G : SimpleGraph V), ⨆ e ∈ G.edgeSet, SimpleGraph.fromEdgeSet {e} = G
-- Lean.Meta.ArgsPacker
/-- Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type
```
(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z]
```
 -/
Lean.Meta.ArgsPacker.uncurryType : Lean.Meta.ArgsPacker → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_lt : ∀ {a b : UInt8}, a.toUInt32 < b.toUInt32 ↔ a < b
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticOnNhd_derivWeierstrassP : ∀ (L : PeriodPair), AnalyticOnNhd ℂ L.derivWeierstrassP (↑L.lattice)ᶜ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (hvw : G.Adj v w),
  (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- The cofan `mapBifunctorLeftUnitorCofan F X e p hp Y j` is a colimit.  -/
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimit : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
                    (X : C) →
                      (e : F.obj X ≅ CategoryTheory.Functor.id D) →
                        [inst_5 :
                            ∀ (Y : D),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] →
                          (p : I × J → J) →
                            (hp : ∀ (j : J), p (0, j) = j) →
                              (Y : CategoryTheory.GradedObject J D) →
                                (j : J) →
                                  CategoryTheory.Limits.IsColimit
                                    (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j)
-- Init.Data.List.Monadic
List.mapM'_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [inst : Monad m] {f : α → m β},
  List.mapM' f (a :: l) = do
    let __do_lift ← f a
    let __do_lift_1 ← List.mapM' f l
    pure (__do_lift :: __do_lift_1)
-- Mathlib.Topology.EMetricSpace.Basic
/-- If a `PseudoEMetricSpace` is a T₀ space, then it is an `EMetricSpace`.  -/
EMetricSpace.ofT0PseudoEMetricSpace : (α : Type u_2) → [inst : PseudoEMetricSpace α] → [T0Space α] → EMetricSpace α
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A single function is uniformly integrable.  -/
MeasureTheory.unifIntegrable_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} [Subsingleton ι],
  1 ≤ p → p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
-- Mathlib.Algebra.Group.Conj
addConj_zsmul : ∀ {α : Type u} [inst : AddGroup α] {i : ℤ} {a b : α}, i • (a + b + -a) = a + i • b + -a
-- Init.Data.String.Basic
String.Pos.cast_eq_endPos : ∀ {s t : String} {hst : s = t} {p : s.Pos}, p.cast hst = t.endPos ↔ p = s.endPos
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.mul_iff_left : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : CommGroup G]
  [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G}, Measurable f → (Measurable (g * f) ↔ Measurable g)
-- Mathlib.Algebra.Order.Monovary
Antivary.mul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Antivary f₁ g → Antivary f₂ g → Antivary (f₁ * f₂) g
-- Mathlib.MeasureTheory.PiSystem
IsPiSystem.insert_univ : ∀ {α : Type u_1} {S : Set (Set α)}, IsPiSystem S → IsPiSystem (insert Set.univ S)
-- Mathlib.Data.List.NodupEquivFin
/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
a bijection `Fin l.length → α`.  See `List.Nodup.getEquivOfForallMemList`
for a version giving an equivalence when there is decidable equality.  -/
List.Nodup.getBijectionOfForallMemList : {α : Type u_1} → (l : List α) → l.Nodup → (∀ (x : α), x ∈ l) → { f // Function.Bijective f }
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The 2-morphism underlying the lax functoriality constraint.  -/
CategoryTheory.LaxFunctor.mapComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.LaxFunctor B C) →
          {a b c : B} →
            (f : a ⟶ b) →
              (g : b ⟶ c) →
                CategoryTheory.CategoryStruct.comp (self.map f) (self.map g) ⟶
                  self.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getD_rightInvSeq_mul_self : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_symmDiff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
-- Init.Data.SInt.Bitwise
Int8.shiftRight_or : ∀ {a b c : Int8}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Init.Control.Lawful.MonadLift.Lemmas
monadLift_map : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α),
  monadLift (f <$> ma) = f <$> monadLift ma
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_counitIso_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  (CategoryTheory.Comma.equivProd L R).counitIso.inv.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.IsSupFiniteCompact.isSupClosedCompact : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupFiniteCompact α → CompleteLattice.IsSupClosedCompact α
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.toAlgebra : {K : Type u} → [inst : Field K] → (s : Subfield K) → Algebra (↥s) K
-- Mathlib.Logic.Relation
/-- The map of a relation `r` through a pair of functions pushes the
relation to the codomains of the functions.  The resulting relation is
defined by having pairs of terms related if they have preimages
related by `r`.
 -/
Relation.Map : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α → β → Prop) → (α → γ) → (β → δ) → γ → δ → Prop
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.nontrivial_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], Nontrivial (LieSubmodule R L M) ↔ Nontrivial M
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom_C : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] (f : P.Hom P') (r : R), f.toAlgHom (MvPolynomial.C r) = MvPolynomial.C ((algebraMap R R') r)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rightComm_symm : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P], (TensorProduct.rightComm R M N P).symm = TensorProduct.rightComm R M P N
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.inclLiftToTerminal_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (x : C),
  (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app x = CategoryTheory.CategoryStruct.id (F.obj x)
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.not_isField : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K],
  ¬IsField ↥(FunctionField.ringOfIntegers F K)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.array : Lean.Lsp.SymbolKind
-- Init.Data.Vector.Lemmas
Vector.foldr_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β},
  Vector.foldr f b xs.reverse = Vector.foldl (fun x y => f y x) b xs
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_x : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).pt = Y
-- Mathlib.Data.Num.Lemmas
Num.castNum_shiftRight : ∀ (m : Num) (n : ℕ), ↑(m >>> n) = ↑m >>> n
-- Mathlib.Data.Matrix.Mul
Matrix.addMonoidHomMulRight_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (M : Matrix m n α) (x : Matrix l m α), M.addMonoidHomMulRight x = x * M
-- Mathlib.Data.Finset.Basic
Finset.filter_ne' : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), {a ∈ s | a ≠ b} = s.erase b
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'.map f =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f)
-- Mathlib.Control.Fold
Traversable.foldMap_map : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] [inst_2 : Monoid γ] (f : α → β)
  (g : β → γ) (xs : t α), Traversable.foldMap g (f <$> xs) = Traversable.foldMap (g ∘ f) xs
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.pp : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_left_zero' : ∀ {α : Type u_2} [inst : AddGroup α] {a : α}, Finset.preimage 0 (fun x => -a + x) ⋯ = {a}
-- Mathlib.Data.Rel.Cover
/-- For an entourage `U`, a set `N` is a *`U`-cover* of a set `s` if every point of `s` is `U`-close
to some point of `N`.

This is also called a *`U`-net* in the literature.

[R. Vershynin, *High Dimensional Probability*][vershynin2018high], 4.2.1.  -/
SetRel.IsCover : {X : Type u_1} → SetRel X X → Set X → Set X → Prop
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_endPos : ∀ {s : String.Slice} {pos : s.Pos}, String.Slice.Pos.ofSliceFrom (s.sliceFrom pos).endPos = s.endPos
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.eq_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E₂} {y : E}, y = e.symm x ↔ e y = x
-- Batteries.Data.List.Basic
/-- `sublists l` is the list of all (non-contiguous) sublists of `l`; cf. `sublists'`
for a different ordering.
```
sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]
```
 -/
List.sublists : {α : Type u_1} → List α → List (List α)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_apply : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : ι → M') (x : M),
  ((b.constr S) f) x = (b.repr x).sum fun b a => a • f b
-- Mathlib.RingTheory.Congruence.Hom
/-- The **first isomorphism theorem for semirings**.  -/
RingCon.quotientKerEquivRangeS : {M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring P] → (f : M →+* P) → (RingCon.ker f).Quotient ≃+* ↥f.rangeS
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.eq_1 : ∀ (x : ℝ*) (r : ℝ), x.IsSt r = ∀ (δ : ℝ), 0 < δ → ↑r - ↑δ < x ∧ x < ↑r + ↑δ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_lt_rpow_of_pos_of_lt_one_of_neg : ∀ {x z : ℝ}, 0 < x → x < 1 → z < 0 → 1 < x ^ z
-- Mathlib.Algebra.Order.SuccPred
strictAntiOn_of_lt_sub_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.arrowSucc.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (i : J) (hi : i < j),
  CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi =
    CategoryTheory.SmallObject.SuccStruct.arrowMap F i (Order.succ i) ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- **Alias** of the reverse direction of `Matrix.isHyperbolic_neg_iff`. -/
Matrix.IsHyperbolic.neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  m.IsHyperbolic → (-m).IsHyperbolic
-- Std.Time.Zoned.RecurringRule
/-- Returns the `Day.Offset` (days since epoch) for a `TransitionSpec.julian0` in the given year.

`n`: zero-based day 0–365. Feb 29 is counted normally in leap years.
 -/
Std.Time.TimeZone.TransitionSpec.toEpochDayJulian0 : Std.Time.Year.Offset → Std.Time.Internal.Bounded.LE 0 365 → Std.Time.Day.Offset
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.carrier_eq_coe : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s : ClosedSubmodule R M), (↑s).carrier = ↑s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- A complex measure is said to `HaveLebesgueDecomposition` with respect to a positive measure
if both its real and imaginary part `HaveLebesgueDecomposition` with respect to that measure.  -/
MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α → MeasureTheory.Measure α → Prop
-- Lean.Elab.App
/-- Return the next argument to be processed.
The result is `.none` if it is an implicit argument which was not provided using a named argument.
The result is `.undef` if `args` is empty and `namedArgs` does contain an entry for `binderName`.
 -/
Lean.Elab.Term.ElabElim.getNextArg? : Lean.Name → Lean.BinderInfo → Lean.Elab.Term.ElabElim.M (Lean.LOption Lean.Elab.Term.Arg)
-- Mathlib.Algebra.Module.NatInt
Nat.smul_one_eq_cast : ∀ {R : Type u_5} [inst : NonAssocSemiring R] (m : ℕ), m • 1 = ↑m
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of probability measures `f* : ProbabilityMeasure X → ProbabilityMeasure Y`
is continuous (in the topologies of convergence in distribution).  -/
MeasureTheory.ProbabilityMeasure.continuous_map : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] [inst_2 : TopologicalSpace Ω]
  [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω'] [inst_5 : BorelSpace Ω'] {f : Ω → Ω'}
  (f_cont : Continuous f), Continuous fun ν => ν.map ⋯
-- Mathlib.AlgebraicTopology.CechNerve
/-- The morphism between augmented Čech conerves associated to a morphism of arrows.  -/
CategoryTheory.Arrow.mapAugmentedCechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
        [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] →
          (f ⟶ g) → (f.augmentedCechConerve ⟶ g.augmentedCechConerve)
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_lt_of_le'`. -/
LT.lt.trans_le' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b < a → c ≤ b → c < a
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.isGLB_Ioi : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], Order.IsPredLimit a → IsGLB (Set.Ioi a) a
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → Filter.Tendsto g l (uniformity α) → Filter.Tendsto (f * g) l (uniformity α)
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌊(b - v) / r⌋ - ⌊(a - v) / r⌋` numbers congruent to `v` mod `r` in `(a, b]`,
if `a ≤ b`. `Nat` version of `Int.Ioc_filter_modEq_card`.  -/
Nat.Ioc_filter_modEq_card : ∀ (a b : ℕ) {r : ℕ},
  0 < r → ∀ (v : ℕ), ↑{x ∈ Finset.Ioc a b | x ≡ v [MOD r]}.card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelZeroIsoSource_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.kernelZeroIsoSource.inv =
    CategoryTheory.Limits.kernel.lift 0 (CategoryTheory.CategoryStruct.id X) ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  ContDiffOn 𝕜 n Φ s ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => Φ x i) s
-- Mathlib.Topology.Order.Basic
pi_Ioc_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' b' x' : ι → α} [Nonempty ι], (∀ (i : ι), a' i < x' i) → (∀ (i : ι), x' i < b' i) → Set.Ioc a' b' ∈ nhds x'
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β), (f.comp g).withTop = f.withTop.comp g.withTop