mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_3 : ∀ (m n : ℕ), (Int.ofNat m.succ).fdiv (Int.negSucc n) = Int.negSucc (m / n.succ)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_notMem_finset : ∀ {α : Type u_1} (a : α), MeasurableSet {s | a ∉ s}
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_le_bsup_succ : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), o.blsub f ≤ Order.succ (o.bsup f)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_zero_of_constantCoeff_zero : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {f : PowerSeries R}, PowerSeries.constantCoeff f = 0 → PowerSeries.subst 0 f = 0
-- Mathlib.Algebra.Group.Action.Units
/-- This is not the usual `smul_eq_mul` because `mulAction'` creates a diamond.

Discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/units.2Emul_action'.20diamond/near/246400399).  -/
Units.smul_eq_mul : ∀ {M : Type u_6} [inst : CommMonoid M] (u₁ u₂ : Mˣ), u₁ • u₂ = u₁ * u₂
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_div' : ∀ {r p : NNReal} [NeZero r], ↑(p / r) = ↑p / ↑r
-- Init.Grind.Lemmas
Lean.Grind.dite_cond_eq_true' : ∀ {α : Sort u} {c : Prop} {x : Decidable c} {a : c → α} {b : ¬c → α} {r : α} (h₁ : c = True), a ⋯ = r → dite c a b = r
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Frequently.forall_exists_of_atTop : ∀ {α : Type u_3} [inst : Preorder α] {p : α → Prop}, (∃ᶠ (x : α) in Filter.atTop, p x) → ∀ (a : α), ∃ b, a ≤ b ∧ p b
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.leftRel_apply : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, (QuotientGroup.leftRel s) x y ↔ x⁻¹ * y ∈ s
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.norm_mkOfCompact : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)), ‖BoundedContinuousFunction.mkOfCompact f‖ = ‖f‖
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C),
  ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Init.Prelude
/-- A fallback `Backtrackable` instance that saves no information from a state. This allows every type
to be used as a state in `EStateM`, with no rollback.

Because this is the first declared instance of `Backtrackable _ σ`, it will be picked only if there
are no other `Backtrackable _ σ` instances registered.
 -/
EStateM.nonBacktrackable : {σ : Type u} → EStateM.Backtrackable PUnit.{u + 1} σ
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonM.run : {α : Type u_1} → Lean.ShareCommon.ShareCommonM α → α
-- Mathlib.RingTheory.Localization.Integer
/-- The numerator of a fraction after clearing the denominators
of a `Finset`-indexed family of fractions.  -/
IsLocalization.integerMultiple : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → [IsLocalization M S] → {ι : Type u_4} → (s : Finset ι) → (ι → S) → ↥s → R
-- Std.Time.Zoned.RecurringRule
/-- How the transition date is specified.
 -/
Std.Time.TimeZone.TransitionRule.spec : Std.Time.TimeZone.TransitionRule → Std.Time.TimeZone.TransitionSpec
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.smul` -/
MeasureTheory.StronglyMeasurable.fun_smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i • g i
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instSubcanonicalFppfTopology : AlgebraicGeometry.Scheme.fppfTopology.Subcanonical
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.nonempty_of_affineSpan_eq_top : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P}, affineSpan k s = ⊤ → s.Nonempty
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameCases : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.tau.eq_1 : ∀ {A B : GrpCat} (f : A ⟶ B),
  GrpCat.SurjectiveOfEpiAuxs.tau f =
    Equiv.swap (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩)
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_zero : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.support 0 = ∅
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankD_findAux : ∀ {i : ℕ} {self : Batteries.UnionFind} {x : Fin self.size}, Batteries.UnionFind.rankD (self.findAux x).s i = self.rank i
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ 2 = 1
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.needAnswer.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Event.needAnswer = 1
-- Mathlib.Control.Bitraversable.Instances
Bicompl.bitraverse.eq_1 : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] (F G : Type u → Type u) [inst_1 : Traversable F]
  [inst_2 : Traversable G] {m : Type u → Type u} [inst_3 : Applicative m] {α β α' β' : Type u} (f : α → m β)
  (f' : α' → m β'), Bicompl.bitraverse F G f f' = bitraverse (traverse f) (traverse f')
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- Given a function with an invertible strict derivative at `a`, returns an `OpenPartialHomeomorph`
with `to_fun = f` and `a ∈ source`. This is a part of the inverse function theorem.
The other part `HasStrictFDerivAt.to_localInverse` states that the inverse function
of this `OpenPartialHomeomorph` has derivative `f'.symm`.  -/
HasStrictFDerivAt.toOpenPartialHomeomorph : {𝕜 : 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} →
                    {a : E} → [CompleteSpace E] → HasStrictFDerivAt f (↑f') a → OpenPartialHomeomorph E F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} {l : List α} {k : α},
  t.insertManyIfNewUnit (k :: l) = (t.insertIfNew k ()).insertManyIfNewUnit l
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charMonoidHom_apply : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (w : Multiplicative W) (v : V),
  ((BoundedContinuousFunction.charMonoidHom he hL) w) v = ↑(e ((L v) (Multiplicative.toAdd w)))
-- Mathlib.Topology.UniformSpace.Closeds
/-- When `Set` is equipped with the Hausdorff uniformity, taking the image under a uniformly
continuous map is uniformly continuous.  -/
UniformContinuous.image_hausdorff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → UniformContinuous fun x => f '' x
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- the map between the underlying types of indices  -/
ComplexShape.Embedding.f : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → ι → ι'
-- Init.Data.String.Defs
String.instDecidableEqPos.decEq : {s : String} → (x x_1 : s.Pos) → Decidable (x = x_1)
-- Mathlib.NumberTheory.Divisors
Int.dvd_of_mem_divisors : ∀ {x z : ℤ}, x ∈ z.divisors → x ∣ z
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.finite_of_toPiLocalization_pi_surjective : ∀ {ι : Type u_5} {R : ι → Type u_4} [inst : (i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)],
  Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i)) → Finite ι
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.of_mem_closure : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x y z : S},
  f.IsIntegralElem x → f.IsIntegralElem y → z ∈ Subring.closure {x, y} → f.IsIntegralElem z
-- Mathlib.Order.Closure
LowerAdjoint.closure_iSup₂_closure : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [inst : CompleteLattice α] [inst_1 : Preorder β]
  {u : β → α} (l : LowerAdjoint u) (f : (i : ι) → κ i → α),
  u (l.toFun (⨆ i, ⨆ j, u (l.toFun (f i j)))) = u (l.toFun (⨆ i, ⨆ j, f i j))
-- Mathlib.Data.Nat.Factorial.Basic
/-- `(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See
`Nat.ascFactorial_eq_div` for the version with ℕ-division.  -/
Nat.factorial_mul_ascFactorial : ∀ (n k : ℕ), n.factorial * (n + 1).ascFactorial k = (n + k).factorial
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : γ → α) (g : γ → β),
  (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t
-- Mathlib.Analysis.Convex.Between
sbtw_midpoint_of_ne : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y : P},
  x ≠ y → Sbtw R x (midpoint R x y) y
-- Mathlib.NumberTheory.MahlerMeasure
/-- If an integer non-constant polynomial has Mahler measure equal to 1 and is not a multiple of
`X`, then it is divisible by a cyclotomic polynomial.  -/
Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 →
    ¬Polynomial.X ∣ p → p.degree ≠ 0 → ∃ n, 0 < n ∧ Polynomial.cyclotomic n ℤ ∣ p
-- Mathlib.CategoryTheory.Action.Monoidal
Action.associator_inv_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y Z : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.V Y.V Z.V).inv
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt32
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_3 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDTreeMap.Const.ofList l cmp).getKey! k = default
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
          (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) h)))
-- Mathlib.RingTheory.Morita.Matrix
IsMoritaEquivalent.matrix : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (R₀ : Type u_1)
  [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] [Nonempty ι], IsMoritaEquivalent R₀ R (Matrix ι ι R)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.foldM_iter : ∀ {n : Type (max u_1 u_2) → Type u_3} {ps : Std.Do.PostShape} [inst : Monad n] [inst_1 : Std.Do.WPMonad n ps]
  {α β : Type u_2} {γ : Type (max u_1 u_2)} [inst_2 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {init : γ} {f : γ → β → n γ}
  (inv : Std.Do.Invariant it.toList γ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f b cur ⦃(fun b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := it.toList, property := ⋯ }, init)⦄
      Std.Iter.foldM f init it ⦃(fun b => inv.1 ({ «prefix» := it.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Analysis.InnerProductSpace.Calculus
Homeomorph.contDiff_unitBall : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  ContDiff ℝ ↑n fun x => ↑(Homeomorph.unitBall x)
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithLawson α)
-- Mathlib.Logic.Relation
Relation.ReflTransGen.le_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, r ≤ Relation.ReflTransGen r
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `(C, r)`-Hölder and `(C, s)`-Hölder,
then it is `(C, r * t₁ + s * t₂)`-Hölder for all `t₁ t₂ : ℝ≥0` such that
`t₁ + t₂ = 1`.  -/
HolderWith.interpolate_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C s t₁ t₂ : NNReal}, HolderWith C r f → HolderWith C s f → t₁ + t₂ = 1 → HolderWith C (r * t₁ + s * t₂) f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `g` is a power series over a complete local ring,
such that its image in the residue field is not zero, then there is a natural isomorphism
`A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g)` where `f` is `PowerSeries.weierstrassDistinguished g`.  -/
PowerSeries.algEquivQuotientWeierstrassDistinguished : {A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A] →
        {g : PowerSeries A} →
          (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0) →
            (Polynomial A ⧸ Ideal.span {g.weierstrassDistinguished hg}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {g}
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.exists_of_le_vertexCoverNum : ∀ {V : Type u_1} {G : SimpleGraph V} (n : ℕ),
  G.vertexCoverNum ≤ ↑n → ↑n ≤ ENat.card V → ∃ s, s.encard = ↑n ∧ G.IsVertexCover s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_le_coe : ∀ {α : Type u} [inst : One α] [inst_1 : LE α] {a : α}, 1 ≤ ↑a ↔ 1 ≤ a
-- Mathlib.Logic.Equiv.List
Encodable.decodeList_encodeList_eq_self : ∀ {α : Type u_1} [inst : Encodable α] (l : List α), Encodable.decodeList (Encodable.encodeList l) = some l
-- Mathlib.Order.Filter.Map
Filter.image_mem_of_mem_comap : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {c : β → α},
  Set.range c ∈ f → ∀ {W : Set β}, W ∈ Filter.comap c f → c '' W ∈ f
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_add_eq_sum_add_of_exists : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} {b₁ b₂ : M},
  ∀ a ∈ s, f a + b₁ = f a + b₂ → ∑ a ∈ s, f a + b₁ = ∑ a ∈ s, f a + b₂
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
/-- An object property is local if it holds for `X` if and only if it holds for all `Uᵢ` where
`{Uᵢ}` is a `K`-cover of `X`.  -/
CategoryTheory.ObjectProperty.IsLocal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.Precoverage C → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.dist_edist : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), dist f g = (edist f g).toReal
-- Mathlib.Topology.Inseparable
/-- A subset `S` of a topological space is stable under specialization
if `x ∈ S → y ∈ S` for all `y ⤳ x`.  -/
StableUnderGeneralization : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Data.Finset.Sups
Finset.disjSups_empty_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s : Finset α}, s.disjSups ∅ = ∅
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The restriction of a compatible family is compatible.  -/
CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) {x : CategoryTheory.Presieve.FamilyOfElements P R₂},
  x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).Compatible
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α}, Std.DHashMap.Raw.Const.get? ∅ a = none
-- Mathlib.Algebra.CubicDiscriminant
Cubic.d_of_eq : ∀ {R : Type u_1} {P Q : Cubic R} [inst : Semiring R], P.toPoly = Q.toPoly → P.d = Q.d
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.ext : ∀ {C : Type u_1} {ι : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} ι} {inst_2 : CategoryTheory.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.HasShift C ℤ} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {x y : X.Hom Y}, x.hom = y.hom → x = y
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkGateCached.go_eval_eq_mkGate_eval : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput}, ⟦assign, Std.Sat.AIG.mkGateCached.go aig input⟧ = ⟦assign, aig.mkGate input⟧
-- Mathlib.LinearAlgebra.Basis.Defs
/-- If `b` is a basis for `M` and `b'` a basis for `M'`,
and `f`, `g` form a bijection between the basis vectors,
`b.equiv' b' f g hf hg hgf hfg` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `f (b i)`.
 -/
Module.Basis.equiv' : {ι' : Type u_2} →
  {ι : Type u_10} →
    {R : Type u_14} →
      {M : Type u_15} →
        {M' : Type u_16} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : AddCommMonoid M'] →
                  [inst_4 : Module R M'] →
                    (b : Module.Basis ι R M) →
                      (b' : Module.Basis ι' R M') →
                        [SMulCommClass R R M'] →
                          (f : M → M') →
                            (g : M' → M) →
                              (∀ (i : ι), f (b i) ∈ Set.range ⇑b') →
                                (∀ (i : ι'), g (b' i) ∈ Set.range ⇑b) →
                                  (∀ (i : ι), g (f (b i)) = b i) → (∀ (i : ι'), f (g (b' i)) = b' i) → M ≃ₗ[R] M'
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.vcomp_eq_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.vcomp α β = CategoryTheory.CategoryStruct.comp α β
-- Mathlib.Data.PEquiv
PEquiv.single_trans_single : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  (a : α) (b : β) (c : γ), (PEquiv.single a b).trans (PEquiv.single b c) = PEquiv.single a c
-- Aesop.Util.Basic
Aesop.Name.ofComponents : List Lean.Name → Lean.Name
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarContent.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ K₀_1 : TopologicalSpace.PositiveCompacts G),
  K₀ = K₀_1 → MeasureTheory.Measure.haar.haarContent K₀ = MeasureTheory.Measure.haar.haarContent K₀_1
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_lineMap_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → ∀ {t : R}, 0 ≤ t → s.WSameSide y ((AffineMap.lineMap x y) t)
-- Lean.Compiler.Specialize
_private.Lean.Compiler.Specialize.0.Lean.Compiler.elabSpecArgs : Lean.Name → Array Lean.Syntax → Lean.MetaM (Array ℕ)
-- Mathlib.Algebra.Homology.QuasiIso
/-- A morphism of homological complexes `f : K ⟶ L` is a quasi-isomorphism in degree `i`
when it induces a quasi-isomorphism of short complexes `K.sc i ⟶ L.sc i`.  -/
QuasiIsoAt : {ι : Type u_1} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} → (K ⟶ L) → (i : ι) → [K.HasHomology i] → [L.HasHomology i] → Prop
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.top_eq_univ : ∀ {α : Type u_1} [inst : Fintype α], ⊤ = Finset.univ
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_toReal : ∀ {a : ENNReal}, a ≠ ⊤ → ENNReal.ofReal a.toReal = a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (P : Ideal (NumberField.RingOfIntegers K))
  [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})], P = Ideal.span {hζ.toInteger - 1}
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.sumElim_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {ι' : Type u_4} {y : ι' → A},
  AlgebraicIndependent R (Sum.elim y x) ↔
    AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(Algebra.adjoin R (Set.range x))) y
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.ppOrigin : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Meta.Origin → m Lean.MessageData
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_dvd_true : ∀ {a b a' b' c : ℤ}, Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.mul c = b' → a ∣ b
-- Mathlib.Algebra.MvPolynomial.Basic
/-- **Alias** of `MvPolynomial.coeff_addMonoidAlgebraMap`. -/
MvPolynomial.coeff_mapRange : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (g : S₁ →+ R)
  (φ : MvPolynomial σ S₁) (m : σ →₀ ℕ), MvPolynomial.coeff m (AddMonoidAlgebra.map g φ) = g (MvPolynomial.coeff m φ)