mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LocalExtr.Polynomial
/-- **Alias** of `Polynomial.card_roots_toFinset_le_card_roots_derivative_sdiff_roots_succ`.

---

The number of roots of a real polynomial `p` is at most the number of roots of its derivative
that are not roots of `p` plus one.  -/
Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ : ∀ (p : Polynomial ℝ), p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
-- Init.Data.List.Basic
List.Pairwise.below : {α : Type u} →
  {R : α → α → Prop} → {motive : (a : List α) → List.Pairwise R a → Prop} → {a : List α} → List.Pairwise R a → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `f` is a monomorphism, then `(𝟙 _, 𝟙 _)` is a kernel pair for `f`.  -/
CategoryTheory.IsKernelPair.id_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.IsKernelPair f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `G` is a right adjoint, then so is `post G : Over Y ⥤ Over (G Y)`.

If the left adjoint of `G` is `F`, then the left adjoint of `post G` is given by
`(X ⟶ G Y) ↦ (F X ⟶ F G Y ⟶ Y)`.  -/
CategoryTheory.Over.postAdjunctionRight : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {Y : D} →
          {F : CategoryTheory.Functor T D} →
            {G : CategoryTheory.Functor D T} →
              (a : F ⊣ G) →
                (CategoryTheory.Over.post F).comp (CategoryTheory.Over.map (a.counit.app Y)) ⊣
                  CategoryTheory.Over.post G
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_left_Ioo : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addLeftEmbedding c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
-- Init.Data.List.Count
List.countP_filter : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, List.countP p (List.filter q l) = List.countP (fun a => p a && q a) l
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.one_isLittleO_log_log : (fun x => 1) =o[Filter.atTop] fun x => Real.log (Real.log x)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)} {hl : l.isEmpty = false},
  Std.Internal.List.DistinctKeys l → ∀ (hp : l.Perm l'), Std.Internal.List.maxKey l hl = Std.Internal.List.maxKey l' ⋯
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars'.eq_1 : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K],
  P.restrictScalars' K =
    {
      toLinearMap :=
        (Submodule.span K (Set.range ⇑P.root)).subtype.restrictScalarsRange₂
          (Submodule.span K (Set.range ⇑P.coroot)).subtype (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯,
      isPerfPair_toLinearMap := ⋯, root := { toFun := fun i => ⟨P.root i, ⋯⟩, inj' := ⋯ },
      coroot := { toFun := fun i => ⟨P.coroot i, ⋯⟩, inj' := ⋯ }, root_coroot_two := ⋯,
      reflectionPerm := P.reflectionPerm, reflectionPerm_root := ⋯, reflectionPerm_coroot := ⋯ }
-- Lean.Elab.ConfigEval.Basic
/-- Applies the configuration `cfg` to `init` using `eval.set`.
If `logExceptions` is true, then catches and logs exceptions.

The `onErr` callback is used for invalid configuration syntax.

Note: this should be run from within `runConfigElab`.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.setConfigs : {α : Type} →
  Lean.Elab.ConfigEval.EvalConfigItem α →
    α →
      Array Lean.Syntax →
        (optParam (α → Lean.Syntax → Lean.Elab.TermElabM α) fun cfg cfgItem =>
            Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr cfg cfgItem) →
          optParam Bool false → Lean.Elab.TermElabM α
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_vadd_eq_or_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ (g : G), g +ᵥ B = B ∨ Disjoint (g +ᵥ B) B
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.hereditary : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M], FirstOrder.Language.Hereditary (L.age M)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toArray_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n},
  (xs.iterM m).toArray = pure xs.toArray
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection between the set of prime factors of the ideal `⟨r⟩` and the set of prime factors
of `r` preserves `count` of the corresponding multisets. See
`multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity` for the version
stated in terms of multiplicity.  -/
Ideal.count_span_normalizedFactors_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] [inst_4 : DecidableEq R] {r X : R},
  r ≠ 0 →
    Prime X →
      Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) =
        Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instMul : {K : Type u} → [inst : CommRing K] → Mul (RatFunc K)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.isScalarTower' : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {S' : Type u_1} [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : SMul S' R] [inst_5 : SMul S' M]
  [inst_6 : SMul S S'] [inst_7 : IsScalarTower S' R M] [IsScalarTower S S' M] [inst_9 : IsScalarTower S R M],
  IsScalarTower S S' ↥p
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_top_right : ∀ {E : Type v} [inst : Field E] (A : Subfield E), A.relrank ⊤ = Module.rank (↥A) E
-- Mathlib.Dynamics.Ergodic.RadonNikodym
/-- The Radon-Nikodym derivative of a finite invariant measure of a self-map `f`
with respect to another finite invariant measure of `f` is a.e. invariant under `f`.  -/
MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : X → X},
  MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.MeasurePreserving f ν ν → μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.Algebra.Order.Group.Synonym
toLex_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), toLex a⁻¹ = (toLex a)⁻¹
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A group homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
`continuous_of_continuousAt_one`.  -/
uniformContinuous_of_continuousAt_one : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : Group β] [IsUniformGroup β] [inst_6 : FunLike hom α β] [MonoidHomClass hom α β]
  (f : hom), ContinuousAt (⇑f) 1 → UniformContinuous ⇑f
-- Mathlib.Topology.Sets.VietorisTopology
/-- **Alias** of `TopologicalSpace.Compacts.dense_setOfPred_finite`. -/
TopologicalSpace.Compacts.dense_setOf_finite : ∀ {α : Type u_1} [inst : TopologicalSpace α], Dense {K | (↑K).Finite}
-- Mathlib.Algebra.DirectSum.Decomposition
/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
an additive monoid to a direct sum of components.  -/
DirectSum.decomposeAddEquiv : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) → [DirectSum.Decomposition ℳ] → M ≃+ DirectSum ι fun i => ↥(ℳ i)
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_three : ∀ {R : Type u_6} [inst : AddCommMonoid R] (A : Matrix (Fin 3) (Fin 3) R), A.trace = A 0 0 + A 1 1 + A 2 2
-- Mathlib.Order.WithBot
/-- Deconstruct a `x : WithBot α` to the underlying value in `α`, given a proof that `x ≠ ⊥`.  -/
WithBot.unbot : {α : Type u_1} → (x : WithBot α) → x ≠ ⊥ → α
-- Init.Data.Order.Factories
/-- Derives a `LawfulOrderMax α` instance for `LE.ofLT` from two properties involving `LT α` and
`Max α` instances.

The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
Std.LawfulOrderMax.of_lt : ∀ {α : Type u} [inst : Max α] [inst_1 : LT α],
  (∀ (a b c : α), c < a ⊔ b ↔ c < a ∨ c < b) → (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) → Std.LawfulOrderMax α
-- Mathlib.Data.Sym.Basic
_private.Mathlib.Data.Sym.Basic.0.SymOptionSuccEquiv.decode.match_1.eq_1 : ∀ {α : Type u_1} {n : ℕ} (motive : Sym (Option α) n ⊕ Sym α n.succ → Sort u_2) (s : Sym (Option α) n)
  (h_1 : (s : Sym (Option α) n) → motive (Sum.inl s)) (h_2 : (s : Sym α n.succ) → motive (Sum.inr s)),
  (match Sum.inl s with
    | Sum.inl s => h_1 s
    | Sum.inr s => h_2 s) =
    h_1 s
-- Mathlib.FieldTheory.KummerExtension
isGalois_of_isSplittingField_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K},
      Irreducible (Polynomial.X ^ n - Polynomial.C a) →
        ∀ (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
          [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)], IsGalois K L
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`,
as long as `ι` is finite.  -/
Module.Basis.ofEquivFun : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Finite ι] → (M ≃ₗ[R] ι → R) → Module.Basis ι R M
-- Mathlib.Logic.Denumerable
/-- If `α` is denumerable, then so is `Option α`.  -/
Denumerable.option : {α : Type u_1} → [Denumerable α] → Denumerable (Option α)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- Given `AddCommMonoid A` and `e : G ≃ H`, `domCongr e` is the corresponding `Equiv` between
`SkewMonoidAlgebra A G` and `SkewMonoidAlgebra A H`.  -/
SkewMonoidAlgebra.domCongr : {G : Type u_2} →
  {H : Type u_3} → {A : Type u_4} → [inst : AddCommMonoid A] → G ≃ H → SkewMonoidAlgebra A G ≃+ SkewMonoidAlgebra A H
-- Mathlib.Order.Hom.Bounded
BotHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β] [inst_3 : OrderBot β]
  [inst_4 : LE γ] [inst_5 : OrderBot γ] (g : BotHom β γ) (f : BotHom α β),
  BotHom.dual (g.comp f) = (BotHom.dual g).comp (BotHom.dual f)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ),
  (CategoryTheory.simplicialCosimplicialEquiv C).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.id_pow : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ),
  LinearMap.id ^ n = LinearMap.id
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.prop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] {X : C} (h : P.LimitOfShape J X), P X
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} [inst : DecidableEq o]
  [inst_1 : Fintype n] [inst_2 : Fintype o] [inst_3 : NonUnitalNonAssocSemiring α] (M : o → Matrix m n α)
  (N : o → Matrix n p α), (Matrix.blockDiagonal fun k => M k * N k) = Matrix.blockDiagonal M * Matrix.blockDiagonal N
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.simpleGraphOfStructure_adj : ∀ (V : Type u) [inst : FirstOrder.Language.graph.Structure V] [inst_1 : V ⊨ FirstOrder.Language.Theory.simpleGraph]
  (x y : V),
  (FirstOrder.Language.simpleGraphOfStructure V).Adj x y =
    FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]
-- Mathlib.Data.Finset.Card
Finset.card_le_card_of_surjOn : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β), Set.SurjOn f ↑s ↑t → t.card ≤ s.card
-- Mathlib.Data.Nat.Factorization.Defs
Nat.eq_of_factorization_eq : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (∀ (p : ℕ), a.factorization p = b.factorization p) → a = b
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddZeroClass.eq_1 : ∀ {α : Type u_1} [inst : AddZeroClass α],
  AddOpposite.instAddZeroClass = { toAddZero := AddOpposite.instAddZero, zero_add := ⋯, add_zero := ⋯ }
-- Init.Control.StateRef
StateRefT'.instMonadLift : {ω σ : Type} → {m : Type → Type} → MonadLift m (StateRefT' ω σ m)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffOn.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E}, UniqueDiffOn 𝕜 s → IsOpen t → UniqueDiffOn 𝕜 (s ∩ t)
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.finset_sup : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M),
  (∀ i ∈ s, (P i).FG) → (s.sup P).FG
-- Mathlib.Topology.NhdsSet
Filter.HasBasis.nhdsSet_interior : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set X} {t : Set X},
  (nhdsSet t).HasBasis p s → (nhdsSet t).HasBasis p fun x => interior (s x)
-- Mathlib.Data.Stream.Init
Stream'.mem_interleave_left : ∀ {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α), a ∈ s₁ → a ∈ s₁ ⋈ s₂
-- Mathlib.Order.Directed
isTop_or_exists_gt : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] (a : α), IsTop a ∨ ∃ b, a < b
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instFiniteSubtypePSingle : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular] (j : J),
  Finite (Subtype (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).P)
-- Mathlib.Algebra.Algebra.Equiv
ULift.algEquiv_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (self : ULift.{w, v} A), ULift.algEquiv.{u, v, w} self = self.down
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.fintypeWalkingParallelPair : Fintype CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.CategoryTheory.Limits.Preserves.Ulift
/-- The functor `uliftFunctor : Type u ⥤ Type (max u v)` creates `u`-small colimits.
 -/
CategoryTheory.Limits.Types.instCreatesColimitsOfSizeUliftFunctor : CategoryTheory.CreatesColimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_vadd_eq_ofPred_exists : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β},
  ⋃ g, g +ᵥ s = {a | ∃ g, g +ᵥ a ∈ s}
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_eq_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {he : t ≠ ∅}, t.max he = t.max!
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The functor `G` has a limit if `C` has `K`-shaped limits and `(curry.obj G ⋙ lim)` has a limit.
 -/
CategoryTheory.Limits.instHasLimitProd : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)],
  CategoryTheory.Limits.HasLimit G
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RoiSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenToSpec_app_top : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) ⊤ =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f)
        (AlgebraicGeometry.Proj.basicOpen 𝒜 f).topIso.inv)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.diff_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.isCoveringMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → IsCoveringMap f
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- The centralizer of a subset of a monoid `M`.  -/
Submonoid.centralizer : {M : Type u_1} → Set M → [inst : Monoid M] → Submonoid M
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.copy_eq : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toIntLinearEquiv_symm : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {modM : Module ℤ M}
  {modM₂ : Module ℤ M₂} (e : M ≃+ M₂), e.symm.toIntLinearEquiv = e.toIntLinearEquiv.symm
-- Std.Do.SPred.SPred
Std.Do.SPred.apply_pure_cons : ∀ {σs : List (Type u)} {σ : Type u} {P : Prop} {s : σ}, ⌜P⌝ s = ⌜P⌝
-- Mathlib.Util.Delaborators
PiNotation.piNotation.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.map_id : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp},
  Std.ExtTreeMap.map (fun x v => v) t = t
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_roo' : ∀ {m n k : ℕ}, List.map (fun x => k + x) (m<...n).toList = ((k + m)<...k + n).toList
-- Mathlib.Algebra.Group.Commute.Hom
addCommute_map_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] {f : F}, Function.Injective ⇑f → ∀ {x y : M}, AddCommute (f x) (f y) ↔ AddCommute x y
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAgainst.isStableUnderCobaseChangeAlong : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P P' : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderCobaseChangeAgainst P'] ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.IsStableUnderCobaseChangeAlong f
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_mono : ∀ {α : Type u_2} (M : Matroid α), Monotone M.closure
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roc_eq_add : ∀ {m n i : ℕ}, i < n - m → (m<...=n).toList[i]! = m + 1 + i
-- Mathlib.GroupTheory.Coprod.Basic
/-- Coproduct of two additive monoids or groups.  -/
AddMonoid.Coprod : (M : Type u_1) → (N : Type u_2) → [AddZeroClass M] → [AddZeroClass N] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.asIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.IsIso f], CategoryTheory.asIso f = CategoryTheory.asIso f_1
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.inv Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q
-- Mathlib.Geometry.Manifold.Instances.Sphere
hasFDerivAt_stereoInvFunAux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v : E),
  HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
-- Init.Data.List.Sublist
List.isSuffixOf_iff_suffix : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isSuffixOf l₂ = true ↔ l₁ <:+ l₂
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.coe_support_mkOfMemSupportIff : ∀ {X : AlgebraicGeometry.Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
        ideal (X.affineBasicOpen f))
  (supportSet : Set ↥X)
  (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)),
  ↑(AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff ideal map_ideal_basicOpen supportSet
          supportSet_inter).support =
    supportSet
-- Std.Async.Signal
/-- Unix style signals for Unix and Windows.
SIGKILL and SIGSTOP are missing because they cannot be caught.
SIGBUS, SIGFPE, SIGILL, and SIGSEGV are missing because they cannot be caught safely by libuv.
SIGPIPE is not present because the runtime ignores the signal.
 -/
Std.Async.Signal : Type
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.nhds_basis_closedEBall`. -/
EMetric.nhds_basis_closed_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedEBall x)
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- Implementation: If each costructured arrow category on `G` has a terminal object, an equivalence
which is helpful for constructing a right adjoint to `G`.
 -/
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] →
            (B : D) → (A : C) → (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X A : C}
  {Y Z : CategoryTheory.Over X} (f₁ f₂ : A ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z).left),
  CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ChosenPullbacksAlong.fst Y.hom Z.hom) =
      CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ChosenPullbacksAlong.fst Y.hom Z.hom) →
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ChosenPullbacksAlong.snd Y.hom Z.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ChosenPullbacksAlong.snd Y.hom Z.hom) →
      f₁ = f₂