mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos.eq_1 : ∀ (x : ℝ), Real.cos x = (Complex.cos ↑x).re
-- Mathlib.Order.Max
Prod.isBot_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x ↔ IsBot x.1 ∧ IsBot x.2
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.coe_toLinearMap : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (f : E₁ →ₚ[R] E₂), ⇑f.toLinearMap = ⇑f
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.algHom_bijective₂ : ∀ {K : Type u_1} {L : Type u_2} {R : Type u_3} [inst : CommRing K] [IsDomain K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [Module.IsTorsionFree K L] [inst_5 : DivisionRing R] [inst_6 : Algebra K R]
  [Algebra.IsAlgebraic K L] (f : L →ₐ[K] R) (g : R →ₐ[K] L), Function.Bijective ⇑f ∧ Function.Bijective ⇑g
-- Mathlib.Computability.AkraBazzi.AkraBazzi
/-- The **Akra-Bazzi theorem**: `T ∈ Θ(n^p (1 + ∑_u^n g(u) / u^{p+1}))`  -/
AkraBazziRecurrence.isTheta_asympBound : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), T =Θ[Filter.atTop] AkraBazziRecurrence.asympBound g a b
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), (⨅ i, f i).compl = ⨅ i, (f i).compl
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- Constructs a `SubPDIdeal` given an ideal `J` satisfying `hI.IsSubDPIdeal J`.  -/
DividedPowers.SubDPIdeal.mk' : {A : Type u_1} →
  [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → {J : Ideal A} → hI.IsSubDPIdeal J → hI.SubDPIdeal
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Add G] [μ.IsAddLeftInvariant],
  MeasureTheory.VAddInvariantMeasure G G μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f = ∅ ↔ t.erase k = ∅ ∧ f (Std.ExtDTreeMap.Const.get? t k) = none
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_preconnected : ∀ {n : ℕ}, (SimpleGraph.cycleGraph n).Preconnected
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
  {X Y : CategoryTheory.Idempotents.Karoubi C} (f : X ⟶ Y),
  ((CategoryTheory.Idempotents.FunctorExtension₁.obj F).map f).f = (F.map f.f).f
-- Mathlib.Algebra.Star.SelfAdjoint
IsUnit.isSelfAdjoint_conjugate_iff' : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {a u : R},
  IsUnit u → (IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a)
-- Aesop.Script.Step
Aesop.Script.LazyStep.tacticBuilders_ne : ∀ (self : Aesop.Script.LazyStep), 0 < self.tacticBuilders.size
-- Mathlib.Data.TypeVec
TypeVec.comp.eq_1 : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} {γ : TypeVec.{w} n} (g : β.Arrow γ) (f : α.Arrow β) (i : Fin2 n)
  (x : α i), TypeVec.comp g f i x = g i (f i x)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.comp_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Y]
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.diag Y) = CategoryTheory.Limits.prod.lift f f
-- Std.Time.Duration
/-- Adds a `Nanosecond.Offset` to a `Duration`
 -/
Std.Time.Duration.addNanoseconds : Std.Time.Duration → Std.Time.Nanosecond.Offset → Std.Time.Duration
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.Measure.toFinite.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [inst : MeasureTheory.SFinite μ], μ.toFinite = μ_1.toFinite
-- Mathlib.Topology.Neighborhoods
tendsto_atTop_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} [Nonempty α] [inst_2 : SemilatticeSup α] {f : α → X},
  Filter.Tendsto f Filter.atTop (nhds x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U
-- Lean.Meta.ArgsPacker
/-- Given types `#[t₁, t₂,…]`, returns the type `t₁ ⊕' t₂ …`.  -/
Lean.Meta.ArgsPacker.Mutual.packType : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.instInvOneClass : {n : Type u'} → {α : Type v} → [Fintype n] → [DecidableEq n] → [CommRing α] → InvOneClass (Matrix n n α)
-- Mathlib.Topology.Sequences
FirstCountableTopology.seq_compact_of_compact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] [CompactSpace X], SeqCompactSpace X
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_equal : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {t₁ t₂ : L.Term α} {x : α → M},
  (t₁.equal t₂).Realize x ↔ FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Build the `grw` discrimination tree?  -/
Mathlib.Tactic.ClickSuggestions.Choice.grw : Mathlib.Tactic.ClickSuggestions.Choice → Bool
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.nnnorm_fst_eq_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.1‖₊ = ‖a.toProd.2‖₊
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.restrict.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w}
  [inst_1 : SizeOf C] [inst_2 : (a : C) → SizeOf (ι a)] {X Y : C} (f : X ⟶ Y)
  (a : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y),
  sizeOf (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f a) =
    1 + sizeOf X + sizeOf Y + sizeOf f + sizeOf a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipPrefix?_string_empty : ∀ {s : String.Slice}, s.skipPrefix? "" = some s.startPos
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- The volume of the image measured by Euclidean Hausdorff measure is equal to the Lebesgue measure
scaled by `LinearMap.normDet`.
 -/
LinearMap.euclideanHausdorffMeasure_image_eq_normDet_mul_volume : ∀ {U : Type u_5} {V : Type u_6} [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : FiniteDimensional ℝ U] [inst_3 : NormedAddCommGroup V] [inst_4 : InnerProductSpace ℝ V]
  [inst_5 : MeasurableSpace U] [inst_6 : BorelSpace U] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  (f : U →ₗ[ℝ] V) (s : Set U),
  (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (⇑f '' s) =
    ENNReal.ofReal f.normDet * MeasureTheory.volume s
-- Mathlib.CategoryTheory.EqToHom
/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.  -/
CategoryTheory.eqToHom_iso_inv_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
  {j j' : β} (w : j = j') {Z : C} (h : f j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j').inv h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.inl_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc h k w) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.isIso_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupCohomology X.X₂ n) →
    CategoryTheory.Limits.IsZero (groupCohomology X.X₂ (n + 1)) →
      CategoryTheory.IsIso (groupCohomology.δ hX n (n + 1) ⋯)
-- Plausible.Gen
Plausible.instPartialOrderExceptGenError : {α : Type u_1} → Lean.Order.PartialOrder (Except Plausible.GenError α)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_abs_eq_abs_num : ∀ (q : ℚ), |q|.num = |q.num|
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If for each `x : α`, exactly one of `g +ᵥ x`, `g : G`, belongs to a measurable set
`s`, then `s` is a fundamental domain for the additive action of `G` on `α`.  -/
MeasureTheory.IsAddFundamentalDomain.mk' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.NullMeasurableSet s μ → (∀ (x : α), ∃! g, g +ᵥ x ∈ s) → MeasureTheory.IsAddFundamentalDomain G s μ
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.nnnorm_approxOn_le : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ),
  ‖(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
-- Mathlib.Data.Prod.Basic
Prod.swap_leftInverse : ∀ {α : Type u_1} {β : Type u_2}, Function.LeftInverse Prod.swap Prod.swap
-- Init.Data.Rat.Lemmas
Rat.intCast_add : ∀ (a b : ℤ), ↑(a + b) = ↑a + ↑b
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.toWorkDoneProgressParams : Lean.Lsp.CodeAction → Lean.Lsp.WorkDoneProgressParams
-- Init.SizeOf
Lean.ParserDescr.unicodeSymbol.sizeOf_spec : ∀ (val asciiVal : String) (preserveForPP : Bool),
  sizeOf (Lean.ParserDescr.unicodeSymbol val asciiVal preserveForPP) =
    1 + sizeOf val + sizeOf asciiVal + sizeOf preserveForPP
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `AddMonoidAlgebra.coeff_mul`. -/
AddMonoidAlgebra.mul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] [inst_2 : DecidableEq M]
  (x y : AddMonoidAlgebra R M) (m : M),
  (x * y).coeff m = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => if m₁ + m₂ = m then r₁ * r₂ else 0
-- Mathlib.Order.Hom.BoundedLattice
/-- `Subtype.val` as a `BoundedLatticeHom`.  -/
BoundedLatticeHom.subtypeVal : {β : Type u_3} →
  [inst : Lattice β] →
    [inst_1 : BoundedOrder β] →
      {P : β → Prop} →
        (Pbot : P ⊥) →
          (Ptop : P ⊤) →
            (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) →
              (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) → BoundedLatticeHom { x // P x } β
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i},
  HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') x
-- Mathlib.Probability.Kernel.Posterior
/-- If `κ ω ≪ κ ∘ₘ μ` for `μ`-almost every `ω`, then for `κ ∘ₘ μ`-almost every `x`,
`κ†μ x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x)`.
This is a form of **Bayes' theorem**.
The condition is true for example for countable `Ω`.  -/
ProbabilityTheory.posterior_eq_withDensity : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ,
      (ProbabilityTheory.posterior κ μ) x =
        μ.withDensity fun ω => κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) ω x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List (α × β)} {k : α}, (t.insertMany l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.NumberTheory.Padics.Complex
/-- `𝓞_ℂ_[p]` is the ring of integers of `ℂ_[p]`.  -/
PadicComplexInt.integers : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Valued.v.Integers ↥𝓞_ℂ_[p]
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.toNonUnitalStarAlgHom_restrictScalars : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : Module S A] [inst_6 : Module S B] [inst_7 : Module R A] [inst_8 : Module R B] [inst_9 : IsScalarTower R S A]
  [inst_10 : IsScalarTower R S B] [inst_11 : Star A] [inst_12 : Star B] (e : A ≃⋆ₐ[S] B),
  (StarAlgEquiv.restrictScalars R e).toNonUnitalStarAlgHom =
    NonUnitalStarAlgHom.restrictScalars R e.toNonUnitalStarAlgHom
-- Init.Meta.Defs
Lean.Name.instDecidableEq : DecidableEq Lean.Name
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymmPart.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] {n : ℕ} (μ : n.Partition),
  MvPolynomial.esymmPart σ R μ = (Multiset.map (MvPolynomial.esymm σ R) μ.parts).prod
-- Mathlib.Topology.Compactness.Lindelof
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is Lindelöf
if and only if `s` is compact.  -/
Topology.IsInducing.isLindelof_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsInducing f → (IsLindelof s ↔ IsLindelof (f '' s))
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.neg_add : ∀ {R : Type u_2} [inst : CommRing R] {a₁ a₂ b₁ b₂ : R}, -a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂
-- Std.Http.Protocol.H1.Parser
/-- Checks if a byte is optional whitespace (`OWS = SP / HTAB`, RFC 9110 §5.6.3).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.isOwsByte : UInt8 → Bool
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_neg_right : ∀ {R : Type u_1} [inst : CommRing R] (a b : Polynomial R), a.wronskian (-b) = -a.wronskian b
-- Mathlib.Order.Preorder.Finsupp
Finsupp.partialorder : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [PartialOrder M] → PartialOrder (ι →₀ M)
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupComap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H' : Subgroup G'),
  f.subgroupComap H' = f.submonoidComap H'.toSubmonoid
-- Mathlib.Topology.Bases
/-- A separable space is one with a countable dense subset, available through
`TopologicalSpace.exists_countable_dense`. If `α` is also known to be nonempty, then
`TopologicalSpace.denseSeq` provides a sequence `ℕ → α` with dense range, see
`TopologicalSpace.denseRange_denseSeq`.

If `α` is a uniform space with countably generated uniformity filter (e.g., an `EMetricSpace`), then
this condition is equivalent to `SecondCountableTopology α`. In this case the
latter should be used as a typeclass argument in theorems because Lean can automatically deduce
`TopologicalSpace.SeparableSpace` from `SecondCountableTopology` using
`TopologicalSpace.SecondCountableTopology.to_separableSpace`, but deducing
`SecondCountableTopology` from `TopologicalSpace.SeparableSpace` requires more assumptions.
 -/
TopologicalSpace.SeparableSpace : (α : Type u) → [t : TopologicalSpace α] → Prop
-- Mathlib.Data.Fin.SuccPredOrder
Fin.instSuccOrder : {n : ℕ} → SuccOrder (Fin n)
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The projection from a trivial fiber bundle to its base is open.  -/
IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} [Nonempty F],
  IsHomeomorphicTrivialFiberBundle F proj → Topology.IsQuotientMap proj
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Computability.Encoding
/-- Deprecated: Use `inferInstanceAs (Fintype Γ)` instead.  -/
Computability.FinEncoding.ΓFin : {α : Type u} → {Γ : Type v} → [h : Fintype Γ] → Computability.Encoding α Γ → Fintype Γ
-- Mathlib.Topology.GDelta.MetrizableSpace
IsGδ.setOfPred_continuousAt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.PseudoMetrizableSpace Y] (f : X → Y), IsGδ {x | ContinuousAt f x}
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₄]
  [inst_8 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_9 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₄]
  [inst_10 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₃ F₄],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₃ F₄)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₃ F₄))
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₃ F₄)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₂ F₃ F₄))
      (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₄)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Run monadic function `f` on each element of the tree (in increasing order).  -/
RBTree.RBSet.forM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {cmp : α → α → Ordering} → [Monad m] → (α → m PUnit.{u_1 + 1}) → RBTree.RBSet α cmp → m PUnit.{u_1 + 1}
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ (S : Submonoid M) (x : M), x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Order.Hom.Lattice
/-- The type of `⊔`-preserving functions from `α` to `β`.  -/
SupHom : (α : Type u_6) → (β : Type u_7) → [Max α] → [Max β] → Type (max u_6 u_7)
-- Mathlib.Topology.Constructions
Function.Surjective.isEmbedding_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {n : Type u_9} {m : Type u_10} (f : m → n),
  Function.Surjective f → Topology.IsEmbedding fun x => x ∘ f
-- Lean.Parser.Extra
Lean.Parser.manyIndent.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {c : ℕ}, (Std.HashMap.Raw.emptyWithCapacity c).size = 0
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1} [inst : SizeOf α]
  [inst_1 : SizeOf β] (inner : Std.DTreeMap.Raw α (fun x => β) cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- An element of the comma category `Comma (𝟭 (C ⥤ D)) (Functor.const C)` can be seen as a
functor `WithTerminal C ⥤ D`.  -/
CategoryTheory.WithTerminal.ofCommaObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C) →
          CategoryTheory.Functor (CategoryTheory.WithTerminal C) D
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
IsConjRoot.eq_1 : ∀ (R : Type u_1) {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x y : A),
  IsConjRoot R x y = (minpoly R x = minpoly R y)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instNatCast : {α : Type u_2} → [inst : Preorder α] → [NatCast α] → NatCast (NonemptyInterval α)
-- Lean.Elab.Arg
Lean.Elab.Term.instInhabitedNamedArg : Inhabited Lean.Elab.Term.NamedArg
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.ext_iff : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {s t : SSet.prodStdSimplex.pairingCore.Type₁ k n}, s = t ↔ s.x = t.x
-- Mathlib.Order.Filter.Basic
/-- `GenerateSets g s`: `s` is in the filter closure of `g`.  -/
Filter.GenerateSets : {α : Type u} → Set (Set α) → Set α → Prop
-- Init.Data.ULift
instSubsingletonULift : ∀ {α : Type u_1} [Subsingleton α], Subsingleton (ULift.{u_2, u_1} α)
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
/-- The action on an additive submonoid corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
AddSubmonoid.pointwiseMulAction : {M : Type u_3} →
  {A : Type u_4} → [inst : Monoid M] → [inst_1 : AddMonoid A] → [DistribMulAction M A] → MulAction M (AddSubmonoid A)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i ≤ j),
  CategoryTheory.SmallObject.SuccStruct.ofCocone.map c i i ⋯ hi =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.SuccStruct.ofCocone.obj c i)