mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Quandle
Rack.self_act_eq_iff_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Shelf.act x x = Shelf.act y y ↔ x = y
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_right_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
  normalize b = b → (gcd a b = b ↔ b ∣ a)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Construct the term with type hint `(Eq.refl a : a = b)` -/
Lean.Elab.Tactic.Omega.mkEqReflWithExpectedType : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_le_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α}, a ≤ b → -a ≤ b → |a| ≤ |b|
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W.addX P Q = WeierstrassCurve.Jacobian.addU P Q ^ 2
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk'_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R}
  (ha : ↑sa = s), (Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpParams : Lean.ToJson Lean.Lsp.SignatureHelpParams
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.vaddConst_symm_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p p' : P),
  (Homeomorph.vaddConst p).symm p' = p' -ᵥ p
-- Init.Data.Bool
Bool.not_beq_self : ∀ (x : Bool), ((!x) == x) = false
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.someOctahedron.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  [inst_6 : CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (h₁₃ :
    CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  CategoryTheory.Triangulated.someOctahedron comm h₁₂ h₂₃ h₁₃ =
    CategoryTheory.Triangulated.someOctahedron comm h₁₂ h₂₃ h₁₃
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Norm α] [inst_1 : Norm β] (f : WithLp ⊤ (α × β)), ‖f‖ = max ‖f.fst‖ ‖f.snd‖
-- Init.System.IO
IO.FS.Mode.writeNew.sizeOf_spec : sizeOf IO.FS.Mode.writeNew = 1
-- Init.Data.String.Defs
String.instDecidableLePos_1 : {s : String.Slice} → (l r : s.Pos) → Decidable (l ≤ r)
-- Mathlib.Data.Set.Lattice
Set.sInter_eq_iInter : ∀ {α : Type u_1} {s : Set (Set α)}, ⋂₀ s = ⋂ i, ↑i
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_nonneg_of_nonpos_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a / b
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.instIsOpenImmersionHomOfLE : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U ≤ V), AlgebraicGeometry.IsOpenImmersion (X.homOfLE e)
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Submodule.eq_iSup_inf_genEigenspace : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
  {f : Module.End K V} [FiniteDimensional K V] (k : ℕ∞),
  (∀ x ∈ p, f x ∈ p) → ⨆ μ, (f.genEigenspace μ) k = ⊤ → p = ⨆ μ, p ⊓ (f.genEigenspace μ) k
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.hasTypeMsg : Lean.Expr → Lean.Expr → Lean.MessageData
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → ((out' : γ) → motive (some out')) → (Unit → motive none) → motive __do_lift
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom
        h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app j) h
-- Mathlib.Order.PartialSups
/-- `partialSups` forms a Galois insertion with the coercion from monotone functions to functions.
 -/
partialSups.gi : {α : Type u_1} →
  {ι : Type u_3} →
    [inst : SemilatticeSup α] →
      [inst_1 : Preorder ι] → [inst_2 : LocallyFiniteOrderBot ι] → GaloisInsertion partialSups DFunLike.coe
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMap_prodSnd : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  {p : TangentBundle (I.prod I') (M × M')}, tangentMap (I.prod I') I' Prod.snd p = ⟨p.proj.2, p.snd.2⟩
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isIso_iff₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0} (f : F ⟶ G),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (f.app 0)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α), Filter.limsup f ⊥ = ⊥
-- Init.Data.SInt.Lemmas
Int32.toFin_toBitVec : ∀ (x : Int32), x.toBitVec.toFin = x.toUInt32.toFin
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termδ : Lean.ParserDescr
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {g : γ → α} {c : γ},
  UpperSemicontinuousAt f (g c) → ContinuousAt g c → UpperSemicontinuousAt (f ∘ g) c
-- Init.Data.UInt.Basic
instDivUInt64 : Div UInt64
-- Init.Data.SInt.Bitwise
Int64.zero_xor : ∀ {a : Int64}, 0 ^^^ a = a
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Init.Control.Basic
«term_<||>_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_π_subtype : ∀ {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]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.Limits.biproduct.π f ↑j) =
    CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j
-- Init.Sym.Simp.SimprocDSL
/-- Pre-processing simproc chain.  -/
Lean.Parser.Command.symSimpFieldPre : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given functors `F : C ⥤ D` and `G : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ (Dᵒᵖ ⥤ Type max w v₁ v₂)`,
and a natural transformation `φ : F ⋙ uliftYoneda ⟶ uliftYoneda ⋙ G`, this is
the canonical natural transformation `F.op.lan ⟶ G`, which is part of the
fact that `F.op.lan : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂`
is the left Kan extension of `F ⋙ uliftYoneda : C ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂`
along `uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂`.  -/
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G :
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
                (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))} →
            (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶
                CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G) →
              [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] →
                F.op.lan ⟶ G
-- Lean.DocString.Types
Lean.Doc.instOrdInline : {i : Type u_1} → [Ord i] → Ord (Lean.Doc.Inline i)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.proofs.withType : Lean.Option Bool
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_simpleFunc_eq_setToSimpleFunc : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) μ → MeasureTheory.setToFun μ T hT ⇑f = MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.tensor_smul_left : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (a : A) (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π), (a • f).tensor g = a • f.tensor g
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → ∀ (c : F), HasFDerivAtFilter (fun x => c - f x) (-f') L
-- Mathlib.AlgebraicGeometry.Noetherian
/-- If `𝒰` is an open cover of a scheme `X`, then `X` is locally Noetherian if and only if
`𝒰.X i` are all locally Noetherian.  -/
AlgebraicGeometry.isLocallyNoetherian_iff_openCover : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsLocallyNoetherian (𝒰.X i)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd_zero : ∀ (a : ℤ), a.gcd 0 = a.natAbs
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split'.eq_1 : ONote.zero.split' = (0, 0)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- A category has all finite colimits if every functor `J ⥤ C` with a `FinCategory J`
instance and `J : Type` has a colimit.

This is often called 'finitely cocomplete'.
 -/
CategoryTheory.Limits.HasFiniteColimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItemTag : Inhabited Lean.Lsp.CompletionItemTag
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv₂.measurable_div : ∀ {G₀ : Type u_2} {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv₂ G₀],
  Measurable fun p => p.1 / p.2
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors`. -/
idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J),
  J ≠ ⊥ →
    ∀ {L : Ideal R} (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I),
      ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofBitVec : ∀ (b : BitVec 32), { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (p p_1 : G.Walk v w) (e_p : p = p_1) (u : V)
  (a : u ∈ p.support), p.takeUntil u a = p_1.takeUntil u ⋯
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_map_eval : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] (x : ι → R),
  Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) =
    LinearMap.charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- Let `Q` be a property of ring maps that implies `Q'` on stalks.
Then if the associated property of scheme morphisms holds for `f`, `Q'` holds on all stalks.  -/
AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  {Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q') →
    (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
        Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      P f → ∀ (x : ↥X), Q' (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.var : Lean.IR.VarId → Lean.IR.Arg
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compRightAlgHom_continuous : ∀ (R : Type u_2) [inst : CommSemiring R] (A : Type u_3) [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsTopologicalSemiring A] {α : Type u_5} {β : Type u_6} [inst_5 : TopologicalSpace α]
  [inst_6 : TopologicalSpace β] (f : C(α, β)), Continuous ⇑(ContinuousMap.compRightAlgHom R A f)
-- Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
/-- In a GCD domain, an integral ideal that is invertible as a fractional ideal is principal.

Public API note: see `ClassGroup.isPrincipal_of_isUnit_coeIdeal`.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup.0.IsGCDMonoid.isPrincipal_of_isUnit_fractionalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsGCDMonoid R] (I : Ideal R), IsUnit ↑I → Submodule.IsPrincipal I
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- If `J : CardinalFilteredPoset κ` and `κ'` is any regular cardinal,
this is a colimit cocone which exhibits `J.withTop` as the `κ'`-filtered
colimit of its subsets that are of cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalDirectedPoset.coconeWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      (κ' : Cardinal.{u}) →
        [inst_1 : Fact κ'.IsRegular] →
          CategoryTheory.Limits.Cocone
            (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet (J.PropSetWithTop κ'))
-- Init.Core
/-- The relation `x ≈ y` is an equivalence relation.  -/
Setoid.iseqv : ∀ {α : Sort u} [self : Setoid α], Equivalence ⇑self
-- Mathlib.MeasureTheory.Function.EssSup
essSup_mono_measure' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β},
  ν ≤ μ →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae ν) f) essSup_mono_measure'._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) essSup_mono_measure'._auto_3 →
        essSup f ν ≤ essSup f μ
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.mk.sizeOf_spec : ∀ (pendingProducer : Option Std.Http.Body.Channel.Producer✝) (pendingConsumer : Option Std.Http.Body.Channel.Consumer✝)
  (interestWaiter : Option (Std.Async.Waiter Bool)) (closed : Bool) (knownSize : Option Std.Http.Body.Length)
  (pendingIncompleteChunk : Option Std.Http.Chunk),
  sizeOf
      { pendingProducer := pendingProducer, pendingConsumer := pendingConsumer, interestWaiter := interestWaiter,
        closed := closed, knownSize := knownSize, pendingIncompleteChunk := pendingIncompleteChunk } =
    1 + sizeOf pendingProducer + sizeOf pendingConsumer + sizeOf interestWaiter + sizeOf closed + sizeOf knownSize +
      sizeOf pendingIncompleteChunk
-- Mathlib.RingTheory.AdicCompletion.Basic
Hausdorffification.instIsHausdorff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff I (Hausdorffification I M)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t.op : Cone F.op` is a limit cone, then `t : Cocone F` is a colimit cocone.  -/
CategoryTheory.Limits.isColimitOfOp : {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} → CategoryTheory.Limits.IsLimit t.op → CategoryTheory.Limits.IsColimit t
-- Init.Data.Array.Lemmas
Array.shrink_eq_take : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.shrink i = xs.take i
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Eta-expanded form of `OmegaCompletePartialOrder.ωScottContinuous.id` -/
OmegaCompletePartialOrder.ωScottContinuous.fun_id : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α], OmegaCompletePartialOrder.ωScottContinuous fun x => x
-- Mathlib.Order.PFilter
Order.PFilter.principal_le_principal_iff : ∀ {P : Type u_1} [inst : Preorder P] {p q : P}, Order.PFilter.principal q ≤ Order.PFilter.principal p ↔ p ≤ q
-- Mathlib.Data.EReal.Inv
EReal.sign_mul_inv_abs : ∀ (a : EReal), ↑(SignType.sign a) * (↑a.abs)⁻¹ = a⁻¹
-- Lean.Elab.Tactic.Omega.Core
/-- Equations that have already been used to eliminate variables,
along with the variable which was removed, and its coefficient (either `1` or `-1`).
The earlier elements are more recent,
so if these are being reapplied it is essential to use `List.foldr`.
 -/
Lean.Elab.Tactic.Omega.Problem.eliminations : Lean.Elab.Tactic.Omega.Problem → List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.mk.injEq : ∀ (finset : BigOperators.FinsetResult✝) (filter : Option Lean.Term) (finset_1 : BigOperators.FinsetResult✝)
  (filter_1 : Option Lean.Term),
  ({ finset := finset, filter := filter } = { finset := finset_1, filter := filter_1 }) =
    (finset = finset_1 ∧ filter = filter_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The functor that takes a 2-truncated simplicial set to its homotopy category.  -/
SSet.Truncated.hoFunctor₂ : CategoryTheory.Functor (SSet.Truncated 2) CategoryTheory.Cat
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The projection onto the second summand of a binary biproduct.  -/
CategoryTheory.Limits.biprod.snd : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⊞ Y ⟶ Y
-- Mathlib.GroupTheory.GroupAction.Basic
IsCancelSMul.stabilizer_eq_bot : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [IsCancelSMul G α] (a : α),
  MulAction.stabilizer G a = ⊥
-- Mathlib.Analysis.Normed.Group.Int
Int.instNormedAddCommGroup : NormedAddCommGroup ℤ
-- Mathlib.Tactic.Says
/-- Run `evalTactic`, capturing a "Try this:" message and converting it back to syntax.
 -/
Mathlib.Tactic.Says.evalTacticCapturingTryThis : Lean.TSyntax `tactic → Lean.Elab.Tactic.TacticM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.subgroupMap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G') (H : Subgroup G),
  e.subgroupMap H = e.submonoidMap H.toSubmonoid
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : Add α],
  Function.Periodic f c → ∀ (g : β → γ), Function.Periodic (g ∘ f) c
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of the reverse direction of `measurableSet_inr_image`. -/
MeasurableSet.inr_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β},
  MeasurableSet s → MeasurableSet (Sum.inr '' s)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → s.incenter = s_1.incenter