mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pi64 : Std.Internal.Parsec.ByteArray.Parser ℤ
-- Std.Data.ExtHashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtHashMap.alter : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → (Option β → Option β) → Std.ExtHashMap α β
-- Mathlib.Data.Seq.Basic
/-- The `bind` operator for the `Seq1` monad,
which maps `f` on each element of `s` and appends the results together.
(Not all of `s` may be evaluated, because the first few elements of `s`
may already produce an infinite result.)  -/
Stream'.Seq1.bind : {α : Type u} → {β : Type v} → Stream'.Seq1 α → (α → Stream'.Seq1 β) → Stream'.Seq1 β
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `λₗ _` as an isomorphism of functors.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft D
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
              CategoryTheory.Functor.id D
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B_two : CartanMatrix.B 2 = !![2, -2; -1, 2]
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonMessage : Lean.FromJson Lean.JsonRpc.Message
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_startPos_of_slice_ne_startPos : ∀ {s : String.Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁},
  p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).startPos → p ≠ s.startPos
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Coalgebra F} (h : CategoryTheory.Limits.IsTerminal A),
  CategoryTheory.CategoryStruct.comp A.str (CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv h) =
    CategoryTheory.CategoryStruct.id A.V
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_zero : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Zero α], Matrix.replicateRow ι 0 = 0
-- Mathlib.Tactic.LinearCombinationPrime
/-- Performs macro expansion of a linear combination expression,
using `+`/`-`/`*`/`/` on equations and values.
* `.proof p` means that `p` is a syntax corresponding to a proof of an equation.
  For example, if `h : a = b` then `expandLinearCombo (2 * h)` returns `.proof (c_add_pf 2 h)`
  which is a proof of `2 * a = 2 * b`.
* `.const c` means that the input expression is not an equation but a value.
 -/
Mathlib.Tactic.LinearCombinationPrime.expandLinearCombo : Lean.Expr → Lean.Term → Lean.Elab.TermElabM Mathlib.Tactic.LinearCombinationPrime.Expanded
-- Mathlib.RingTheory.Trace.Quotient
Algebra.intTrace.congr_simp : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B], Algebra.intTrace A B = Algebra.intTrace A B
-- Mathlib.LinearAlgebra.Matrix.WithConv
instCommSemiringWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [CommSemiring α] → CommSemiring (WithConv (Matrix m n α))
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt8
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
AddGroupLieAlgebra.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4)
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G],
  AddGroupLieAlgebra I G = TangentSpace I 0
-- Mathlib.Topology.NoetherianSpace
/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets.  -/
TopologicalSpace.NoetherianSpace.exists_finset_irreducible : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : TopologicalSpace.Closeds α),
  ∃ S, (∀ (k : ↥S), IsIrreducible ↑↑k) ∧ s = S.sup id
-- Mathlib.Data.Nat.GCD.BigOperators
/-- See `IsCoprime.prod_right` for the corresponding lemma about `IsCoprime`  -/
Nat.Coprime.prod_right : ∀ {ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ}, (∀ i ∈ t, x.Coprime (s i)) → x.Coprime (∏ i ∈ t, s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuous_sinh : Continuous Real.sinh
-- Mathlib.Algebra.Group.Basic
AddCommMonoid.toGrindNatModule : (α : Type u_5) → [s : AddCommMonoid α] → Lean.Grind.NatModule α
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterExists_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).ExcenterExists = s.ExcenterExists
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {Z : C} (h : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.leftHomologyπ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `upperBound? k` retrieves the largest entry smaller than or equal to `k`,
if it exists.
 -/
RBTree.RBSet.upperBound? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → α → Option α
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.lift_apply : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (P : Type u_7) [inst_7 : NonAssocSemiring P] (g : (i : ι) → G i →+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.Ring.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.Algebra.Lie.TraceForm
LieSubmodule.idealizer.congr_simp : ∀ {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]
  (N N_1 : LieSubmodule R L M), N = N_1 → N.idealizer = N_1.idealizer
-- Mathlib.Tactic.AdaptationNote
/-- General function implementing adaptation notes.  -/
reportAdaptationNote : (Lean.Syntax → Lean.Meta.Tactic.TryThis.Suggestion) → Lean.MetaM Unit
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_a : ∀ {u : PNat.XgcdType}, u.r = 0 → u.reduce = u.finish
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.eq_def : ∀ (k : ℕ) (i : ℤ) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : ℕ),
  Int.trailingZeros.aux k i hi hk acc =
    match k, ⋯, hk with
    | k.succ, x, hk => if h : i % 2 = 0 then Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1) else acc
-- Lean.ErrorExplanation
/-- Returns an error explanation for the given name if one exists.  -/
Lean.getErrorExplanation? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.ErrorExplanation)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertIfNew : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {k a : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl a =
    if compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 1
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- Construct the Beck cofork in the category of algebras. This cofork is reflexive as well as a
coequalizer.
 -/
CategoryTheory.Monad.beckAlgebraCofork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      (X : T.Algebra) →
        CategoryTheory.Limits.Cofork (CategoryTheory.Monad.FreeCoequalizer.topMap X)
          (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)
-- Aesop.Rule
Aesop.RegularRule.safe : Aesop.SafeRule → Aesop.RegularRule
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_comp_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty AlgebraicTopology.DoldKan.PInfty = 0
-- Mathlib.Data.Set.Sigma
Set.preimage_image_sigmaMk_of_ne : ∀ {ι : Type u_1} {α : ι → Type u_3} {i j : ι}, i ≠ j → ∀ (s : Set (α j)), Sigma.mk i ⁻¹' Sigma.mk j '' s = ∅
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_ric : ∀ {b : ℕ}, (*...=b).toArray.size = b + 1
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_eq : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (s : Finset ι) (v : ι → R),
  Lagrange.nodal s v = ∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))
-- Mathlib.Analysis.Fourier.Convolution
SchwartzMap.convolution.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace ℂ F₁]
  [inst_8 : NormedSpace 𝕜 F₁] [inst_9 : SMulCommClass ℂ 𝕜 F₁] [inst_10 : NormedAddCommGroup F₂]
  [inst_11 : NormedSpace ℂ F₂] [inst_12 : NormedSpace 𝕜 F₂] [inst_13 : SMulCommClass ℂ 𝕜 F₂]
  [inst_14 : NormedAddCommGroup F₃] [inst_15 : NormedSpace ℂ F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
  SchwartzMap.convolution B =
    {
      toFun := fun f =>
        FourierTransform.fourierInvCLM 𝕜 (SchwartzMap E F₃) ∘SL
          (SchwartzMap.pairing B) (FourierTransform.fourier f) ∘SL FourierTransform.fourierCLM 𝕜 (SchwartzMap E F₂),
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_mul : ∀ {ι : 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} (x y : P.Equiv P),
  RootPairing.Equiv.weightEquiv P P x * RootPairing.Equiv.weightEquiv P P y =
    RootPairing.Equiv.weightEquiv P P y ≪≫ₗ RootPairing.Equiv.weightEquiv P P x
-- Mathlib.Topology.Algebra.Algebra
/-- Copy of a `ContinuousAlgHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
ContinuousAlgHom.copy : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (f : A →A[R] B) → (f' : A → B) → f' = ⇑f → A →A[R] B
-- Mathlib.Data.Int.Basic
Int.natAbs_surjective : Function.Surjective Int.natAbs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R}, W'.Equation P → W'.addX P P = 0
-- Mathlib.Tactic.Algebraize
/-- This function takes an array of expressions `t`, all of which are assumed to be `RingHom`s,
and searches through the local context to find any additional properties of these `RingHoms`, after
which it tries to add the corresponding `Algebra` properties to the context. It only looks for
properties that have been tagged with the `algebraize` attribute, and uses this tag to find the
corresponding `Algebra` property.  -/
Mathlib.Tactic.Algebraize.addProperties : Array Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.Limits.kernelSubobjectMap sq =
    (CategoryTheory.Limits.kernelSubobject f').factorThru
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow
        (CategoryTheory.Arrow.Hom.left sq))
      ⋯
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.toPartitionOfUnity_toFun_apply : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (i : ι) (a : M),
  (f.toPartitionOfUnity i) a = (f i) a
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_of_degree_sub_lt_of_eval_index_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι),
  Set.InjOn v ↑s → (f - g).degree < ↑s.card → (∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_target_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0), f = 0
-- Mathlib.Control.Traversable.Equiv
Equiv.comp_traverse : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t]
  {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t' α),
  Equiv.traverse eqv (Functor.Comp.mk ∘ Functor.map f ∘ g) x =
    Functor.Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
-- Batteries.Data.String.Legacy
/-- Creates a new string by removing the longest prefix from `s` in which `p` returns `true` for all
characters.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.dropWhile`.

Examples:
* `"red green blue".dropWhile (·.isLetter) = " green blue"`
* `"red green blue".dropWhile (· == 'r') = "ed green blue"`
* `"red green blue".dropWhile (· != 'n') = "n blue"`
* `"red green blue".dropWhile (fun _ => true) = ""`
 -/
String.Legacy.dropWhile : String → (Char → Bool) → String
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.coe_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : A),
  (↑𝕜 a).toProd.2 = (ContinuousLinearMap.mul 𝕜 A).flip a
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
SSet.coconeN'_pt : ∀ (X : SSet) [inst : X.Nonsingular], X.coconeN'.pt = X
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
FiniteMultiplicity.of_prime_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a b : α},
  Prime a → b ≠ 0 → FiniteMultiplicity a b
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.instCoeAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → Coe (A →ₐc[R] B) (A →ₐ[R] B)
-- Mathlib.MeasureTheory.Group.Measure
/-- An alternative way to prove that `μ` is right invariant under addition.  -/
MeasureTheory.forall_measure_preimage_add_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G),
  (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h + g) ⁻¹' A) = μ A) ↔ μ.IsAddRightInvariant
-- Init.Data.Ord.UInt
USize.instOrd : Ord USize
-- Mathlib.Data.Seq.Computation
Computation.results_bind : ∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} {m n : ℕ},
  s.Results a m → (f a).Results b n → (s.bind f).Results b (n + m)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.mk : ∀ {E : Type u_4} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E],
  (∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖star x * x‖) → CStarRing E
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_piecewise_of_subset_right : ∀ {ι : Type u_1} {π : ι → Sort u_2} {s t : Finset ι} [inst : (i : ι) → Decidable (i ∈ s)]
  [inst_1 : (i : ι) → Decidable (i ∈ t)],
  t ⊆ s → ∀ (f g₁ g₂ : (a : ι) → π a), s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.map_obj : ∀ {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 : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.map F).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => CategoryTheory.WithInitial.of (F.obj x)
    | CategoryTheory.WithInitial.star => CategoryTheory.WithInitial.star
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.zero_mem_smul_set_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] {a : α} {t : Set β}, a ≠ 0 → (0 ∈ a • t ↔ 0 ∈ t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.chainComplexMap_PInfty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C),
  CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R) AlgebraicTopology.DoldKan.PInfty =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (SSet.chainComplexMap f R)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isOpen_iff_dirSupInacc : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [t : TopologicalSpace α] [Topology.IsScottHausdorff α Set.univ],
  IsOpen s ↔ DirSupInacc s
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.eq_1 : ∀ (R : Type u_1) {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A),
  IsIntegral R x = (algebraMap R A).IsIntegralElem x
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonAssocSemiring : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonAssocSemiring α] → NonAssocSemiring (Shrink.{v, u_1} α)
-- Mathlib.FieldTheory.Separable
Polynomial.separable_map : ∀ {F : Type u} [inst : Field F] {S : Type u_1} [inst_1 : CommRing S] [Nontrivial S] (f : F →+* S) {p : Polynomial F},
  (Polynomial.map f p).Separable ↔ p.Separable
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.revSkip?_char_eq_none_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, pos.revSkip? c = none ↔ ∀ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ ≠ c
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  AddMonoidAlgebra.single m r = AddMonoidAlgebra.ofCoeff fun₀ | m => r
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalMin f a → ∀ {g : β → γ}, Monotone g → IsLocalMin (g ∘ f) a
-- Mathlib.Data.NNRat.Defs
NNRat.coe_nonneg : ∀ (q : ℚ≥0), 0 ≤ ↑q
-- Std.Async.Signal
Std.Async.Signal.sigquit.sizeOf_spec : sizeOf Std.Async.Signal.sigquit = 1
-- Mathlib.Data.PNat.Defs
PNat.div_coe : ∀ (m k : ℕ+), m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k
-- Mathlib.FieldTheory.Extension
/-- Given an integral element `s : E` over `F` whose `F`-conjugates are all in `K`,
any lift can be extended to one whose carrier contains `s`.  -/
IntermediateField.Lifts.exists_lift_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] (x : IntermediateField.Lifts F E K) {s : E},
  IsIntegral F s → (Polynomial.map (algebraMap F K) (minpoly F s)).Splits → ∃ y, x ≤ y ∧ s ∈ y.carrier
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.comp_le_lemma : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y Z : CategoryTheory.Dial C} (F : X.Hom Y) (G : Y.Hom Z),
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F))
              F.F))).obj
      X.rel ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp F.f G.f)
            (CategoryTheory.CategoryStruct.id Z.tgt))).obj
      Z.rel
-- Mathlib.Topology.Compactness.Lindelof
coLindelof_le_coclosedLindelof : ∀ {X : Type u} [inst : TopologicalSpace X], Filter.coLindelof X ≤ Filter.coclosedLindelof X
-- Init.System.IO
/-- Checks whether the task has finished execution, at which point calling `Task.get` will return
immediately.
 -/
IO.hasFinished : {α : Type u_1} → Task α → BaseIO Bool
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.mulIndicator_const_iff_of_ne : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : One β] {s : Set α} {c : β},
  c ≠ 1 → (Filter.EventuallyConst (s.mulIndicator fun x => c) l ↔ Filter.EventuallyConst s l)
-- Lean.Data.KVMap
Lean.KVMap.contains : Lean.KVMap → Lean.Name → Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k} {h₁ : a ∈ m.insert k v}, (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯
-- Mathlib.Order.Max
isMax_iff_forall_not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMax a ↔ ∀ (b : α), ¬a < b
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right'`, which requires sigma-finite `ν` and `μ`.  -/
MeasureTheory.Measure.rnDeriv_smul_right : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν]
  [ν.HaveLebesgueDecomposition μ] {r : NNReal}, r ≠ 0 → ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ