mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan.eq_1 : ∀ {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 D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J),
  CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j =
    CategoryTheory.GradedObject.CofanMapObjFun.mk
      (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) p j
      (X j) fun a ha =>
      if ha_1 : a.2 = 0 then
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha_1).hom
          (CategoryTheory.eqToHom ⋯)
      else (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitial F Y X a ha_1).to (X j)
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_shiftLeft : ∀ (a b : UInt16), (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 16)
-- Init.Data.List.Find
List.IsPrefix.lookup_eq_none : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)},
  l₁ <+: l₂ → List.lookup k l₂ = none → List.lookup k l₁ = none
-- Batteries.Data.String.Lemmas
String.endPos_mk : ∀ (cs : List Char), (String.ofList cs).rawEndPos = { byteIdx := String.utf8Len cs }
-- Mathlib.Data.Fintype.Powerset
Set.fintype : {α : Type u_1} → [Fintype α] → Fintype (Set α)
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.univ_shatters : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} [inst_1 : Fintype α], Finset.univ.Shatters s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).isEmpty = false ↔
      ∃ k, ∃ (h : m.contains k = true), (f k (m.get k h)).isSome = true)
-- Mathlib.Combinatorics.SimpleGraph.Hall
SimpleGraph.exists_bijective_of_forall_ncard_le : ∀ {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V},
  G.IsBipartiteWith p₁ p₂ →
    (∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) →
      ∃ h, Function.Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (Φ : CategoryTheory.Functor C D) [inst_4 : Φ.Additive],
  CochainComplex.HomComplex.Cochain.map 0 Φ = 0
-- Mathlib.Data.Num.ZNum
ZNum.cast_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α], ↑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.inl_codiagonal_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.codiagonal f) h) =
    h
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
/-- The inverse functor `Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C)` of
the Dold-Kan equivalence for additive categories.  -/
CategoryTheory.Preadditive.DoldKan.Γ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
          (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceRpcCallParams : Lean.Lsp.FileSource Lean.Lsp.RpcCallParams
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarRing A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SizeOf R] [inst_7 : SizeOf A]
  (toSubalgebra : Subalgebra R A) (star_mem' : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier),
  sizeOf { toSubalgebra := toSubalgebra, star_mem' := star_mem' } = 1 + sizeOf toSubalgebra
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.map_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y),
  (CategoryTheory.Limits.BinaryCofan.map F s).inr = F.map s.inr
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The monoid algebra over a semiring `R` generated by the monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product.  -/
MonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.of_carrier : ∀ (R : CommRingCat), CommRingCat.of ↑R = R
-- Init.Data.Float.Float32
/-- Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller
than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`ceilf`.

Examples:
 * `Float32.ceil 1.5 = 2`
 * `Float32.ceil (-1.5) = (-1)`
 -/
Float32.ceil : Float32 → Float32
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_zero : ∀ (α : Type u_1) {m : MeasurableSpace α} (ε' : Type u_8) [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε']
  (μ : MeasureTheory.Measure α), MeasureTheory.Integrable 0 μ
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.le_sSup_iff : ∀ {s : Set ℝ} {a : ℝ}, BddAbove s → s.Nonempty → (a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x)
-- Init.Data.Vector.Lemmas
Vector.getElem_push_last : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x)[n] = x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  k ∈ Std.ExtDTreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f k (t.get k h)).isSome = true
-- Lean.ErrorExplanation
Lean.ErrorExplanation.mk : String → Lean.ErrorExplanation.Metadata → Option Lean.DeclarationLocation → Lean.ErrorExplanation
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {n : ℕ} (m k : ℕ)
  (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n) {T : Type u_4} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (f : Polynomial.UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) (g : S →ₐ[R] T),
  (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv T m k hn p) (g.comp f))).1 =
    (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv S m k hn p) f)).1.map ↑g
-- Mathlib.Order.Filter.Bases.Basic
Filter.Tendsto.basis_left : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β}
  {f : α → β}, Filter.Tendsto f la lb → la.HasBasis pa sa → ∀ t ∈ lb, ∃ i, pa i ∧ Set.MapsTo f (sa i) t
-- Mathlib.Analysis.Normed.Group.Completion
UniformSpace.Completion.enorm_coe : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (x : E), ‖↑x‖ₑ = ‖x‖ₑ
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.traceClsClean : Lean.Name
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
Nat.toNat_emultiplicity : ∀ (p n : ℕ), (emultiplicity p n).toNat = padicValNat p n
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_map_comp_assoc : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15}
  {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : AddCommMonoid N₂]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂)
  (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) (f : M →ₗ[R] TensorProduct R M M₃),
  ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂ ∘ₗ f₁₂) f₃ ∘ₗ f =
    TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id ∘ₗ f
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.is_max_iff_card_eq : ∀ {α : Type u_1} [inst : BooleanAlgebra α] [Nontrivial α] [inst_2 : Fintype α] {s : Finset α},
  (↑s).Intersecting → ((∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- A functor that preserves and reflects terminal objects induces an equivalence on
`IsTerminal`.  -/
CategoryTheory.Limits.IsTerminal.isTerminalIffObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] →
            [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] →
              (X : C) → CategoryTheory.Limits.IsTerminal X ≃ CategoryTheory.Limits.IsTerminal (G.obj X)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.instIsOverToPartialMapOfIsSeparatedOfIsOver : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsReduced X] [inst_1 : Y.IsSeparated] [S.IsSeparated]
  [inst_3 : X.Over S] [inst_4 : Y.Over S] (f : X.RationalMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f],
  AlgebraicGeometry.Scheme.PartialMap.IsOver S f.toPartialMap
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.subset_pathComponentIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F s : Set X},
  IsPathConnected s → x ∈ s → s ⊆ F → s ⊆ pathComponentIn F x
-- Init.Data.List.MinMax
List.min?_nil : ∀ {α : Type u_1} [inst : Min α], [].min? = none
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.pairwise_disjoint : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V}, Pairwise fun C D => Disjoint ↑C ↑D
-- Mathlib.Analysis.Seminorm
Seminorm.toAddGroupSeminorm : {𝕜 : Type u_12} →
  {E : Type u_13} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Seminorm 𝕜 E → AddGroupSeminorm E
-- Mathlib.Analysis.Calculus.VectorField
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[f • V, W] = - (df W) • V + f • [V, W]`
 -/
VectorField.lieBracket_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E} {f : E → 𝕜},
  DifferentiableAt 𝕜 f x →
    DifferentiableAt 𝕜 V x →
      VectorField.lieBracket 𝕜 (fun y => f y • V y) W x =
        -(fderiv 𝕜 f x) (W x) • V x + f x • VectorField.lieBracket 𝕜 V W x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isPreconnected_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : TopologicalSpace.Compacts α},
  K ≠ ⊥ → IsPreconnected ↑L → IsPreconnected (Set.Icc K L)
-- Mathlib.RingTheory.RingHom.OpenImmersion
/-- The identity map of a ring is a standard open immersion.  -/
RingHom.IsStandardOpenImmersion.id : ∀ (R : Type u_1) [inst : CommRing R], (RingHom.id R).IsStandardOpenImmersion
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) (u : ↥C), C.toSimpleGraph_hom u = ↑u
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousLinearMap.integrableOn_comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α} {E : Type u_7} {H : Type u_8}
  {𝕜 : Type u_9} {𝕜' : Type u_10} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜' E] [inst_4 : NormedAddCommGroup H] [inst_5 : NormedSpace 𝕜 H]
  {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {f : α → H} (L : H →SL[σ] E),
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn (⇑L ∘ f) s μ
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.comp_homOfVector : ∀ {n : Type u} {S X Y : AlgebraicGeometry.Scheme} (v : n → ↑(Y.presheaf.obj (Opposite.op ⊤))) (f : X ⟶ Y) (g : Y ⟶ S),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.AffineSpace.homOfVector g v) =
    AlgebraicGeometry.AffineSpace.homOfVector (CategoryTheory.CategoryStruct.comp f g)
      (⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) ∘ v)
-- Mathlib.Analysis.Complex.Basic
Complex.slitPlane_ne_zero : ∀ {z : ℂ}, z ∈ Complex.slitPlane → z ≠ 0
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.mk.inj : ∀ {html : ProofWidgets.Html} {idx : ℕ} {html_1 : ProofWidgets.Html} {idx_1 : ℕ},
  { html := html, idx := idx } = { html := html_1, idx := idx_1 } → html = html_1 ∧ idx = idx_1
-- Mathlib.Data.Int.Basic
Int.pow_right_injective : ∀ {a : ℤ}, 1 < a.natAbs → Function.Injective fun x => a ^ x
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.leftUnitor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.composePath_mem_of_id_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y},
  W.paths p → W (CategoryTheory.CategoryStruct.id X) → W (CategoryTheory.composePath p)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- Elements in `M ⊗ N` can be represented by sum of elements of basis of `M` tensor elements of
`N`.  -/
TensorProduct.eq_repr_basis_left : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ℬ : Module.Basis ι R M)
  (x : TensorProduct R M N), ∃ c, (c.sum fun i n => ℬ i ⊗ₜ[R] n) = x
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_iff_getElem_ge_getElem_of_le`. -/
List.sortedGE_of_getElem_ge_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]) → l.SortedGE
-- Std.Sync.Channel
Std.CloseableChannel.instAsyncStreamOptionOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncStream (Std.CloseableChannel α) (Option α)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instIsNegApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsNegApply (CuspForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Topology.MetricSpace.Polish
/-- A metric space structure on a subset `s` of a metric space, designed to make it complete
if `s` is open. It is given by `dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|`, where the
second term blows up close to the boundary to ensure that Cauchy sequences for `dist'` remain well
inside `s`.

This definition ensures the `TopologicalSpace` structure on
`TopologicalSpace.Opens.CompleteCopy s` is definitionally equal to the original one.
 -/
TopologicalSpace.Opens.CompleteCopy.instMetricSpace : {α : Type u_1} → [inst : MetricSpace α] → {s : TopologicalSpace.Opens α} → MetricSpace s.CompleteCopy
-- Std.Sat.AIG.Basic
/-- Flip the current inverter settings of the `BinaryInput` if `linv` or `rinv` is set respectively.
 -/
Std.Sat.AIG.BinaryInput.invert : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.BinaryInput → Bool → Bool → aig.BinaryInput
-- Mathlib.Order.BoundedOrder.Basic
OrderTop.toTop : {α : Type u} → {inst : LE α} → [self : OrderTop α] → Top α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.contains a = false → Std.DTreeMap.Raw.Const.getD t a fallback = fallback
-- Mathlib.Order.Antisymmetrization
instInhabitedAntisymmetrization : {α : Type u_1} → (r : α → α → Prop) → [inst : IsPreorder α r] → [Inhabited α] → Inhabited (Antisymmetrization α r)
-- Mathlib.Algebra.Order.Group.End
RelHom.mul_apply : ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r →r r) (x : α), (e₁ * e₂) x = e₁ (e₂ x)
-- Mathlib.Data.Fintype.Order
Bool.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Bool
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.isNatEquiv_piEquivLim : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (nat : InverseSystem.IsNatEquiv f equiv) {equivLim : F i ≃ ↑(InverseSystem.limit f i)} (hi : Order.IsSuccPrelimit i)
  [InverseSystem f],
  (∀ (x : F i) (l : ↑(Set.Iio i)), ↑(equivLim x) l = f ⋯ x) →
    InverseSystem.IsNatEquiv f (InverseSystem.piEquivLim nat equivLim hi)
-- Mathlib.RingTheory.IntegralDomain
Polynomial.div_eq_quo_add_rem_div : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (K : Type u_3) [inst_2 : Field K] [inst_3 : Algebra (Polynomial R) K]
  [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g : Polynomial R},
  g.Monic →
    ∃ q r,
      r.degree < g.degree ∧
        (algebraMap (Polynomial R) K) f / (algebraMap (Polynomial R) K) g =
          (algebraMap (Polynomial R) K) q + (algebraMap (Polynomial R) K) r / (algebraMap (Polynomial R) K) g
-- Mathlib.GroupTheory.Exponent
/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element
of order `lcm n m`. The result actually gives an explicit (computable) element, written as the
product of a power of `x` and a power of `y`. See also the result below if you don't need the
explicit formula.  -/
Commute.orderOf_mul_pow_eq_lcm : ∀ {G : Type u} [inst : Monoid G] {x y : G},
  Commute x y →
    orderOf x ≠ 0 →
      orderOf y ≠ 0 →
        orderOf
            (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
              y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
          (orderOf x).lcm (orderOf y)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_not_le : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ¬m ≤ m₀ → ProbabilityTheory.condVar m X μ = 0
-- Init.Data.Rat.Lemmas
Rat.divInt_nonneg_iff_of_pos_right : ∀ {a b : ℤ}, 0 < b → (0 ≤ Rat.divInt a b ↔ 0 ≤ a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_insert_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β k},
  (t.insert k v).toArray.Perm ((Array.filter (fun x => decide ¬(k == x.fst) = true) t.toArray).push ⟨k, v⟩)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_nhdsWithin_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {s t : Set α}, s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.ball x ε ∩ t ⊆ s
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.toFin.eq_1 : ∀ {lo hi : ℤ} (n : Std.Time.Internal.Bounded.LE lo hi) (h₀ : 0 ≤ lo), n.toFin h₀ = ⟨(↑n).toNat, ⋯⟩
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_inv_atTop_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {x y : G},
  (MapClusterPt x⁻¹ Filter.atTop fun x => y ^ x) ↔ MapClusterPt x Filter.atTop fun x => y ^ x
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instReprRange : Repr Lean.Lsp.Range
-- Std.Data.ExtDHashMap.Lemmas
/-- Variant of `get!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtDHashMap.Const.get!_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.map f m) k =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.ExtDHashMap.Const.get? m k) ⋯).get!
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length.eq_1 : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) (s : Set R),
  f.length s = if IsEmpty R then 0 else ⨅ a, ⨅ b, ⨅ (_ : s \ botSet ⊆ Set.Ioc a b), ENNReal.ofReal (↑f b - ↑f a)
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  IsLocalMaxOn f s a → f =ᶠ[nhdsWithin a s] g → a ∈ s → IsLocalMaxOn g s a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhdsWithin_basis_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {s : Set α},
  (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.ball x ε ∩ s
-- Lean.DocString.Markdown
/-- Produces a fenced code block as a line array (with no surrounding blank lines), with a sufficiently
long fence.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.codeBlockLines : String → Array String
-- Mathlib.Algebra.Category.Ring.Constructions
/-- `ULift.{u} ℤ` is initial in `CommRingCat`.  -/
CommRingCat.isInitial : CategoryTheory.Limits.IsInitial (CommRingCat.of (ULift.{u, 0} ℤ))
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.toTemperedDistributionCLM_apply_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : SecondCountableTopology E]
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toTemperedDistributionCLM_apply_apply._auto_1)
  [hμ : μ.HasTemperateGrowth] (f : SchwartzMap E F) (g : SchwartzMap E ℂ),
  ((SchwartzMap.toTemperedDistributionCLM E F μ) f) g = ∫ (x : E), g x • f x ∂μ
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_succ : ∀ {a n : ℕ}, 1 < a → a ^ n < a ^ (n + 1)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Two regular measures are equal iff they induce the same positive linear functional
on `C_c(X, ℝ)`.  -/
RealRMK.integralPositiveLinearMap_inj : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [inst_5 : μ.Regular] [inst_6 : ν.Regular],
  CompactlySupportedContinuousMap.integralPositiveLinearMap μ =
      CompactlySupportedContinuousMap.integralPositiveLinearMap ν ↔
    μ = ν
-- Init.Data.Vector.Lemmas
Vector.toArray_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, (Vector.ofFn f).toArray = Array.ofFn f
-- Mathlib.Order.Quotient
Quotient.mk_le_mk : ∀ {α : Type u_1} {s : Setoid α} [inst : LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected]
  {x y : α}, ⟦x⟧ ≤ ⟦y⟧ ↔ x ≤ y ∨ x ≈ y
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_find : ∀ {a b : ℕ} {self : Batteries.UnionFind} {x : Fin self.size}, (self.find x).fst.Equiv a b ↔ self.Equiv a b
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.Visitor : Type