mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S.eq_4 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.S R (Int.negSucc n) =
    Polynomial.X * Polynomial.Chebyshev.S R (-↑n) - Polynomial.Chebyshev.S R (-↑n + 1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mk : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              (asHomogeneousIdeal : HomogeneousIdeal 𝒜) →
                asHomogeneousIdeal.toIdeal.IsPrime →
                  ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal → ProjectiveSpectrum 𝒜
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.zsmul.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (n : ℤ) (q : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.zsmul n q =
    Quot.liftOn q
      (fun x =>
        match x with
        | (a, b) =>
          if n < 0 then Lean.Grind.IntModule.OfNatModule.Q.mk (n.natAbs • b, n.natAbs • a)
          else Lean.Grind.IntModule.OfNatModule.Q.mk (n.natAbs • a, n.natAbs • b))
      ⋯
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom : ∀ (Y : Type u_1) (X : Type u_2) [inst : TopologicalSpace Y],
  (CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap Y X).hom = TypeCat.ofHom fun f => ↑f
-- Mathlib.Algebra.Lie.Basic
/-- A morphism of Lie algebras (denoted as `L₁ →ₗ⁅R⁆ L₂`)
is a linear map respecting the bracket operations.  -/
«term_→ₗ⁅_⁆_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.mk_add_of_mem : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {b : α} (a : α), b ∈ s → ↑(a + b) = ↑a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {i : ι}, (∀ (ω : Ω), τ ω ≤ ↑i) → hτ.measurableSpace ≤ ↑f i
-- Mathlib.Algebra.Order.Hom.Monoid
monotone_iff_map_nonneg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], Monotone ⇑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ f a
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsCompleteMultipartite.induce : ∀ {α : Type u} {G : SimpleGraph α} {s : Set α},
  G.IsCompleteMultipartite → (SimpleGraph.induce s G).IsCompleteMultipartite
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCodetector (Opposite.op G) ↔ CategoryTheory.IsDetector G
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.hasColimits : CategoryTheory.Limits.HasColimits Profinite
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_inf_mul_relfinrank : ∀ {E : Type v} [inst : Field E] (A B C : Subfield E), A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- A single step in encoding an `Expr` into `Key`s.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodingStepWithEta : Lean.Expr →
  Bool →
    Lean.Meta.RefinedDiscrTree.LazyEntry →
      ReaderT Lean.Meta.RefinedDiscrTree.Context✝ Lean.MetaM
        (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))
-- Mathlib.Logic.Basic
/-- **Alias** of `forall_comm`. -/
forall_swap : ∀ {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop}, (∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_leftUnitor_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X))
-- Lean.Meta.LazyDiscrTree
/-- Specialization of Lean.Meta.DiscrTree.pushArgs
 -/
Lean.Meta.LazyDiscrTree.pushArgs : Bool → Array Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.Key × Array Lean.Expr)
-- Mathlib.RingTheory.IntegralDomain
/-- In an integral domain, a sum indexed by a homomorphism from a finite group is zero,
unless the homomorphism is trivial, in which case the sum is equal to the cardinality of the group.
 -/
sum_hom_units : ∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Group G] [inst_3 : Fintype G] (f : G →* R)
  [inst_4 : Decidable (f = 1)], ∑ g, f g = ↑(if f = 1 then Fintype.card G else 0)
-- Mathlib.Order.BoundedOrder.Basic
isMax_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α], IsMax ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_star : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfcₙ (fun x => star (f x)) a = star (cfcₙ f a)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_isColimit₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).isColimit₂ = c.isColimit₂.whiskerEquivalence (CategoryTheory.Discrete.equivalence e)
-- Std.Time.Format.Modifier
Std.Time.Modifier.N.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.N presentation = Std.Time.Modifier.N presentation_1 → presentation = presentation_1
-- Init.Data.UInt.Lemmas
USize.ofBitVec_uInt8ToBitVec : ∀ (n : UInt8), { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize
-- Mathlib.GroupTheory.Nilpotent
Subgroup.is_descending_rev_series_of_is_ascending : ∀ (G : Type u_1) [inst : Group G] {H : ℕ → Subgroup G} {n : ℕ},
  H n = ⊤ → Subgroup.IsAscendingCentralSeries H → Subgroup.IsDescendingCentralSeries fun m => H (n - m)
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_functor_obj_unop_X : ∀ (R : Type u) [inst : CommRing R] (A : CommHopfAlgCat R),
  (Opposite.unop ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)
-- Mathlib.Data.Nat.Nth
Nat.count_nth_succ : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ},
  (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → Nat.count p (Nat.nth p n + 1) = n + 1
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.naive_relation_apply : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
  (i : ι), (Algebra.Presentation.naive s hs).relation i = v i
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
IsConjRoot.instIsEquiv : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A], IsEquiv A (IsConjRoot R)
-- Mathlib.Topology.SeparatedMap
IsLocallyInjective.comp_right : ∀ {X : Type u_1} {Y : Type u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y},
  IsLocallyInjective f → ∀ {g : A → X}, Continuous g → Function.Injective g → IsLocallyInjective (f ∘ g)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_smulRight : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G), ‖f.smulRight z‖ = ‖f‖ * ‖z‖
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instRing : {𝕜₁ : Type u_1} →
  [inst : NormedField 𝕜₁] →
    {E : Type u_3} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] → [inst_3 : Module 𝕜₁ E] → [IsTopologicalAddGroup E] → Ring (E →WOT[𝕜₁] E)
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_empty : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (f : ι → M),
  (∅.expect fun i => f i) = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsBridge.not_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.IsBridge s(u, v) → ¬G.IsEdgeReachable 2 u v
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.union : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s t : Set ι} {f : ι → α},
  s.PairwiseDisjoint f →
    t.PairwiseDisjoint f →
      (∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)) → (s ∪ t).PairwiseDisjoint f
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
/-- A property of objects `P` is inherited from the source of morphisms satisfying `Q` if
whenever `P` holds for `X` and `f : X ⟶ Y` is a `Q`-morphism, then `P` holds for `Y`.  -/
CategoryTheory.ObjectProperty.InheritedFromSource : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_toPartialMap : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y ⟶ Z),
  f.comp (AlgebraicGeometry.Scheme.Hom.toPartialMap g) = f.compHom g
-- Init.Data.Array.Nat
Array.min_le_sum_div_length_nat : ∀ {xs : Array ℕ} (h : xs ≠ #[]), xs.min h ≤ xs.sum / xs.size
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSetMap_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))))
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)),
  ↑(NumberField.mixedEmbedding.fundamentalCone.idealSetMap K J a) = ↑a
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  K.extendHomologyIso e hj' = K.extendHomologyIso e hj'
-- Init.Data.SInt.Lemmas
Int64.eq_iff_toBitVec_eq : ∀ {a b : Int64}, a = b ↔ a.toBitVec = b.toBitVec
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`.  -/
le_mul_inv_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, b ≤ 0 → b ≤ a * (a⁻¹ * b)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_smul_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq β] [inst_1 : DecidableEq γ] [inst_2 : SMul α β]
  [inst_3 : SMul α γ] (f : β → γ) (a : α) (s : Finset β),
  (∀ (b : β), f (a • b) = a • f b) → Finset.image f (a • s) = a • Finset.image f s
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_emod_self_left : ∀ (a b c : ℤ), (a - b * c) % b = a % b
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.trans_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) {Z : C}
  (h' : CategoryTheory.Retract Y Z), (h.trans h').r = CategoryTheory.CategoryStruct.comp h'.r h.r
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.fderiv_right_succ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x₀ : E}
  {n : WithTop ℕ∞}, ContDiffAt 𝕜 (n + 1) f x₀ → ContDiffAt 𝕜 n (fderiv 𝕜 f) x₀
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_pos : ∀ {a b : ℤ}, 0 < a → 0 < b → 0 ≤ a / b
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvOneClass : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : InvOneClass G] → [ContinuousInv G] → InvOneClass (SeparationQuotient G)
-- Mathlib.GroupTheory.Torsion
/-- Quotienting an additive group by its torsion additive subgroup yields a torsion-free additive
group.  -/
QuotientAddGroup.instIsAddTorsionFree : ∀ (G : Type u_1) [inst : AddCommGroup G], IsAddTorsionFree (G ⧸ AddCommGroup.torsion G)
-- Mathlib.Analysis.RCLike.Inner
/-- Discrete inner product giving rise to the discrete L2 norm.  -/
RCLike.«term⟪_,_⟫_[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  {s : UpperSet (MulArchimedeanClass M)},
  s ≠ ⊤ → ↑(MulArchimedeanClass.subsemigroup s) = ↑(MulArchimedeanClass.subgroup s)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F'),
  (F'.isColimitCoconeOfIsLeftKanExtension α hc).desc s =
    hc.desc { pt := s.1, ι := CategoryTheory.CategoryStruct.comp α (L.whiskerLeft s.ι) }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.getKey! (t.minKey he) = t.minKey he
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property of a function in a charted space, by requiring that it holds
in the preferred chart around every point.  -/
ChartedSpace.LiftProp : {H : Type u_1} →
  {M : Type u_2} →
    {H' : Type u_3} →
      {M' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [ChartedSpace H M] →
              [inst : TopologicalSpace H'] →
                [inst_2 : TopologicalSpace M'] → [ChartedSpace H' M'] → ((H → H') → Set H → H → Prop) → (M → M') → Prop
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `normalize`.  -/
CategoryTheory.FreeMonoidalCategory.normalizeObj : {C : Type u} →
  CategoryTheory.FreeMonoidalCategory C →
    CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C →
      CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C
-- Init.Data.SInt.Lemmas
Int64.neg_mul_neg : ∀ (a b : Int64), -a * -b = a * b
-- Init.Data.Order.PackageFactories
Std.instDecidableLE : {α : Type u_1} → [inst : Std.PreorderPackage α] → DecidableLE α
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,
any `S`-morphism `Spec K(X) ⟶ Y` spreads out to a rational map from `X` to `Y`.
 -/
AlgebraicGeometry.Scheme.RationalMap.ofFunctionField : {X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [inst : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          (f : AlgebraicGeometry.Spec X.functionField ⟶ Y) →
            CategoryTheory.CategoryStruct.comp f sY =
                CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) sX →
              X.RationalMap Y
-- Mathlib.Logic.Embedding.Set
/-- Given an embedding `f : α ↪ β` and a point outside of `Set.range f`, construct an embedding
`Option α ↪ β`.  -/
Function.Embedding.optionElim : {α : Type u_1} → {β : Type u_2} → (f : α ↪ β) → (x : β) → x ∉ Set.range ⇑f → Option α ↪ β
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The geometric sequence `fun n ↦ φ^n` is a solution of `fibRec`.  -/
Real.geom_goldenRatio_isSol_fibRec : Real.fibRec.IsSolution fun x => Real.goldenRatio ^ x
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.ext_iff : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] {f g : StieltjesFunction R},
  f = g ↔ ∀ (x : R), ↑f x = ↑g x
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_eq_self : ∀ {α : Type u_1} [inst : LinearOrder α] {a x : α}, Set.projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instBEqAuxLemmaKey : BEq Lean.Meta.AuxLemmaKey
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getOne : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_3.eq_1 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1)
  (h_1 : Unit → motive Lean.Meta.Grind.SolverTerms.nil Lean.Meta.Grind.SolverTerms.nil)
  (h_2 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive Lean.Meta.Grind.SolverTerms.nil (Lean.Meta.Grind.SolverTerms.next solverId e rest))
  (h_3 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive (Lean.Meta.Grind.SolverTerms.next solverId e rest) Lean.Meta.Grind.SolverTerms.nil)
  (h_4 :
    (id₁ : ℕ) →
      (rhs : Lean.Expr) →
        (rhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (lhs : Lean.Expr) →
              (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil with
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil => h_1 ()
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest => h_2 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil => h_3 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms =>
      h_4 id₁ rhs rhsTerms id₂ lhs lhsTerms) =
    h_1 ()
-- Mathlib.Algebra.Group.Conj
/-- Given an additive conjugacy class `a`, `carrier a` is the set it represents.  -/
AddConjClasses.carrier : {α : Type u} → [inst : AddMonoid α] → AddConjClasses α → Set α
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.mk.inj : ∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}} {W : CategoryTheory.MorphismProperty J}
  {P : CategoryTheory.ObjectProperty J} {src : ∀ {i j : J} {f : i ⟶ j}, W f → P i}
  {tgt : ∀ {i j : J} {f : i ⟶ j}, W f → P j} {hW : W.HasCardinalLT κ} {hP : P.HasCardinalLT κ}
  {W_1 : CategoryTheory.MorphismProperty J} {P_1 : CategoryTheory.ObjectProperty J}
  {src_1 : ∀ {i j : J} {f : i ⟶ j}, W_1 f → P_1 i} {tgt_1 : ∀ {i j : J} {f : i ⟶ j}, W_1 f → P_1 j}
  {hW_1 : W_1.HasCardinalLT κ} {hP_1 : P_1.HasCardinalLT κ},
  { W := W, P := P, src := src, tgt := tgt, hW := hW, hP := hP } =
      { W := W_1, P := P_1, src := src_1, tgt := tgt_1, hW := hW_1, hP := hP_1 } →
    W = W_1 ∧ P = P_1
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.normFn : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_sup_left : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} {x : M}, x ∈ N → x ∈ N ⊔ N'
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.isTorsionFree : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), Module.IsTorsionFree R M
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_subset_Iic : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], Finset.Iic a ⊆ Finset.Iic b ↔ a ≤ b
-- Lean.ProjFns
Lean.Environment.isProjectionFn : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ G) [inst_1 : ∀ (X : C), (α.app X).toFunctor.Final]
  (H : CategoryTheory.Functor (CategoryTheory.Grothendieck G) (Type u₂)),
  CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence α H =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Limits.HasColimit.isoOfNatIso
            (((CategoryTheory.Grothendieck.ι F X).associator (CategoryTheory.Grothendieck.map α) H).symm ≪≫
              CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Grothendieck.ιCompMap α X) H ≪≫
                (α.app X).toFunctor.associator (CategoryTheory.Grothendieck.ι G X) H) ≪≫
          CategoryTheory.Functor.Final.colimitIso (α.app X).toFunctor ((CategoryTheory.Grothendieck.ι G X).comp H))
      ⋯
-- Mathlib.Algebra.Tropical.BigOperators
trop_iInf : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : Fintype S] (f : S → WithTop R),
  Tropical.trop (⨅ i, f i) = ∑ i, Tropical.trop (f i)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.symm.symm = e
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.opFunctor_comp_unopFunctor_eq : CategoryTheory.RelCat.opFunctor.comp CategoryTheory.RelCat.unopFunctor = CategoryTheory.Functor.id CategoryTheory.RelCat
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_top : ∀ {α : Type u_1} [Nontrivial α], ⊤.radius = 1
-- Mathlib.Data.Sigma.Order
/-- The lexicographical linear order on a sigma type.  -/
Sigma.Lex.orderTop : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : OrderTop ι] → [inst_2 : (i : ι) → Preorder (α i)] → [OrderTop (α ⊤)] → OrderTop (Σₗ (i : ι), α i)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), Disjoint I (hC.disjointOfDiffUnion hs hI)