mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `f : M →* N` is a Localization map for a Submonoid `S` and `k : N ≃* P` is an isomorphism
of `CommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`.  -/
Submonoid.LocalizationMap.ofMulEquivOfLocalizations : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} → [inst_2 : CommMonoid P] → S.LocalizationMap N → N ≃* P → S.LocalizationMap P
-- Mathlib.Algebra.Star.StarAlgHom
/-- A unital morphism of ⋆-algebras is a `NonUnitalStarAlgHom`.  -/
StarAlgHom.toNonUnitalStarAlgHom : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → (A →⋆ₐ[R] B) → A →⋆ₙₐ[R] B
-- Lean.Meta.Tactic.Grind.Types
/-- Internalizes a local declaration which is not a proposition.
**Note**: We must internalize local variables because their types may be empty, and may not be
referenced anywhere else. Example:
```
example (a : { x : Int // x < 0 ∧ x > 0 }) : False := by grind
```
`etaStruct` may also be applicable.
 -/
Lean.Meta.Grind.internalizeLocalDecl : Lean.LocalDecl → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
/-- See `Functor.injective_obj` for a variant taking `Injective X` as a typeclass argument.  -/
CategoryTheory.Functor.injective_obj_of_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.PreservesInjectiveObjects] {X : C},
  CategoryTheory.Injective X → CategoryTheory.Injective (F.obj X)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Universe lift functor for monoids.  -/
MonCat.uliftFunctor : CategoryTheory.Functor MonCat MonCat
-- Mathlib.Data.List.Sublists
List.sublistsLen.eq_1 : ∀ {α : Type u} (n : ℕ) (l : List α), List.sublistsLen n l = List.sublistsLenAux n l id []
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b_relation_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.b₂ * W.b₆ = W.b₄ ^ 2
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.ext : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst_1 : TopologicalSpace Y}
  {Z : Type v'} {inst_2 : TopologicalSpace Z} {x y : Topology.ContinuousMapGeneratedBy X Y Z}, x.toFun = y.toFun → x = y
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_eq_sInter : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  e ∈ M.closure I → M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_comap_eq_self : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S} {t : Subring S},
  t ≤ f.range → Subring.map f (Subring.comap f t) = t
-- Mathlib.Data.Fin.SuccPred
Fin.rightInverse_cast : ∀ {n m : ℕ} (eq : n = m), Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)
-- Init.Data.Iterators.PostconditionMonad
/-- Lifts an operation from `m` to `PostConditionT m` and then applies `PostconditionT.map`.
 -/
Std.Iterators.PostconditionT.liftMap : {m : Type w → Type w'} → [Monad m] → {α β : Type w} → (α → β) → m α → Std.Iterators.PostconditionT m β
-- Mathlib.Topology.TietzeExtension
/-- One step in the proof of the Tietze extension theorem. If `e : C(X, Y)` is a closed embedding
of a topological space into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous
function, then there exists a bounded continuous function `g : Y →ᵇ ℝ` of the norm `‖g‖ ≤ ‖f‖ / 3`
such that the distance between `g ∘ e` and `f` is at most `(2 / 3) * ‖f‖`.  -/
BoundedContinuousFunction.tietze_extension_step : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)),
  Topology.IsClosedEmbedding ⇑e → ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
-- Mathlib.Computability.Primrec.List
Primrec.nat_strong_rec : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] (f : α → ℕ → σ)
  {g : α → List σ → Option σ},
  Primrec₂ g → (∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)) → Primrec₂ f
-- Init.Prelude
/-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`.  -/
Lean.Syntax.getArgs : Lean.Syntax → Array Lean.Syntax
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.comp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans X Y) (θ : CategoryTheory.Lax.LaxTrans Y Z)
  {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b))
            (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).hom)))
-- Mathlib.Topology.Compactness.Paracompact
ParacompactSpace.mk : ∀ {X : Type v} [inst : TopologicalSpace X],
  (∀ (α : Type v) (s : α → Set X),
      (∀ (a : α), IsOpen (s a)) →
        ⋃ a, s a = Set.univ →
          ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a) →
    ParacompactSpace X
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.InnerRegular.inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [ContinuousInv G] [μ.InnerRegular], μ.inv.InnerRegular
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- `IsAssociatedPrime I M` if the prime ideal `I` is the radical of the annihilator
of some `x : M`.  -/
IsAssociatedPrime : {R : Type u_1} → [inst : CommSemiring R] → Ideal R → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_le_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A), (CategoryTheory.Subobject.inf.obj f).obj g ≤ f
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddCommGrpCat.Hom.mk.inj : ∀ {A B : AddCommGrpCat} {hom' hom'_1 : ↑A →+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_eq_gcd_filter_ne_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidablePred fun x => f x = 0], s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.instConvexSpace : {R : Type u_2} →
  [inst : Semiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_3} →
          {Y : Type u_4} → [Convexity.ConvexSpace R X] → [Convexity.ConvexSpace R Y] → Convexity.ConvexSpace R (X × Y)
-- Mathlib.Data.Num.ZNum
Num.ofZNum_toNat : ∀ (n : ZNum), ↑(Num.ofZNum n) = (↑n).toNat
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on `s` and `a : X → A` is continuous and `a x` satisfies the
predicate `p` associated to `𝕜` and `s` is a common neighborhood of the spectra of `a x` for
all `x`, then `fun x ↦ cfc f (a x)` is continuous.

This is weaker than `Continuous.cfc` since it requires `f` to be continuous on a *neighborhood* of
the spectra, but in practice it is often easier to apply because `s` is not required to be compact,
nor does it require an indexed family of compact sets. This is proven using `Continuous.cfc` and
`upperHemicontinuous_spectrum` to produce the necessary family of compact sets.  -/
Continuous.cfc_of_mem_nhdsSet : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [CompleteSpace A] [inst_7 : TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A},
  s ∈ nhdsSet (⋃ x, spectrum 𝕜 (a x)) →
    Continuous a →
      autoParam (∀ (x : X), p (a x)) Continuous.cfc_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) Continuous.cfc_of_mem_nhdsSet._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.Data.Finset.Range
/-- Equivalence between the set of natural numbers which are `≥ k` and `ℕ`, given by `n → n - k`.  -/
notMemRangeEquiv : (k : ℕ) → { n // n ∉ Finset.range k } ≃ ℕ
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedAddCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E],
  OrderDual.seminormedAddCommGroup =
    { toNorm := OrderDual.toNorm, toAddCommGroup := OrderDual.instAddCommGroup,
      toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Real
cauchySeq_of_summable_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α}, (Summable fun n => dist (f n) (f n.succ)) → CauchySeq f
-- Mathlib.Topology.UniformSpace.Ascoli
UniformOnFun.ofFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)),
  UniformOnFun.ofFun 𝔖 = { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp] {k : α}, k ∈ t.keysArray ↔ k ∈ t
-- Mathlib.Data.Matrix.Basis
/-- `Matrix.single` as a bundled additive map.  -/
Matrix.singleAddMonoidHom : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_7} → [DecidableEq m] → [DecidableEq n] → [inst : AddCommMonoid α] → m → n → α →+ Matrix m n α
-- Init.Grind.ToInt
/-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and
a `sub_eq_add_neg` assumption.  -/
Lean.Grind.ToInt.Sub.of_sub_eq_add_neg : ∀ {α : Type u} [inst : Add α] [inst_1 : Neg α] [inst_2 : Sub α],
  (∀ (x y : α), x - y = x + -y) →
    ∀ {I : Lean.Grind.IntInterval},
      I.isFinite = true →
        ∀ [inst_3 : Lean.Grind.ToInt α I] [Lean.Grind.ToInt.Add α I] [Lean.Grind.ToInt.Neg α I],
          Lean.Grind.ToInt.Sub α I
-- Mathlib.Algebra.Algebra.Defs
Algebra.compHom_algebraMap_eq : ∀ {R : Type u} {S : Type v} (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (f : S →+* R), algebraMap S A = (algebraMap R A).comp f
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.aeval_derivative_ne_zero : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] [Nontrivial S] [inst_3 : Algebra R S]
  {p : Polynomial R},
  p.Separable → ∀ {x : S}, (Polynomial.aeval x) p = 0 → (Polynomial.aeval x) (Polynomial.derivative p) ≠ 0
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_eq_inducedOuterMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  μ s = (MeasureTheory.inducedOuterMeasure (fun s x => μ s) ⋯ ⋯) s
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAtFilter.add` -/
HasFDerivAtFilter.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → HasFDerivAtFilter g g' L → HasFDerivAtFilter (fun i => f i + g i) (f' + g') L
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.equivalence_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Preadditive.DoldKan.equivalence.functor = CategoryTheory.Preadditive.DoldKan.N
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_eq_half_log : ∀ {x : ℝ}, x ∈ Set.Icc (-1) 1 → Real.artanh x = 1 / 2 * Real.log ((1 + x) / (1 - x))
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.map` as an `AlgHom`  -/
LocallyConstant.mapₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        (R : Type u_7) →
          [inst_1 : CommSemiring R] →
            [inst_2 : Semiring Y] →
              [inst_3 : Algebra R Y] →
                [inst_4 : Semiring Z] →
                  [inst_5 : Algebra R Z] → (Y →ₐ[R] Z) → LocallyConstant X Y →ₐ[R] LocallyConstant X Z
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.mk.injEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (decDom : FredholmDecomposition 𝕜 E)
  (decCodom : FredholmDecomposition 𝕜 F) (equiv : ↥decDom.X₁ ≃L[𝕜] ↥decCodom.X₁)
  (eq_equiv : u = decCodom.X₁.subtypeL ∘SL ↑equiv ∘SL decDom.proj) (decDom_1 : FredholmDecomposition 𝕜 E)
  (decCodom_1 : FredholmDecomposition 𝕜 F) (equiv_1 : ↥decDom_1.X₁ ≃L[𝕜] ↥decCodom_1.X₁)
  (eq_equiv_1 : u = decCodom_1.X₁.subtypeL ∘SL ↑equiv_1 ∘SL decDom_1.proj),
  ({ decDom := decDom, decCodom := decCodom, equiv := equiv, eq_equiv := eq_equiv } =
      { decDom := decDom_1, decCodom := decCodom_1, equiv := equiv_1, eq_equiv := eq_equiv_1 }) =
    (decDom = decDom_1 ∧ decCodom = decCodom_1 ∧ equiv ≍ equiv_1)
-- Std.Http.Data.Headers.Basic
_private.Std.Http.Data.Headers.Basic.0.Std.Http.Header.parseTokenList : Std.Http.Header.Value → Option (Array String)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : CommGroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Std.Do.SPred.SPred
Std.Do.SPred.entails_cons : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, (P ⊢ₛ Q) = ∀ (s : σ), P s ⊢ₛ Q s
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- A variant of `app_invApp` that gives an `eqToHom` instead of `homOfLE`.  -/
AlgebraicGeometry.Scheme.Hom.app_invApp' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  (hU : U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv =
    Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.LinearAlgebra.Trace
/-- The trace of an endomorphism given a basis.  -/
LinearMap.traceAux : (R : Type u) →
  [inst : CommSemiring R] →
    {M : Type v} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {ι : Type w} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R M → (M →ₗ[R] M) →ₗ[R] R
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.main : Lean.MVarId → Lean.Try.Config → Lean.MetaM Lean.Meta.Try.Collector.Result
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_one_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) {Z_1 : C} (h : M ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.partition_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, (Std.DTreeMap.Raw.partition f t).1.WF
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_shiftLeft_of_lt : ∀ (a b : UInt8), b < 8 → (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 256
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Auxiliary definition for `counitIso`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (F : CategoryTheory.Mon C) →
        (((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp
                  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C)).obj
              F).X ≅
          ((CategoryTheory.Functor.id (CategoryTheory.Mon C)).obj F).X
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundle_model_space_coe_chartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  (p : TangentBundle I H), ↑(chartAt (ModelProd H E) p).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_sub : ∀ {R : Type u} {A : Type z} [inst : CommRing R] {p q : Polynomial R} [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aeval x) (p - q) = (Polynomial.aeval x) p - (Polynomial.aeval x) q
-- Lean.Meta.MkIffOfInductiveProp
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.updateLambdaBinderInfoD! : Lean.Expr → Lean.Expr
-- Mathlib.Data.Nat.Nth
Nat.nth_eq_getD_sort : ∀ {p : ℕ → Prop} (h : (Set.ofPred p).Finite) (n : ℕ), Nat.nth p n = (h.toFinset.sort fun a b => a ≤ b).getD n 0
-- Std.Time.Format.Modifier
Std.Time.Modifier.W.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.W presentation = Std.Time.Modifier.W presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.smithNormalFormCoeffs_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] {N : Submodule R M} [inst_5 : Finite ι]
  (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) (i : ι),
  Submodule.smithNormalFormCoeffs b h i ≠ 0
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isLimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.limit.isLimit F = (CategoryTheory.Limits.getLimitCone F).isLimit
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (f : 𝒜 →+*ᵍ 𝒜)
  (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Algebra.Group.Commute.Units
Commute.isUnit_mul_iff : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → (IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.embedding_mk_eq : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ),
  (NumberField.InfinitePlace.mk φ).embedding = φ ∨
    (NumberField.InfinitePlace.mk φ).embedding = NumberField.ComplexEmbedding.conjugate φ
-- Mathlib.Order.Hom.WithTopBot
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithTop α →o WithTop β`.  -/
OrderHom.withTopMap : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → WithTop α →o WithTop β
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instModule : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) → {S : Type u_3} → [inst_2 : AddCommMonoid S] → [Module R S] → Module (WithVal v) S
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- **Alias** of `isUniformGroup_of_commGroup`. -/
comm_topologicalGroup_is_uniform : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G], IsUniformGroup G
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.emod.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (m : ℕ) (n : ℤ) (h_1 : (m : ℕ) → (n : ℤ) → motive (Int.ofNat m) n)
  (h_2 : (m : ℕ) → (n : ℤ) → motive (Int.negSucc m) n),
  (match Int.ofNat m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_1 m n
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_self_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P}, s.WSameSide x x ↔ (↑s).Nonempty
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.op_w : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.RightResolution X₂), L.op.w = L.w.op
-- Mathlib.Order.WithBot
WithBot.map_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), WithBot.map f ↑a = ↑(f a)
-- Mathlib.Tactic.NormNum.Inv
/-- The `norm_num` extension which identifies expressions of the form `a⁻¹`,
such that `norm_num` successfully recognises `a`.  -/
Mathlib.Meta.NormNum.evalInv : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.GroupTheory.Index
AddSubgroup.IsFiniteRelIndex.mk : ∀ {G : Type u_3} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K ≠ 0 → H.IsFiniteRelIndex K
-- Mathlib.Topology.Connected.Basic
IsPreconnected.subset_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α}, IsPreconnected s → x ∈ s → s ⊆ connectedComponent x
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_π_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C),
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊥_ J))