mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Newton
Polynomial.isFixedPt_newtonMap_of_isUnit_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S},
  IsUnit ((Polynomial.aeval x) (Polynomial.derivative P)) →
    (Function.IsFixedPt P.newtonMap x ↔ (Polynomial.aeval x) P = 0)
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.closure_le_centralizer_centralizer : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M),
  AddSubmonoid.closure s ≤ AddSubmonoid.centralizer ↑(AddSubmonoid.centralizer s)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.disjoint_iff_comap_eq_bot : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M}, Disjoint p q ↔ Submodule.comap p.subtype q = ⊥
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.symm_symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.symm.symm = F
-- Init.System.IO
/-- Requests cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to
react to the cancellation.
 -/
IO.cancel : {α : Type u_1} → Task α → BaseIO Unit
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coeMonoidHom.eq_1 : ∀ {ι : Type u_1} {R : ι → Type u_2} {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)],
  RestrictedProduct.coeMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β) (h : ∀ {a b : α}, e.toFun a ≤ e.toFun b ↔ a ≤ b),
  { toRingEquiv := e.toRingEquiv, map_le_map_iff' := h } = e
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- A set is complete iff its image under a uniform inducing map is complete.  -/
isComplete_image_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {m : α → β} {s : Set α},
  IsUniformInducing m → (IsComplete (m '' s) ↔ IsComplete s)
-- Lean.Parser.Basic
Lean.Parser.withPositionAfterLinebreak : Lean.Parser.Parser → Lean.Parser.Parser
-- Init.Data.Ord.Basic
/-- Constructs an `Ord` instance from two existing instances by combining them lexicographically.

The resulting instance compares elements first by `ord₁` and then, if this returns `Ordering.eq`, by
`ord₂`.

The function `compareLex` can be used to perform this comparison without constructing an
intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
comparisons.
 -/
Ord.lex' : {α : Type u_1} → Ord α → Ord α → Ord α
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_norm_norm`. -/
Asymptotics.IsBigO.norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, f' =O[l] g' → (fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.hasForgetToAddSemigroup.eq_1 : AddMonCat.hasForgetToAddSemigroup =
  {
    forget₂ :=
      { obj := fun M => AddSemigrp.of ↑M, map := fun {X Y} f => AddSemigrp.ofHom ↑(AddMonCat.Hom.hom f),
        map_id := AddMonCat.hasForgetToAddSemigroup._proof_1, map_comp := @AddMonCat.hasForgetToAddSemigroup._proof_2 },
    forget_comp := AddMonCat.hasForgetToAddSemigroup._proof_4 }
-- Mathlib.MeasureTheory.Integral.Gamma
Complex.integral_rpow_mul_exp_neg_rpow : ∀ {p q : ℝ}, 1 ≤ p → -2 < q → ∫ (x : ℂ), ‖x‖ ^ q * Real.exp (-‖x‖ ^ p) = 2 * Real.pi / p * Real.Gamma ((q + 2) / p)
-- Mathlib.Algebra.Lie.Basis.Basic
/-- These elements constitute a base for the root system of the Lie algebra relative to the
associated Cartan subalgebra.  -/
LieAlgebra.Basis.baseSupp : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] →
              {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → [Fintype ι] → ι → Module.Dual R ↥H
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.values_empty : ∀ {α : Type u} {β : Type v}, ∅.values = []
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.invOf_iff : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x : R) [inst_2 : Invertible x],
  IsSelfAdjoint ⅟x ↔ IsSelfAdjoint x
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGT! : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α → α × β
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valuation_isClosedMap : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  IsClosedMap ⇑Valued.v.restrict
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.right_adjoint_additive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive], G.Additive
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- A subspace `K : Submodule 𝕜 E` has an orthogonal projection if every vector `v : E` admits an
orthogonal projection to `K`.  -/
Submodule.HasOrthogonalProjection : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → Submodule 𝕜 E → Prop
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_eq_zero_iff : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Zero R] {A : Matrix m n R}, A.vec = 0 ↔ A = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- A category has all countable limits if every functor `J ⥤ C` with a `CountableCategory J`
instance and `J : Type` has a limit.
 -/
CategoryTheory.Limits.HasCountableLimits : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.Algebra.Group.Int.Units
/-- **Alias** of the forward direction of `Int.isUnit_iff_natAbs_eq`. -/
Int.IsUnit.natAbs_eq : ∀ {u : ℤ}, IsUnit u → u.natAbs = 1
-- Mathlib.Data.Int.Order.Basic
/-- **Alias** of the forward direction of `Int.mul_eq_zero`. -/
Int.eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : ℤ}, a * b = 0 → a = 0 ∨ b = 0
-- Mathlib.Algebra.DirectSum.Module
DirectSum.toModule.eq_1 : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (N : Type u₁) [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] (φ : (i : ι) → M i →ₗ[R] N), DirectSum.toModule R ι N φ = (DFinsupp.lsum ℕ) φ
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.mk.injEq : ∀ {m : Type w → Type w'} {α : Type w} (Property : α → Prop) (operation : m (Subtype Property)) (Property_1 : α → Prop)
  (operation_1 : m (Subtype Property_1)),
  ({ Property := Property, operation := operation } = { Property := Property_1, operation := operation_1 }) =
    (Property = Property_1 ∧ operation ≍ operation_1)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] [inst_6 : LieModule R L M], ⇑0 = 0
-- Mathlib.Analysis.Normed.Ring.Basic
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers.  -/
norm_sub_mul_le : ∀ {α : Type u_2} [inst : SeminormedRing α] {a b c : α}, ‖a‖ ≤ 1 → ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖
-- Mathlib.Algebra.Group.Prod
AddUnits.embedProduct_apply : ∀ (α : Type u_6) [inst : AddMonoid α] (x : AddUnits α), (AddUnits.embedProduct α) x = (↑x, AddOpposite.op ↑(-x))
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.Ici_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → Set.Ici (⨆ i, f i) = ⋂ i, Set.Ici (f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.C_addPolynomial_slope : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
          -(Polynomial.C (Polynomial.X - Polynomial.C x₁) * Polynomial.C (Polynomial.X - Polynomial.C x₂) *
              Polynomial.C (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_filter_le_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool}, m.WF → (Std.DHashMap.Raw.filter f m).size ≤ m.size
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instCommGroupWithZero : {α : Type u_1} → [CommGroupWithZero α] → CommGroupWithZero (Lex α)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Lemmas
List.cons_ne_nil : ∀ {α : Type u_1} (a : α) (l : List α), a :: l ≠ []
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- If `X` and `Y` are isomorphic augmented simplicial objects, then an extra
degeneracy for `X` gives also an extra degeneracy for `Y`  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : CategoryTheory.SimplicialObject.Augmented C} → (X ≅ Y) → X.ExtraDegeneracy → Y.ExtraDegeneracy
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_sup : ∀ {R : Type u} [inst : Semiring R] (I J K : Ideal R), I * (J ⊔ K) = I * J ⊔ I * K
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulRightMap_apply_single : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : IsScalarTower R S S] {M N : Submodule R S} {ι : Type u_5} (n : ι → ↥N)
  (i : ι) (m : ↥M), ((M.mulRightMap n) fun₀ | i => m) = ↑m * ↑(n i)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  [inst_5 : IsLocalizedModule S f] (m m_1 : M),
  m = m_1 → ∀ (s s_1 : ↥S), s = s_1 → IsLocalizedModule.mk' f m s = IsLocalizedModule.mk' f_1 m_1 s_1
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.deleteMin.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.deleteMin le (Batteries.BinomialHeap.Imp.Heap.cons rank val c s) =
    match
      Batteries.BinomialHeap.Imp.Heap.findMin le (Batteries.BinomialHeap.Imp.Heap.cons rank val c) s
        { val := val, node := c, next := s } with
    | { before := before, val := val, node := node, next := next } =>
      some (val, Batteries.BinomialHeap.Imp.Heap.merge le node.toHeap (before next))
-- Mathlib.Data.List.Perm.Subperm
List.subperm_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ ↔ ∃ l, l.Perm l₂ ∧ l₁.Sublist l
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.BifibrantObject.ι.obj X)
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.le_iff_subset`. -/
HasSubset.Subset.le : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ⊆ t
-- Mathlib.Data.FinEnum
FinEnum.down_equiv_symm : ∀ {α : Type u} [inst : FinEnum α] (i : Fin (FinEnum.card α)), (FinEnum.equiv.symm i).down = FinEnum.equiv.symm i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_inv_inl_op_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl.op h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.le_iff_specializes : ∀ {X : AlgebraicGeometry.Scheme} {a b : ↥X}, a ≤ b ↔ b ⤳ a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.comp : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G H : CategoryTheory.Functor J C} {α : F ⟶ G} {β : G ⟶ H},
  CategoryTheory.NatTrans.Equifibered α →
    CategoryTheory.NatTrans.Equifibered β → CategoryTheory.NatTrans.Equifibered (CategoryTheory.CategoryStruct.comp α β)
-- Mathlib.Analysis.Calculus.VectorField
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[V, f • W] = (df V) • W + f • [V, W]`
 -/
VectorField.lieBracket_smul_right : ∀ {𝕜 : 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 𝕜 W x →
      VectorField.lieBracket 𝕜 V (fun y => f y • W y) x =
        (fderiv 𝕜 f x) (V x) • W x + f x • VectorField.lieBracket 𝕜 V W x
-- Qq.Macro
Qq.Impl.UnquoteM : Type → Type
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_one_apply : ∀ {R : Type u_2} [inst : CommRing R] (f : PowerSeries R), (PowerSeries.expand 1 ⋯) f = f
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Given a cardinal `κ`, this is a representative family of all categories `C`
such that `HasCardinalLT C κ`.  -/
CategoryTheory.SmallCategoryCardinalLT.categoryFamily : (κ : Cardinal.{w}) → CategoryTheory.SmallCategoryCardinalLT κ → Type w
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.quot_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat),
  Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) CommRingCat.Colimits.Prequotient.zero = 0
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_symm_zero : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [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] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)), (LieAlgebra.ofProd c).symm 0 = 0
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_primitiveCharacter : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n),
  (DirichletCharacter.changeLevel ⋯) χ.primitiveCharacter = χ
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.forIn_eq_forIn_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : Std.DHashMap.Raw α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init l = forIn (Std.DHashMap.Internal.toListModel l.buckets) init fun a d => f a.fst a.snd d
-- Mathlib.Combinatorics.Hindman
Ultrafilter.semigroup.eq_1 : ∀ {M : Type u_1} [inst : Semigroup M], Ultrafilter.semigroup = { toMul := Ultrafilter.mul, mul_assoc := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Do not use this. Use `le_of_add_le_add_right` instead.  -/
AddRightReflectLE.le_of_add_le_add_right : ∀ {M : Type u_1} {inst : Add M} {inst_1 : LE M} [self : AddRightReflectLE M] {b a₁ a₂ : M}, a₁ + b ≤ a₂ + b → a₁ ≤ a₂
-- Lean.Meta.DiscrTree.Util
/-- Monadically fold over the keys and values stored in a `DiscrTree`.
 -/
Lean.Meta.DiscrTree.foldM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} → [Monad m] → (σ → Array Lean.Meta.DiscrTree.Key → α → m σ) → σ → Lean.Meta.DiscrTree α → m σ
-- Std.Async.UDP
Std.Async.UDP.Membership.noConfusionType : Sort v✝ → Std.Async.UDP.Membership → Std.Async.UDP.Membership → Sort v✝
-- Lean.Widget.InteractiveDiagnostic
/-- Nested text is ignored.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.trace : Lean.Name →
  Std.Format → Bool → Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData) → Lean.Widget.EmbedFmt✝
-- Mathlib.Order.BoundedOrder.Monotone
Antitone.exists : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop},
  (∀ (x : β), Antitone (P x)) → Antitone fun y => ∃ x, P x y
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comap_cobounded : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F),
  Filter.comap (⇑f) (Bornology.cobounded β) = Bornology.cobounded α
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.even_odd₇ : ∀ (a b c : ℕ) (r : ℤ),
  a % 2 = 0 →
    b % 8 = 7 → a / 2 = c → Mathlib.Meta.NormNum.jacobiSymNat c b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- `C` has disjoint coproducts if every coproduct is disjoint.  -/
CategoryTheory.Limits.CoproductsOfShapeDisjoint : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type u_2 → Prop
-- Mathlib.Data.PNat.Defs
PNat.ne_zero : ∀ (n : ℕ+), ↑n ≠ 0
-- Mathlib.RingTheory.Binomial
Ring.choose_natCast : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (n k : ℕ),
  Ring.choose (↑n) k = ↑(n.choose k)
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A space is totally disconnected iff its connected components are singletons.  -/
totallyDisconnectedSpace_iff_connectedComponent_singleton : ∀ {α : Type u} [inst : TopologicalSpace α], TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
-- Std.Internal.Do.WP.Conjunctive
_private.Std.Internal.Do.WP.Conjunctive.0.Std.Internal.Do.EStateM.wpInst.match_1.splitter : {ε σ α : Type} →
  (motive : EStateM.Result ε σ α → Sort u_1) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((el : ε) → (s' : σ) → motive (EStateM.Result.error el s')) → motive x
-- Std.Data.TreeMap.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.TreeMap.keyAtIdx! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → ℕ → α
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Result.mk : Lean.Meta.Try.Collector.OrdSet Lean.Name →
  Lean.Meta.Try.Collector.OrdSet Lean.Name →
    Lean.Meta.Try.Collector.OrdSet Lean.Name →
      Lean.Meta.FunInd.SeenCalls →
        Array Lean.Meta.Try.Collector.InductionCandidate →
          Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind) →
            Lean.Meta.Try.Collector.Result
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- `Multicofork.ofSigmaCofork` as a functor.  -/
CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan I.right} →
              CategoryTheory.Functor
                (CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))
                (CategoryTheory.Limits.Multicofork I)
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_toUInt64 : ∀ (n : UInt32), n.toUInt64.toUInt8 = n.toUInt8
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.continuous_normAtPlace : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K),
  Continuous ⇑(NumberField.mixedEmbedding.normAtPlace w)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The first right fraction.  -/
CategoryTheory.MorphismProperty.RightFraction₂.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.RightFraction₂ X Y → W.RightFraction X Y
-- Std.Http.Server.Config
/-- Maximum length of header field value (default: 8192 bytes)
 -/
Std.Http.Config.maxHeaderValueLength : Std.Http.Config → ℕ
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonAssocRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonAssocRing R] → NonAssocRing (l.Germ R)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardSliceSearcher.toList_atEnd_eq : ∀ {s : String.Slice}, { internalState := String.Slice.Pattern.ForwardSliceSearcher.atEnd }.toList = []
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_erase_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size ≤ t.size
-- Lean.Meta.Tactic.Grind.Theorems
/-- It is local, but we don't have a local hypothesis for it.  -/
Lean.Meta.Grind.Origin.local : Lean.Name → Lean.Meta.Grind.Origin
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyMetrizableSpace.univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X],
  TopologicalSpace.IsCompletelyMetrizableSpace ↑Set.univ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.prodCategoryInstance1 : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Category.{max u₁ v₁, max u₁ (max (v₁ + 1) u₁) v₁} (CategoryTheory.Functor Cᵒᵖ (Type v₁) × Cᵒᵖ)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_mul_eq_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β] (f : MeasureTheory.SimpleFunc α β) (b : β),
  MeasureTheory.SimpleFunc.const α b * f = MeasureTheory.SimpleFunc.map (fun a => b * a) f
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.covariant_sequence_exact₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {n₁ : ℕ}
  (x₁ : CategoryTheory.Abelian.Ext X S.X₁ n₁),
  x₁.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = 0 →
    ∀ {n₀ : ℕ} (hn₀ : n₀ + 1 = n₁), ∃ x₃, x₃.comp hS.extClass hn₀ = x₁
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The isomorphism `K.homology i ≅ L.homology i` induced by an isomorphism
in `HomologicalComplex`.  -/
HomologicalComplex.homologyMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (K ≅ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.homology i ≅ L.homology i
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.hom_cast_eq_of_cons_eq_cons : ∀ {U : Type u_1} [inst : Quiver U] {u v v' w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w}
  {e' : v' ⟶ w} (h : p.cons e = p'.cons e'), Quiver.Hom.cast ⋯ ⋯ e = e'