mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l (fun x => -u x) fun x => -v x
-- Mathlib.Order.Interval.Set.LinearOrder
Set.notMem_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a c : α}, c ∉ Set.Ici a ↔ c < a
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.prop_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderSubobjects] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], P Y → P X
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_C : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R),
  (Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.  -/
CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ)
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, max (max (max v₂ w) u₁) v₁, v₂,
      max (max (max (v₂ + 1) (w + 1)) u₁) (v₁ + 1), u₂}
    (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.leftKanExtension A)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- The connecting homomorphism on the homology sequence attached to a distinguished
triangle in the derived category.  -/
DerivedCategory.HomologySequence.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) →
          (n₀ n₁ : ℤ) →
            autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.δ._auto_1 →
              ((DerivedCategory.homologyFunctor C n₀).obj T.obj₃ ⟶ (DerivedCategory.homologyFunctor C n₁).obj T.obj₁)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.map_π_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  (P.map F η).generators.π =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F P.generators.I η).hom (F.map P.generators.π)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderiv_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E} (n : ℕ),
  DifferentiableAt 𝕜 f x →
    fderiv 𝕜 (f ^ n) x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderiv 𝕜 f x
-- Mathlib.Util.Superscript
Mathlib.Tactic.superscriptTerm.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forM_eq_forM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.1) = Array.forM f t.keysArray
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- An Unoriented angle is unchanged by replacing the first point by one strictly further away on
the same ray.  -/
Sbtw.angle_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p p₂ : P} (p₃ : P),
  Sbtw ℝ p₂ p₁ p → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p p₂ p₃
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The `n`th Taylor polynomial of `log` at `1`, as a function `ℂ → ℂ`  -/
Complex.logTaylor : ℕ → ℂ → ℂ
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_eq_univ₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s : Finset β} {a : α} [inst_3 : Fintype β], a ≠ 0 → (a • s = Finset.univ ↔ s = Finset.univ)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_sdiff_right`. -/
Set.diff_subset_diff_right : ∀ {α : Type u_1} {s t u : Set α}, t ⊆ u → s \ u ⊆ s \ t
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg : Lean.Expr → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Lean.Message
Lean.NamingContext.mk : Lean.Name → List Lean.OpenDecl → Lean.NamingContext
-- Mathlib.NumberTheory.Primorial
/-- **Alias** of `primorial_le_four_pow`. -/
primorial_le_4_pow : ∀ (n : ℕ), primorial n ≤ 4 ^ n
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.gc : ∀ {α : Type u_2} [inst : TopologicalSpace α], GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?_eq_dif : ∀ {s : String.Slice} {p : s.Pos}, p.prev? = if h : p = s.startPos then none else some (p.prev h)
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The result of gluing the `colim Dᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                      [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        [Quiver.IsThin 𝒰.I₀] →
                          [Small.{u, u_2} 𝒰.I₀] → [AlgebraicGeometry.IsZariskiLocalAtTarget P] → P.Over ⊤ S
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.isSameExpr : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (X_1 : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ),
  (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).hom.hom.c.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (f.hom.c.app
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f.hom).obj (Opposite.unop X_1))))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_sups_of_notMem : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α} [inst_2 : DecidableLE α]
  [inst_3 : BoundedOrder α], a ∉ upperClosure ↑s ⊔ upperClosure ↑t → (s ⊻ t).truncatedInf a = ⊥
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval₂_denom_ne_zero : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] {f : K →+* L} {a : L} {x : RatFunc K},
  RatFunc.eval f a x ≠ 0 → Polynomial.eval₂ f a x.denom ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.rel_irrefl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)},
  Std.Irrefl (SimpleGraph.TripartiteFromTriangles.Rel t)
-- Mathlib.Topology.IsLocalHomeomorph
/-- The point `x` lies in the target of `localInverseAt x`.  -/
IsLocalHomeomorph.self_mem_localInverseAt_target : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) {x : X}, x ∈ (hf.localInverseAt x).target
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.start : Std.Http.Internal.UnquoteState✝
-- Mathlib.Probability.Kernel.Condexp
/-- The conditional expectation of `f` with respect to a σ-algebra `m` is almost everywhere equal to
the integral `∫ y, f y ∂(condExpKernel μ m ω)`.  -/
ProbabilityTheory.condExp_ae_eq_integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F],
  m ≤ mΩ →
    MeasureTheory.Integrable f μ → μ[f | m] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Mathlib.Data.List.Induction
List.recNeNil_cons : ∀ {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (x : α) (xs : List α) (h : xs ≠ [])
  (singleton : (x : α) → motive [x] ⋯)
  (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯),
  List.recNeNil singleton cons (x :: xs) ⋯ = cons x xs h (List.recNeNil singleton cons xs h)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.const_mul_right' : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, IsUnit c → f =O[l] g → f =O[l] fun x => c * g x
-- Lean.SubExpr
/-- Map from subexpr positions to values.  -/
Lean.SubExpr.PosMap : Type u → Type (max 0 u)
-- Mathlib.Data.DFinsupp.FiniteInfinite
/-- See `DFinsupp.infinite_of_exists_right` for the case that only one `π ι` is infinite.  -/
DFinsupp.infinite_of_right : ∀ {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Infinite (π i)] [inst : (i : ι) → Zero (π i)] [Nonempty ι],
  Infinite (Π₀ (i : ι), π i)
-- Lean.Elab.Match
Lean.Elab.Term.elabInaccessible : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.smul'.eq_1 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S),
  SetLike.smul' s = { smul := fun r x => ⟨r • ↑x, ⋯⟩ }
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.mk : Array Lean.Elab.Structural.RecArgCandidate → Lean.MessageData → Lean.Elab.Structural.RecArgCandidates
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.lt_iff_encode_lt : ∀ {α : Type u} {inst : LE α} {inst_1 : LT α} {β : outParam (Type v)} {inst_2 : LE β} {inst_3 : LT β}
  {inst_4 : Std.PRange.UpwardEnumerable β} {inst_5 : Std.PRange.LawfulUpwardEnumerable β}
  {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β}
  [self : HasModel✝ α β] {x y : α}, x < y ↔ HasModel.encode✝ x < HasModel.encode✝ y
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNonUnitalSeminormedRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : NonUnitalSeminormedRing R] → NonUnitalSeminormedRing (BoundedContinuousFunction α R)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation'.app_apply : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : M.Derivation' φ')
  {X : Dᵒᵖ} (b : ↑(R.obj X)), (d.app X).d b = d.d b
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Legendre symbol `legendreSym p a` with an integer `a` and a prime number `p`
is the same as the Jacobi symbol `J(a | p)`.  -/
jacobiSym.legendreSym.to_jacobiSym : ∀ (p : ℕ) [fp : Fact (Nat.Prime p)] (a : ℤ), legendreSym p a = jacobiSym a p
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.probCharDual.eq_1 : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (L : StrongDual ℝ F),
  BoundedContinuousFunction.probCharDual L = BoundedContinuousFunction.char Real.continuous_probChar ⋯ L
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.isOpen_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.one_le_divConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G}, A.Nonempty → B.Nonempty → 1 ≤ A.divConst B
-- Mathlib.Data.List.Basic
List.exists_mem_iff_get : ∀ {α : Type u} {l : List α} {p : α → Prop}, (∃ x ∈ l, p x) ↔ ∃ i, p (l.get i)
-- Mathlib.Data.PNat.Basic
PNat.lt_add_left : ∀ (n m : ℕ+), n < m + n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedDelayedTheoremInstance : Inhabited Lean.Meta.Grind.DelayedTheoremInstance
-- Mathlib.Data.Ordmap.Invariants
Ordnode.All.eq_def : ∀ {α : Type u_1} (P : α → Prop) (x : Ordnode α),
  Ordnode.All P x =
    match x with
    | Ordnode.nil => True
    | Ordnode.node size l x r => Ordnode.All P l ∧ P x ∧ Ordnode.All P r
-- Mathlib.Logic.Function.Basic
Function.Injective.isStrictTotalOrder_onFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [IsStrictTotalOrder β r], IsStrictTotalOrder α (Function.onFun r f)
-- Mathlib.Order.Ideal
/-- Given an element `p : P` and a family `𝒟` of cofinal subsets of a preorder `P`,
indexed by a countable type, `idealOfCofinals p 𝒟` is an ideal in `P` which
- contains `p`, according to `mem_idealOfCofinals p 𝒟`, and
- intersects every set in `𝒟`, according to `cofinal_meets_idealOfCofinals p 𝒟`.

This proves the Rasiowa–Sikorski lemma.  -/
Order.idealOfCofinals : {P : Type u_1} → [inst : Preorder P] → P → {ι : Type u_2} → [Encodable ι] → (ι → Order.Cofinal P) → Order.Ideal P
-- Mathlib.CategoryTheory.Iso
/-- The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`.  -/
CategoryTheory.Iso.homFromEquiv : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → {Z : C} → (X ⟶ Z) ≃ (Y ⟶ Z)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.uniqueUpToIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
  (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).inv = CategoryTheory.Limits.biproduct.desc b.ι
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b h) (t.truncLEι b) = t.truncLEι a
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.lipschitzWith : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (self : ODE.FunSpace t₀ x₀ r L), LipschitzWith L self.toFun
-- Lean.Meta.Basic
/-- Save cache, execute `x`, restore cache  -/
_private.Lean.Meta.Basic.0.Lean.Meta.savingCacheImpl : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Aesop.Tree.Data
Aesop.MVarClusterData.state : {Goal Rapp : Type} → Aesop.MVarClusterData Goal Rapp → Aesop.NodeState
-- Init.Data.Vector.Attach
Vector.attach_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β},
  (Vector.map f xs).attach =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      xs.attach
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.ite : {x : Type} →
  (c : Prop) →
    [Decidable c] →
      Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.IsBounded
BddBelow.isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α} {s : Set β},
  s ∈ f → BddBelow (u '' s) → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.Data.Matrix.Basic
Matrix.instIsStablyFiniteRingOfFinite : ∀ {α : Type u_11} [inst : Semiring α] [Finite α], IsStablyFiniteRing α
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
/-- The Grothendieck topology on the category of topological spaces is the topology given by
jointly surjective open embeddings.  -/
TopCat.grothendieckTopology : CategoryTheory.GrothendieckTopology TopCat
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1_cert : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- The functor sending a `G`-representation `A` to `Hₙ(G, A)`.  -/
groupHomology.functor : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → ℕ → CategoryTheory.Functor (Rep.{u, u, u} k G) (ModuleCat k)
-- Mathlib.Control.Traversable.Equiv
/-- Given a functor `t`, a function `t' : Type u → Type u`, and
equivalences `t α ≃ t' α` for all `α`, then every function `α → β` can
be mapped to a function `t' α → t' β` functorially (see
`Equiv.functor`).  -/
Equiv.map : {t t' : Type u → Type u} → ((α : Type u) → t α ≃ t' α) → [Functor t] → {α β : Type u} → (α → β) → t' α → t' β
-- Mathlib.Order.JordanHolder
CompositionSeries.isMaximal_eraseLast_last : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X},
  0 < s.length → JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)
-- Mathlib.Algebra.Category.Semigrp.Basic
addEquivIsoAddMagmaIso.eq_1 : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y],
  addEquivIsoAddMagmaIso =
    { hom := TypeCat.ofHom fun e => e.toAddMagmaCatIso, inv := TypeCat.ofHom fun i => i.addMagmaCatIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Algebra.Algebra.Spectrum.Basic
resolventSet.eq_1 : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  resolventSet R a = {r | IsUnit ((algebraMap R A) r - a)}
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
AddMonoidAlgebra.instHopfAlgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [HopfAlgebra R A] → {G : Type u_3} → [inst_3 : AddGroup G] → HopfAlgebra R (AddMonoidAlgebra A G)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.exists_of_eq : ∀ {R : Type u_1} {inst : CommSemiring 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'} {S : Submonoid R} {f : M →ₗ[R] M'}
  [self : IsLocalizedModule S f] {x₁ x₂ : M}, f x₁ = f x₂ → ∃ c, c • x₁ = c • x₂
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- Given a formal multilinear series `p` and a vector `x`, then `p.partialSum n x` is the sum
`Σ pₖ xᵏ` for `k ∈ {0,..., n-1}`.  -/
FormalMultilinearSeries.partialSum : {𝕜 : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [inst_7 : ContinuousAdd E] →
                      [inst_8 : ContinuousAdd F] →
                        [inst_9 : ContinuousConstSMul 𝕜 E] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → FormalMultilinearSeries 𝕜 E F → ℕ → E → F
-- Init.Data.SInt.Bitwise
instAssociativeInt16HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Lean.Syntax
Lean.Syntax.isTokenAntiquot : Lean.Syntax → Bool
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The characterization of this multiplication on partially homogeneous elements.  -/
GradedTensorProduct.tmul_coe_mul_coe_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {j₁ i₂ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (a₂ : ↥(𝒜 i₂)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.isAlgClosed_of_model_ACF : ∀ (p : ℕ) (K : Type u_2) [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K]
  [h : K ⊨ FirstOrder.Language.Theory.ACF p], IsAlgClosed K
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
/-- The injective dimension of an object in an abelian category.  -/
CategoryTheory.injectiveDimension : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → WithBot ℕ∞
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.categories : Lean.Parser.ParserExtension.State → Lean.Parser.ParserCategories
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_disjoint_left : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s₁ s₂ : Finset α},
  Disjoint s₁ s₂ → ∀ (t : Finset α), Disjoint (G.interedges s₁ t) (G.interedges s₂ t)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).size = t.size
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- `α →₂[μ] E` is the type of `L²` or square-integrable functions from `α` to `E`.  -/
MeasureTheory.«term_→₂[_]_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- The Euler-Mascheroni constant `γ`.  -/
_private.Mathlib.NumberTheory.Harmonic.ZetaAsymp.0.termγ : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- The isometry `lp G 2 → E` induced by the orthogonal family is surjective.  -/
IsHilbertSum.surjective_isometry : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (self : IsHilbertSum 𝕜 G V), Function.Surjective ⇑⋯.linearIsometry
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Any permutation matrix is doubly stochastic.  -/
permMatrix_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {σ : Equiv.Perm n},
  Equiv.Perm.permMatrix R σ ∈ doublyStochastic R n
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_toBitVec : ∀ (a : UInt16), { toBitVec := a.toBitVec } = a