mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.coe_starClosure : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A),
  ↑S.starClosure = ↑(S ⊔ star S)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α}, (m₁.diff m₂ ⋯).getKey? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else m₁.getKey? k
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_insert_le_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp ((t.insert k).min ⋯) (t.min he)).isLE = true
-- Lean.Meta.Basic
Lean.Meta.withLocalInstancesImp : {α : Type} → List Lean.LocalDecl → Lean.MetaM α → Lean.MetaM α
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- All eigenvalues are generalized eigenvalues.  -/
Module.End.hasGenEigenvalue_of_hasEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, 0 < k → f.HasEigenvalue μ → f.HasGenEigenvalue μ k
-- Std.Time.Duration
/-- Represents a time interval with nanoseconds precision.
 -/
Std.Time.Duration : Type
-- Mathlib.Probability.Moments.Basic
/-- The moment-generating function is antitone in the random variable for `t ≤ 0`.  -/
ProbabilityTheory.mgf_anti_of_nonpos : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ},
  X ≤ᵐ[μ] Y →
    t ≤ 0 →
      MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
        ProbabilityTheory.mgf Y μ t ≤ ProbabilityTheory.mgf X μ t
-- Std.Tactic.Do.Syntax
/-- `mright` is like `right`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
  mintro HP
  mright
  mexact HP
```
 -/
Lean.Parser.Tactic.mright : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given an element `m : M.Elements` of a presheaf of modules `M`, this is
the canonical morphism `m.freeYoneda ⟶ M`.  -/
PresheafOfModules.Elements.fromFreeYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → (m : M.Elements) → m.freeYoneda ⟶ M
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift.tmul' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N),
  (TensorProduct.lift f').toAddHom (x ⊗ₜ[R] y) = (f' x) y
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑(c1 * c2).den = ↑c1.den * ↑c2.den
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.fvar.injEq : ∀ (fvarId : Lean.FVarId) (nargs : ℕ) (fvarId_1 : Lean.FVarId) (nargs_1 : ℕ),
  (Lean.Meta.RefinedDiscrTree.Key.fvar fvarId nargs = Lean.Meta.RefinedDiscrTree.Key.fvar fvarId_1 nargs_1) =
    (fvarId = fvarId_1 ∧ nargs = nargs_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_insertEntry_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue! k (Std.Internal.List.insertEntry k v l) = v
-- Init.Data.String.Pattern.Basic
/-- Converts a `SearchStep s` into a `SearchStep t` by applying `Slice.Pos.cast` to the
start and end position.
 -/
String.Slice.Pattern.SearchStep.cast : {s t : String.Slice} → s.copy = t.copy → String.Slice.Pattern.SearchStep s → String.Slice.Pattern.SearchStep t
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getSimpCongrTheorems : Lean.Meta.SimpM Lean.Meta.SimpCongrTheorems
-- Mathlib.Data.Multiset.Bind
Multiset.bind_singleton : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β), (s.bind fun x => {f x}) = Multiset.map f s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S),
  (AddLocalization.mk a b).liftOn f H = f a b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃)
      (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom
      (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃))
-- Mathlib.Order.Fin.Basic
/-- If `e` is an `orderIso` between `Fin n` and `Fin m`, then `n = m` and `e` is the identity
map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i : ℕ)`.  -/
Fin.coe_orderIso_apply : ∀ {m n : ℕ} (e : Fin n ≃o Fin m) (i : Fin n), ↑(e i) = ↑i
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.below.empty : ∀ {α : Type u_3} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop},
  MeasurableSpace.DynkinSystem.GenerateHas.below ⋯
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- The relation `r` satisfies `r (a % b) b`.  -/
EuclideanDomain.remainder_lt : ∀ {R : Type u} [self : EuclideanDomain R] (a : R) {b : R}, b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The explicit pullback cone is a limit cone.
 -/
CompHausLike.pullback.isLimit : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) →
      (g : Y ⟶ B) →
        [inst : CompHausLike.HasExplicitPullback f g] → CategoryTheory.Limits.IsLimit (CompHausLike.pullback.cone f g)
-- Mathlib.Analysis.Normed.Group.Defs
/-- An e-seminormed commutative monoid is an additive commutative monoid endowed with a continuous
enorm.

We don't have `ESeminormedAddCommMonoid` extend `EMetricSpace`, since the canonical instance `ℝ≥0∞`
is not an `EMetricSpace`. This is because `ℝ≥0∞` carries the order topology, which is distinct from
the topology coming from `edist`.  -/
ESeminormedAddCommMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_functor_map_toFun : ∀ {X Y : PartialFun} (f : X ⟶ Y) (a : Option X),
  (partialFunEquivPointed.functor.map f).toFun a = Option.elim' none (fun a => (f a).toOption) a
-- Init.Data.Nat.Basic
Nat.add_one_ne : ∀ (n : ℕ), n + 1 ≠ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two monotone functions is monotone.  -/
Monotone.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [MulLeftMono α]
  [MulRightMono α], Monotone f → Monotone g → Monotone fun x => f x * g x
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of an addition with zero is commutative and associative.  -/
AddSubmonoid.center.addCommMonoid' : {M : Type u_1} → [inst : AddZeroClass M] → AddCommMonoid ↥(AddSubmonoid.center M)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation from
`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to
`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b`. (This is an isomorphism.)  -/
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : EInt) →
                  (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶
                    (t.eTruncGE.obj a).comp (t.eTruncLT.obj b)
-- Mathlib.Order.Hom.Lattice
SupHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] {g : SupHom β γ}
  {f₁ f₂ : SupHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Topology.Irreducible
irreducibleComponent_property : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X),
  IsPreirreducible (irreducibleComponent x) ∧
    {x} ⊆ irreducibleComponent x ∧
      ∀ (u : Set X), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.infinite : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Infinite R] [Nontrivial M], Infinite M
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- Applying a good compression will decrease measure, keep cardinality, keep sizes and decrease
shadow. In particular, 'good' means it's useful, and every smaller compression won't make a
difference.  -/
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.compression_improved : ∀ {α : Type u_1} [inst : LinearOrder α] {U V : Finset α} (𝒜 : Finset (Finset α)),
  Finset.UV.UsefulCompression✝ U V →
    (∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression✝ U₁ V₁ → U₁.card < U.card → UV.IsCompressed U₁ V₁ 𝒜) →
      (UV.compression U V 𝒜).shadow.card ≤ 𝒜.shadow.card
-- Init.Data.Vector.Lex
Vector.lex_empty : ∀ {α : Type u_1} [inst : BEq α] {lt : α → α → Bool} (xs : Vector α 0), xs.lex #v[] lt = false
-- Init.Data.Ord.Basic
List.isGE_compareLex_nil_right : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, (List.compareLex cmp xs []).isGE = true
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_left_bijective : ∀ {x : ℝ}, x ≠ 0 → Function.Bijective fun y => y ^ x
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Given a family of topological spaces `X i`, and a topological space `Y`,
this is a type synonym for `Y` which we endow with the `X`-generated topology.  -/
Topology.WithGeneratedByTopology : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → (Y : Type v) → [TopologicalSpace Y] → Type v
-- Mathlib.Topology.Algebra.Order.Field
/-- If `g` tends to zero and there exists a constant `C : 𝕜` such that eventually `|f x| ≤ C`,
then the product `f * g` tends to zero.  -/
bdd_le_mul_tendsto_zero' : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} (C : 𝕜),
  (∀ᶠ (x : α) in l, |f x| ≤ C) → Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Mathlib.Algebra.Lie.Quotient
/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
is a natural linear map from `L` to the endomorphisms of `M` leaving `N` invariant.  -/
LieSubmodule.Quotient.lieSubmoduleInvariant : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                {N : LieSubmodule R L M} →
                  [inst_5 : LieAlgebra R L] → [LieModule R L M] → L →ₗ[R] ↥((↑N).compatibleMaps ↑N)
-- Mathlib.Order.Monotone.Defs
StrictAnti.comp_strictAntiOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, StrictAnti g → StrictAntiOn f s → StrictMonoOn (g ∘ f) s
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_indicator_index_eq_sum_attach : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset α}
  (f : (a : α) → a ∈ s → M) {h : α → M → N},
  (∀ a ∈ s, h a 0 = 0) → (Finsupp.indicator s f).sum h = ∑ x ∈ s.attach, h (↑x) (f ↑x ⋯)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.assignExpr : ℕ → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_map_fst : ∀ {α : Type u_1} (s : Multiset α), Multiset.map Prod.fst s.antidiagonal = s.powerset
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.instIsTopologicalAddGroupSubtypeMem : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  IsTopologicalAddGroup ↥S
-- Lean.Data.NameTrie
Lean.instToStringNamePart : ToString Lean.NamePart
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAux_symm_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M] (s : S) (m : M),
  (Algebra.IsPushout.cancelBaseChangeAux R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coeFnAddMonoidHom_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (a : BoundedContinuousFunction α R) (a_1 : α),
  BoundedContinuousFunction.coeFnAddMonoidHom a a_1 = a a_1
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_finset_lcm : ∀ {α : Type u_2} (s : Finset α) (f : α → ℕ),
  ArithmeticFunction.carmichael (s.lcm f) = s.lcm (⇑ArithmeticFunction.carmichael ∘ f)
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIco a b ↔ a ≤ x ∧ x < b`  -/
LocallyFiniteOrder.finset_mem_Ico : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrder α] (a b x : α),
  x ∈ LocallyFiniteOrder.finsetIco a b ↔ a ≤ x ∧ x < b
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The natural transformation `K.truncGE' e ⟶ K.restriction e` for all `K`.  -/
ComplexShape.Embedding.truncLE'ToRestrictionNatTrans : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [inst : e.IsTruncLE] →
            (C : Type u_4) →
              [inst_1 : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [inst_3 : CategoryTheory.CategoryWithHomology C] → e.truncLE'Functor C ⟶ e.restrictionFunctor C
-- Init.Grind.ToInt
/-- The embedding takes division to division (without needing to wrap into the range interval).
One might expect a `wrap` on the right hand side,
but in practice this stronger statement is usually true.
 -/
Lean.Grind.ToInt.Div.toInt_div : ∀ {α : Type u} {inst : Div α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Div α I] (x y : α), ↑(x / y) = ↑x / ↑y
-- Mathlib.RingTheory.Localization.NumDen
/-- `f.num x` is the numerator of `x : f.codomain` as a reduced fraction.  -/
IsFractionRing.num : (A : Type u_1) →
  [inst : CommRing A] →
    [IsDomain A] →
      [UniqueFactorizationMonoid A] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra A K] → [IsFractionRing A K] → K → A
-- Init.Notation
/-- `-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator). -/
«term-_» : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.cechConerveEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C)
  (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X),
  (CategoryTheory.CosimplicialObject.cechConerveEquiv F X).symm G =
    CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G
-- Std.Sync.Notify
Std.Notify.State.mk.inj : ∀ {consumers consumers_1 : Std.Queue (Std.Notify.Consumer Unit)},
  { consumers := consumers } = { consumers := consumers_1 } → consumers = consumers_1
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_iff_smallSets : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l] g ↔
    ∀ U ∈ nhds 0,
      ∀ᶠ (V : Set F) in (nhds 0).smallSets,
        ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.joinString.eq_1 : ∀ {α β : Type} [inst : Std.Iterator α Id β] [inst_1 : ToString β] (it : Std.Iter β),
  it.joinString = Std.Iter.fold (fun x1 x2 => x1 ++ x2) "" (Std.Iter.map toString it)
-- Init.Data.ByteArray.Basic
ByteArray.instInhabited : Inhabited ByteArray
-- Batteries.Data.Fin.Coding
Fin.encodePi_decodePi : ∀ {n : ℕ} (f : Fin n → ℕ) (x : Fin (Fin.prod f)), Fin.encodePi f (Fin.decodePi f x) = x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.univ_pi' : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [Countable δ] {t : (i : δ) → Set (X i)},
  (∀ (i : δ), MeasurableSet (t i)) → MeasurableSet {f | ∀ (i : δ), f i ∈ t i}
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The difference between `Linear_CC'₁` and `Linear_CC'₀`.  -/
Profinite.NobelingProof.Linear_CC' : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          Profinite.NobelingProof.contained C (Order.succ o) →
            (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
              LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.pow_dp : ∀ {R : Type u_4} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m : M)
  (k : ℕ), DividedPowerAlgebra.dp R n m ^ k = ↑(k • {n}).multinomial * DividedPowerAlgebra.dp R (k * n) m
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- Given a cone over a functor F into `Type*` and an element in the cone point,
construct a section of F.  -/
CategoryTheory.Limits.Types.sectionOfCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J (Type u)} → (c : CategoryTheory.Limits.Cone F) → c.pt → ↑F.sections
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_add_left_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅a + b, c⁆ + ⁅c + a, b⁆ + ⁅b + c, a⁆ = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_zero_left : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  uniformity G = Filter.comap (fun p => -p.1 + p.2) (nhds 0)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.hom_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X.Hom Y), f.hom.left = f.left
-- Mathlib.Probability.Distributions.Fernique
/-- The rotation in `E × E` with angle `θ`, as a continuous linear map.  -/
ContinuousLinearMap.rotation : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → ℝ → E × E →L[ℝ] E × E
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instPartialOrder.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupNorm.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ {k : α}, k ∈ t₁ ↔ k ∈ t₂
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] [inst_2 : Fintype α] (G G_1 : SimpleGraph α),
  G = G_1 → G.IsHamiltonian = G_1.IsHamiltonian
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec_Γ_naturality : ∀ {R S : CommRingCat} (f : R ⟶ S),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.toSpecΓ S) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ R)
      (AlgebraicGeometry.LocallyRingedSpace.Γ.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.map f.op).op)
-- Std.Async.Process
/-- Size of shared memory segments (kilobytes)
 -/
Std.IO.Process.ResourceUsageStats.sharedMemorySizeKb : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y X' Y' : C}
  (f : X ≅ Y) (g : X' ≅ Y'),
  (CategoryTheory.MonoidalCategory.tensorIso f g).inv = CategoryTheory.MonoidalCategoryStruct.tensorHom f.inv g.inv
-- Mathlib.Algebra.AddConstMap.Basic
/-- Typeclass for maps satisfying `f (x + a) = f x + b`.

Note that `a` and `b` are `outParam`s,
so one should not add instances like
`[AddConstMapClass F G H a b] : AddConstMapClass F G H (-a) (-b)`.  -/
AddConstMapClass : (F : Type u_1) →
  (G : outParam (Type u_2)) →
    (H : outParam (Type u_3)) → [Add G] → [Add H] → outParam G → outParam H → [FunLike F G H] → Prop
-- Mathlib.Tactic.Ring.Common
/-- Embed `ExProd` in `ExSum` by adding 0.  -/
Mathlib.Tactic.Ring.Common.ExProd.toSum : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} → Mathlib.Tactic.Ring.Common.ExProd bt sα e → Mathlib.Tactic.Ring.Common.ExSum bt sα q(«$e» + 0)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
SimpleGraph.turanDensity.eq_1 : ∀ {W : Type u_1} (H : SimpleGraph W),
  H.turanDensity = Filter.atTop.limUnder fun n => ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.r.setoid.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LocalizedModule.r.setoid S M = { r := LocalizedModule.r S M, iseqv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ) {Z : C} (h : Y.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h 0) (CategoryTheory.CategoryStruct.comp (Y.δ 0) h) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n })) h
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_le_iff_sle : ∀ (a b : BitVec 32), Int32.ofBitVec a ≤ Int32.ofBitVec b ↔ a.sle b = true