mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ}, ProbabilityTheory.IsSFiniteKernel (κ.parallelComp η)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.exists_multiset_of_mem_closure : ∀ {M : Type u_4} [inst : AddCommMonoid M] {s : Set M} {x : M},
  x ∈ AddSubmonoid.closure s → ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.sum = x
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.mk : {α : Type} →
  Std.Queue (α × IO.Promise Bool) →
    Std.Queue (Std.CloseableChannel.Consumer✝ α) → Bool → Std.CloseableChannel.Zero.State✝ α
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.toSearcher_eq : ∀ {pat : String} {s : String.Slice},
  String.Slice.Pattern.ToForwardSearcher.toSearcher pat s =
    String.Slice.Pattern.ToForwardSearcher.toSearcher pat.toSlice s
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.IsDescendingCentralSeries`.

---

A sequence of subgroups of `G` is a descending central series if `H 0` is `G` and
`⁅H n, G⁆ ⊆ H (n + 1)` for all `n`. Note that we do not require that `H n = {1}` for some `n`.  -/
IsDescendingCentralSeries : {G : Type u_1} → [inst : Group G] → (ℕ → Subgroup G) → Prop
-- Mathlib.Topology.Algebra.Support
tsupport_fun_neg : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : SubtractionMonoid α] (f : X → α),
  (tsupport fun x => -f x) = tsupport f
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_insert_one : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set R), Subring.closure (insert 1 s) = Subring.closure s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_top_iff_nat : ∀ {α : Type u_1} {m : α → ENNReal} {f : Filter α}, Filter.Tendsto m f (nhds ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.appLE U.ι U ⊤ ⋯)
-- Lean.Server.Requests
Lean.Server.instMonadLiftIORequestM : MonadLift IO Lean.Server.RequestM
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex hyperbolic sine function, defined via `exp`  -/
Complex.sinh : ℂ → ℂ
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, panicking if no such element exists.
 -/
Std.ExtTreeSet.getLE! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the first
vector in each angle negated, results in π. If the vectors add to 0, this is a version of the
sum of the angles of a triangle.  -/
Orientation.oangle_add_cyc3_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V},
  x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑Real.pi
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_map : ∀ {R : Type u} [inst : Semiring R] {A : Type u_1} [inst_1 : Semiring A] (f : R →+* A) (p : Polynomial R),
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).integralNormalization = Polynomial.map f p.integralNormalization
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableLtOffset : {x y : Std.Time.Minute.Offset} → Decidable (x < y)
-- Mathlib.Topology.Algebra.AsymptoticCone
/-- If `v` is in the asymptotic cone of a closed convex set `s`, then for every `p ∈ s`, the ray of
direction `v` starting from `p` is contained in `s`.  -/
Convex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : TopologicalSpace k] [OrderTopology k] [inst_5 : AddCommGroup V] [inst_6 : Module k V]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V},
  Convex k s → IsClosed s → 0 ≤ c → v ∈ asymptoticCone k s → p ∈ s → c • v +ᵥ p ∈ s
-- Init.Prelude
instBEqOfDecidableEq : {α : Type u_1} → [DecidableEq α] → BEq α
-- Mathlib.Algebra.Group.Action.Sigma
/-- This is not an instance because `i` becomes a metavariable.  -/
Sigma.FaithfulVAdd' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (i : ι) [FaithfulVAdd M (α i)],
  FaithfulVAdd M ((i : ι) × α i)
-- Lean.DocString.Markdown
/-- Looks up the block Markdown renderer registered for `typeName`, if any.  -/
Lean.Doc.blockRendererFor : Lean.Name → Lean.CoreM (Option Lean.Doc.BlockMdRenderer)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.Existence.of_specializingMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (AlgebraicGeometry.topologically @SpecializingMap).universally f → AlgebraicGeometry.ValuativeCriterion.Existence f
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_symm_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm.symm = α
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.coprodMap.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N),
  DFinsupp.coprodMap f = ((DFinsupp.lsum ℕ) fun x => LinearMap.id) ∘ₗ DFinsupp.mapRange.linearMap f
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonProgressParams.toJson : {α : Type} → [Lean.ToJson α] → Lean.Lsp.ProgressParams α → Lean.Json
-- Mathlib.Data.List.Basic
List.getLastI_eq_getLast? : ∀ {α : Type u} [inst : Inhabited α] (l : List α), l.getLastI = l.getLast?.getD default
-- Init.Data.UInt.Bitwise
UInt16.toNat_shiftLeft : ∀ (a b : UInt16), (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16
-- Lean.Expr
/-- `.bvar idx` is now the preferred form.  -/
Lean.mkBVar : ℕ → Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.smul_mem_pointwise_smul_iff : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S : Submonoid M} {x : M}, a • x ∈ a • S ↔ x ∈ S
-- Init.Control.Basic
/-- Runs a monadic action and returns the negation of its result.
 -/
notM : {m : Type → Type v} → [Functor m] → m Bool → m Bool
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (s.sup' hne f) t x
-- Init.Data.List.Lemmas
List.getElem?_set_ne : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≠ j → ∀ {a : α}, (l.set i a)[j]? = l[j]?
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.head_val : ∀ {m a : ℕ} {L : List ℕ} (hl : SimplexCategoryGenRel.IsAdmissible m (a :: L)), ↑hl.head = a
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : Lex β) (a : α), ofLex b • a = b • a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLED.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  Std.DTreeMap.Internal.Impl.getKeyLED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLE? k t).getD fallback
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_ofScientific : ∀ {K : Type u_1} [inst : RCLike K] (m : ℕ) (s : Bool) (e : ℕ),
  ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.Analysis.Normed.Module.Basic
Metric.diam_closedBall_eq : ∀ {E : Type u_6} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ},
  0 ≤ r → Metric.diam (Metric.closedBall x r) = 2 * r
-- Init.Data.SInt.Lemmas
Int8.lt_trans : ∀ {a b c : Int8}, a < b → b < c → a < c
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
cantorToHilbert_surjective : Function.Surjective cantorToHilbert
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_apply_inr_snd : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι'), ((b.prod b') (Sum.inr i)).2 = b' i
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_appLE : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens) (W' : (↑U).Opens)
  (e' : W' ≤ (TopologicalSpace.Opens.map (X.homOfLE e).base).obj W),
  AlgebraicGeometry.Scheme.Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_comm : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M}, a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} [inst_1 : SizeOf C] (base : X.base ⟶ Y.base)
  (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber),
  sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.degree 0 = ⊥
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
DifferentiableWithinAt.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E} {x : E},
  DifferentiableWithinAt 𝕜' f s x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.e2Summand_even : ∀ (z : UpperHalfPlane), Function.Even fun x => EisensteinSeries.e2Summand x z
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_eq_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens},
  AlgebraicGeometry.Scheme.Hom.appLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯ =
    AlgebraicGeometry.Scheme.Hom.app f U
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_mul_top : ∀ (a : ENNReal), (a * ⊤).toNNReal = 0
-- Mathlib.Analysis.Convex.Segment
segment_eq_image : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), segment 𝕜 x y = (fun θ => (1 - θ) • x + θ • y) '' Set.Icc 0 1
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α],
  MeasureTheory.Measure.count = MeasureTheory.Measure.sum MeasureTheory.Measure.dirac
-- Mathlib.Algebra.Order.Kleene
ofNat_eq_one : ∀ {α : Type u_1} [inst : IdemSemiring α] {n : ℕ} [inst_1 : n.AtLeastTwo], OfNat.ofNat n = 1
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiableWithinAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {z : E},
  z ∈ Set.range ↑I → MDiffAt[Set.range ↑I] ↑I.symm z
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The type of morphisms of a disjoint union of categories: for `X : C i` and `Y : C j`, a morphism
`(i, X) ⟶ (j, Y)` when `i = j` is just a morphism `X ⟶ Y`, and if `i ≠ j` then there are no such
morphisms.
 -/
CategoryTheory.Sigma.SigmaHom : {I : Type w₁} →
  {C : I → Type u₁} →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → (i : I) × C i → (i : I) × C i → Type (max w₁ v₁ u₁)
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.map : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  {P : Type u_4} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] P) {N : Submodule R M}, N.FG → (Submodule.map f N).FG
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_eq_restrict : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops = M.restrict {e | M.IsNonloop e}
-- Batteries.Control.AlternativeMonad
/-- Type-class for monad lifts that preserve the `Alternative` operations.  -/
LawfulAlternativeLift : (m : semiOutParam (Type u → Type v)) →
  (n : Type u → Type w) → [Alternative m] → [Alternative n] → [MonadLift m n] → Prop
-- Mathlib.Data.Set.Image
Set.preimage_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective (Set.preimage f) ↔ Function.Injective f
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.div_right : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y x' y' : G₀},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x / x') (y / y')
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instPreorder : {M : Type u_2} →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedAddMonoid M] → Preorder (ArchimedeanOrder M)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey! = t.maxKey!
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂.fun_cases_unfolding : ∀ (w x : UInt8) (motive : Option Char → Prop),
  (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true → motive none) →
    (¬ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true →
        have r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x;
        r < 128 → motive none) →
      (¬ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true →
          let r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x;
          ¬r < 128 → motive (some { val := r, valid := ⋯ })) →
        motive (ByteArray.utf8DecodeChar?.assemble₂ w x)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_bot : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] (f : α → E) (g : α → F), f =O[⊥] g
-- Mathlib.FieldTheory.LinearDisjoint
/-- The same-universe version of
`IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`.  -/
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L →
      Module.rank ↥A ↥(IntermediateField.extendScalars ⋯) = Module.rank F L
-- Mathlib.Data.ZMod.Basic
ZMod.cast_natCast' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (k : ℕ), (↑k).cast = ↑k
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf_succ : ∀ (n : ℕ), (n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - Nat.fib (n + 1).greatestFib).zeckendorf
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessage.default : Lean.JsonRpc.Message
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f : ∀ {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s),
  (X.openCoverOfIsOpenCover U hU).f i = (U i).ι
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isClosed_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s : Set A), IsClosed (ProjectiveSpectrum.zeroLocus 𝒜 s)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subset_closure_of_subset' : ∀ {α : Type u_2} {X Y : Set α} (M : Matroid α),
  X ⊆ Y → autoParam (X ⊆ M.E) Matroid.subset_closure_of_subset'._auto_1 → X ⊆ M.closure Y
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The measurable equivalence `(∀ i, π i) ≃ᵐ π ⋆` when the domain of `π` only contains `⋆`  -/
MeasurableEquiv.piUnique : {δ' : Type u_5} →
  (π : δ' → Type u_6) → [inst : (x : δ') → MeasurableSpace (π x)] → [inst_1 : Unique δ'] → ((i : δ') → π i) ≃ᵐ π default
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.functor_obj : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (k : ℕ)
  (A : CommAlgCat R), (Module.Grassmannian.functor k).obj A = Module.Grassmannian (↑A) (TensorProduct R (↑A) M) k
-- Mathlib.Topology.EMetricSpace.BoundedVariation
MonotoneOn.eVariationOn_le : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α} {a b : α},
  MonotoneOn f s → a ∈ s → b ∈ s → eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- Uniformizers exist in a DVR.  -/
IsDiscreteValuationRing.exists_irreducible : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], ∃ ϖ, Irreducible ϖ
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddAssocClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : VAdd α β] [inst_2 : VAdd α γ]
  [inst_3 : VAdd β γ] [VAddAssocClass α β γ], VAddAssocClass α β (Finset γ)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.one_ne_of : ∀ {α : Type u} (x : α), 1 ≠ FreeCommRing.of x