mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Raw
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.Raw.getKey : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.HashMap.Raw α β) → (a : α) → a ∈ m → α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F) {c : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cocone G),
  ((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h) P).desc s =
    CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app c).hom
      (CategoryTheory.CategoryStruct.comp (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom
        (h.unitIso.inv.app s).hom)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.LawfulEqOrd α]
  [Std.TransOrd α] {k : α}, t.WF → (k ∈ t.keys ↔ k ∈ t)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (a : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ), Turing.TM1to0.trAux M s (Turing.TM1.Stmt.load a q) x = Turing.TM1to0.trAux M s q (a s x)
-- Lean.Elab.Quotation.Precheck
/-- Registers a double backtick syntax quotation pre-check.

`@[quot_precheck k]` registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the
syntax node kind `k`. It should implement eager name analysis on the passed syntax by throwing an
exception on unbound identifiers, and calling `precheck` recursively on nested terms, potentially
with an extended local context (`withNewLocal`). Macros without registered precheck hook are
unfolded, and identifier-less syntax is ultimately assumed to be well-formed.
 -/
Lean.Elab.Term.Quotation.precheckAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Term.Quotation.Precheck
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.over_forget_coverPreserving : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
  CategoryTheory.CoverPreserving (J.over X) J (CategoryTheory.Over.forget X)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.exists_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x y : M}, f x = f y → ∃ c, ↑c + x = ↑c + y
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval₂_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S)
  [inst_2 : Semiring T] (g : S →+* T) (x : T),
  Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.eval₂ (g.comp f) x p
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} [inst_2 : SizeOf J] [inst_3 : SizeOf C]
  (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j)
      CategoryTheory.Limits.IsColimit.fac._autoParam)
  (uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s)
      CategoryTheory.Limits.IsColimit.uniq._autoParam),
  sizeOf { desc := desc, fac := fac, uniq := uniq } = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.restrictScalars_add : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] [inst_11 : ContinuousAdd M₂] (f g : M₁ →L[A] M₂),
  ContinuousLinearMap.restrictScalars R (f + g) =
    ContinuousLinearMap.restrictScalars R f + ContinuousLinearMap.restrictScalars R g
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.ιK.congr_simp : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₁ : A} {X₃ : C}
  (f₃ f₃_1 : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)),
  f₃ = f₃_1 →
    ∀ {K : A} (α α_1 : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃),
      α = α_1 →
        ∀ [inst_3 : ι.Full],
          CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α =
            CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃_1 α_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α}
  {k : α} {fallback : Unit},
  Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k fallback = ()
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.equivOfIsometry_symm : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂),
  (CliffordAlgebra.equivOfIsometry e).symm = CliffordAlgebra.equivOfIsometry e.symm
-- Mathlib.CategoryTheory.Category.Cat.Adjunction
/-- `typeToCat : Type ⥤ Cat` is left adjoint to `Cat.objects : Cat ⥤ Type`  -/
CategoryTheory.Cat.typeToCatObjectsAdj : CategoryTheory.typeToCat ⊣ CategoryTheory.Cat.objects
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_comap_comap_eq_relrank_of_surjective : ∀ {E : Type v} [inst : Field E] (A B : Subfield E) {L : Type v} [inst_1 : Field L] (f : L →+* E),
  Function.Surjective ⇑f → (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank B
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.subLeft : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X)
  {b c : FreeNonUnitalNonAssocAlgebra R X}, FreeLieAlgebra.Rel R X b c → FreeLieAlgebra.Rel R X (a - b) (a - c)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → t.minKey?.isSome = true
-- Mathlib.Data.List.Cycle
List.prev_getLast_cons' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y : α) (hxy : x ∈ y :: l),
  x = y → (y :: l).prev x hxy = (y :: l).getLast ⋯
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Adj.isPath_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.IsPath
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsLT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Ioc a c ∈ nhdsWithin b (Set.Iio b)
-- Init.Data.Array.Count
Array.countP_set : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} {a : α} (h : i < xs.size),
  Array.countP p (xs.set i a h) = (Array.countP p xs - if p xs[i] = true then 1 else 0) + if p a = true then 1 else 0
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_f : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), b.symm.f = b.e
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_mul_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p * q).natDegree ≤ p.natDegree + q.natDegree
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_eq_map' : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.Limits.biprod.map f g = CategoryTheory.Limits.biprod.map' f g
-- Std.Time.Format.Modifier
Std.Time.Modifier.E.injEq : ∀ (presentation presentation_1 : Std.Time.Text),
  (Std.Time.Modifier.E presentation = Std.Time.Modifier.E presentation_1) = (presentation = presentation_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The functor `pointwiseRightKanExtension L F` is a pointwise right Kan
extension of `F` along `L`.  -/
CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseRightKanExtension F] →
                  (CategoryTheory.Functor.RightExtension.mk (L.pointwiseRightKanExtension F)
                      (L.pointwiseRightKanExtensionCounit F)).IsPointwiseRightKanExtension
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- To construct an isomorphism of costructured arrows,
we need an isomorphism of the objects underlying the source,
and to check that the triangle commutes.
 -/
CategoryTheory.CostructuredArrow.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {f f' : CategoryTheory.CostructuredArrow S T} →
              (g : f.left ≅ f'.left) →
                autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom)
                    CategoryTheory.CostructuredArrow.isoMk._auto_1 →
                  (f ≅ f')
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_bot : ∀ {α : Type u_1} [inst : BooleanRing α], ofBoolAlg ⊥ = 0
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Two equivalent open partial homeomorphisms have coinciding `invFun` on the target  -/
OpenPartialHomeomorph.EqOnSource.symm_eqOn_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → Set.EqOn (↑e.symm) (↑e'.symm) e.target
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.instIsIsoFst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.fst
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X Y
-- Mathlib.Algebra.Ring.Opposite
RingHom.toOpposite_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S)
  (hf : ∀ (x y : R), Commute (f x) (f y)), ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
-- Mathlib.Data.W.Constructions
WType.ofList.eq_def : ∀ (γ : Type u) (x : List γ),
  WType.ofList γ x =
    match x with
    | [] => WType.mk WType.Listα.nil PEmpty.elim
    | hd :: tl => WType.mk (WType.Listα.cons hd) fun x => WType.ofList γ tl
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A `V`-category is a category enriched in a monoidal category `V`.

Note that we do not assume that `V` is a concrete category,
so there may not be an "honest" underlying category at all!
 -/
CategoryTheory.EnrichedCategory : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] → [CategoryTheory.MonoidalCategory V] → Type u₁ → Type (max (max u₁ v) w)
-- Mathlib.RingTheory.Ideal.Over
Ideal.instLiesOverUnder : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B)
  [𝔓.LiesOver P], 𝔓.LiesOver (Ideal.under A P)
-- Lean.Meta.Coe
/-- Return true iff `declName` is one of the auxiliary definitions/projections used to implement
coercions.
 -/
Lean.Meta.isCoeDecl : Lean.Environment → Lean.Name → Bool
-- Mathlib.Order.Filter.TendstoCofinite
/-- Given `f : α → β` with `Filter.TendstoCofinite f` and `v : α → M`,
`Filter.TendstoCofinite.mapDomain f v : β → M` is the function whose value at `b : β` is
the sum of `v x` over all `x` such that `f x = b`.  -/
Filter.TendstoCofinite.mapDomain : {α : Type u_1} →
  {β : Type u_2} → {M : Type u_5} → (f : α → β) → [AddCommMonoid M] → [Filter.TendstoCofinite f] → (α → M) → β → M
-- Init.Data.Array.MapIdx
Array.toList_mapIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : ℕ → α → m β}, Array.toList <$> Array.mapIdxM f xs = List.mapIdxM f xs.toList
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeObj_unitor : ∀ {C : Type u} (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C)).normalizeObj n = n
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_singleton_eq : ∀ {α : Type u_1} {M : Matroid α} {e : α} [M.Loopless],
  autoParam (e ∈ M.E) Matroid.eRk_singleton_eq._auto_1 → M.eRk {e} = 1
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UniformIntegrable.spec : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.UniformIntegrable f p μ →
        ∀ {ε : ℝ},
          0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
/-- The set of fixed points under a group action, as a subring.  -/
FixedPoints.subring : (B : Type u_2) → [inst : Ring B] → (G : Type u_4) → [inst_1 : Monoid G] → [MulSemiringAction G B] → Subring B
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformRight e x).2 = x.2 ∩ e⁻¹ • x.2
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.instChosenPullbacksAlongHomMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      {f : I ⟶ J} →
        [CategoryTheory.ChosenPullbacksAlong f] → CategoryTheory.ChosenPullbacksAlong (CategoryTheory.Over.mk f).hom
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.trace.eq_1 : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : SlashInvariantFormClass F 𝒢 k] [inst_2 : 𝒢.IsFiniteRelIndex ℋ],
  SlashInvariantForm.trace ℋ f =
    {
      toFun :=
        have this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
        ∑ q, SlashInvariantForm.quotientFunc f q,
      slash_action_eq' := ⋯ }
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_neg_add_chainBot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M (-α + ⇑(LieModule.chainBot α β)) = ⊥
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.secondCountableTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SecondCountableTopology Y]
  (h : X ≃ₜ Y), SecondCountableTopology X
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r)) = X.toΓSpecCApp r
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piCongrLeft_apply_apply : ∀ {ι : Type u_8} {ι' : Type u_9} (e : ι ≃ ι') {β : ι' → Type u_10} [inst : (i' : ι') → MeasurableSpace (β i')]
  (x : (i : ι) → β (e i)) (i : ι), (MeasurableEquiv.piCongrLeft (fun i' => β i') e) x (e i) = x i
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.range_coe : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι},
  Set.range DFunLike.coe = {x | ∀ᶠ (i : ι) in 𝓕, x i ∈ A i}
-- Mathlib.Analysis.Convex.Body
ConvexBody.instAddCommMonoid : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → [ContinuousAdd V] → AddCommMonoid (ConvexBody V)
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The operator norm is submultiplicative.  -/
ContinuousLinearMap.opNorm_comp_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_7}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃]
  (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F), ‖h ∘SL f‖ ≤ ‖h‖ * ‖f‖
-- Mathlib.RingTheory.WittVector.Defs
_private.Mathlib.RingTheory.WittVector.Defs.0.term𝕎 : Lean.ParserDescr
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeft_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  (MulEquiv.refl M).monoidHomCongrLeft = MulEquiv.refl (M →* N)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeAlgEquiv_symm_apply : ∀ (n : Type u_3) {R : Type u_7} (α : Type v) [inst : Fintype n] [inst_1 : CommSemiring R] [inst_2 : StarRing R]
  [inst_3 : TrivialStar R] [inst_4 : Semiring α] [inst_5 : StarRing α] [inst_6 : Algebra R α] [inst_7 : StarModule R α]
  (a : (Matrix n n α)ᵐᵒᵖ), (Matrix.conjTransposeAlgEquiv n α).symm a = (MulOpposite.unop a).conjTranspose
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An open embedding `f : X ⟶ Y` induces an adjunction between `OpenNhds x` and `OpenNhds (f x)`.
We define `IsOpenEmbedding.adjunctionNhds` as `IsOpenEmbedding.isOpenMap.adjunctionNds`, so it
won't default to `IsInducing.adjunctionNhds`, which is an adjunction in the other direction.
 -/
Topology.IsOpenEmbedding.adjunctionNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) →
      (x : ↑X) → ⋯.functorNhds x ⊣ TopologicalSpace.OpenNhds.map f x
-- Init.Data.UInt.Basic
instAndOpUInt8 : AndOp UInt8
-- Init.Prelude
/-- Run `x` with an incremented recursion depth counter.  -/
Lean.Macro.withIncRecDepth : {α : Type} → Lean.Syntax → Lean.MacroM α → Lean.MacroM α
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_isIdealMorphism : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  I.incl.IsIdealMorphism
-- Std.Async.Basic
/-- A `Task` that may resolve to either a value of type `α` or an error value of type `ε`.
 -/
Std.Async.ETask : Type → Type → Type
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.quiverGenerators : {G : Type u_1} → {inst : CategoryTheory.Groupoid G} → [self : IsFreeGroupoid G] → Quiver (IsFreeGroupoid.Generators G)
-- Std.Http.Internal.IndexMultiMap
/-- Flat array of all key-value entries in insertion order.
 -/
Std.Internal.IndexMultiMap.entries : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → Array (α × β)
-- Lean.Parser.Extension
Lean.Parser.getSyntaxKindOfParserAlias? : Lean.Name → IO (Option Lean.SyntaxNodeKind)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_le_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  a ⊓ b ≤ b
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.mk : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          {IB : ModelWithCorners ℝ EB HB} →
            {n : WithTop ℕ∞} →
              {B : Type u_3} →
                [inst_3 : TopologicalSpace B] →
                  [inst_4 : ChartedSpace HB B] →
                    {F : Type u_4} →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace ℝ F] →
                          {E : B → Type u_5} →
                            [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_8 : (b : B) → TopologicalSpace (E b)] →
                                [inst_9 : (b : B) → AddCommGroup (E b)] →
                                  [inst_10 : (b : B) → Module ℝ (E b)] →
                                    [inst_11 : FiberBundle F E] →
                                      [inst_12 : VectorBundle ℝ F E] →
                                        (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) →
                                          (∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v) →
                                            (∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v) →
                                              (∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}) →
                                                (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n
                                                    fun b => ⟨b, inner b⟩) →
                                                  Bundle.ContMDiffRiemannianMetric IB n F E
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.codRestrict.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : SubmonoidClass S N] (f f_1 : M →* N) (e_f : f = f_1) (s : S) (h : ∀ (x : M), f x ∈ s),
  f.codRestrict s h = f_1.codRestrict s ⋯
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.exists_is_const_of_deriv_eq_zero : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜}, IsOpen s → IsPreconnected s → DifferentiableOn 𝕜 f s → Set.EqOn (deriv f) 0 s → ∃ a, ∀ x ∈ s, f x = a