mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.Body.Basic
Std.Http.Body.mk : {α : Type} →
  (α → Std.Async.Async (Option Std.Http.Chunk)) →
    (α → Std.Async.Async Unit) →
      (α → Std.Async.Async Bool) →
        (α → Std.Async.Selector (Option Std.Http.Chunk)) →
          (α → Std.Async.Async (Option (Option Std.Http.Chunk))) →
            (α → Std.Async.Async (Option Std.Http.Body.Length)) →
              (α → Option Std.Http.Body.Length → Std.Async.Async Unit) → Std.Http.Body α
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with multiplication.  `UniqueProds G` asserts that any two non-empty
finite subsets of `G` have the `UniqueMul` property, with respect to some element of their
product `A * B`.  -/
UniqueProds : (G : Type u_1) → [Mul G] → Prop
-- Mathlib.Algebra.Category.MonCat.Basic
mulEquivIsoCommMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y],
  mulEquivIsoCommMonCatIso =
    { hom := TypeCat.ofHom fun e => e.toCommMonCatIso, inv := TypeCat.ofHom fun i => i.commMonCatIsoToMulEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Data.Set.Sigma
Set.singleton_sigma_singleton : ∀ {ι : Type u_1} {α : ι → Type u_3} {i : ι} {a : (i : ι) → α i}, ({i}.sigma fun i => {a i}) = {⟨i, a i⟩}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.rightUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (P : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)],
  (CategoryTheory.Limits.prod.rightUnitor P).inv =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.terminal.from P)
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.isZero_homology_of_hasDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C] (n d : ℕ)
  [X.HasDimensionLT d],
  autoParam (d ≤ n) SSet.isZero_homology_of_hasDimensionLT._auto_1 → CategoryTheory.Limits.IsZero (X.homology R n)
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the left-most term is zero in terms of modules.
For a diagram explaining the variables, see the module docstring.  -/
LinearMap.surjective_of_surjective_of_injective_of_left_exact : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_7} {N₂ : Type u_8}
  {N₃ : Type u_9} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁]
  [inst_8 : AddCommGroup N₂] [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂]
  [inst_12 : Module R N₃] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₂ → Function.Injective ⇑i₃ → Function.Injective ⇑g₁ → Function.Surjective ⇑i₁
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- Invertibility in the exterior algebra is the same as invertibility of the base ring.  -/
ExteriorAlgebra.invertibleAlgebraMapEquiv : {R : Type u1} →
  [inst : CommRing R] →
    (M : Type u2) →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (r : R) → Invertible ((algebraMap R (ExteriorAlgebra R M)) r) ≃ Invertible r
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_one_right_eq_X_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ),
  (SkewPolynomial.monomial n) 1 = SkewPolynomial.X ^ n
-- Mathlib.Algebra.Group.Basic
neg_unique : ∀ {M : Type u_4} [inst : AddCommMonoid M] {x y z : M}, x + y = 0 → x + z = 0 → y = z
-- Mathlib.Algebra.Group.Semiconj.Basic
AddSemiconjBy.neg_right_iff : ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.symm_bijective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ : C(X, Y)}, Function.Bijective ContinuousMap.HomotopyWith.symm
-- Mathlib.Algebra.Algebra.Operations
Submodule.instMulRightMono : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], MulRightMono (Submodule R A)
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.mk : Lean.Lsp.MessageType → String → Option (Array Lean.Lsp.MessageActionItem) → Lean.Lsp.ShowMessageRequestParams
-- Mathlib.Topology.Category.CompactlyGenerated
/-- `compactlyGeneratedToTop` is fully faithful.  -/
CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.FullyFaithful
-- Mathlib.RingTheory.Perfection
ModP.preVal_mul : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} {x y : ModP O p}, x * y ≠ 0 → ModP.preVal K v O p (x * y) = ModP.preVal K v O p x * ModP.preVal K v O p y
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_sup : ∀ {M : Type u_2} [inst : Add M] (S₁ S₂ : AddSubsemigroup Mᵃᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfcₙ_mem : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A]
  [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] {𝕜' : Type u_3} {S : Type u_4} [inst_12 : Monoid 𝕜']
  [inst_13 : MulAction 𝕜' A] [inst_14 : SetLike S A] [NonUnitalSubringClass S A] [inst_16 : SMul 𝕜 𝕜']
  [IsScalarTower 𝕜 𝕜' A] [SMulMemClass S 𝕜' A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : 𝕜 → 𝕜) {a : A},
  a ∈ s → cfcₙ f a ∈ s
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_mul_op : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable MulOpposite.op
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.smul_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Polynomial R)
  (g : PolynomialModule R M) (n : ℕ),
  (f • g).coeff n = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, f.coeff x.1 • g.coeff x.2
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_extend_bot_mem_frontier : ∀ {x y : ℝ} [hxy : Fact (x < y)],
  ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊥ ∈
    frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))
-- Mathlib.Algebra.Free
FreeAddSemigroup.ext_iff : ∀ {α : Type u} {x y : FreeAddSemigroup α}, x = y ↔ x.head = y.head ∧ x.tail = y.tail
-- Lean.Parser.Command
/-- `assert_not_imported Mod1 Mod2` asserts that the modules `Mod1` and `Mod2` are not
transitively imported by the current file. Used for dependency management.
 -/
Lean.Parser.Command.assertNotImported : Lean.Parser.Parser
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π / 2`, the first two points are not equal.  -/
EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₁ ≠ p₂
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The cofiltered limit of nonempty finite types is nonempty.

See `nonempty_sections_of_finite_inverse_system` for a specialization to inverse limits.  -/
nonempty_sections_of_finite_cofiltered_system : ∀ {J : Type u} [inst : CategoryTheory.Category.{w, u} J] [CategoryTheory.IsCofilteredOrEmpty J]
  (F : CategoryTheory.Functor J (Type v)) [∀ (j : J), Finite (F.obj j)] [∀ (j : J), Nonempty (F.obj j)],
  F.sections.Nonempty
-- Mathlib.RingTheory.Perfection
Perfection.instPerfectRing : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ}, PerfectRing (Perfection M p) p
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_iSizeToBitVec : ∀ (x : ISize), Int16.ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Topology.Basic.0.TopModuleCat.Hom.ofHom'.inj : ∀ {R : Type u} {inst : Ring R} {inst_1 : TopologicalSpace R} {X Y : TopModuleCat R}
  {hom' hom'_1 : ↑X.toModuleCat →L[R] ↑Y.toModuleCat}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-closed right-open.

The type of the resulting slices is `γ`.
 -/
Std.Rco.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.IsBridge.sup_edge_of_not_reachable`. -/
SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → (G ⊔ SimpleGraph.edge u v).IsBridge s(u, v)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i j : ι},
  b.IsPos i → j ∈ b.support → i ≠ j → b.IsPos ((P.reflectionPerm j) i)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_rco_iff : ∀ {m n i : ℕ}, 0 < (m...n).toArray[i]! ↔ i < n - m ∧ 0 < i + m
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.prepathObject_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  K.prepathObject.ι = HomologicalComplex.pathObject.ι K
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_sSup : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)), (sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α}
  [inst_1 : Inhabited (β a)], ∅.get! a = default
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_or : ∀ (a b : UInt16), (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
-- Lean.Elab.Do.Basic
/-- Whether a code block is alive or dead.  -/
Lean.Elab.Do.CodeLiveness : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospan_map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (a : J.R),
  I.multicospan.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd a) = I.snd a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.mk : Lean.Lsp.WorkDoneProgressParams → Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.Range → Lean.Lsp.InlayHintParams
-- Mathlib.Computability.NFA
NFA.eval.eq_1 : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.eval = M.evalFrom M.start
-- Std.Internal.UV.TCP
/-- Cancels a receive operation in the form of `recv?` or `waitReadable` if there is currently one
pending. This resolves their returned `IO.Promise` to `none`. This function is considered dangerous,
as improper use can cause data loss, and is therefore not exposed to the top-level API.

Note that this function is idempotent and as such can be called multiple times on the same socket
without causing errors, in particular also without a receive running in the first place.
 -/
Std.Internal.UV.TCP.Socket.cancelRecv : Std.Internal.UV.TCP.Socket → IO Unit
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
AlgebraicGeometry.continuousMapPresheaf_obj : ∀ (T : Type v) [inst : TopologicalSpace T] (U : AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.continuousMapPresheaf T).obj U = C(↥(Opposite.unop U), T)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup.eq_1 : ∀ (u : ℕ → ENNReal), ExpGrowth.expGrowthSup u = Filter.limsup (fun n => (u n).log / ↑n) Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.inv_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y) [inst_3 : CategoryTheory.IsIso f],
  (CategoryTheory.inv f).snd = CategoryTheory.inv f.snd
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_surjective : ∀ {R : Type u_1} (M : Type u_2) {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid P]
  [inst_3 : Module R M] [inst_4 : Module R P] (f : M →ₗ[R] P),
  Function.Surjective ⇑f → ∀ [IsArtinian R M], IsArtinian R P
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.smul_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X),
  m • x =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x) CategoryTheory.ModObj.smul
-- Mathlib.Algebra.Group.TypeTags.Hom
Additive.addMonoidHom_ext_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] {f g : Additive α →+ β},
  f = g ↔ AddMonoidHom.toMultiplicativeRight f = AddMonoidHom.toMultiplicativeRight g
-- Mathlib.Analysis.Convex.Combination
/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive.  -/
Finset.centerMass_id_mem_convexHull_of_nonpos : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (t : Finset E) {w : E → R},
  (∀ i ∈ t, w i ≤ 0) → ∑ i ∈ t, w i < 0 → t.centerMass w id ∈ (convexHull R) ↑t
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₁_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupHomology.cycles₁ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.toCycles A 2 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.f' h)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtensionUnique_inv : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : F ⟶ L.comp F'')
  [inst_4 : F''.IsLeftKanExtension α'], (F'.leftKanExtensionUnique α F'' α').inv = F''.descOfIsLeftKanExtension α' F' α
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.fstL_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (x : WithLp p (α × β)), (WithLp.fstL p 𝕜 α β) x = x.fst
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : GL n R),
  ↑A⁻¹ = (↑A)⁻¹
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_div_pure : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (a b : α),
  NonemptyInterval.pure a / NonemptyInterval.pure b = NonemptyInterval.pure (a / b)
-- Init.Core
/-- Notation type class for the subset relation `⊆`.  -/
HasSubset : Type u → Type u
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.isScalarTower' : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_5} [inst_1 : CommSemiring S] [inst_2 : Algebra S R] (M : Type u)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower S R M],
  IsScalarTower S (Polynomial R) (PolynomialModule R M)
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_injective : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], Function.Injective Associates.out
-- Mathlib.Data.ENNReal.Inv
ENNReal.top_zpow_def : ∀ (n : ℤ), ⊤ ^ n = if n = 0 then 1 else if 0 < n then ⊤ else 0
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.pi` as an `Equiv`.  -/
ContinuousMultilinearMap.piEquiv : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
          [inst_2 : (i : ι) → Module R (M₁ i)] →
            [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] →
              {ι' : Type u_1} →
                {M' : ι' → Type u_2} →
                  [inst_4 : (i : ι') → AddCommMonoid (M' i)] →
                    [inst_5 : (i : ι') → TopologicalSpace (M' i)] →
                      [inst_6 : (i : ι') → Module R (M' i)] →
                        ((i : ι') → ContinuousMultilinearMap R M₁ (M' i)) ≃
                          ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_vadd_const_iff`. -/
Sbtw.vadd_const : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : V} (p : P), Sbtw R x y z → Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] [JacobsonSpace ↥Y],
  JacobsonSpace ↥X
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.instLawfulMonadULiftT : ∀ {n : Type (max u v) → Type v'} [inst : Monad n] [LawfulMonad n], LawfulMonad (Std.Iterators.ULiftT n)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.objOpOp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (X_1 : Cᵒᵖ),
  (CategoryTheory.Coyoneda.objOpOp X).hom.app X_1 = (CategoryTheory.opEquiv (Opposite.op X) X_1).toIso.hom
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.prod_rightl : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α},
  f =O[l] g' → f =O[l] fun x => (g' x, k' x)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Comon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.summable_norm_pow_inv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L] (n : ℕ), Module.finrank ℤ ↥L < n → Summable fun z => ‖z‖⁻¹ ^ n
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_left' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Iic ↑n)) (nhds ↑n)
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_top_left : ∀ {E : Type v} [inst : Field E] (A : Subfield E), ⊤.relrank A = 1
-- Aesop.Forward.State
Aesop.ClusterState.AddM.Context.mk.inj : ∀ {premiseMVars : Array Lean.MVarId} {premiseLMVars : Array Lean.LMVarId} {premiseMVars_1 : Array Lean.MVarId}
  {premiseLMVars_1 : Array Lean.LMVarId},
  { premiseMVars := premiseMVars, premiseLMVars := premiseLMVars } =
      { premiseMVars := premiseMVars_1, premiseLMVars := premiseLMVars_1 } →
    premiseMVars = premiseMVars_1 ∧ premiseLMVars = premiseLMVars_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.beq'_eq : ∀ (pw₁ pw₂ : Lean.Grind.CommRing.Power), (pw₁.beq' pw₂ = true) = (pw₁ = pw₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_top_le_unionProd : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), S.prod ⊤ ≤ S.unionProd T
-- Mathlib.Order.WellFounded
instWellFoundedLTULift : ∀ {α : Type u_1} [inst : LT α] [h : WellFoundedLT α], WellFoundedLT (ULift.{u_4, u_1} α)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toZeroHom : {α : Type u_7} → {β : Type u_8} → [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → (α →*₀ β) → ZeroHom α β
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_finsetSum_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {ι : Type u_6}
  {m : MeasurableSpace α} {f : α → G} {μ : ι → MeasureTheory.Measure α} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (a : α), f a ∂μ i
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.IsPartition.compl_eq_bot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] {π : BoxIntegral.Prepartition I}, π.IsPartition → π.compl = ⊥
-- Lean.Syntax
/-- Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
Indices are allowed to be out-of-bound, in which case `cur` is `Syntax.missing`.
If the `Traverser` is used linearly, updates are linear in the `Syntax` object as well.
 -/
Lean.Syntax.Traverser : Type
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {inv : Bool}
  {aig : Std.Sat.AIG α} (curr : ℕ) (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Data.Set.Functor
Set.instLawfulAlternative : LawfulAlternative Set