mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instVAddAssocClass : ∀ (M : Type v) (N : Type w) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd N X]
  [inst_3 : VAdd M N] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X] [VAddAssocClass M N X],
  VAddAssocClass M N (UniformSpace.Completion X)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTypeAscriptions : Lean.Options → Bool
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.radius_logSizeBallSeq_add_one : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c (i + 1)).radius =
    PairReduction.logSizeRadius (PairReduction.logSizeBallSeq J hJ a c (i + 1)).point
      (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset a c
-- Mathlib.Analysis.Convex.Combination
convexHullAddMonoidHom_apply : ∀ (R : Type u_1) (E : Type u_3) [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [inst_4 : IsStrictOrderedRing R] (a : Set E),
  (convexHullAddMonoidHom R E) a = (convexHull R) a
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toLocallyRingedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y),
  AlgebraicGeometry.Spec.toLocallyRingedSpace.map f = AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.post_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.post L R F).map f).left = f.left
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting'.eq_1 : Nat.primeCounting' = Nat.count Nat.Prime
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap_comp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c') [inst_3 : e.IsRelIff] {Z : HomologicalComplex C c'} (h : M.stupidTrunc e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.stupidTruncMap (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.stupidTruncMap φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.stupidTruncMap φ' e) h)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_of_valuation_le_one : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), A.valuation x ≤ 1 → x ∈ A
-- Mathlib.Algebra.Category.Ring.Instances
Localization.epi : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R),
  CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R (Localization M)))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.branch.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a : Γ → σ → Bool} {a_1 a_2 : Turing.TM1.Stmt Γ Λ σ} {a_3 : Γ → σ → Bool}
  {a_4 a_5 : Turing.TM1.Stmt Γ Λ σ},
  Turing.TM1.Stmt.branch a a_1 a_2 = Turing.TM1.Stmt.branch a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [inst_1 : SizeOf C]
  [inst_2 : (a : C) → SizeOf (P a)] (obj : C) (property : P obj),
  sizeOf { obj := obj, property := property } = 1 + sizeOf obj + sizeOf property
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (rk : α) →
                  (rv : β rk) →
                    (size_1 : ℕ) →
                      (k : α) →
                        (v : β k) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                                (Std.DTreeMap.Internal.Impl.inner size_1 k v l r))) →
              ((size : ℕ) →
                  (rk : α) →
                    (rv : β rk) →
                      (size_1 : ℕ) →
                        (rlk : α) →
                          (rlv : β rlk) →
                            (l r : Std.DTreeMap.Internal.Impl α β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size rk rv
                                  (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                                  Std.DTreeMap.Internal.Impl.leaf)) →
                ((rs : ℕ) →
                    (rk : α) →
                      (rv : β rk) →
                        (rls : ℕ) →
                          (rlk : α) →
                            (rlv : β rlk) →
                              (rll rlr : Std.DTreeMap.Internal.Impl α β) →
                                (size : ℕ) →
                                  (k : α) →
                                    (v : β k) →
                                      (l r : Std.DTreeMap.Internal.Impl α β) →
                                        motive
                                          (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                            (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                            (Std.DTreeMap.Internal.Impl.inner size k v l r))) →
                  motive r
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root_coroot_two : ∀ {ι : 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] (self : RootPairing ι R M N) (i : ι),
  (self.toLinearMap (self.root i)) (self.coroot i) = 2
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`.
Let `f : ℂ → E` be a function such that

* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |im z|))` on `U` for some `c < π / (b - a)`;
* `f z = 0` on the boundary of `U`.

Then `f` is equal to zero on the closed strip `{z : ℂ | a ≤ re z ≤ b}`.
 -/
PhragmenLindelof.eq_zero_on_vertical_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E},
  DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.im|))) →
      (∀ (z : ℂ), z.re = a → f z = 0) → (∀ (z : ℂ), z.re = b → f z = 0) → Set.EqOn f 0 (Complex.re ⁻¹' Set.Icc a b)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The isomorphism of categories between
`(X ⊗ Y).HomotopyCategory` and `X.HomotopyCategory ⥤ Y.HomotopyCategory`.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.iso : (X Y : SSet.Truncated 2) →
  CategoryTheory.Cat.of (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory ≅
    CategoryTheory.Cat.of (X.HomotopyCategory × Y.HomotopyCategory)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.functorHomEquiv_symm_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F G : CategoryTheory.Functor C D) (A : CategoryTheory.Functor C (Type (max u v v'))) (x : F.HomObj G A) (X : C),
  ((F.functorHomEquiv G A).symm x).app X =
    TypeCat.ofHom fun a =>
      { app := fun Y f => x.app Y ((CategoryTheory.ConcreteCategory.hom (A.map f)) a), naturality := ⋯ }
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (i : Fin (k + 1)),
  F.intervalGapsWithin h a b i = (Finset.intervalGapsWithin.fst F h a i, Finset.intervalGapsWithin.snd F h b i)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_6 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (cf cg : Nat.Partrec.Code)
  (h_1 : (x : Nat.Partrec.Code) → motive 0 x) (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero)
  (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ) (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left)
  (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, cf.pair cg with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_6 k cf cg
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.isBigO_sub : ∀ {𝕜 : 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 : E → F}
  {x₀ : E}, DifferentiableAt 𝕜 f x₀ → (fun x => f x - f x₀) =O[nhds x₀] fun x => x - x₀
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.infLELeft_apply_mk : ∀ {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (x : ↑X) (m : x ∈ U ⊓ V), (U.infLELeft V) ⟨x, m⟩ = ⟨x, ⋯⟩
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.DiscrInfo.mk.inj : ∀ {hName? hName?_1 : Option Lean.Name}, { hName? := hName? } = { hName? := hName?_1 } → hName? = hName?_1
-- Mathlib.RingTheory.Congruence.Hom
RingCon.congr_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M}
  {d : RingCon N} (e : M ≃+* N) (h : c = d.comap e), (RingCon.congr e h).symm = RingCon.congr e.symm ⋯
-- Lean.Elab.DocString
/-- Determines whether docstring suggestions are to be provided as part of editing the string or in a
later report.
 -/
Lean.Doc.SuggestionMode : Type
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- Given `X : DerivedCategory.Plus C` and `n : ℤ`, this property means
that `X` is `≤ n` for the canonical t-structure.  -/
DerivedCategory.Plus.IsLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory.Plus C → ℤ → Prop
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Iic : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R},
  Int.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋
-- Mathlib.Logic.Small.Set
small_sInter : ∀ {α : Type u1} {s : Set (Set α)} {t : Set α}, t ∈ s → ∀ [Small.{u, u1} ↑t], Small.{u, u1} ↑(⋂₀ s)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinKernel_def : ∀ (a x : ℝ), ↑(HurwitzZeta.sinKernel (↑a) x) = jacobiTheta₂' (↑a) (Complex.I * ↑x) / (-2 * ↑Real.pi)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.sum_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x}
  {s : Finset ι},
  (∀ i ∈ s, ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u x₀) →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ i ∈ s, t i x⟩) u x₀
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The free sheaf of modules on a certain type `I`.  -/
SheafOfModules.free : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → Type u → SheafOfModules R
-- Mathlib.Data.List.Nodup
List.Nodup.sigma : ∀ {α : Type u} {l₁ : List α} {σ : α → Type u_1} {l₂ : (a : α) → List (σ a)},
  l₁.Nodup → (∀ (a : α), (l₂ a).Nodup) → (l₁.sigma l₂).Nodup
-- Init.Data.Range.Polymorphic.Char
Char.instHasSize_2 : Std.Rxi.HasSize Char
-- Mathlib.NumberTheory.FactorisationProperties
Nat.deficient_iff_not_abundant_and_not_perfect : ∀ {n : ℕ}, n ≠ 0 → (n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect)
-- Init.Data.String.TakeDrop
/-- Creates a string slice by removing the longest prefix from `s` in which `pat` matched
\(potentially repeatedly\).

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropWhile Char.isLower == " green blue".toSlice`

* `"red green blue".dropWhile 'r' == "ed green blue".toSlice`

* `"red red green blue".dropWhile "red " == "green blue".toSlice`

* `"red green blue".dropWhile (fun (_ : Char) => true) == "".toSlice`
 -/
String.dropWhile : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_5 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.mul with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_5 ()
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_left : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Iio ↑n)) (nhdsWithin (↑n - 1) (Set.Iic (↑n - 1)))
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `lt_of_tsub_lt_tsub_right_of_le` for a weaker statement in a partial order.  -/
lt_of_tsub_lt_tsub_right : ∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α],
  a - c < b - c → a < b
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_le_const : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  {f : α → ENNReal} {c : ENNReal}, (∀ᵐ (x : α) ∂μ, f x ≤ c) → ∫⁻ (x : α), f x ∂μ ≤ c
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The map that picks up the initial vertex of a 2-simplex, as a morphism in the 2-truncated
simplex category.  -/
SSet.Truncated.ι0₂ : { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValRat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.  -/
padicValRat.mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ}, q ≠ 0 → r ≠ 0 → padicValRat p (q * r) = padicValRat p q + padicValRat p r
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_idem_right : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] (f g₁ g₂ : (a : ι) → π a),
  s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.ext : ∀ {R : Type u_1} {inst : CommSemiring R} {x y : PrimeSpectrum R}, x.asIdeal = y.asIdeal → x = y
-- Aesop.Forward.Substitution
/-- Insert the mapping `pi ↦ inst` into the substitution `s`. Precondition: `pi`
is in the domain of `s`.  -/
Aesop.Substitution.insert : Aesop.PremiseIndex → Lean.Expr → Aesop.Substitution → Aesop.Substitution
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.mk : {R : Type u} → [inst : Ring R] → (toTopologicalSpace : TopologicalSpace R) → IsTopologicalRing R → RingTopology R
-- Mathlib.MeasureTheory.Measure.Support
/-- A regular measure has conull support.  -/
MeasureTheory.Measure.support_mem_ae_of_regular : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.Regular],
  μ.support ∈ MeasureTheory.ae μ
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Ioi : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0),
  NNRat.cast ⁻¹' Set.Ioi ↑p = Set.Ioi p
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- When the domain is non-empty, we do not need the `0 ≤ C` condition in the formula for `‖f‖` as a
`sInf`.  -/
BoundedContinuousFunction.norm_eq_of_nonempty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) [h : Nonempty α], ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
-- Lean.Parser.Extra
Lean.Parser.nonReservedSymbol.parenthesizer : String → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `a : X → A` is continuous on `t : Set X`,
and `a x` satisfies the predicate `p` associated to `𝕜` and has spectrum contained in `s` for all
`x ∈ t`, then `fun x ↦ cfc f (a x)` is continuous on `t`.  -/
ContinuousOn.cfc' : ∀ {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] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
      ContinuousOn a t →
        (∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s) →
          (∀ x ∈ t, p (a x)) →
            autoParam (ContinuousOn f s) ContinuousOn.cfc'._auto_1 → ContinuousOn (fun x => cfc f (a x)) t
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isCoverDense' : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} (J : CategoryTheory.GrothendieckTopology C)
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D}
  [self : CategoryTheory.Functor.IsDenseSubsite J K G], G.IsCoverDense K
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsTheta.isBigO_symm : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =Θ[l] g → g =O[l] f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_equiv_eq_comap_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (K : Subsemigroup M),
  Subsemigroup.map (↑f) K = Subsemigroup.comap (↑f.symm) K
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeSortType : CoeSort AddCommGrpCat (Type u)
-- Init.Data.Array.Attach
Array.foldl_attachWith : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {xs : Array α} {q : α → Prop} (H : ∀ a ∈ xs, q a) {f : β → { x // q x } → β}
  {b : β},
  stop = xs.size →
    Array.foldl f b (xs.attachWith q H) 0 stop =
      Array.foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
        b xs.attach
-- Lean.Meta.Tactic.Grind.EMatch
/-- We represent an `E-matching` problem as a list of constraints.  -/
Lean.Meta.Grind.EMatch.Cnstr : Type
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_union : ∀ {X : Type u_1} (g₁ g₂ : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))),
  DiffeologicalSpace.generateFrom (g₁ ∪ g₂) = DiffeologicalSpace.generateFrom g₁ ⊔ DiffeologicalSpace.generateFrom g₂
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZifV1.repr : Std.Time.TimeZone.TZif.TZifV1 → ℕ → Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The lower part of the second column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₁.X₂, X₂ := S.L₂.X₂, X₃ := S.L₃.X₂, f := S.v₁₂.τ₂, g := S.v₂₃.τ₂, zero := ⋯ }.Exact
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_rio : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rio._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {bound : α},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e bound).isLT) t.toList
-- Mathlib.Order.SupClosed
subset_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, s ⊆ infClosure s
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity is a filter on α × α (inferred from an ambient uniform space
structure on α).  -/
uniformity : (α : Type u) → [UniformSpace α] → Filter (α × α)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae.eq_1 : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  (μ : F), MeasureTheory.ae μ = Filter.ofCountableUnion (fun x => μ x = 0) ⋯ ⋯
-- Mathlib.Topology.Defs.Basic
/-- Notation for `Continuous` with respect to non-standard topologies.  -/
Topology.Continuous_of : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.CompMul
derivWithin_comp_mul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (c : 𝕜) (f : 𝕜 → E) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (c * x)) s x = c • derivWithin f (c • s) (c * x)
-- Mathlib.Order.Antichain
/-- **Alias** of `IsAntichain.insert_of_symm`. -/
IsAntichain.insert_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsAntichain r s → ∀ [Std.Symm r], (∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b) → IsAntichain r (insert a s)