mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The second projection from the glued scheme into `Y`.  -/
AlgebraicGeometry.Scheme.Pullback.p2 : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ Y
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.subtype_apply : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x : ↥H),
  ↑H x = ↑x
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- Just a computational lemma we need for the next main proof.  -/
GenContFract.compExactValue_correctness_of_stream_eq_some_aux_comp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {a : K} (b c : K),
  Int.fract a ≠ 0 → (↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.symm_bijective : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Bijective PartialHomeomorph.symm
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- Given `OverClass X S` and `OverClass Y S` and `f : X ⟶ Y`,
`HomIsOver f S` is the typeclass asserting `f` commutes with the structure morphisms.  -/
CategoryTheory.HomIsOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (X ⟶ Y) → (S : C) → [CategoryTheory.OverClass X S] → [CategoryTheory.OverClass Y S] → Prop
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the entries of a dependent hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.iter : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.Iter ((a : α) × β a)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsVarsEquivLeft_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : (L.withConstants γ).Term (α ⊕ β)),
  FirstOrder.Language.Term.constantsVarsEquivLeft t =
    FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β).symm) t.constantsToVars
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.edist_le_ediam_of_mem`.

---

If two points belong to some set, their edistance is bounded by the diameter of the set  -/
EMetric.edist_le_diam_of_mem : ∀ {X : Type u_2} {s : Set X} {x y : X} [inst : PseudoEMetricSpace X], x ∈ s → y ∈ s → edist x y ≤ Metric.ediam s
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.univ_pos : 0 < Cardinal.univ.{u, v}
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under division.  -/
IntermediateField.div_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x y : L}, x ∈ S → y ∈ S → x / y ∈ S
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens},
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app M) U =
    CategoryTheory.CategoryStruct.id
      (((AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.id X)).obj M).presheaf.obj
        (Opposite.op U))
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.mk.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] {F : C → D}
  {P : CategoryTheory.MorphismProperty D} [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.InducedWideCategory D F P}
  (hom : F X ⟶ F Y) (property : P hom) (hom_1 : F X ⟶ F Y) (property_1 : P hom_1),
  ({ hom := hom, property := property } = { hom := hom_1, property := property_1 }) = (hom = hom_1)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.mem_torsion_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  x ∈ Submodule.torsion R M ↔ ∃ a, a • x = 0
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_homothety_center : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- In the commutative diagram
```
             f     g
    0 --→ X₁ --→ X₂ --→ X₃
          ↑      ↑      ↑
         v|     u|     w|
          ι  → ι ⊕ ι' ← ι'
```
where the top row is an exact sequence of modules and the maps on the bottom are `Sum.inl` and
`Sum.inr`. If `u` is injective and `v` and `w` are linearly independent, then `u` is linearly
independent.  -/
ModuleCat.linearIndependent_leftExact : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁},
      LinearIndependent R v →
        ∀ {u : ι ⊕ ι' → ↑S.X₂},
          LinearIndependent R (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) →
            CategoryTheory.Mono S.f →
              u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v → LinearIndependent R u
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.instCoeFunForallReal : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [FiniteDimensional ℝ E] → {c : M} → CoeFun (SmoothBumpFunction I c) fun x => M → ℝ
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- The number of fixed points of a `p ^ n`-th root of the identity function over a finite set
and the set's cardinality have the same residue modulo `p`, where `p` is a prime.  -/
Equiv.Perm.card_fixedPoints_modEq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Function.End α} {p n : ℕ} [hp : Fact (Nat.Prime p)],
  f ^ p ^ n = 1 → Fintype.card α ≡ Fintype.card ↑(Function.fixedPoints f) [MOD p]
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.postcomp_homotopyClass : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex}
  {ψ : B.toSSet ⟶ C.toSSet} (f : SSet.RelativeMorphism A B φ) (f' : SSet.RelativeMorphism B C ψ)
  {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
  f.homotopyClass.postcomp f' fac = (f.comp f' fac).homotopyClass
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instRing : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Ring (WithVal v)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_iff : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k k' : α}, m.get? k = some k' ↔ ∃ (h : k ∈ m), m.get k h = k'
-- Mathlib.Algebra.Algebra.Tower
Submodule.orderIsoOfAlgebraMapSurjective_symm_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (h : Function.Surjective ⇑(algebraMap R S)) (N : Submodule R M),
  (RelIso.symm (Submodule.orderIsoOfAlgebraMapSurjective h)) N = { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.under_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Under X),
  U.left = { as := PUnit.unit }
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExistsAt.integrable : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : Sub G] {x : G},
  MeasureTheory.ConvolutionExistsAt f g x L μ → MeasureTheory.Integrable (fun t => (L (f t)) (g (x - t))) μ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.exists_real_pos_lt_infEDist_of_notMem_closure`. -/
EMetric.exists_real_pos_lt_infEdist_of_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α},
  x ∉ closure E → ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < Metric.infEDist x E
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  k ∈ m₂ → Std.ExtDHashMap.Const.get! (m₁ ∩ m₂) k = Std.ExtDHashMap.Const.get! m₁ k
-- Mathlib.Order.Atoms
/-- Every element is a `sInf` of a set of coatoms.  -/
IsCoatomistic.isGLB_coatoms : ∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderTop α} [self : IsCoatomistic α] (b : α),
  ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork f} (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Mono f],
  CategoryTheory.Limits.IsZero c.pt
-- Init.Data.List.Monadic
List.mapM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {l₁ l₂ : List α},
  List.mapM f (l₁ ++ l₂) = do
    let __do_lift ← List.mapM f l₁
    let __do_lift_1 ← List.mapM f l₂
    pure (__do_lift ++ __do_lift_1)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeriesAux.eq_1 : ∀ (G : Type u_2) [inst : AddGroup G], AddSubgroup.upperCentralSeriesAux G 0 = ⟨⊥, ⋯⟩
-- Mathlib.NumberTheory.SumTwoSquares
/-- A (positive) natural number `n` is a sum of two squares if and only if the exponent of
every prime `q` such that `q % 4 = 3` in the prime factorization of `n` is even.
(The assumption `0 < n` is not present, since for `n = 0`, both sides are satisfied;
the right-hand side holds, since `padicValNat q 0 = 0` by definition.)  -/
Nat.eq_sq_add_sq_iff : ∀ {n : ℕ}, (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instCommRingObjForgetRingHomCarrier : {R : CommRingCat} → CommRing ((CategoryTheory.forget CommRingCat).obj R)
-- Lean.Expr
Lean.Expr.fvarId! : Lean.Expr → Lean.FVarId
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromSource Q], P.op.InheritedFromTarget Q.op
-- Init.Data.Vector.Lemmas
Vector.toList_setIfInBounds : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α}, (xs.setIfInBounds i x).toList = xs.toList.set i x
-- Init.Data.UInt.Bitwise
USize.toUInt8_shiftLeft : ∀ (a b : USize), b < 8 → (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (cons a s ha)` for all `s`
and `a ∉ s`.  -/
Finset.monotone_iff_forall_le_cons : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
  Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (Finset.cons a s ha)
-- Init.SizeOf
Lean.ParserDescr.cat.sizeOf_spec : ∀ (catName : Lean.Name) (rbp : ℕ), sizeOf (Lean.ParserDescr.cat catName rbp) = 1 + sizeOf catName + sizeOf rbp
-- Mathlib.Algebra.Order.Hom.Basic
RingNormClass.toAddGroupNormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonUnitalNonAssocRing α]
  [inst_1 : Semiring β] [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [self : RingNormClass F α β],
  AddGroupNormClass F α β
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.getD_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (a b : R),
  W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.of_append_right : ∀ {left right : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (left ++ right) → Tactic.ComputeAsymptotics.WellFormedBasis right
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.completion_coe : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f)
  (a : α), (f.completion hf) ↑a = ↑(f a)
-- Mathlib.GroupTheory.Exponent
Submonoid.pow_exponent_eq_one : ∀ {G : Type u} [inst : Monoid G] {S : Submonoid G} {g : G}, g ∈ S → g ^ Monoid.exponent ↥S = 1
-- Mathlib.Algebra.Group.Basic
div_mul_div_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a / b * (c / d) = a * c / (b * d)
-- Mathlib.Data.Set.Sups
Set.infs_left_comm : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t u : Set α), s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_pow_comp_lieHom : ∀ {R : Type u} {L : Type v} {M : Type w} [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] {M₂ : Type w₁}
  [inst_7 : AddCommGroup M₂] [inst_8 : Module R M₂] [inst_9 : LieRingModule L M₂] [inst_10 : LieModule R L M₂]
  (f : M →ₗ⁅R,L⁆ M₂) (k : ℕ) (x : L), ((LieModule.toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (LieModule.toEnd R L M) x ^ k
-- Mathlib.Control.Fold
Monoid.foldrM.get.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α : Type u} (x : Monoid.foldrM m α), x.get = x
-- Std.Do.SPred.Notation
/-- Tautology in `SPred`; sugar for `SPred.entails ⌜True⌝`.  -/
Std.Do.«term⊢ₛ_» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.pop : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (k : K) → (σ → Option (Γ k) → σ) → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.tendsto_div_nhds_zero : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
  f =o[l] g → Filter.Tendsto (fun x => f x / g x) l (nhds 0)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The inclusion of `H¹(L_{S/R})` into the conormal space of a presentation.  -/
Algebra.Extension.h1Cotangentι : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → P.H1Cotangent →ₗ[S] P.Cotangent
-- Mathlib.Analysis.Normed.Module.Convex
/-- The norm on a real normed space is convex on the whole space. See also `Seminorm.convexOn`
and `convexOn_norm`.  -/
convexOn_univ_norm : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ConvexOn ℝ Set.univ norm
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.mk.inj : ∀ {A : Type uA} {B : A → Type uB} {A_1 : Type uA} {B_1 : A_1 → Type uB},
  { A := A, B := B } = { A := A_1, B := B_1 } → A = A_1 ∧ B ≍ B_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_toArray_rio : ∀ {n : ℕ}, (*...=n).toArray = (*...n + 1).toArray
-- Lean.Elab.Level
Lean.Elab.Level.State.mk.sizeOf_spec : ∀ (ngen : Lean.NameGenerator) (mctx : Lean.MetavarContext) (levelNames : List Lean.Name),
  sizeOf { ngen := ngen, mctx := mctx, levelNames := levelNames } = 1 + sizeOf ngen + sizeOf mctx + sizeOf levelNames
-- Init.Prelude
instInhabitedBool : Inhabited Bool
-- Mathlib.Data.Sigma.Basic
PSigma.forall : ∀ {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) ×' β a → Prop},
  (∀ (x : (a : α) ×' β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Given two refinement morphism `f, g : E ⟶ F`, this is a `1`-hypercover `W` that
admits a morphism `h : W ⟶ E` such that `h ≫ f` and `h ≫ g` are homotopic. Hence
they become equal after quotienting out by homotopy.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.cylinder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} →
        {E : J.OneHypercover S} →
          {F : J.OneHypercover S} → [CategoryTheory.Limits.HasPullbacks C] → E.Hom F → E.Hom F → J.OneHypercover S
-- Mathlib.Analysis.Normed.Group.Defs
ENorm.mk : {E : Type u_8} → (E → ENNReal) → ENorm E
-- Lean.Message
/-- Structured result status of a trace node action, produced by `withTraceNode` and
`withTraceNodeBefore` and included in the `TraceData` of trace messages. Either
`.success` (✅️), `.failure` (❌️), or `.error` (💥️).

This is used both to render emojis in trace messages and to allow more
robust inspection of trace logs via metaprogramming.

See also `Except.toTraceResult` for converting an `Except ε α` to a `TraceResult`.  -/
Lean.TraceResult : Type
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.typelessBinder? : Lean.Syntax → Option (Array (Lean.TSyntax [`ident, `Lean.Parser.Term.hole]) × Lean.BinderInfo)
-- Init.System.IOError
/-- No such file or directory.

This corresponds to the POSIX error `ENOENT`.
 -/
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
-- Mathlib.Data.Holor
_private.Mathlib.Data.Holor.0.HolorIndex.take.match_1.splitter : {ds₂ : List ℕ} →
  (motive : (x : List ℕ) → HolorIndex (x ++ ds₂) → Sort u_1) →
    (x : List ℕ) →
      (x_1 : HolorIndex (x ++ ds₂)) → ((ds : List ℕ) → (is : HolorIndex (ds ++ ds₂)) → motive ds is) → motive x x_1
-- Mathlib.Analysis.Convex.Between
Sbtw.wbtw : ∀ {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] {x y z : P}, Sbtw R x y z → Wbtw R x y z
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.leftUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : CategoryTheory.Center C) → CategoryTheory.Center.tensorUnit.tensorObj X ≅ X
-- Batteries.Data.List.Perm
List.Subperm.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁.length ≤ l₂.length
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {ι : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              (toAlgHom : A →ₐ[R] B) →
                                (∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom.toRingHom x ∈ ℬ i) → 𝒜 →ₐᵍ[R] ℬ
-- Mathlib.Algebra.Quandle
/-- The preliminary definition of the induced map from the enveloping group.
See `toEnvelGroup.map`.
 -/
Rack.toEnvelGroup.mapAux : {R : Type u_1} →
  [inst : Rack R] → {G : Type u_2} → [inst_1 : Group G] → ShelfHom R (Quandle.Conj G) → Rack.PreEnvelGroup R → G
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.sigmaToPi_injective : ∀ {ι : Type u_3} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)],
  Function.Injective (PrimeSpectrum.sigmaToPi R)
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle_C_eq_smul_fourier_zero : ∀ {c : ℂ}, Polynomial.toAddCircle (Polynomial.C c) = c • fourier 0
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasZeroObject D
-- Mathlib.Topology.Algebra.Group.Pointwise
IsDiscrete.exists_nhds_eq_zero_of_image_addRight_inter_nonempty : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  IsDiscrete ↑S → ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => x + g) '' U ∩ U).Nonempty → g = 0
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.HasMap.map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] {P : StandardEtalePair R} {x : S},
  P.HasMap x → ∀ (f : S →ₐ[R] T), P.HasMap (f x)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_eq_of_preservesColimit_coyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} [CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone D} (hc : CategoryTheory.Limits.IsColimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D (CategoryTheory.coyoneda.obj (Opposite.op X))] {i j : J} (f : X ⟶ D.obj i)
  (g : X ⟶ D.obj j),
  CategoryTheory.CategoryStruct.comp f (c.ι.app i) = CategoryTheory.CategoryStruct.comp g (c.ι.app j) →
    ∃ k u v, CategoryTheory.CategoryStruct.comp f (D.map u) = CategoryTheory.CategoryStruct.comp g (D.map v)
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.instToMessageData : Lean.ToMessageData Aesop.ElabRuleTerm
-- Mathlib.Data.Sym.Sym2
Set.sym2_eq_mk_image : ∀ {α : Type u_1} {s : Set α}, s.sym2 = Function.uncurry Sym2.mk '' s ×ˢ s
-- Mathlib.Tactic.Linarith.Parsing
Mathlib.Tactic.Linarith.instOrdMonom : Ord Mathlib.Tactic.Linarith.Monom
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.homogeneousComponent_of_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {p : ℕ},
  ↑p = f.order → (MvPowerSeries.homogeneousComponent p) f ≠ 0
-- Mathlib.Data.Set.Basic
Set.subset_of_mem_powerset : ∀ {α : Type u} {x s : Set α}, x ∈ 𝒫 s → x ⊆ s
-- Lean.Message
Lean.instBEqTraceResult.beq : Lean.TraceResult → Lean.TraceResult → Bool
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fb : γ) → motive (some fb)),
  (match none with
    | none => h_1 ()
    | some fb => h_2 fb) =
    h_1 ()
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (V : CategoryTheory.Endofunctor.Coalgebra F) → Inhabited (V.Hom V)
-- Mathlib.Data.Nat.Cast.Defs
AddMonoidWithOne.toNatCast : {R : Type u_2} → [self : AddMonoidWithOne R] → NatCast R