mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPushoutsAlongOfHasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.HasPushouts]
  {X Y : C} {f : X ⟶ Y}, P.HasPushoutsAlong f
-- Lean.Language.Basic
Lean.Language.ProcessingContext.toInputContext : Lean.Language.ProcessingContext → Lean.Parser.InputContext
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.toMonoidWithZeroHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
  ⇑f.toMonoidWithZeroHom = ⇑f
-- Mathlib.FieldTheory.Minpoly.Basic
/-- An element is a root of its minimal polynomial.  -/
minpoly.aeval : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
  (Polynomial.aeval x) (minpoly A x) = 0
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is strictly convex, then for any three points `x < y < z` the slope of the
secant line of `f` on `[x, y]` is strictly less than the slope of the secant line of `f` on
`[y, z]`.  -/
StrictConvexOn.slope_strict_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)],
  (E.pullbackCoverOfLeft f g).toPreZeroHypercover = E.pullbackCoverOfLeft f g
-- Mathlib.Analysis.Normed.Algebra.Exponential
Prod.fst_exp : ∀ {𝔸 : Type u_1} {𝔹 : Type u_2} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : NormedRing 𝔹]
  [NormedAlgebra ℚ 𝔹] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹), (NormedSpace.exp x).1 = NormedSpace.exp x.1
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- Precomposing with a pullback-preserving functor preserves the equalizer condition.  -/
CategoryTheory.regularTopology.equalizerCondition_precomp_of_preservesPullback : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor E C)
  [∀ {X B : E} (π : X ⟶ B) [CategoryTheory.EffectiveEpi π],
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) F]
  [F.PreservesEffectiveEpis],
  CategoryTheory.regularTopology.EqualizerCondition P → CategoryTheory.regularTopology.EqualizerCondition (F.op.comp P)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given a coalgebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.
 -/
CategoryTheory.Comonad.algebra_mono_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra}
  (f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_prod : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'],
  Module.annihilator R (M × M') = Module.annihilator R M ⊓ Module.annihilator R M'
-- Mathlib.Probability.Kernel.Basic
/-- The deterministic kernel that maps `x : α` to the Dirac measure at `(x, x) : α × α`.  -/
ProbabilityTheory.Kernel.copy : (α : Type u_4) → [inst : MeasurableSpace α] → ProbabilityTheory.Kernel α (α × α)
-- Lean.Elab.Exception
Lean.Elab.unsupportedSyntaxExceptionId : Lean.InternalExceptionId
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note that `IsSelfAdjoint.zpow` does not apply to matrices as they are not a division ring.  -/
Matrix.IsHermitian.zpow : ∀ {α : Type u_1} {m : Type u_3} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {A : Matrix m m α}, A.IsHermitian → ∀ (k : ℤ), (A ^ k).IsHermitian
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_one : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S],
  Polynomial.aroots 1 S = 0
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.isMaximal' : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (self : T.CompleteType α), (↑self).IsMaximal
-- Mathlib.Tactic.DefEqTransformations
/-- `unfold_projs at loc` unfolds projections of class instances at the given location.
This also exists as a `conv`-mode tactic.
 -/
Mathlib.Tactic.unfoldProjsStx : Lean.ParserDescr
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.completelyDistribLattice : {α : Type u_1} → [inst : LE α] → CompletelyDistribLattice (LowerSet α)
-- Batteries.Util.Cache
/-- Creates a `DeclCache`.

First, if `pre` is nonempty, run that for a value,
and if successful populate the cache with that value.

If `pre` is empty, or it fails,
the cached structure `α` is initialized with `empty`,
and then `addLibraryDecl` is called for every imported constant.
After all imported constants have been added, we run `post`.
Finally, the result is cached.

When `get` is called, `addDecl` is also called for every constant in the current file.
 -/
Batteries.Tactic.DeclCache.mk : {α : Type} →
  String →
    optParam (Lean.MetaM α) failure →
      α →
        (addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) →
          optParam (Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) addDecl →
            (optParam (α → Lean.MetaM α) fun a => pure a) → IO (Batteries.Tactic.DeclCache α)
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.map_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommRing S] [inst_4 : Module S M] [inst_5 : Algebra R S] [IsScalarTower R S M],
  IsHausdorff (Ideal.map (algebraMap R S) I) M ↔ IsHausdorff I M
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
/-- If `R` is a projective resolution of `X`, then `Ext X Y n` identifies
to the type of cohomology classes of degree `n` from `R.cochainComplex`
to `(singleFunctor C 0).obj Y`.  -/
CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass : {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 : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃+
                CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_hom_associator : ∀ {R : Type u} [inst : CommRing R] {M N K : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom = ↑(TensorProduct.assoc R ↑M ↑N ↑K)
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationPrime`
if `P` holds for `R` whenever `P` holds for `Rₘ` for all prime ideals `p`.  -/
RingHom.OfLocalizationPrime : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.diff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α},
  BaireMeasurableSet s → BaireMeasurableSet t → BaireMeasurableSet (s \ t)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.instToExprPoly : Lean.ToExpr Int.Internal.Linear.Poly
-- Mathlib.Algebra.Star.Center
Set.union_star_self_comm : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {s : Set R},
  (∀ x ∈ s, ∀ y ∈ s, y * x = x * y) →
    (∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) → ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const_obj_map : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) {X_1 Y : J} (x : X_1 ⟶ Y), ((CategoryTheory.Functor.const J).obj X).map x = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the presheaf of modules obtained by
taking a colimit in the category of modules over `R.obj X` for all `X`.  -/
PresheafOfModules.colimitPresheafOfModules : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
                  CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
                    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] →
              [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] →
                PresheafOfModules R
-- Mathlib.Algebra.Group.TransferInstance
/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`.  -/
Finite.exists_type_univ_nonempty_addEquiv : ∀ (G : Type u) [inst : AddGroup G] [Finite G], ∃ G' x x_1, Nonempty (G ≃+ G')
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsScalarTower : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} {S : Type u_7}
  [inst_4 : Semiring R] [inst_5 : Semiring S] [inst_6 : Module R F] [inst_7 : Module S F] [inst_8 : SMulCommClass ℝ R F]
  [inst_9 : SMulCommClass ℝ S F] [inst_10 : ContinuousConstSMul R F] [inst_11 : ContinuousConstSMul S F]
  [inst_12 : SMul R S] [IsScalarTower R S F], IsScalarTower R S (TestFunction Ω F n)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_rename : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {τ : Type u_1} {f : σ → τ},
  Function.Injective f →
    ∀ (x : σ) (p : MvPolynomial σ R),
      (MvPolynomial.pderiv (f x)) ((MvPolynomial.rename f) p) = (MvPolynomial.rename f) ((MvPolynomial.pderiv x) p)
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_countablePartitionSet_subtype : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ)
  (m : MeasurableSpace ↑(MeasurableSpace.countablePartition α n)),
  Measurable fun a => ⟨MeasurableSpace.countablePartitionSet n a, ⋯⟩
-- Mathlib.Probability.Distributions.Uniform
/-- Check that indeed any uniform random variable has the uniformPDF.  -/
MeasureTheory.pdf.uniformPDF_eq_pdf : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasurableSet s →
    MeasureTheory.pdf.IsUniform X s ℙ μ → (fun x => MeasureTheory.pdf.uniformPDF s x μ) =ᵐ[μ] MeasureTheory.pdf X ℙ μ
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂_iso_hom_app_app₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F)
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₁.IsLocalization W₁]
  [inst_6 : L₂.IsLocalization W₂] [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities] (X₁ : C₁) (X₂ : C₂),
  ((CategoryTheory.Localization.Lifting₂.iso L₁ L₂ W₁ W₂ F (CategoryTheory.Localization.lift₂ F hF L₁ L₂)).hom.app
          X₁).app
      X₂ =
    (CategoryTheory.Localization.Lifting.iso L₁ W₁ (F.flip.obj X₂)
            ((CategoryTheory.Localization.lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))).hom.app
      X₁
-- Lean.Elab.Tactic.Omega.Frontend
/-- Match on the two defeq expressions for successor: `n+1`, `n.succ`.  -/
Lean.Elab.Tactic.Omega.succ? : Lean.Expr → Option Lean.Expr
-- Mathlib.Topology.Algebra.Algebra
/-- `Prod.fst` as a `ContinuousAlgHom`.  -/
ContinuousAlgHom.fst : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          (B : Type u_3) →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → A × B →A[R] A
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.unopEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : ⋯.LiftStruct),
  (CategoryTheory.CommSq.LiftStruct.unopEquiv sq).symm l = l.op
-- Lean.Parser.Extra
Lean.Parser.setExpected.parenthesizer : List String → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Prod
Prod.instAddSemigroup : {M : Type u_3} → {N : Type u_4} → [AddSemigroup M] → [AddSemigroup N] → AddSemigroup (M × N)
-- Qq.AssertInstancesCommute
Qq.Impl.isRedundantLocalInst? : Lean.FVarId → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Array.Monadic
/-- This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Array.foldlM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : β → { x // p x } → m β} {g : β → α → m β} {x : β},
  (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) →
    stop = xs.size → Array.foldlM f x xs 0 stop = Array.foldlM g x xs.unattach 0 stop
-- Mathlib.Topology.Irreducible
isIrreducible_irreducibleComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsIrreducible (irreducibleComponent x)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The action of the projection on a basis element `e i`.  -/
GeneralSchauderBasis.proj_apply_basis_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β)
  (i : β), (b.proj A) (↑b i) = if i ∈ A then ↑b i else 0
-- Mathlib.Util.FormatTable
Alignment.noConfusionType : Sort v✝ → Alignment → Alignment → Sort v✝
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  ⦃(Std.Do.wp (f x.run)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)⦄ MonadFunctor.monadMap (fun {β} => f) x ⦃Q⦄
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentSyncOptions.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentSyncOptions
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_compMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.MeasurePreserving f μ ν), ↑(g.compMeasurePreserving f hf) =ᵐ[μ] ↑g ∘ f
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.forkOfIsColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A),
  E.forkOfIsColimit hc hd F =
    CategoryTheory.Limits.Fork.ofι (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f).op) ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_weakEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C) {Y Z : C}
  [HomotopicalAlgebra.IsCofibrant X] (g : Y ⟶ Z) [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z]
  [HomotopicalAlgebra.WeakEquivalence g], Function.Bijective fun f => f.postcomp g
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_C : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) {r : S} (hr : MvPolynomial.C r ∈ Q.ker),
  (Algebra.Generators.H1Cotangent.δ Q P) ⟨Algebra.Extension.Cotangent.mk ⟨MvPolynomial.C r, hr⟩, ⋯⟩ =
    1 ⊗ₜ[S] (KaehlerDifferential.D R S) r
-- Mathlib.RingTheory.AdjoinRoot
/-- The natural isomorphism `R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))` for `α` a root of
`f : R[X]` and `I : Ideal R`.

See `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot`
for the isomorphism with `(R/I)[X] / (f mod I)`.  -/
AdjoinRoot.quotMapOfEquivQuotMapCMapMk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I ≃+*
          AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instMulAction : {S : Type u_1} →
  {R : Type u_3} → {c₁ c₂ c₃ : R} → [inst : Monoid S] → [MulAction S R] → MulAction S (QuaternionAlgebra R c₁ c₂ c₃)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.offset.inj : ∀ {e o : Lean.Expr} {n : ℕ} {e_1 o_1 : Lean.Expr} {n_1 : ℕ},
  Nat.NatOffset.offset✝ e o n = Nat.NatOffset.offset✝ e_1 o_1 n_1 → e = e_1 ∧ o = o_1 ∧ n = n_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Atom.tgt : Mathlib.Tactic.BicategoryLike.Atom → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Raised.dist_le : ∀ {n m : ℕ}, Ordnode.Raised n m → n.dist m ≤ 1
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams : Type
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).functor = CategoryTheory.simplicialToCosimplicialAugmented C
-- Mathlib.GroupTheory.Congruence.Basic
/-- The **second isomorphism theorem for monoids**.  -/
Con.comapQuotientEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (c : Con M) → (f : N →* M) → (Con.comap ⇑f ⋯ c).Quotient ≃* ↥(MonoidHom.mrange (c.mk'.comp f))
-- Mathlib.RingTheory.EssentialFiniteness
RingHom.EssFiniteType.ext : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} (hf : f.EssFiniteType) {g₁ g₂ : S →+* T},
  g₁.comp f = g₂.comp f → (∀ x ∈ hf.finset, g₁ x = g₂ x) → g₁ = g₂
-- Mathlib.GroupTheory.Sylow
Sylow.coe_coe : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G), ↑↑P = ↑P
-- Mathlib.Algebra.Polynomial.Splits
/-- A polynomial `Splits` if it is a product of constant and monic linear polynomials.  -/
Polynomial.Splits : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Prop
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `f` is continuously polynomial at a point, then it is continuously polynomial in a
nonempty ball around that point.  -/
CPolynomialAt.exists_ball_cpolynomialOn : ∀ {𝕜 : 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},
  CPolynomialAt 𝕜 f x → ∃ r, 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwise_smul_toAddSubmonoid : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (S : Submodule R M),
  (a • S).toAddSubmonoid = a • S.toAddSubmonoid
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.eq_dual_iff_dual_eq : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂✶ ↔ M₁✶ = M₂
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections.congr_simp : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f f_1 : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (e_f : f = f_1) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤),
  AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf = AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f_1 ⋯
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.pmap_eq_dmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {x : Option α} {f : (a : α) → p a → β} (h : ∀ a ∈ x, p a),
  Option.pmap f x h = Std.Internal.List.Option.dmap✝ x fun a h' => f a ⋯
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- All weights are non-negative.  -/
Convexity.StdSimplex.nonneg : ∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} (self : Convexity.StdSimplex R M),
  0 ≤ self.weights
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.arrayEnd.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.arrayEnd✝ = 1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00FL](https://stacks.math.columbia.edu/tag/00FL) -/
PrimeSpectrum.denseRange_comap_iff_minimalPrimes : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  DenseRange (PrimeSpectrum.comap f) ↔
    ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (PrimeSpectrum.comap f)
-- Mathlib.GroupTheory.Nilpotent
Group.isNilpotent_iff : ∀ (G : Type u_2) [inst : Group G], Group.IsNilpotent G ↔ ∃ n, Subgroup.upperCentralSeries G n = ⊤
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.algebra₁ : (R : Type u_1) →
  [inst : CommRing R] →
    {A : Type u} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra A B] →
                (D : Algebra.Smooth.DescentAux✝ A B) → Algebra (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_one_lt_of_prod_one_of_exists_ne_one' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : LinearOrder M] {s : Finset ι} [IsOrderedCancelMonoid M]
  (f : ι → M), ∏ i ∈ s, f i = 1 → (∃ i ∈ s, f i ≠ 1) → ∃ i ∈ s, 1 < f i
-- Mathlib.Data.ENNReal.BigOperators
/-- A product of finite numbers is still finite.  -/
ENNReal.prod_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (∀ a ∈ s, f a ≠ ⊤) → ∏ a ∈ s, f a ≠ ⊤