mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.getD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap.Raw α β cmp → (a : α) → β a → β a
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.semigroupWithZero : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → SemigroupWithZero (α i)] → SemigroupWithZero ((i : ι) → α i)
-- Mathlib.FieldTheory.Separable
/-- An integral field extension in characteristic 0 is separable.  -/
Algebra.IsSeparable.of_integral : ∀ (F : Type u_1) [inst : Field F] (K : Type u_2) [inst_1 : Ring K] [inst_2 : Algebra F K] [IsDomain K]
  [Algebra.IsIntegral F K] [CharZero F], Algebra.IsSeparable F K
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.transcendental_iff_transcendental_val : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A} {x : ↥S},
  Transcendental R x ↔ Transcendental R ↑x
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
/-- Let `F : J ⥤ Cᵒᵖ` be a functor, `c'` a colimit cocone for `F.leftOp ⋙ shrinkYoneda.{w}`.
For any `P : Cᵒᵖ ⥤ Type w`, this is the bijection between `c'.pt ⟶ P` and the type
of sections of `F ⋙ P`.  -/
CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
          {F : CategoryTheory.Functor J Cᵒᵖ} →
            {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})} →
              CategoryTheory.Limits.IsColimit c' →
                {P : CategoryTheory.Functor Cᵒᵖ (Type w)} → (c'.pt ⟶ P) ≃ ↑(F.comp P).sections
-- Lean.Elab.DefView
Lean.Elab.DefKind : Type
-- Lean.Meta.Tactic.Grind.Action
/-- Returns `.closed [← mk]` if tracing is enabled, and `.closed []` otherwise.  -/
Lean.Meta.Grind.Action.closeWith : Lean.Meta.Grind.GrindM Lean.Meta.Grind.TGrind → Lean.Meta.Grind.GrindM Lean.Meta.Grind.ActionResult
-- Mathlib.GroupTheory.Exponent
neg_eq_self_of_exponent_two : ∀ {G : Type u} [inst : AddGroup G], AddMonoid.exponent G = 2 → ∀ (x : G), -x = x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_nthRoots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
  0 < n → ∀ {a x : R}, x ∈ Polynomial.nthRoots n a ↔ x ^ n = a
-- Std.Data.ExtTreeMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.ExtTreeMap.erase : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Std.ExtTreeMap α β cmp
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- An auxiliary lemma that combines two double exponential estimates into a similar estimate
on the difference of the functions.  -/
PhragmenLindelof.isBigO_sub_exp_exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} {u : ℂ → ℝ},
  (∃ c < a, ∃ B, f =O[l] fun z => Real.exp (B * Real.exp (c * |u z|))) →
    (∃ c < a, ∃ B, g =O[l] fun z => Real.exp (B * Real.exp (c * |u z|))) →
      ∃ c < a, ∃ B, (f - g) =O[l] fun z => Real.exp (B * Real.exp (c * |u z|))
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.isLocallyInjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → IsLocallyInjective f
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with real-valued functions.  -/
Real.inner_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → ℝ) {p q : ℝ},
  p.HolderConjugate q → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_f : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (C : PrimeSpectrum.BasicConstructibleSetData R), (PrimeSpectrum.BasicConstructibleSetData.map φ C).f = φ C.f
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret a `⨆`-homomorphism as an `⨅`-homomorphism between the dual orders.  -/
sSupHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : SupSet α] → [inst_1 : SupSet β] → sSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Auxiliary definition for `HasCokernels SemiNormedGrp`.  -/
SemiNormedGrp.cokernelCocone : {X Y : SemiNormedGrp} → (f : X ⟶ Y) → CategoryTheory.Limits.Cofork f 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.ker_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] (f : CategoryTheory.Arrow C),
  (CategoryTheory.Limits.ker C).obj f = CategoryTheory.Limits.kernel f.hom
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, (m.insertMany l).contains k = (m.contains k || (List.map Sigma.fst l).contains k)
-- Init.Conv
/-- `skip` does nothing.  -/
Lean.Parser.Tactic.Conv.skip : Lean.ParserDescr
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_mul : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (t : Interval α), ⊥ * t = ⊥
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- The canonical isomorphism between families of additive monoid homomorphisms `α → (M →+ N)`
and monoid homomorphisms `(α →₀ M) →+ N`.  -/
Finsupp.liftAddHom : {α : Type u_1} →
  {M : Type u_8} →
    {N : Type u_10} → [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → (α → M →+ N) ≃+ ((α →₀ M) →+ N)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
IsAssociatedPrime.isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsAssociatedPrime I M → I.IsPrime
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- For `1 < re s` the L-function of a Dirichlet character agrees with the sum of the naive Dirichlet
series.
 -/
DirichletCharacter.LFunction_eq_LSeries : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re → DirichletCharacter.LFunction χ s = LSeries (fun x => χ ↑x) s
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.of_restrict : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α}, (M.restrict R).IsNonloop e → M.IsNonloop e
-- Std.Time.Format.DateFormat
/-- Full era names (2 elements: index 0 = Before Common Era, index 1 = Common Era).
 -/
Std.Time.DateFormatSymbols.eraLong : Std.Time.DateFormatSymbols → Vector String 2
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km fallback : α}, Std.Internal.List.minKey? l = some km → Std.Internal.List.getKeyD km l fallback = km
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id a)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv)
        (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom h))
-- Lean.Parser.Extension
Lean.Parser.withSetOption : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_some_some : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a b : α}, edist (some a) (some b) = edist a b
-- Mathlib.Data.Finset.Empty
/-- Attempt to prove that a finset is nonempty using the `finsetNonempty` aesop rule-set.

You can add lemmas to the rule-set by tagging them with either:
* `aesop safe apply (rule_sets := [finsetNonempty])` if they are always a good idea to follow or
* `aesop unsafe apply (rule_sets := [finsetNonempty])` if they risk directing the search to a blind
  alley.

TODO: should some of the lemmas be `aesop safe simp` instead?
 -/
Mathlib.Meta.proveFinsetNonempty : {u : Lean.Level} → {α : Q(Type u)} → (s : Q(Finset «$α»)) → Lean.MetaM (Option Q(«$s».Nonempty))
-- Mathlib.Order.Interval.Set.LinearOrder
Set.compl_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Iio a)ᶜ = Set.Ici a
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.str : String → Lean.JsonRpc.RequestID
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- If `v : HeightOneSpectrum R` then `natGenerator v` is the generator in `ℕ` of the corresponding
ideal in `ℤ`.  -/
Rat.HeightOneSpectrum.natGenerator : {R : Type u_2} →
  [inst : CommRing R] → [inst_1 : Algebra R ℚ] → [IsIntegralClosure R ℤ ℚ] → IsDedekindDomain.HeightOneSpectrum R → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.getMsb?_of_ge : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), w ≤ i → x.getMsb? i = none
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α}
  {b : β a}, t.WF → (t.containsThenInsertIfNew a b).2.WF
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.sum : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {ι : Type} {t : Finset ι} {f : ι → M → E'},
  (∀ i ∈ t, MDiffAt (f i) z) → MDiffAt (∑ i ∈ t, f i) z
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_mul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ),
  WittVector.init n (x * y) = WittVector.init n (WittVector.init n x * WittVector.init n y)
-- Mathlib.Algebra.MvPolynomial.Invertible
/-- A natural number that is invertible when coerced to a commutative semiring `R`
is also invertible when coerced to any polynomial ring with rational coefficients.

Short-cut for typeclass resolution.  -/
MvPolynomial.invertibleCoeNat : (σ : Type u_1) → (R : Type u_2) → (p : ℕ) → [inst : CommSemiring R] → [Invertible ↑p] → Invertible ↑p
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.instHasDimensionLTToSSetBoundary : ∀ {n : ℕ}, (SSet.boundary n).toSSet.HasDimensionLT n
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_empty : ∀ {α : Type u}, ∅.Subsingleton
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A `weightedVSub` with sum of weights 0 is in the `vectorSpan` of
an indexed family.  -/
weightedVSub_mem_vectorSpan : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 0 → ∀ (p : ι → P), (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instPreservesColimitsTopCatForgetOfHasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.PreservesColimits (AlgebraicGeometry.SheafedSpace.forget C)
-- Mathlib.Algebra.Notation.Defs
SMul.ext_iff : ∀ {M : Type u} {α : Type v} {x y : SMul M α}, x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Analysis.Convex.BetweenList
List.Sbtw.eq_1 : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (l : List P),
  List.Sbtw R l = (List.Wbtw R l ∧ List.Pairwise (fun x1 x2 => x1 ≠ x2) l)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
/-- Given a projective resolution `R` of an object `X` of an abelian category,
this is a constructor for elements in `Ext X Y n` which takes as an input
a "cocycle" `f : R.cocomplex.X n ⟶ Y`.  -/
CategoryTheory.ProjectiveResolution.extMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.ProjectiveResolution X) →
            {n : ℕ} →
              (f : R.complex.X n ⟶ Y) →
                (m : ℕ) →
                  n + 1 = m →
                    CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0 → CategoryTheory.Abelian.Ext X Y n
-- Lean.Meta.Match.Match
Lean.Meta.Match.getMkMatcherInputInContext : Lean.Meta.MatcherApp → Bool → Lean.MetaM Lean.Meta.Match.MkMatcherInput
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical.eq_1 : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  (a : E), EuclideanDomain.divRadical a = a / UniqueFactorizationMonoid.radical a
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.mem_support_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → v ∈ G.support
-- Mathlib.Topology.Inseparable
SeparationQuotient.instNontrivialOfNontrivialTopology : ∀ {α : Type u_4} [inst : TopologicalSpace α] [NontrivialTopology α], Nontrivial (SeparationQuotient α)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.meromorphicOrderAt_comp_smul : ∀ {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane} {g : GL (Fin 2) ℝ},
  0 < (↑g).det →
    meromorphicOrderAt (fun z => f (g • ↑UpperHalfPlane.ofComplex z)) ↑τ =
      meromorphicOrderAt (fun z => f (↑UpperHalfPlane.ofComplex z)) ↑(g • τ)
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.lie_baseChange : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] {I : LieIdeal R L} {N : LieSubmodule R L M},
  LieSubmodule.baseChange A ⁅I, N⁆ = ⁅LieSubmodule.baseChange A I, LieSubmodule.baseChange A N⁆
-- Init.Data.Option.Basic
Option.max_none_right : ∀ {α : Type u_1} [inst : Max α] {o : Option α}, o ⊔ none = o
-- Mathlib.Logic.Function.Basic
/-- **Cantor's diagonal argument** implies that there are no injective functions from `Set α`
to `α`.  -/
Function.cantor_injective : ∀ {α : Type u_4} (f : Set α → α), ¬Function.Injective f
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ofHom_comp : ∀ {M N P : Type u} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : AddCommMonoid P] (f : M →+ N)
  (g : N →+ P),
  AddCommMonCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddCommMonCat.ofHom f) (AddCommMonCat.ofHom g)
-- Aesop.Rule.Basic
Aesop.Rule.name : {α : Type} → Aesop.Rule α → Aesop.RuleName
-- Mathlib.Data.Nat.Count
Nat.count_succ' : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ),
  Nat.count p (n + 1) = Nat.count (fun k => p (k + 1)) n + if p 0 then 1 else 0
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.gate_mk : ∀ {g : ℕ} {i : Bool}, (Std.Sat.AIG.Fanin.mk g i).gate = g
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.mulHeight_mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι] {x : ι → K}
  (hx : x ≠ 0), (Projectivization.mk K x hx).mulHeight = Height.mulHeight x
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧),
  π.IsProper ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (f : LaurentPolynomial R) (n : ℤ),
  (LaurentPolynomial.invert f).coeff n = f.coeff (-n)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.slice.sizeOf_spec : ∀ (numPrefix numSuffix : ℕ),
  sizeOf (Lean.Elab.Term.Quotation.HeadCheck.slice numPrefix numSuffix) = 1 + sizeOf numPrefix + sizeOf numSuffix
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a presheaf `F` on the topological space `X` and a family of opens `U` of `X`,
the natural cone associated to `F` and `U` used in the definition of
`F.IsSheafOpensLeCover` is a limit cone iff the natural cone associated to `F`
and the sieve generated by the presieve associated to `U` is a limit cone.  -/
TopCat.Presheaf.isLimitOpensLeEquivGenerate₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Presheaf C X) →
        {ι : Type u_2} →
          (U : ι → TopologicalSpace.Opens ↑X) →
            {Y : TopologicalSpace.Opens ↑X} →
              Y = iSup U →
                CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≃
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Functor.mapCone F
                      (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows.cocone.op)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- Inversion on a `Group` or `GroupWithZero` is a permutation of the underlying type.  -/
Equiv.inv : (G : Type u_14) → [InvolutiveInv G] → Equiv.Perm G
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X.obj Y.obj
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- A Gram matrix is positive semidefinite.  -/
Matrix.posSemidef_gram : ∀ {E : Type u_1} {n : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [Finite n] (v : n → E), (Matrix.gram 𝕜 v).PosSemidef
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resIndAdjunction_unit_app : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (B : Rep.{max w u v, u, v} k G),
  (Rep.resIndAdjunction k S).unit.app B =
    CategoryTheory.CategoryStruct.comp ((Rep.resCoindAdjunction k S.subtype).unit.app B)
      (Rep.res S.subtype B).indCoindIso.inv
-- Mathlib.GroupTheory.ArchimedeanDensely
denselyOrdered_additive_iff : ∀ {X : Type u_2} [inst : LT X], DenselyOrdered (Additive X) ↔ DenselyOrdered X
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_hom_fst' : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap S (TensorProduct R S T)))) =
    CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_π_self_assoc : ∀ {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]
  (j : J) {Z : C} (h : f j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) =
    h
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comp_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂),
  (h.comp h').h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₃
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.List.TProd.mk.match_1.splitter : {ι : Type u_1} →
  (motive : List ι → Sort u_2) →
    (x : List ι) → (Unit → motive []) → ((i : ι) → (is : List ι) → motive (i :: is)) → motive x
-- Mathlib.Data.String.Basic
String.ltb.eq_def : ∀ (s₁ s₂ : String.Legacy.Iterator),
  String.ltb s₁ s₂ =
    if s₂.hasNext = true then
      if s₁.hasNext = true then if s₁.curr = s₂.curr then String.ltb s₁.next s₂.next else decide (s₁.curr < s₂.curr)
      else true
    else false
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to infinity along a filter, then `f` divided by a positive
constant also tends to infinity.  -/
Filter.Tendsto.atTop_div_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x / r) l Filter.atTop
-- Mathlib.RingTheory.Regular.ProjectiveDimension
ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular : ∀ {R : Type u} [inst : CommRing R] [Small.{v, u} R] [inst_2 : IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M] (x : R),
  IsSMulRegular (↑M) x →
    x ∈ IsLocalRing.maximalIdeal R →
      CategoryTheory.projectiveDimension (ModuleCat.of R (QuotSMulTop x ↑M)) = CategoryTheory.projectiveDimension M + 1
-- Lean.Server.FileWorker.Utils
/-- The document.  -/
Lean.Server.FileWorker.EditableDocumentCore.meta : Lean.Server.FileWorker.EditableDocumentCore → Lean.Server.DocumentMeta
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizePersistentExtensions : Lean.Environment → Array Lean.ModuleData → Lean.Options → IO Lean.Environment
-- Mathlib.Data.Set.Prod
Set.eqOn_prod_iff : ∀ {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {s : Set α} {a b : α → γ × δ},
  Set.EqOn a b s ↔ Set.EqOn (Prod.fst ∘ a) (Prod.fst ∘ b) s ∧ Set.EqOn (Prod.snd ∘ a) (Prod.snd ∘ b) s
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap.mk : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {F : CategoryTheory.Functor C D} (X : C), P X → P.strictMap F (F.obj X)
-- Mathlib.Algebra.Star.Unitary
Unitary.instIsStarNormal : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (u : ↥(unitary R)), IsStarNormal u
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (ringInst semiringInst : Lean.Expr) (charInst? : Option (Lean.Expr × ℕ))
  (addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr),
  sizeOf
      { id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one? } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf ringInst + sizeOf semiringInst + sizeOf charInst? + sizeOf addFn? +
                  sizeOf mulFn? +
                sizeOf subFn? +
              sizeOf negFn? +
            sizeOf powFn? +
          sizeOf intCastFn? +
        sizeOf natCastFn? +
      sizeOf one?