mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Config
/-- Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
the characteristic of a ring.
 -/
Lean.Grind.Config.exp : Lean.Grind.Config → ℕ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The product of additive subsemigroups is isomorphic to their product as additive semigroups  -/
AddSubsemigroup.prodEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (s : AddSubsemigroup M) → (t : AddSubsemigroup N) → ↥(s.prod t) ≃+ ↥s × ↥t
-- Init.Data.Array.MinMax
Array.get_min? : ∀ {α : Type u_1} [inst : Min α] {xs : Array α} {h : xs.min?.isSome = true}, xs.min?.get h = xs.min ⋯
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- `A ↦ S ⊗[R] A` is naturally isomorphic to `A ↦ pushout A.hom (algebraMap R S)`.  -/
CommRingCat.tensorProdIsoPushout : (R S : CommRingCat) →
  [inst : Algebra ↑R ↑S] → R.tensorProd S ≅ CategoryTheory.Under.pushout (CommRingCat.ofHom (algebraMap ↑R ↑S))
-- Mathlib.Data.Set.Basic
Set.ofPred_true : ∀ {α : Type u}, {_x | True} = Set.univ
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypePreimage_symm_apply_coe_pos : ∀ {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β)
  (a : α) (h : p a), ↑((Equiv.subtypePreimage p x₀).symm x) a = x₀ ⟨a, h⟩
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- (Implementation detail): The inverse of `tensorModelOfHasCoeffsHom`.  -/
Algebra.Presentation.tensorModelOfHasCoeffsInv : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.Presentation R S ι σ) →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] →
                          [inst_7 : P.HasCoeffs R₀] →
                            S →ₐ[R] TensorProduct R₀ R (Algebra.Presentation.ModelOfHasCoeffs R₀)
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.TypeVec.append1.match_1.splitter : {n : ℕ} →
  (motive : Fin2 (n + 1) → Sort u_1) →
    (x : Fin2 (n + 1)) → ((i : Fin2 n) → motive i.fs) → (Unit → motive Fin2.fz) → motive x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : Inhabited β] {a : α},
  Std.DHashMap.Const.get! ∅ a = default
-- Mathlib.Data.List.Lex
List.cons_le_cons : ∀ {α : Type u} [inst : LinearOrder α] (a : α) {l l' : List α}, l' ≤ l → a :: l' ≤ a :: l
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.subset : ∀ {α : Type u_1} {G : SimpleGraph α} {s t : Set α}, t ⊆ s → G.IsClique s → G.IsClique t
-- Mathlib.Topology.UniformSpace.Basic
/-- Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained
by taking independently an entourage of the diagonal in the first part, and an entourage of
the diagonal in the second part.  -/
Sum.instUniformSpace : {α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → UniformSpace (α ⊕ β)
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.mk.inj : ∀ {prec quotDepth : ℕ} {suppressInsideQuot : Bool} {savedPos? : Option String.Pos.Raw}
  {forbiddenTk? : Option Lean.Parser.Token} {prec_1 quotDepth_1 : ℕ} {suppressInsideQuot_1 : Bool}
  {savedPos?_1 : Option String.Pos.Raw} {forbiddenTk?_1 : Option Lean.Parser.Token},
  { prec := prec, quotDepth := quotDepth, suppressInsideQuot := suppressInsideQuot, savedPos? := savedPos?,
        forbiddenTk? := forbiddenTk? } =
      { prec := prec_1, quotDepth := quotDepth_1, suppressInsideQuot := suppressInsideQuot_1, savedPos? := savedPos?_1,
        forbiddenTk? := forbiddenTk?_1 } →
    prec = prec_1 ∧
      quotDepth = quotDepth_1 ∧
        suppressInsideQuot = suppressInsideQuot_1 ∧ savedPos? = savedPos?_1 ∧ forbiddenTk? = forbiddenTk?_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instCompleteLattice : {α : Type u} → [inst : AddGroup α] → CompleteLattice (AddGroupTopology α)
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.coe_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : SMul R S] (a : { c // 0 ≤ c })
  (x : S), ↑a • x = a • x
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.finiteType_of_monoid_fg : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] [Monoid.FG ↥M], Algebra.FiniteType R S
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl : ∀ (x : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x).hom.τl =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x.as)).hom
-- Lean.Meta.LetToHave
/-- Executes `m` in a context where `letFVars := fvars`.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.withLetFVars : {α : Type} → List Lean.FVarId → Lean.Meta.LetToHave.M✝ α → Lean.Meta.LetToHave.M✝ α
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremsArray.find : {α : Type} → Lean.Meta.Grind.TheoremsArray α → Lean.Meta.Grind.Origin → List α
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instDescScheme : ∀ {U V X : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : V ⟶ X) [AlgebraicGeometry.IsIntegralHom f]
  [AlgebraicGeometry.IsIntegralHom g], AlgebraicGeometry.IsIntegralHom (CategoryTheory.Limits.coprod.desc f g)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.count_take_firstReturn_add_one : ∀ {p : DyckWord},
  p ≠ 0 →
    List.count DyckStep.U (List.take (p.firstReturn + 1) ↑p) = List.count DyckStep.D (List.take (p.firstReturn + 1) ↑p)
-- Mathlib.Order.UpperLower.Closure
lowerClosure_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone lowerClosure
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.insertMany l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' } :=
        __s
      pure r).run
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.notMem_iff_subset : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → (x ∉ y ↔ y ⊆ x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.enumMember.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.enumMember = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        Std.Internal.List.getKeyD k l₁ fallback
-- Std.Async.Signal
Std.Async.Signal.sigchld.sizeOf_spec : sizeOf Std.Async.Signal.sigchld = 1
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toAddEquiv_eq_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  f.toAddEquiv = ↑f
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) =
    X.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.CategoryTheory.Square
CategoryTheory.Functor.mapSquare_map_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (F.mapSquare.map φ).τ₂ = F.map φ.τ₂
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) [inst_2 : S.HasHomology],
  h.left.homologyIso = h.right.homologyIso ≪≫ h.iso.symm
-- Mathlib.Algebra.Group.Center
Set.neg_mem_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : AddGroup M] {a : M}, a ∈ S.addCentralizer → -a ∈ S.addCentralizer
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.mul_inf : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] (I J K_1 : FractionalIdeal (nonZeroDivisors A) K), I * (J ⊓ K_1) = I * J ⊓ I * K_1
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.exists_le_of_sum_le : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∀ {f g : α → ENNReal}, ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i → ∃ i ∈ s, f i ≤ g i
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀),
  (TopologicalSpace.Opens.map d.toBase.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i)) =
    AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.colimit.ι d.functor i)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.Red.decidableRel : {α : Type u_1} → [DecidableEq α] → DecidableRel FreeGroup.Red
-- Mathlib.Control.Applicative
Functor.Comp.applicative_id_comp : ∀ {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F], Functor.Comp.instApplicativeComp = AF
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial_injective : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (i : σ), Function.Injective ⇑(Polynomial.toMvPolynomial i)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.constantCoeff_coe : ∀ {R : Type u_1} [inst : Semiring R] (φ : Polynomial R), PowerSeries.constantCoeff ↑φ = φ.coeff 0
-- Init.Data.String.Lemmas.Order
String.Pos.ne_endPos_of_slice_ne_endPos : ∀ {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁},
  p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos → p ≠ s.endPos
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, the `Specializes` relation is symmetric, dot notation version.  -/
Specializes.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {x y : X}, x ⤳ y → y ⤳ x
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toAddMonoidWithOne : {R : Type u} → [self : AddGroupWithOne R] → AddMonoidWithOne R
-- Mathlib.Algebra.Polynomial.Degree.Monomial
Polynomial.monomial_natDegree_leadingCoeff_eq_self : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.support.card ≤ 1 → (Polynomial.monomial p.natDegree) p.leadingCoeff = p
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  (f : sSupHom β γ) (g : sSupHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Group.Conj
/-- The quotient type of additive conjugacy classes of an additive group.  -/
AddConjClasses : (α : Type u_1) → [AddMonoid α] → Type u_1
-- Mathlib.Order.Filter.Defs
/-- Two functions `f` and `g` are *eventually equal* along a filter `l` if the set of `x` such that
`f x = g x` belongs to `l`.  -/
Filter.«term_=ᶠ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.one_le_rpow : ∀ {x : ENNReal} {z : ℝ}, 1 ≤ x → 0 < z → 1 ≤ x ^ z
-- Mathlib.Algebra.Order.Module.Defs
Prod.instSMulPosReflectLE : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosReflectLE α β]
  [SMulPosReflectLE α γ], SMulPosReflectLE α (β × γ)
-- Mathlib.Analysis.Complex.Order
Complex.not_le_iff : ∀ {z w : ℂ}, ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_2 a x
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.subsingleton_dual_iff : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Subsingleton (Module.Dual K V) ↔ Subsingleton V
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_iUnion : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}},
  (x ∈ ZFSet.iUnion fun i => f i) ↔ ∃ i, x ∈ f i
-- Mathlib.NumberTheory.Divisors
Nat.nodup_divisorsAntidiagonalList : ∀ {n : ℕ}, n.divisorsAntidiagonalList.Nodup
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f g h : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g}
  {θ : g ≅ h} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf)
  (η_h : CategoryTheory.CategoryStruct.comp p h ≅ pf),
  CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.Bicategory.whiskerLeftIso p θ ≪≫ η_h = η_g →
      CategoryTheory.Bicategory.whiskerLeftIso p (η ≪≫ θ) ≪≫ η_h = η_f
-- Mathlib.Data.Finset.Empty
Finset.not_nonempty_iff_eq_empty : ∀ {α : Type u_1} {s : Finset α}, ¬s.Nonempty ↔ s = ∅
-- Mathlib.Data.Stream.Init
Stream'.take_get : ∀ {α : Type u} (m n : ℕ) (a : Stream' α) (h : m < (Stream'.take n a).length), (Stream'.take n a)[m] = a.get m
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instSmooth : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.Etale R A],
  Algebra.Smooth R A
-- Mathlib.Analysis.InnerProductSpace.Dual
_private.Mathlib.Analysis.InnerProductSpace.Dual.0.InnerProductSpace.«term_♯» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.instIsAddTorsionFree : ∀ {M : Type u_8}, IsAddTorsionFree (Multiset M)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_of_ne : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {l : Filter α} {c : F''}, c ≠ 0 → ((f =O[l] fun _x => c) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Given a collection of maps out of the summands, we obtain a map out of the biproduct.  -/
CategoryTheory.Limits.biproduct.desc : {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 : C} → ((b : J) → f b ⟶ P) → (⨁ f ⟶ P)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_neg : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S], (-p).rootSet S = p.rootSet S
-- Mathlib.Data.Num.Basic
Num.instDiv : Div Num
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- Every matrix indexed by a subsingleton is diagonal.  -/
Matrix.isDiag_of_subsingleton : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [Subsingleton n] (A : Matrix n n α), A.IsDiag
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPUniverses : Lean.Options → Bool
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.mk : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R], ¬IsSumNonzeroSq 0 → IsFormallyReal R
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.toInt32 : ByteArray → ℤ
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the type of `CommMonoid` homomorphisms `f : M →* N` such that `N`
is isomorphic to the Localization of `M` at the Submonoid generated by `x`.  -/
Submonoid.LocalizationMap.AwayMap : {M : Type u_1} → [CommMonoid M] → M → (N' : Type u_4) → [CommMonoid N'] → Type (max u_1 u_4)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sSup_neg : ∀ (s : Set ℝ), sSup (-s) = -sInf s
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.map f it)).toListRev = (Std.IterM.filterMapM (fun b => g (f b)) it).toListRev
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₃_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_prod_of_submultiplicative_on_pred : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β) (p : α → Prop),
  f 1 ≤ 1 →
    p 1 →
      (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
        (∀ (a b : α), p a → p b → p (a * b)) → ∀ (s : Multiset α), (∀ a ∈ s, p a) → f s.prod ≤ (Multiset.map f s).prod
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.coe_mk : ∀ {X : Type u_1} {Y : Type u_2} (f : X → Y), ⇑{ toFun := f } = f
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_self_apply : ∀ {F : Type u_1} [inst : Field F] [inst_1 : CharZero F] (a : F), (Algebra.normalizedTrace F F) a = a
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetryIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [inst_3 : F.Faithful],
  (hf'.symmetryIso hg).hom = hf'.symmetry hg
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.sub_const : ∀ {𝕜 : 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}
  {s : Set E}, DifferentiableOn 𝕜 f s → ∀ (c : F), DifferentiableOn 𝕜 (fun y => f y - c) s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)] {h : a ∈ t}, t.get a h = t.get! a
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.IsHomological.of_iso : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.Preadditive C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.Abelian A] {F₁ F₂ : CategoryTheory.Functor C A}
  [F₁.IsHomological] (e : F₁ ≅ F₂), F₂.IsHomological
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.ExtTreeMap.getEntryLT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α × β
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.ext : ∀ {R : Type u_1} [inst : Ring R] {f g : RingTopology R}, TopologicalSpace.IsOpen = TopologicalSpace.IsOpen → f = g
-- Lean.Elab.Do.Basic
/-- If `e` is syntactically a `pure …` application, return the pure value; otherwise `none`.
Used by `DoElemCont.mkBindUnlessPure` to contract `e >>= pure` to `e` and
`pure e >>= k` to `let x := e; k x`.
 -/
Lean.Elab.Do.DoOps.isPureApp? : Lean.Elab.Do.DoOps → Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Homology.Square
/-- A commutative square in a preadditive category is a pushout square iff
the corresponding diagram `X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₄` a cokernel.  -/
CategoryTheory.Square.isPushoutEquivIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (sq : CategoryTheory.Square C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          sq.IsPushout ≃ CategoryTheory.Limits.IsColimit sq.cokernelCofork
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toOrderHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), f.toOrderHom = { toFun := (↑f.toAddMonoidHom).toFun, monotone' := ⋯ }