mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.RatFunc.Defs
/-- Non-dependent recursion principle for `K⟮X⟯`: if `f p q : P` for all `p q`,
such that `f (a * p) (a * q) = f p q`, then we can find a value of `P`
for all elements of `K⟮X⟯` by setting `lift_on' (p / q) f _ = f p q`.

The value of `f p 0` for any `p` is never used and in principle this may be anything,
although many usages of `lift_on'` assume `f p 0 = f 0 1`.
 -/
RatFunc.liftOn' : {K : Type u_1} →
  [inst : CommRing K] →
    [IsDomain K] →
      {P : Sort u_2} →
        RatFunc K →
          (f : Polynomial K → Polynomial K → P) →
            (∀ {p q a : Polynomial K}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) → P
-- ProofWidgets.Component.RefreshComponent
/-- The server-side state of a `RefreshComponent`.  -/
ProofWidgets.RefreshComponent.RefreshState : Type
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.mor₃ = hS.singleδ
-- Mathlib.RingTheory.Ideal.Oka
Ideal.IsOka.top : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop}, Ideal.IsOka P → P ⊤
-- Mathlib.Algebra.Regular.Basic
/-- Any power of a regular element is regular.  -/
IsRegular.pow : ∀ {R : Type u_1} [inst : Monoid R] {a : R} (n : ℕ), IsRegular a → IsRegular (a ^ n)
-- Init.Data.UInt.Lemmas
USize.toUInt64_mod : ∀ (a b : USize), (a % b).toUInt64 = a.toUInt64 % b.toUInt64
-- Init.GrindInstances.ToInt
Lean.Grind.instMulUInt16UintOfNatNat : Lean.Grind.ToInt.Mul UInt16 (Lean.Grind.IntInterval.uint 16)
-- Lean.Environment
/-- Like `findAsync?`, but blocks until the constant's info is fully available.   -/
Lean.Environment.find? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.ConstantInfo
-- Mathlib.Order.Disjointed
disjoint_disjointed_of_lt : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α) {i j : ι}, i < j → Disjoint (disjointed f i) (disjointed f j)
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for iterators
of type `Iter`.
 -/
Std.Rxo.Iterator.Monadic.step : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LT α] → [DecidableLT α] → Std.IterM Id α → Std.IterStep (Std.IterM Id α) α
-- Mathlib.Topology.Sheaves.PUnit
TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat},
  X.str = ⊤ → ∀ (F : TopCat.Presheaf C X) (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))), F.IsSheaf
-- Mathlib.Order.Irreducible
supPrime_iff_supIrred : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, SupPrime a ↔ SupIrred a
-- Lean.Util.MonadBacktrack
Lean.observing? : {m : Type → Type} →
  {s : Type} →
    {ε : Type u_1} → {α : Type} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadExcept ε m] → m α → m (Option α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (a : E.I₀),
  (CategoryTheory.CategoryStruct.id E).s₀ a = a
-- Init.SimpLemmas
and_congr_left_iff : ∀ {a c b : Prop}, (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.toMixed.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.euclidean.toMixed K = NumberField.mixedEmbedding.euclidean.toMixed K
-- Mathlib.CategoryTheory.Sigma.Basic
/-- If `q₁` and `q₂` when restricted to each subcategory `C i` agree, then `q₁` and `q₂` are isomorphic.
 -/
CategoryTheory.Sigma.natIso : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {q₁ q₂ : CategoryTheory.Functor ((i : I) × C i) D} →
            ((i : I) → (CategoryTheory.Sigma.incl i).comp q₁ ≅ (CategoryTheory.Sigma.incl i).comp q₂) → (q₁ ≅ q₂)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.smul_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (r : AdicCompletion I R) (x : AdicCompletion I M), ↑(r • x) n = ↑r n • ↑x n
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The cocone on `F₂` with apex `B` is a colimit cocone.  -/
CategoryTheory.IndParallelPairPresentation.isColimit₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (self : CategoryTheory.IndParallelPairPresentation f g) →
          CategoryTheory.Limits.IsColimit { pt := B, ι := self.ι₂ }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α} {b : β}, (t.insert a b).getKeyD a fallback = a
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mk : {α : Type u_4} → [inst : TopologicalSpace α] → (carrier : Set α) → IsClopen carrier → TopologicalSpace.Clopens α
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- If `f : FreeAbelianGroup (α → β)`, then `f <*>` is an additive morphism
`FreeAbelianGroup α →+ FreeAbelianGroup β`.  -/
FreeAbelianGroup.seqAddGroupHom : {α β : Type u} → FreeAbelianGroup (α → β) → FreeAbelianGroup α →+ FreeAbelianGroup β
-- Std.Data.ExtTreeSet.Basic
/-- Computes the difference of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.ExtTreeSet.diff : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp
-- Init.Data.Ord.Basic
Ordering.isLT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.inl_biprodXIso_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (K.biprodXIso L i).inv =
    CategoryTheory.Limits.biprod.inl.f i
-- Mathlib.CategoryTheory.Core
/-- The core of a category C is the groupoid whose morphisms are all the
isomorphisms of C.  -/
CategoryTheory.Core : Type u₁ → Type u₁
-- Init.Data.UInt.Lemmas
UInt16.mul_two : ∀ {a : UInt16}, a * 2 = a + a
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_continuousAt_log_log_zero : ¬ContinuousAt (fun x => Real.log (Real.log x)) 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_dite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {P : Prop}
  [inst_2 : Decidable P] (X : C) {Y Z : C} (f : P → (Y ⟶ Z)) (f' : ¬P → (Y ⟶ Z)),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (if h : P then f h else f' h) =
    if h : P then CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f h)
    else CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f' h)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)),
  (CategoryTheory.WithTerminal.equivComma.counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.algebraMap₀_mul_algebraMap₀ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r s : R),
  (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) (TensorPower.algebraMap₀ s)) =
    TensorPower.algebraMap₀ (r * s)
-- Init.Ext
/-- `ext1 pat*` is like `ext pat*` except that it only applies a single extensionality theorem rather
than recursively applying as many extensionality theorems as possible.

The `pat*` patterns are processed using the `rintro` tactic.
If no patterns are supplied, then variables are introduced anonymously using the `intros` tactic.
 -/
Lean.Elab.Tactic.Ext.tacticExt1___ : Lean.ParserDescr
-- Mathlib.Tactic.Ring.Common
/-- A raw natural number literal.  -/
Mathlib.Tactic.Ring.Common.ExtractCoeff.k : {e : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExtractCoeff e → Q(ℕ)
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a `C^n` submersion at `x`, then `f` is `C^n` on its domain chart's source,
in particular on an open neighbourhood of `x`.

Prefer using `IsSubmersionAtOfComplement.contMDiffAt` instead.  -/
Manifold.IsSubmersionAtOfComplement.contMDiffOn : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), ContMDiffOn I J n f h.domChart.source
-- Mathlib.Analysis.Convex.Gauge
/-- Gauge is subadditive.  -/
gauge_add_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → Absorbent ℝ s → ∀ (x y : E), gauge s (x + y) ≤ gauge s x + gauge s y
-- Mathlib.RingTheory.FiniteType
/-- A ring morphism `A →+* B` is of `FiniteType` if `B` is finitely generated as `A`-algebra.  -/
RingHom.FiniteType : {A : Type u_1} → {B : Type u_2} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_prop_eq_none_iff_of_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos} {t u : String},
  pos.Splits t u → (pos.find? p = none ↔ ∀ c ∈ u.toList, ¬p c)
-- Mathlib.Order.LatticeIntervals
Set.Iic.coe_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] (a : α), ↑⊥ = ⊥
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit : Lean.Lsp.TextDocumentEdit → Lean.Lsp.WorkspaceEdit
-- Mathlib.Data.Nat.Find
Nat.findGreatest_mono_right : ∀ (P : ℕ → Prop) [inst : DecidablePred P] {m n : ℕ}, m ≤ n → Nat.findGreatest P m ≤ Nat.findGreatest P n
-- Mathlib.Order.Bounded
Set.bounded_ge_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Ioi a)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_support_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {E : Type u_8} [inst : Zero E]
  (μ : autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.measure_support_eq_zero_iff._auto_1) {f : α → E},
  μ (Function.support f) = 0 ↔ f =ᵐ[μ] 0
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.firstVar : Lean.Grind.AC.Seq → Lean.Grind.AC.Var
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictPeriods_Gamma1 : ∀ (N : ℕ),
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)).strictPeriods =
    AddSubgroup.zmultiples 1
-- Mathlib.Data.Set.Prod
Set.pi_update_of_mem : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {i : ι} [inst : DecidableEq ι],
  i ∈ s →
    ∀ (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)),
      (s.pi fun j => t j (Function.update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j => t j (f j)
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.dropWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.dropWhile pat = s.sliceFrom (s.skipPrefixWhile pat)
-- Init.Data.Nat.MinMax
Nat.max_eq_max : ∀ {b : ℕ} (a : ℕ), a.max b = max a b
-- Mathlib.Util.Superscript
/-- Given a predicate `leftOfPartition` which is true for indexes `< i` and false for `≥ i`,
returns `i`, by binary search.  -/
Mathlib.Tactic.Superscript.partitionPoint : {α : Type u} → [Inhabited α] → (as : Array α) → (α → Bool) → optParam ℕ 0 → optParam ℕ as.size → ℕ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk.inj : ∀ {coe : ℂ} {coe_im_pos : 0 < coe.im} {coe_1 : ℂ} {coe_im_pos_1 : 0 < coe_1.im},
  { coe := coe, coe_im_pos := coe_im_pos } = { coe := coe_1, coe_im_pos := coe_im_pos_1 } → coe = coe_1
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.toPointedCone_injective : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E],
  Function.Injective ProperCone.toPointedCone
-- Init.Data.SInt.Lemmas
Int8.add_left_neg : ∀ (a : Int8), -a + a = 0
-- Mathlib.CategoryTheory.Category.Quiv
/-- An unbundled version of the right triangle equality.  -/
CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Paths.of C ⋙q (CategoryTheory.pathComposition C).toPrefunctor = 𝟭q C
-- Lean.Attributes
Lean.EnumAttributes.mk : {α : Type} →
  List Lean.AttributeImpl →
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α) → Lean.EnumAttributes α
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.obj_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (i j : ℕ),
  (AlgebraicTopology.NormalizedMooreComplex.obj X).d i j =
    ChainComplex.of.d
      (fun n => CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n))
      (AlgebraicTopology.NormalizedMooreComplex.objD X) i j
-- Mathlib.Topology.Homotopy.HomotopyGroup
HomotopyGroup.genLoopEquivOfUnique_transAt : ∀ {X : Type u_2} [inst : TopologicalSpace X] {x : X} (N : Type u_3) [inst_1 : DecidableEq N] [inst_2 : Unique N]
  (p q : ↑(GenLoop N X x)),
  (genLoopEquivOfUnique N) (GenLoop.transAt default q p) =
    Path.trans ((genLoopEquivOfUnique N) q) ((genLoopEquivOfUnique N) p)
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.prePrimitive_SL : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  MulAction.IsPreprimitive (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.support_cycleOf_eq_nil_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  (f.cycleOf x).support = ∅ ↔ x ∉ f.support
-- Mathlib.RingTheory.Ideal.Maps
/-- If the target is not the zero ring, then one is not in the kernel.  -/
RingHom.one_notMem_ker : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] [Nontrivial S] (f : F), 1 ∉ RingHom.ker f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.free_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  {F G : CategoryTheory.Functor Cᵒᵖ (Type u)} (φ : F ⟶ G) (X : Cᵒᵖ),
  ((PresheafOfModules.free R).map φ).app X = (ModuleCat.free ↑(R.obj X)).map (φ.app X)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates limits, then `F : Cᵒᵖ ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) → [CategoryTheory.CreatesLimits F.rightOp] → CategoryTheory.CreatesColimits F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he = t.keys.getLast ⋯
-- Mathlib.RingTheory.Extension.Generators
/-- The naive generators for a quotient `R[Xᵢ] ⧸ I`.
If the definitional equality of the section matters, it can be explicitly provided.
 -/
Algebra.Generators.naive : {R : Type u} →
  [inst : CommRing R] →
    {σ : Type u_2} →
      {I : Ideal (MvPolynomial σ R)} →
        (s : optParam (MvPolynomial σ R ⧸ I → MvPolynomial σ R) (Function.surjInv ⋯)) →
          autoParam (∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x) Algebra.Generators.naive._auto_1 →
            Algebra.Generators R (MvPolynomial σ R ⧸ I) σ
-- Mathlib.Order.Filter.ENNReal
Real.limsSup_of_not_isBounded : ∀ {f : Filter ℝ}, ¬Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f → f.limsSup = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α) (n : ℕ),
  Finset.map AddOpposite.opEquiv.toEmbedding (n • s) = n • Finset.map AddOpposite.opEquiv.toEmbedding s
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Parser.ParserContext.currentColumn : Lean.Parser.ParserContext → Lean.Parser.ParserState → ℕ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.of_fg : ∀ {M : Type u_1} [inst : AddCommMonoid M] {P : AddSubmonoid M}, P.FG → IsLinearSet ↑P
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} [Subsingleton V] {u v : V}, G.Reachable u v
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsAlternating.spanningCoe : ∀ {V : Type u_1} {G G' : SimpleGraph V}, G.IsAlternating G' → ∀ (H : G.Subgraph), H.spanningCoe.IsAlternating G'
-- Mathlib.Topology.MetricSpace.Thickening
Metric.closedBall_subset_cthickening_singleton : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (δ : ℝ), Metric.closedBall x δ ⊆ Metric.cthickening δ {x}
-- Init.Data.String.Lemmas.Iterate
String.foldl_eq_foldl_toList : ∀ {α : Type u} {f : α → Char → α} {init : α} {s : String}, String.foldl f init s = List.foldl f init s.toList
-- Init.Data.BitVec.Lemmas
BitVec.concat_induction : ∀ {motive : (w : ℕ) → BitVec w → Prop},
  motive 0 BitVec.nil →
    (∀ {w : ℕ} (bv : BitVec w) (b : Bool), motive w bv → motive (w + 1) (bv.concat b)) →
      ∀ {w : ℕ} (x : BitVec w), motive w x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddMonoidOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddMonoid β] → [ContinuousAdd β] → AddMonoid C(α, β)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instCategory : CategoryTheory.Category.{u, u + 1} MagmaCat
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_sub_union_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
-- Mathlib.Data.List.Sort
/-- `orderedInsert a l` inserts `a` into `l` at such that
`orderedInsert a l` is sorted if `l` is.  -/
List.orderedInsert : {α : Type u_1} → (r : α → α → Prop) → [DecidableRel r] → α → List α → List α
-- Mathlib.Algebra.Homology.Functor
/-- The functorial version of `HomologicalComplex.asFunctor`.  -/
HomologicalComplex.complexOfFunctorsToFunctorToComplex : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {V : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} V] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
          {ι : Type u_3} →
            {c : ComplexShape ι} →
              CategoryTheory.Functor (HomologicalComplex (CategoryTheory.Functor T V) c)
                (CategoryTheory.Functor T (HomologicalComplex V c))
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lt_mem_range_succ : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [OrderTop α],
  (Ordinal.type fun x1 x2 => x1 < x2) ∈ Set.range Order.succ
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.colimitEquivColimitType_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j),
  (CategoryTheory.Limits.Types.colimitEquivColimitType F)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) =
    Quot.mk F.ColimitTypeRel ⟨j, x⟩
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_sub' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), dist a b = ‖b - a‖
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_tail : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.tail k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail k) ∪
      Turing.PartrecToTM2.contSupp k
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.Config.mk : Bool → Mathlib.Tactic.Push.Config
-- Mathlib.Order.Partition.Basic
Partition.subset_sUnion_and_mem_iff_mem : ∀ {α : Type u_1} {S : Set (Set α)} {u t : Set α} {P : Partition u}, S ⊆ ↑P → (t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S)
-- Mathlib.AlgebraicGeometry.Normalization
/-- Given `f : X ⟶ Y`, `f.normalization` is the relative normalization of `Y` in `X`.  -/
AlgebraicGeometry.Scheme.Hom.normalization : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [AlgebraicGeometry.QuasiCompact f] → [AlgebraicGeometry.QuasiSeparated f] → AlgebraicGeometry.Scheme
-- Mathlib.Topology.MetricSpace.Bounded
Metric.mem_cocompact_of_closedBall_compl_subset : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] [ProperSpace α] (c : α),
  (∃ r, (Metric.closedBall c r)ᶜ ⊆ s) → s ∈ Filter.cocompact α
-- Mathlib.Algebra.Group.Units.Hom
Units.coe_map : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (x : Mˣ), ↑((Units.map f) x) = f ↑x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filterAddMonoidHom_apply : ∀ {ι : Type u} (β : ι → Type v) [inst : (i : ι) → AddZeroClass (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (x : Π₀ (i : ι), β i), (DFinsupp.filterAddMonoidHom β p) x = DFinsupp.filter p x
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux_swap : ∀ {n : ℕ} {x y : Fin n}, x ≠ y → (Equiv.swap x y).signAux = -1
-- Mathlib.Order.RelIso.Basic
/-- A relation embedding from an empty type.  -/
RelEmbedding.ofIsEmpty : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [IsEmpty α] → r ↪r s
-- Mathlib.Algebra.Category.Grp.Abelian
/-- In the category of abelian groups, every monomorphism is normal.  -/
AddCommGrpCat.normalMono : {X Y : AddCommGrpCat} → (f : X ⟶ Y) → CategoryTheory.Mono f → CategoryTheory.NormalMono f
-- Init.Data.List.Find
List.findIdx_eq_getD_bind_find?_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool},
  List.findIdx p xs = ((List.find? p xs).bind fun a => List.idxOf? a xs).getD xs.length