mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =O[l] g → ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_empty : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X) in ∅, f x ∂[B; μ] = 0
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.typeFormer.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.PatternArgKind.typeFormer = 1
-- Init.Data.Fin.Fold
Fin.foldlM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] {n k : ℕ} (w : n = k) (f : α → Fin n → m α),
  Fin.foldlM n f = Fin.foldlM k fun x i => f x (Fin.cast ⋯ i)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.resolveInterestWaiter : Std.Async.Waiter Bool → Bool → BaseIO Bool
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instTop.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := ⋯ } }
-- Mathlib.Data.Holor
/-- Left associator for `Holor`  -/
Holor.assocLeft : {α : Type} → {ds₁ ds₂ ds₃ : List ℕ} → Holor α (ds₁ ++ (ds₂ ++ ds₃)) → Holor α (ds₁ ++ ds₂ ++ ds₃)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.rpow_neg_one_le_rpow_neg_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {a b : A},
  a ≤ b → autoParam (IsStrictlyPositive a) CStarAlgebra.rpow_neg_one_le_rpow_neg_one._auto_1 → b ^ (-1) ≤ a ^ (-1)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.le_precoverage_morphismProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C},
  K ≤ K.morphismProperty.precoverage
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.filtration_bot : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : OrderBot ι], f.filtration ⊥ = A
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instIsSimpleOrderOfNonemptyOfIndiscreteTopology : ∀ {α : Type u_2} [inst : TopologicalSpace α] [Nonempty α] [IndiscreteTopology α],
  IsSimpleOrder (TopologicalSpace.Opens α)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.ext_iff : ∀ {D : Type u_1} {Q : Type u_2} {x y : D ≀ᵣ Q}, x = y ↔ x.left = y.left ∧ x.right = y.right
-- Mathlib.Data.Int.DivMod
Int.mul_ediv_le_mul_ediv_assoc : ∀ {a : ℤ}, 0 ≤ a → ∀ (b : ℤ) {c : ℤ}, 0 ≤ c → a * (b / c) ≤ a * b / c
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Array.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.instInhabited : {ι : Type u_1} →
  {𝕜 : Type u_3} → [inst : RCLike 𝕜] → [inst_1 : Fintype ι] → Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι))
-- Mathlib.Data.Finset.Basic
Finset.filter_inter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s t : Finset α),
  Finset.filter p s ∩ t = Finset.filter p (s ∩ t)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.substrEq.loop : String → String → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → Bool
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.join_join : ∀ {α : Type u} (SS : Stream'.Seq (Stream'.Seq1 (Stream'.Seq1 α))),
  SS.join.join = (Stream'.Seq.map Stream'.Seq1.join SS).join
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.pi_map : ∀ {ι : Type u_6} {X : ι → Type u_7} {Y : ι → Type u_8} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i},
  (∀ (i : ι), IsHomeomorph (f i)) → IsHomeomorph fun x i => f i (x i)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.restrictAppIso_smul_Spec : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {S : CommRingCat} (f : R ⟶ S)
  [inst : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map f)] {U : (AlgebraicGeometry.Spec S).Opens}
  (r : ↑R) (x : ↑((M.restrict (AlgebraicGeometry.Spec.map f)).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Modules.restrictAppIso (AlgebraicGeometry.Spec.map f) M U).hom)
      ((CategoryTheory.ConcreteCategory.hom f) r • x) =
    r •
      (CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.Scheme.Modules.restrictAppIso (AlgebraicGeometry.Spec.map f) M U).hom)
        x
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
norm_cexp_neg_mul_sq : ∀ (b : ℂ) (x : ℝ), ‖Complex.exp (-b * ↑x ^ 2)‖ = Real.exp (-b.re * x ^ 2)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_inf_le : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {I J : Ideal R} [RingHomClass F R S], Ideal.map f (I ⊓ J) ≤ Ideal.map f I ⊓ Ideal.map f J
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.negOne_mem_adjoinNegOne : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] (𝒢 : Subgroup (GL n R)),
  -1 ∈ 𝒢.adjoinNegOne
-- Mathlib.Logic.Small.Set
small_image : ∀ {α : Type u1} {β : Type u2} (f : α → β) (s : Set α) [Small.{u, u1} ↑s], Small.{u, u2} ↑(f '' s)
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_singleton_mem_of_forall_separating : ∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] [Nonempty α] (p : Set α → Prop)
  [HasCountableSeparatingOn α p Set.univ], (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ x, {x} ∈ l
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- If `f` is a linear map injective on the span of the range of `v`, then the family `f ∘ v`
is linearly independent if and only if the family `v` is linearly independent.
See `LinearMap.linearIndependent_iff_of_disjoint` for the version with `Set.InjOn` replaced
by `Disjoint` when working over a ring.  -/
LinearMap.linearIndependent_iff_of_injOn : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Set.InjOn ⇑f ↑(Submodule.span R (Set.range v)) → (LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_succ? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.succ? a = some b → Std.PRange.UpwardEnumerable.LT a b
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_mul_I : ∀ (x : ℂ), Complex.tanh (x * Complex.I) = Complex.tan x * Complex.I
-- Mathlib.CategoryTheory.Monad.Products
/-- The equivalence from coalgebras for the product comonad to the over category.  -/
CategoryTheory.coalgebraEquivOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
        (CategoryTheory.prodComonad X).Coalgebra ≌ CategoryTheory.Over X
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- An auxiliary definition used only to construct the true `NormedAddCommGroup` (and `Metric`)
structure provided by `Matrix.instMetricSpaceL2Op` and `Matrix.instNormedAddCommGroupL2Op`.  -/
Matrix.l2OpNormedAddCommGroupAux : {𝕜 : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} → [RCLike 𝕜] → [Fintype m] → [Fintype n] → [DecidableEq n] → NormedAddCommGroup (Matrix m n 𝕜)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁), ↑e x = e x
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- `N.IsFinitelyNormallyGenerated` says that the subgroup `N` is the normal closure
of a finite set.  -/
Subgroup.IsFinitelyNormallyGenerated : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
-- Init.Sym.Lemmas
Lean.Sym.dite_true : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) {ht : c}, dite c a b = a ht
-- Mathlib.MeasureTheory.Integral.IntegrableOn
Continuous.aestronglyMeasurable_of_compactSpace : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [CompactSpace α] [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  {μ : MeasureTheory.Measure α} {f : α → β}, Continuous f → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Topology.Algebra.UniformMulAction
/-- A `DistribSMul` that is continuous on a uniform group is uniformly continuous.
This can't be an instance due to it forming a loop with
`UniformContinuousConstSMul.instContinuousConstSMul`  -/
uniformContinuousConstSMul_of_continuousConstSMul : ∀ (R : Type u) (M : Type v) [inst : AddGroup M] [inst_1 : DistribSMul R M] [inst_2 : UniformSpace M]
  [IsUniformAddGroup M] [ContinuousConstSMul R M], UniformContinuousConstSMul R M
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.applyCell : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      [inst : Ord α] →
        (k : α) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
              δ
-- Lean.Meta.Tactic.Grind.EMatchAction
Lean.Meta.Grind.Action.instantiate : Lean.Meta.Grind.Action
-- Mathlib.Topology.Algebra.GroupWithZero
/-- The map `fun x ↦ x⁻¹` is continuous at all nonzero points.  -/
ContinuousInv₀.continuousAt_inv₀ : ∀ {G₀ : Type u_4} {inst : Zero G₀} {inst_1 : Inv G₀} {inst_2 : TopologicalSpace G₀} [self : ContinuousInv₀ G₀] ⦃x : G₀⦄,
  x ≠ 0 → ContinuousAt Inv.inv x
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some ⁻¹' Set.Ioo ↑b ↑a = Set.Ioo b a
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₃ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₃ =
    CategoryTheory.Functor.whiskerRight φ CategoryTheory.ShortComplex.π₃
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.instBraidedTransportedInverseEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [inst_3 : CategoryTheory.BraidedCategory C] →
              (CategoryTheory.Monoidal.equivalenceTransported e).inverse.Braided
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.mono : ∀ {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Mono f
-- Mathlib.Order.Notation
top_nonempty : ∀ (α : Type u_1) [Top α], Nonempty α
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If a function is equal to a constant at a set of points that accumulates to `x`,
then its derivative at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point.  -/
deriv_zero_of_frequently_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {c : F}, (∃ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, f y = c) → deriv f x = 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.sliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos) (p : s.Pos) (hp : p ≤ startPos),
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat (p.sliceFrom startPos hp) (p.sliceFrom endPos ⋯)
-- Lean.Server.AsyncList
Lean.AsyncList.getFinishedPrefixWithTimeout : {ε α : Type} →
  Lean.AsyncList ε α → UInt32 → optParam (List (Lean.Server.ServerTask Unit)) [] → BaseIO (List α × Option ε × Bool)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_inf_mul_relrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B C : IntermediateField F E),
  A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
-- Mathlib.Order.KrullDimension
Order.height_enat : ∀ (n : ℕ∞), Order.height n = n
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The isomorphism `∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X`.  -/
CategoryTheory.Limits.Sigma.isoColimit : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] →
          [inst_2 : CategoryTheory.Limits.HasColimit X] →
            (∐ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.colimit X
-- Mathlib.Data.Sym.Basic
Sym.coe_cons : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n) (a : α), ↑(a ::ₛ s) = a ::ₘ ↑s
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is algebraic, then an intermediate field of `E / F` is equal to the separable closure
of `F` in `E` if and only if it is separable over `F`, and `E` is purely inseparable
over it.  -/
eq_separableClosure_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E]
  (L : IntermediateField F E), L = separableClosure F E ↔ Algebra.IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E
-- Mathlib.RingTheory.Finiteness.Quotient
QuotientMapQuotient.isNoetherian : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  [IsNoetherian A B], IsNoetherian (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.natEnd.eq_2 : Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.Γ'.cons = true
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.dropWhile : ∀ (p : Char → Bool) {s : Substring.Raw}, s.Valid → (s.dropWhile p).Valid
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- If `S : K → J` is a family of objects of cardinality `< κ` in a `κ`-filtered category,
this is a choice of map `S k ⟶ max S hS` for any `k : K`.  -/
CategoryTheory.IsCardinalFiltered.toMax : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [inst_1 : CategoryTheory.IsCardinalFiltered J κ] →
          {K : Type u'} →
            (S : K → J) → (hS : HasCardinalLT K κ) → (k : K) → S k ⟶ CategoryTheory.IsCardinalFiltered.max S hS
-- Mathlib.Topology.Constructions
Continuous.finInsertNth : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] (i : Fin (n + 1)) {f : X → A i}
  {g : X → (j : Fin n) → A (i.succAbove j)}, Continuous f → Continuous g → Continuous fun a => i.insertNth (f a) (g a)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.stronglyMeasurable_limitProcess : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {E : Type u_4} [inst_1 : Zero E]
  [inst_2 : TopologicalSpace E] {ℱ : MeasureTheory.Filtration ι m} {f : ι → Ω → E} {μ : MeasureTheory.Measure Ω},
  MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.limitProcess f ℱ μ)
-- Mathlib.Data.Set.Constructions
/-- The smallest set of sets containing `S` which is closed under finite intersections.  -/
FiniteInter.finiteInterClosure : {α : Type u_1} → Set (Set α) → Set (Set α)
-- Mathlib.Topology.ClusterPt
IsClosed.mem_of_mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {l : X} {s : Set X} {f : α → X} {b : Filter α},
  IsClosed s → MapClusterPt l b f → (∀ᶠ (x : α) in b, f x ∈ s) → l ∈ s
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_counitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal Cᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).counitIso.inv.app X =
    (match X with
      | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x)
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.whiskerRight_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} {f g : a ⟶ b}
  (f_1 : f ⟶ g) (y : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRight f_1 y).iso.inv = CategoryTheory.Bicategory.whiskerRight f_1.iso.inv y.of
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A unique identifier corresponding to the origin.  -/
Lean.Meta.Origin.key : Lean.Meta.Origin → Lean.Name
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.remainingToString.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.remainingToString = String.Pos.Raw.extract s i s.rawEndPos
-- Lean.MetavarContext
Lean.MonadMCtx.getMCtx : {m : Type → Type} → [self : Lean.MonadMCtx m] → m Lean.MetavarContext
-- Mathlib.Topology.UniformSpace.Defs
isUniformInducing_iff : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
  IsUniformInducing f ↔ Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
-- Mathlib.Data.List.Basic
List.foldl_fixed : ∀ {α : Type u} {β : Type v} {a : α} (l : List β), List.foldl (fun a x => a) a l = a
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.  -/
aux_hasSum_of_le_geometric : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {r C : ℝ} {f : ℕ → α},
  r < 1 → (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) → HasSum (fun n => C * r ^ n) (C / (1 - r))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- **Alias** of `PresheafOfModules.pushforward₀Obj`.

---

Implementation of `pushforward₀`.  -/
PresheafOfModules.pushforward₀_obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (R : CategoryTheory.Functor Dᵒᵖ RingCat) → PresheafOfModules R → PresheafOfModules (F.op.comp R)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toHomeomorph_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), e.symm.toHomeomorph = e.toHomeomorph.symm
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α],
  DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp =
    { smul := fun c f => (MeasureTheory.Lp.compMeasurePreserving (fun x => DomMulAct.mk.symm c • x) ⋯) f }
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_toRingHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- A category has all countable colimits if every functor `J ⥤ C` with a `CountableCategory J`
instance and `J : Type` has a colimit.
 -/
CategoryTheory.Limits.HasCountableColimits : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Init.Prelude
Nat.le_refl : ∀ (n : ℕ), n ≤ n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey! k' = k
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.isProper_pairing_iff : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.pairing.IsProper ↔ h.IsProper
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableAt.fun_finsetProd`. -/
DifferentiableAt.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → DifferentiableAt 𝕜 (fun x => ∏ i ∈ u, f i x) x
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Right whiskering of a lax natural transformation and a modification.  -/
CategoryTheory.Lax.LaxTrans.whiskerRight : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (η ⟶ θ) → (ι : G ⟶ H) → CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι
-- Mathlib.Topology.Order.WithTop
WithTop.tendsto_untopD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (d : ι)
  {a : WithTop ι}, a ≠ ⊤ → Filter.Tendsto (WithTop.untopD d) (nhds a) (nhds (WithTop.untopD d a))
-- Mathlib.Order.Filter.Map
Filter.map_const : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [f.NeBot] {c : β}, Filter.map (fun x => c) f = pure c
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_eq : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {f : γ → (a : α) → β a → γ} {init : γ},
  Std.DHashMap.Raw.fold f init l =
    Array.foldl (fun acc l => Std.DHashMap.Internal.AssocList.foldl f acc l) init l.buckets
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsGT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Ioo c a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.Order.Heyting.Basic
inf_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), a ⊓ aᶜ = ⊥