mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If an antitone function has a derivative within a set at a non-isolated point, then this
derivative is nonpositive.  -/
HasDerivWithinAt.nonpos_of_antitoneOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜},
  AccPt x (Filter.principal s) → HasDerivWithinAt g g' s x → AntitoneOn g s → g' ≤ 0
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSym.eq_def : ∀ (a : ℤ) (b : ℕ),
  fastJacobiSym✝ a b =
    if hb0 : b = 0 then 1
    else
      if x : b % 2 = 0 then
        if a % 2 = 0 then 0
        else
          have this := ⋯;
          fastJacobiSym✝ a (b / 2)
      else if b = 1 then 1 else if hab : a % ↑b = 0 then 0 else fastJacobiSymAux✝ (a % ↑b).natAbs b false ⋯
-- Mathlib.RingTheory.Idempotents
/-- [Stacks Tag 00J9](https://stacks.math.columbia.edu/tag/00J9) -/
existsUnique_isIdempotentElem_eq_of_ker_isNilpotent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) → ∀ e ∈ f.range, IsIdempotentElem e → ∃! e', IsIdempotentElem e' ∧ f e' = e
-- Mathlib.Analysis.Convex.StdSimplex
/-- The barycenter equals the (equal weight) center of mass of vertices (`Finset.centerMass`).  -/
stdSimplex.barycenter_eq_centerMass : ∀ {X : Type u_2} [inst : Fintype X] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : IsStrictOrderedRing 𝕜] [inst_4 : Nonempty X] [inst_5 : DecidableEq X],
  ↑stdSimplex.barycenter = Finset.univ.centerMass (fun x => 1) fun i => Pi.single i 1
-- Init.Data.Rat.Lemmas
Rat.divInt_mul_left : ∀ {n d a : ℤ}, a ≠ 0 → Rat.divInt (a * n) (a * d) = Rat.divInt n d
-- Mathlib.Data.List.Rotate
List.IsRotated.cons_append_singleton : ∀ {α : Type u} {l : List α} {a : α}, a :: l ~r l ++ [a]
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.setIntegral_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β}
  [MeasurableSingletonClass β] (hg : Measurable g) (s : Set β) [inst_4 : Decidable (g a ∈ s)],
  ∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
-- Lean.Meta.Match.Basic
/-- Alternative pattern variables.
 -/
Lean.Meta.Match.Alt.fvarDecls : Lean.Meta.Match.Alt → List Lean.LocalDecl
-- Mathlib.Algebra.Ring.Invertible
AddUnits.val_mulLeft : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R), ↑(x.mulLeft y) = y * ↑x
-- Mathlib.Algebra.Homology.Monoidal
/-- Auxiliary definition for `rightUnitor`.  -/
HomologicalComplex.rightUnitor' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  {c : ComplexShape I} →
                    [inst_7 : c.TensorSigns] →
                      (K : HomologicalComplex C c) →
                        [inst_8 : DecidableEq I] →
                          [inst_9 :
                              ∀ (X₁ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                            (K.tensorObj (HomologicalComplex.tensorUnit C c)).X ≅ K.X
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- The standard basis of the endomorphism algebra of a module
induced by a basis of the module.

If `M` is a module with basis `b` indexed by a finite type `ι`,
then `Basis.end b` is the basis of `Module.End R M` indexed by `ι × ι`
where `(i, j)` indexes the linear map that sends `b j` to `b i`
and sends all other basis vectors to `0`.  -/
Module.Basis.end : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [Fintype ι] → [DecidableEq ι] → Module.Basis ι R M → Module.Basis (ι × ι) R (Module.End R M)
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.fg_ker_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FinitePresentation R M] (l : M →ₗ[R] N),
  Function.Surjective ⇑l → (l.ker.FG ↔ Module.FinitePresentation R N)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
deriv_rpow_const : ∀ {f : ℝ → ℝ} {x p : ℝ},
  DifferentiableAt ℝ f x → f x ≠ 0 ∨ 1 ≤ p → deriv (fun x => f x ^ p) x = deriv f x * p * f x ^ (p - 1)
-- Lean.Compiler.IR.CompilerM
Lean.IR.containsDecl : Lean.Name → Lean.IR.CompilerM Bool
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermTransparencyMode.evalTerm : Lean.Term → Lean.Elab.TermElabM (Lean.Meta.TransparencyMode × Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange A K =
    CategoryTheory.Iso.refl
      (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).flip
-- Mathlib.FieldTheory.SeparablyGenerated
/-- If `F` has minimal total degree among the relations of `a`, then `F` is irreducible.  -/
MvPolynomial.irreducible_of_forall_totalDegree_le : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  (∀ (F' : MvPolynomial ι k), F' ≠ 0 → (MvPolynomial.aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) →
    F ≠ 0 → (MvPolynomial.aeval a) F = 0 → Irreducible F
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- As well as being linear, `ι m` squares to zero.  -/
ExteriorAlgebra.ι_sq_zero : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : M),
  (ExteriorAlgebra.ι R) m * (ExteriorAlgebra.ι R) m = 0
-- Mathlib.Data.Nat.Factors
_private.Mathlib.Data.Nat.Factors.0.Nat.primeFactorsList.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match k.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_3 k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, (m.alter k f)[k]? = f m[k]?
-- Lean.Data.Lsp.CodeActions
/-- Whether the code action supports the `disabled` property.  -/
Lean.Lsp.CodeActionClientCapabilities.disabledSupport? : Lean.Lsp.CodeActionClientCapabilities → Option Bool
-- Mathlib.Analysis.Analytic.Constructions
/-- `f x / g x` is analytic away from `g x = 0`  -/
AnalyticOn.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → (∀ x ∈ s, g x ≠ 0) → AnalyticOn 𝕜 (fun x => f x / g x) s
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasProdLocallyUniformly f g` means that the (potentially infinite) product `∏' i, f i b`
for `b : β` converges locally uniformly to `g b` (in the sense of
`TendstoLocallyUniformly`).  -/
HasProdLocallyUniformly : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → (β → α) → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Special case of `fderiv_const_smul_of_invertible` over a division semiring: any constant is
allowed.

TODO: This would work for scalars in a `GroupWithZero` if we had a `DistribMulActionWithZero`
typeclass.  -/
fderiv_const_smul_field : ∀ {𝕜 : 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}
  {R : Type u_4} [inst_5 : DivisionSemiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R), fderiv 𝕜 (c • f) = c • fderiv 𝕜 f
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_inv : ∀ (x : ℂ), x⁻¹.arg = if x.arg = Real.pi then Real.pi else -x.arg
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.hom.app X).unmop.unmop =
    (CategoryTheory.CategoryStruct.id X.unmop).unmop
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_smul : ∀ {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring S₁] {R : Type u_2} [inst_1 : SMulZeroClass R S₁] (a : R)
  (f : MvPolynomial σ S₁), MvPolynomial.constantCoeff (a • f) = a • MvPolynomial.constantCoeff f
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.trans_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀], (P.trans P').P = CategoryTheory.Limits.pullback P.p₁ P'.p₀
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.regular_actLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C), (Bimod.regular A).actLeft = CategoryTheory.MonObj.mul
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_add_add_comm' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
        CategoryTheory.AddMonObj.add) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
      CategoryTheory.AddMonObj.add
-- Mathlib.Data.Finsupp.Sigma
Finsupp.support_embSigma : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} (f : ι k →₀ M),
  f.embSigma.support = Finset.map (Function.Embedding.sigmaMk k) f.support
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
mem_balancedCoreAux_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E} {x : E},
  x ∈ balancedCoreAux 𝕜 s ↔ ∀ (r : 𝕜), 1 ≤ ‖r‖ → x ∈ r • s
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.freeObj.eq_1 : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (X : TopCat),
  TopModuleCat.freeObj R X = TopModuleCat.of R (↑X →₀ R)
-- Mathlib.Analysis.Complex.AbsMax
_private.Mathlib.Analysis.Complex.AbsMax.0.«term_̂» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- A weighted cone `c : WeightedCone W F` is a limit if it is so
as a cone of `CategoryOfElements.π W ⋙ F : W.Elements ⥤ C`.  -/
CategoryTheory.Limits.WeightedCone.IsLimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {W : CategoryTheory.Functor J (Type w)} →
          {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.WeightedCone W F → Type (max (max (max u w) u') v')
-- Init.Data.Option.Monadic
Option.forIn'_pure_yield_eq_pelim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : (a : α) → a ∈ o → β → β) (b : β),
  (forIn' o b fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) = pure (o.pelim b fun a h => f a h b)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).get? k = none
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.arg.injEq : ∀ (arg : ℕ) (all : Bool) (next : Mathlib.Tactic.Conv.Path) (arg_1 : ℕ) (all_1 : Bool)
  (next_1 : Mathlib.Tactic.Conv.Path),
  (Mathlib.Tactic.Conv.Path.arg arg all next = Mathlib.Tactic.Conv.Path.arg arg_1 all_1 next_1) =
    (arg = arg_1 ∧ all = all_1 ∧ next = next_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.foldM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.foldM f init m = List.foldlM (fun a b => f a b.fst b.snd) init m.toList
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
approximatesLinearOn_empty : ∀ {𝕜 : 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) (c : NNReal), ApproximatesLinearOn f f' ∅ c
-- Batteries.Data.AssocList
Batteries.AssocList.instToStream : {α : Type u_1} → {β : Type u_2} → Std.ToStream (Batteries.AssocList α β) (Batteries.AssocList α β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f},
  (t.alter k f).getKey k hc = k
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.ae_completion : ∀ {α : Type u_2} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.ae μ.completion = MeasureTheory.ae μ
-- Std.Sync.CancellationToken
/-- Gets the cancellation reason if the token is cancelled.
 -/
Std.CancellationToken.getCancellationReason : Std.CancellationToken → BaseIO (Option Std.CancellationReason)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X)
        (CategoryTheory.Limits.terminal.from Y)) =
    CategoryTheory.Limits.prod.snd
-- Init.Data.List.Sublist
List.take_sublist : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.take i l).Sublist l
-- Mathlib.Data.List.Sigma
List.dlookup_map₁ : ∀ {α : Type u} {α' : Type u'} [inst : DecidableEq α] [inst_1 : DecidableEq α'] {β : Type v} (l : List ((_ : α) × β))
  {f : α → α'},
  Function.Injective f → ∀ (a : α), List.dlookup (f a) (List.map (Sigma.map f fun x => id) l) = List.dlookup a l
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) (fs : Turing.ToPartrec.Code) (as : List ℕ)
  (k : Turing.ToPartrec.Cont) (v : List ℕ) (h_1 : (v : List ℕ) → motive Turing.ToPartrec.Cont.halt v)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₁ fs as k) v)
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₂ ns k) v)
  (h_4 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.comp f k) v)
  (h_5 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.fix f k) v),
  (match Turing.ToPartrec.Cont.cons₁ fs as k, v with
    | Turing.ToPartrec.Cont.halt, v => h_1 v
    | Turing.ToPartrec.Cont.cons₁ fs as k, v => h_2 fs as k v
    | Turing.ToPartrec.Cont.cons₂ ns k, v => h_3 ns k v
    | Turing.ToPartrec.Cont.comp f k, v => h_4 f k v
    | Turing.ToPartrec.Cont.fix f k, v => h_5 f k v) =
    h_2 fs as k v
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a ring inherits a ring structure  -/
SubringClass.toRing : {S : Type v} → (s : S) → {R : Type u_1} → [inst : Ring R] → [inst_1 : SetLike S R] → [SubringClass S R] → Ring ↥s
-- Mathlib.Algebra.Algebra.Operations
Submodule.instSMul : {R : Type u} →
  [inst : Semiring R] →
    {A : Type v} →
      [inst_1 : Semiring A] →
        [inst_2 : Module R A] →
          {M : Type u_1} →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] → [IsScalarTower R A M] → SMul (Submodule R A) (Submodule R M)
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shiftFunctorZero_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (X : t.Category),
  (CategoryTheory.shiftFunctorZero t.Category A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X) ((t.shiftIso 0).inv.app X)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).get? k = f (t.get? k)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.ext : ∀ {X : SSet} {n : ℕ} {f g : X.Path n}, f.vertex = g.vertex → f.arrow = g.arrow → f = g
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be an integral domain and `f, g₁, g₂ : R[X]`. Let `g₁` and `g₂` be monic and coprime.
Then `∃ q, r₁, r₂ : R[X]` such that `f / (g₁ * g₂) = q + r₁ / g₁ + r₂ / g₂` and
`degree rᵢ < degree gᵢ`, where the equality is taken in a field `K` containing `R[X]`.
See `quo_add_rem_div_add_rem_div_unique` for the uniqueness of this representation.  -/
Polynomial.div_eq_quo_add_rem_div_add_rem_div : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {g₁ g₂ : Polynomial R},
  g₁.Monic →
    g₂.Monic →
      IsCoprime g₁ g₂ →
        ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.Set.univ.eq_1 : ∀ (α : Type u_6) [inst : MeasurableSpace α],
  MeasurableEquiv.Set.univ α = { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_3 : {α : Type u} → Std.Roc.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.monotone_chain_condition_of_isNoetherianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsNoetherianObject X]
  (f : ℕ →o CategoryTheory.Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx'`. -/
Ideal.IsDedekindDomain.ramificationIdx_le_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {S₀ : Type u_2} [inst_6 : CommRing S₀] [inst_7 : Algebra R S₀]
  [inst_8 : Algebra S₀ S] [IsScalarTower R S₀ S] (p : Ideal R) (P : Ideal S₀) (Q : Ideal S) [Q.LiesOver p]
  [hP : P.LiesOver p] [Q.IsPrime], p ≠ ⊥ → P.ramificationIdx' Q ≤ p.ramificationIdx' Q
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- An `n + 1`-truncated simplicial set satisfies the strict Segal condition if
its `m`-simplices are uniquely determined by their spine for all `m ≤ n + 1`.  -/
SSet.Truncated.StrictSegal : {n : ℕ} → SSet.Truncated (n + 1) → Type u
-- Std.Sync.Channel
Std.Channel.instAsyncWriteOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncWrite (Std.Channel α) α
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap'_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.comp_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) (x : A), (φ₁.comp φ₂) x = φ₁ (φ₂ x)
-- Init.Data.UInt.Bitwise
UInt16.not_neg_one : ~~~(-1) = 0
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.epimorphisms.iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.epimorphisms C f ↔ CategoryTheory.Epi f
-- Mathlib.Data.ENNReal.Basic
ENNReal.instDivInvMonoid : DivInvMonoid ENNReal
-- Mathlib.Algebra.Group.AddChar
AddChar.mk.congr_simp : ∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] (toFun toFun_1 : A → M)
  (e_toFun : toFun = toFun_1) (map_zero_eq_one' : toFun 0 = 1)
  (map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b),
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } =
    { toFun := toFun_1, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_cons_of_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ¬p.Nil),
  (SimpleGraph.Walk.cons h p).dropLast = SimpleGraph.Walk.cons h (p.dropLast.copy ⋯ ⋯)
-- Lean.Attributes
Lean.AttributeImpl.mk : Lean.AttributeImplCore →
  (Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit) → (Lean.Name → Lean.AttrM Unit) → Lean.AttributeImpl
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.comp_inv : ∀ {M : Type u_2} {G : Type u_5} {H : Type u_6} [inst : MulOneClass M] [inst_1 : CommGroup G] [inst_2 : CommGroup H]
  (φ : G →* H) (ψ : M →* G), φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y),
  CategoryTheory.WithInitial.prelaxfunctor.map F = (CategoryTheory.WithInitial.map F.toFunctor).toCatHom
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- `C` has finite products  -/
CategoryTheory.Limits.HasFiniteProducts.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ),
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C