mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_mk_mk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (x : R),
  (DoubleQuot.quotQuotEquivComm I J)
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) x)) =
    (algebraMap R ((R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
-- Mathlib.Topology.Inseparable
SeparationQuotient.lift_comp_mk : ∀ {X : Type u_1} {α : Type u_4} [inst : TopologicalSpace X] {f : X → α} (hf : ∀ (x y : X), Inseparable x y → f x = f y),
  SeparationQuotient.lift f hf ∘ SeparationQuotient.mk = f
-- Mathlib.Algebra.Order.Monovary
Monovary.mul_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g₁ g₂ : ι → β},
  0 ≤ g₁ → 0 ≤ g₂ → Monovary f g₁ → Monovary f g₂ → Monovary f (g₁ * g₂)
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_eval_zero : ∀ (k : ℕ), bernoulliFun k 0 = ↑(bernoulli k)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.instCompleteLattice : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → CompleteLattice (I.Filtration M)
-- Init.Control.Basic
instMonadControlTOfMonadControl : (m : Type u_1 → Type u_2) →
  (n : Type u_1 → Type u_3) → (o : Type u_1 → Type u_4) → [MonadControl n o] → [MonadControlT m n] → MonadControlT m o
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X)
      ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) =
    CategoryTheory.CategoryStruct.id (((t.eTruncGE.obj a).comp (t.eTruncGE.obj b)).obj X)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxEntry.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false),
  x.maxEntry x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_1 =>
      l_1.maxEntry ⋯
-- Mathlib.Data.Set.Disjoint
Set.disjoint_of_subset_right : ∀ {α : Type u} {s t u : Set α}, t ⊆ u → Disjoint s u → Disjoint s t
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- If `c` is a cone over a functor `J ⥤ C` and `f : c.pt ⟶ X`, then for every `j : J` we can take
the pushout of `c.π.app j` and `f`. This gives a new cone with cone point `X`, and this cone is
again a limit cone as long as `J` is connected and `C` has exact limits of shape `J`.
 -/
CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    [CategoryTheory.IsConnected J] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.Limits.HasPushouts C] →
            [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              [CategoryTheory.HasExactLimitsOfShape J C] →
                {F : CategoryTheory.Functor J C} →
                  {c : CategoryTheory.Limits.Cone F} →
                    CategoryTheory.Limits.IsLimit c →
                      {X : C} →
                        (f : c.pt ⟶ X) →
                          CategoryTheory.Limits.IsLimit
                            { pt := X,
                              π := CategoryTheory.Limits.pushout.inr c.π ((CategoryTheory.Functor.const J).map f) }
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.HasSubobjectClassifier.instIsRegularMonoTruth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C],
  CategoryTheory.IsRegularMono (CategoryTheory.HasSubobjectClassifier.truth C)
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasChanged : Lean.Widget.DiffTag
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isClosed_iff_isFlat : ∀ {α : Type u_2} {M : Matroid α} {F : ↑(Set.Iic M.E)}, M.subtypeClosure.IsClosed F ↔ M.IsFlat ↑F
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsOpen
-- Mathlib.Data.Set.Lattice
Set.disjoint_iUnion₂_right : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α},
  Disjoint s (⋃ i, ⋃ j, t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j)
-- Mathlib.NumberTheory.Cyclotomic.Basic
Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) →
    IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {D : Type u_1} [inst_3 : CategoryTheory.Category.{v_1, u_1} D],
  ((CategoryTheory.Functor.whiskeringLeft (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C) D).obj
      DerivedCategory.Qh).Faithful
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.Full.mapGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful], F.mapGrp.Full
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.quotedPairChar.match_1.splitter : (motive : Char → Sort u_1) →
  (c : Char) →
    (Unit → motive '\t') →
      (Unit → motive ' ') → ((x : Char) → (x = '\t' → False) → (x = ' ' → False) → motive x) → motive c
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integral_fintype_prod_volume_eq_pow : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {E : Type u_3} (f : E → 𝕜)
  [inst_2 : MeasureTheory.MeasureSpace E] [MeasureTheory.SigmaFinite MeasureTheory.volume],
  ∫ (x : ι → E), ∏ i, f (x i) = (∫ (x : E), f x) ^ Fintype.card ι
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_le : ∀ {a b : Int16}, a ≤ b → a.toNatClampNeg ≤ b.toNatClampNeg
-- Aesop.Tree.Data
Aesop.MVarCluster : Type
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.Hom.Simps.hom.eq_1 : ∀ (X Y : MonCat) (f : X.Hom Y), MonCat.Hom.Simps.hom X Y f = f.hom
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_comm : ∀ (x y : ℕ), x &&& y = y &&& x
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mapEquiv_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (g : M ≃ₗ[R] N) (a : DividedPowerAlgebra R M),
  (DividedPowerAlgebra.mapEquiv g) a = (DividedPowerAlgebra.map R ↑g) a
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.fix_eval : ∀ (f : Turing.ToPartrec.Code),
  f.fix.eval = PFun.fix fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
-- Mathlib.Topology.Algebra.Module.LocallyConvex
instLocallyConvexSpaceSubtypeMemSubmodule : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] {S : Submodule 𝕜 E},
  LocallyConvexSpace 𝕜 ↥S
-- Mathlib.GroupTheory.GroupAction.Pointwise
Set.MapsTo.vadd_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : VAdd M α]
  [inst_1 : VAdd N β] [inst_2 : FunLike F α β] [AddActionSemiHomClass F σ α β] {f : F} {s : Set α} {t : Set β},
  Set.MapsTo (⇑f) s t → ∀ (c : M), Set.MapsTo (⇑f) (c +ᵥ s) (σ c +ᵥ t)
-- Mathlib.Data.Matrix.Basic
MulOpposite.isStablyFiniteRing_iff : ∀ (α : Type u_14) [inst : MulOne α] [inst_1 : AddCommMonoid α], IsStablyFiniteRing αᵐᵒᵖ ↔ IsStablyFiniteRing α
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_add : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : Add α]
  (M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α), (M + N).blockDiag' = M.blockDiag' + N.blockDiag'
-- Mathlib.RingTheory.Ideal.Maps
Ideal.smul_top_eq_map : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R),
  I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mker (AddMonoidHom.snd M N) = ⊤.prod ⊥
-- Mathlib.Order.Zorn
Flag.exists_mem_mem : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ∃ s, a ∈ s ∧ b ∈ s
-- Mathlib.Analysis.Convex.Segment
segment.lift : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (R : Type u_7) [inst_5 : Semiring R] [inst_6 : PartialOrder R]
  [inst_7 : Module R E] [inst_8 : Module R 𝕜] [IsScalarTower R 𝕜 E] [SMulPosMono R 𝕜] (x y : E),
  segment R x y ⊆ segment 𝕜 x y
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If `G` preserves coequalizers and `C` has them, then the cofork constructed of the mapped morphisms
of a cofork is a colimit.
 -/
CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f g : X ⟶ Y) →
              [inst_2 : CategoryTheory.Limits.HasCoequalizer f g] →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.coequalizer.π f g)) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.opSpan_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpanᵒᵖ),
  (CategoryTheory.Limits.opSpan f g).hom.app X_1 =
    (match Opposite.unop X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).inv
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.mk : {α β σ : Type} →
  Lean.ScopedEnvExtension.Descr α β σ →
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
        (Lean.ScopedEnvExtension.StateStack α β σ) →
      Lean.ScopedEnvExtension α β σ
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalNonAssocCommRing` instance along an injective function.  -/
Function.Injective.nonUnitalNonAssocCommRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : Neg S] →
            [inst_4 : Sub S] →
              [inst_5 : SMul ℕ S] →
                [inst_6 : SMul ℤ S] →
                  [inst_7 : NonUnitalNonAssocCommRing R] →
                    (f : S → R) →
                      Function.Injective f →
                        f 0 = 0 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (x : S), f (-x) = -f x) →
                                (∀ (x y : S), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : S), f (n • x) = n • f x) → NonUnitalNonAssocCommRing S
-- Lean.Parser.Basic
/-- The `LeadingIdentBehavior`, which specifies how the parsing table
lookup function behaves for the first identifier to be parsed.
This is used by the `tactic` parser to avoid creating a reserved
symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.).  -/
Lean.Parser.ParserCategory.behavior : Lean.Parser.ParserCategory → Lean.Parser.LeadingIdentBehavior
-- Init.Core
/-- `Task.pure (a : α)` constructs a task that is already resolved with value `a`.  -/
Task.pure : {α : Type u} → α → Task α
-- Mathlib.AlgebraicTopology.Reedy.Basic
/-- The Reedy factorization of a morphism `f : X ⟶ Y` as a morphism in `W₁`
followed by a morphism in `W₂`.  -/
HomotopicalAlgebra.ReedyStructure.mapFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] →
                  [inst_6 : WellFoundedLT α] →
                    HomotopicalAlgebra.ReedyStructure W₁ W₂ α → {X Y : C} → (f : X ⟶ Y) → W₁.MapFactorizationData W₂ f
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.hasNext : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → (it.hasNext = true ↔ r ≠ [])
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k : α}, k ∈ Std.TreeMap.filter f t → k ∈ t
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.type : Lean.Meta.Sym.Arith.Semiring → Lean.Expr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q),
  CategoryTheory.Subobject.mk P.obj.hom ≤ CategoryTheory.Subobject.mk Q.obj.hom
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.surjective_rangeRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Function.Surjective ⇑f.rangeRestrict
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- See `Real.rpow_inv_log` for the equality when `x ≠ 1` is strictly positive.  -/
Real.rpow_inv_log_le_exp_one : ∀ {x : ℝ}, x ^ (Real.log x)⁻¹ ≤ Real.exp 1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The set of infinite places of `L` that lie above a given infinite place of `K`.  -/
NumberField.InfinitePlace.placesOver : {K : Type u_4} →
  (L : Type u_5) →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace K → Set (NumberField.InfinitePlace L)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The `Y`-coordinate of `(x₁, y₁) + (x₂, y₂)` for two nonsingular affine points `(x₁, y₁)` and
`(x₂, y₂)` on a Weierstrass curve `W`, where the line through them has a slope of `ℓ`.

This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `ℓ`.  -/
WeierstrassCurve.Affine.addY : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → R → R → R
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashSet.ofList l).isEmpty = l.isEmpty
-- Mathlib.FieldTheory.Extension
IntermediateField.nonempty_algHom_of_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K],
  (∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) → Nonempty (E →ₐ[F] K)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- Extension of maps to completions  -/
AbstractCompletion.extend : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) → {β : Type uβ} → [UniformSpace β] → (α → β) → pkg.space → β
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.t3Space : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [T3Space F] (b : B), T3Space (E b)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instNontrivial : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [Nontrivial R] [Nonempty M], Nontrivial (MonoidAlgebra R M)
-- Mathlib.Data.Finset.Powerset
Finset.mem_powersetCard : ∀ {α : Type u_1} {n : ℕ} {s t : Finset α}, s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit : Lean.Expr → optParam Bool false → Lean.Elab.Command.NameGen.MkNameM✝ String
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommGroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommGroup Y],
  LocallyConstant.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: if `a ≤ b` and `f' b < m < f' a`, then `f' c = m` for some `c ∈ (a, b)`.
 -/
exists_hasDerivWithinAt_eq_of_lt_of_gt : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, m < f' a → f' b < m → m ∈ f' '' Set.Ioo a b
-- Mathlib.Analysis.Normed.Group.Pointwise
/-- **Alias** of `infEDist_inv_inv`. -/
infEdist_inv_inv : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (x : E) (s : Set E), Metric.infEDist x⁻¹ s⁻¹ = Metric.infEDist x s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
-- Mathlib.Topology.UniformSpace.Basic
uniformity_setCoe : ∀ {α : Type ua} {s : Set α} [inst : UniformSpace α],
  uniformity ↑s = Filter.comap (Prod.map Subtype.val Subtype.val) (uniformity α)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_basis_Iio' : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] [NoMinOrder α] (a : α),
  Filter.atBot.HasBasis (fun x => x < a) Set.Iio
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.isometry_embedding_of_isReal : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (hv : v.IsReal),
  Isometry ⇑((NumberField.InfinitePlace.embedding_of_isReal hv).comp (WithAbs.equiv ↑v).toRingHom)
-- Lean.Parser.Extension
/-- Result of resolving a parser name.  -/
Lean.Parser.ParserResolution : Type
-- Mathlib.SetTheory.Cardinal.Regular
/-- A cardinal is regular if it is infinite and it equals its own cofinality.  -/
Cardinal.IsRegular : Cardinal.{u_1} → Prop
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.Nat.one_le_cast_of_le : ∀ {α : Type} [inst : AddCommMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, 1 ≤ n → 1 ≤ ↑n
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.K'.elim.match_1.eq_4 : ∀ (motive : Turing.PartrecToTM2.K' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.K'.main)
  (h_2 : Unit → motive Turing.PartrecToTM2.K'.rev) (h_3 : Unit → motive Turing.PartrecToTM2.K'.aux)
  (h_4 : Unit → motive Turing.PartrecToTM2.K'.stack),
  (match Turing.PartrecToTM2.K'.stack with
    | Turing.PartrecToTM2.K'.main => h_1 ()
    | Turing.PartrecToTM2.K'.rev => h_2 ()
    | Turing.PartrecToTM2.K'.aux => h_3 ()
    | Turing.PartrecToTM2.K'.stack => h_4 ()) =
    h_4 ()
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- **Alias** of `MeasureTheory.setIntegral_finset`. -/
MeasureTheory.integral_finset : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X}
  (s : Finset X), MeasureTheory.IntegrableOn f (↑s) μ → ∫ (x : X) in ↑s, f x ∂μ = ∑ x ∈ s, μ.real {x} • f x
-- Lean.DocString.Parser
/-- Parses a block.
 -/
Lean.Doc.Parser.block : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Set.Basic
Set.mem_inter_iff : ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
-- Init.Data.Array.Lex.Lemmas
Array.empty_le : ∀ {α : Type u_1} [inst : LT α] (xs : Array α), #[] ≤ xs
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.instIsIsoMapRAppιOfIsIdempotent : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) [Φ.IsIdempotent] (X : C), CategoryTheory.IsIso (Φ.r.map (Φ.ι.app X))
-- Mathlib.Algebra.Module.Projective
/-- A direct summand of a projective module is projective.  -/
Module.Projective.of_split : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Projective R M] (i : P →ₗ[R] M) (s : M →ₗ[R] P),
  s ∘ₗ i = LinearMap.id → Module.Projective R P
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.im_pos_of_dist_center_le : ∀ {z : UpperHalfPlane} {r : ℝ} {w : ℂ}, dist w ↑(z.center r) ≤ z.im * Real.sinh r → 0 < w.im
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_bitVecToNat : ∀ (n : BitVec System.Platform.numBits), USize.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.cotangentComplex_injective : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  Function.Injective ⇑P.toExtension.cotangentComplex
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_curry_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor (B × C) D),
  CategoryTheory.Functor.uncurry.obj (CategoryTheory.Functor.curry.obj F) = F
-- Init.Data.UInt.Basic
instMinUInt16 : Min UInt16
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFreeOn_of_card_lt : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α}, s.card < n → G.CliqueFreeOn (↑s) n
-- Mathlib.Algebra.Lie.Basic
LieModule.mk : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M],
  (∀ (t : R) (x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆) →
    (∀ (t : R) (x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) → LieModule R L M
-- Mathlib.Topology.MetricSpace.Algebra
Real.isBoundedSMul : IsBoundedSMul ℝ ℝ