mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.isEmptyEquiv_symm_apply : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [inst_1 : IsEmpty σ] (a : R),
  (MvPowerSeries.isEmptyEquiv σ R).symm a = MvPowerSeries.C a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- The integral version of the classical formulation of Hilbert's theorem 90: in the `ABKL`
setting, suppose that `L/K` is a finite Galois extension such that the Galois group is cyclic
generated by `g` and let `η : B` be an element of norm `1` (when viewed as an element of `L`).
Then there exists `ε : B` such that `ε ≠ 0` and `η * g ε = ε`.  -/
groupCohomology.exists_mul_galRestrict_of_norm_eq_one : ∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [inst_4 : IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} {A : Type u_1} {B : Type u_2} [inst_6 : CommRing A]
  [inst_7 : CommRing B] [inst_8 : Algebra A B] [inst_9 : Algebra A L] [inst_10 : Algebra A K] [inst_11 : Algebra B L]
  [inst_12 : IsScalarTower A B L] [inst_13 : IsScalarTower A K L] [inst_14 : IsFractionRing A K] [IsDomain A]
  [inst_16 : IsIntegralClosure B A L],
  (∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) →
    ∀ {η : B}, (Algebra.norm K) ((algebraMap B L) η) = 1 → ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε
-- Mathlib.Data.Multiset.UnionInter
Multiset.le_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ s ∪ t
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.coe_stepBound : ∀ {α : Type u_1} [inst : Semiring α] (n : ℕ), ↑(SzemerediRegularity.stepBound n) = ↑n * 4 ^ n
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.comp : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
  Nat.Primrec.below a → motive f a → Nat.Primrec.below a_1 → motive g a_1 → Nat.Primrec.below ⋯
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.ext_iff : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c}
  {x y : A.Hom B}, x = y ↔ x.f = y.f
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Get the candidate theorems from `pres`.
Used for current file declarations and local hypotheses  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.getCandidates : Lean.Expr →
  Lean.Expr →
    Array Mathlib.Tactic.ClickSuggestions.GrwPos →
      Mathlib.Tactic.ClickSuggestions.RwKind →
        Option Lean.Expr →
          Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
            Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Array Mathlib.Tactic.ClickSuggestions.Candidates✝)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.sSup_mem : ∀ {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α}, s.Finite → s ⊆ ↑L → sSup s ∈ L
-- Mathlib.Order.Concept
Concept.strictAnti_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, StrictAnti Concept.intent
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instNSMul.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)],
  RestrictedProduct.instNSMul R = { smul := fun n x => ⟨fun i => n • x i, ⋯⟩ }
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- A pretopology `K` can be completed to a Grothendieck topology `J` by declaring a sieve to be
`J`-covering if it contains a family in `K`.

See also [MM92] Chapter III, Section 2, Equation (2).
 -/
CategoryTheory.Pretopology.toGrothendieck : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      CategoryTheory.Pretopology C → CategoryTheory.GrothendieckTopology C
-- Init.Omega.Int
Lean.Omega.Fin.lt_or_gt_of_ne : ∀ {n : ℕ} {i j : Fin n}, i ≠ j → i < j ∨ i > j
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.inf_addSubgroupOf_left : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), (K ⊓ H).addSubgroupOf K = H.addSubgroupOf K
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is separable,
then $[E:F] [K:E]_s = [K:F]_s$.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it.  -/
Field.lift_rank_mul_lift_sepDegree_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E],
  Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) =
    Cardinal.lift.{v, w} (Field.sepDegree F K)
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal` as an `AddMonoidHom`.  -/
Matrix.blockDiagonalAddMonoidHom : (m : Type u_2) →
  (n : Type u_3) →
    (o : Type u_4) →
      (α : Type u_12) → [DecidableEq o] → [inst : AddZeroClass α] → (o → Matrix m n α) →+ Matrix (m × o) (n × o) α
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p.content = p.support.gcd p.coeff
-- Mathlib.Data.Semiquot
/-- Assert that a `Semiquot` contains only one possible value.  -/
Semiquot.IsPure : {α : Type u_1} → Semiquot α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                CategoryTheory.Category.{max (max (max (max (max u₃ u₂) u₁) v₆) v₅) v₄,
                                    max
                                      (max
                                          (max
                                              (max (max (max (max (max (max (max (max u₆ u₅) u₄) u₃) u₂) u₁) v₆) v₅) v₄)
                                              v₃)
                                          v₂)
                                      v₁}
                                  (CategoryTheory.Limits.CatCospanTransform F G F' G')
-- Init.Data.Vector.Zip
Vector.map_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α × β → γ} {as : Vector α n} {bs : Vector β n},
  Vector.map f (as.zip bs) = Vector.zipWith (Function.curry f) as bs
-- Init.Grind.AC
Lean.Grind.AC.Seq.startsWithVar_k_cons : ∀ (y x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq), (Lean.Grind.AC.Seq.cons y s).startsWithVar_k x = (x == y)
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedString` from a `ByteArray` with compile-time proofs.
Use this when you have proofs that the byte array is valid.
 -/
Std.Http.URI.EncodedString.new : {r : UInt8 → Bool} →
  (ba : ByteArray) →
    Std.Http.URI.IsAllowedEncodedChars r ba →
      Std.Http.URI.isValidPercentEncoding ba = true → Std.Http.URI.EncodedString r
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams.mk.injEq : ∀ (changes changes_1 : Array Lean.Lsp.FileEvent),
  ({ changes := changes } = { changes := changes_1 }) = (changes = changes_1)
-- Init.Omega.Int
Lean.Omega.Int.add_le_zero_iff_le_neg : ∀ {a b : ℤ}, a + b ≤ 0 ↔ a ≤ -b
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.lengthTRAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        ((n : ℕ) → motive [] n) → ((head : α) → (as : List α) → (n : ℕ) → motive (head :: as) n) → motive x x_1
-- Mathlib.Data.ENat.Pow
ENat.epow_zero : ∀ {x : ℕ∞}, x ^ 0 = 1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_int_neg : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  [inst_3 : Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n ℤ),
  (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) (-g) = -(Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g
-- Mathlib.Order.Filter.IndicatorFunction
Filter.indicator_const_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {l : Filter α} {c : β},
  c ≠ 0 → ∀ {s t : Set α}, ((s.indicator fun x => c) =ᶠ[l] t.indicator fun x => c) ↔ s =ᶠ[l] t
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- **Alias** of `Submonoid.powSaturated_iff_npow`. -/
Subgroup.saturated_iff_npow : ∀ {G : Type u_1} [inst : Monoid G] {H : Submonoid G}, H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instCanLift : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R], CanLift C(X, R) (ContinuousMapZero X R) toContinuousMap fun f => f 0 = 0
-- Init.Data.Array.GetLit
List.drop.eq_2 : ∀ {α : Type u} (n : ℕ), List.drop n.succ [] = []
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.W_of_preservesSheafification : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A} (f : P₁ ⟶ P₂),
  J.W f → J.W (CategoryTheory.Functor.whiskerRight f F)
-- Init.Data.SInt.Bitwise
Int32.or_comm : ∀ (a b : Int32), a ||| b = b ||| a
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.fill.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α)
  (y : α) (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b),
  (match RBTree.RBNode.Path.right c a y parent, b with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left c parent y b, a => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b => h_3 c a y parent b) =
    h_3 c a y parent b
-- Mathlib.Dynamics.Flow
/-- The identity is a semiconjugacy from `ϕ` to `ψ` if and only if `ϕ` and `ψ` are equal.  -/
Flow.isSemiconjugacy_id_iff_eq : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ ψ : Flow τ α), Flow.IsSemiconjugacy id ϕ ψ ↔ ϕ = ψ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ Std.DHashMap.Const.alter m k f},
  Std.DHashMap.Const.get (Std.DHashMap.Const.alter m k f) k h = (f (Std.DHashMap.Const.get? m k)).get ⋯
-- Mathlib.AlgebraicGeometry.Artinian
/-- A commutative ring `R` is Artinian if and only if `Spec R` is an Artinian scheme.  -/
AlgebraicGeometry.Scheme.isLocallyArtinianScheme_Spec : ∀ {R : CommRingCat}, AlgebraicGeometry.IsLocallyArtinian (AlgebraicGeometry.Spec R) ↔ IsArtinianRing ↑R
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin.eq_1 : ∀ (z : ℂ), Complex.sin z = (Complex.exp (-z * Complex.I) - Complex.exp (z * Complex.I)) * Complex.I / 2
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The compatibility of a morphism with the augmentation, on 0-simplices  -/
CategoryTheory.SimplicialObject.Augmented.w₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y)
  {Z : C} (h : Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.left.app (Opposite.op { len := 0 }))
      (CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op { len := 0 })) h) =
    CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 }))
      (CategoryTheory.CategoryStruct.comp f.right h)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.lift_mk : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {α : Type u_3}
  (f : { v // v ≠ 0 } → α) (hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (v : V) (hv : v ≠ 0),
  Projectivization.lift f hf (Projectivization.mk K v hv) = f ⟨v, hv⟩
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.instMonoidalCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategory (AlgCat R)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {n : WithTop ℕ∞}, (∀ x ∈ s, f₁ x = f x) → (ContDiffOn 𝕜 n f₁ s ↔ ContDiffOn 𝕜 n f s)
-- Mathlib.Algebra.Group.Translate
/-- See `translate_add`  -/
translate_add' : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a b : G) (f : G → α),
  translate (a + b) f = translate b (translate a f)
-- Mathlib.Topology.Category.CompHaus.Basic
compHausToTop.createsLimits : CategoryTheory.CreatesLimits compHausToTop
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalNestedTactic : Lean.Elab.Tactic.Tactic
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.returnToTerm : Lean.Syntax → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω),
  μ ≠ 0 → μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'.eq_1 : ∀ (b : Bool) (m : ℕ), Nat.shiftLeft' b m 0 = m
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context : Type
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_map_toDual`. -/
List.SortedLE.of_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, l.SortedLE → (List.map (⇑OrderDual.toDual) l).SortedGE
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point `Φ` of a site `(C, J)`, this is the skyscraper sheaf functor
`A ⥤ Sheaf J A`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] → CategoryTheory.Functor A (CategoryTheory.Sheaf J A)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_singleton : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (f : ι → M) (a : ι), ∑ x ∈ {a}, f x = f a
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.isDetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Balanced C], P.IsSeparating → P.IsDetecting
-- Init.Data.Nat.Lemmas
Nat.mul_le_add_right : ∀ {m k n : ℕ}, k * m ≤ m + n ↔ (k - 1) * m ≤ n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.StronglyAdapted ℱ f →
    a < b → MeasureTheory.Integrable (fun ω => ↑(MeasureTheory.upcrossingsBefore a b f N ω)) μ
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.addParserCategoryCore : Lean.Parser.ParserCategories → Lean.Name → Lean.Parser.ParserCategory → Except String Lean.Parser.ParserCategories
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- The top submodule is linearly equivalent to the module.

This is the module version of `AddSubmonoid.topEquiv`.  -/
Submodule.topEquiv : {R : Type u_1} → {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → ↥⊤ ≃ₗ[R] M
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_const : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Refl r] {l : Filter β} {a : α},
  Filter.IsBoundedUnder r l fun x => a
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.cobounded_le_atBot_sup_atTop : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α],
  Bornology.cobounded α ≤ Filter.atBot ⊔ Filter.atTop
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorRightObjFunctorFlipTensorBifunctor : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (Y : C) →
                        CategoryTheory.Localization.Lifting
                          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) W
                          ((CategoryTheory.MonoidalCategory.tensorRight Y).comp
                            (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε))
                          ((CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).flip.obj
                            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minKey?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.minKey? =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => some k
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      l.minKey?
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ioc_coe_top : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ioc ↑a ⊤ = Finset.insertNone (Finset.Ioi a)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- Given a functor `F : Discrete C ⥤ Type v`, this is a "cofan" for `F`,
but we allow the point to be in `Type w` for an arbitrary universe `w`.  -/
CategoryTheory.Limits.CofanTypes : {C : Type u} → (C → Type v) → Type (max (max u v) (w + 1))
-- Mathlib.Order.Hom.Lattice
InfHom.top_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Top β] (a : α), ⊤ a = ⊤
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.conjTranspose_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Star A] (M : CStarMatrix m n A) (i : n) (j : m),
  M.conjTranspose i j = star (M j i)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.map f = f.unmop
-- Mathlib.CategoryTheory.Retract
/-- If `X` is isomorphic to `Y`, then `X` is a retract of `Y`.  -/
CategoryTheory.Iso.retract : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.Retract X Y
-- Mathlib.Analysis.Asymptotics.Defs
/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l`
(denoted as `u ~[l] v` in the `Asymptotics` namespace)
when `u x - v x = o(v x)` as `x` converges along `l`.  -/
Asymptotics.«term_~[_]_» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Icc : ∀ (a b : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Icc a b)
-- Lean.AuxRecursor
Lean.instInhabitedNoConfusionInfo.default : Lean.NoConfusionInfo
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` moves `h ^ j • x` iff `g` moves `x`.
 -/
MulAction.smul_zpow_movedBy_eq_of_commute : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h : G},
  Commute g h → ∀ (j : ℤ), h ^ j • (MulAction.fixedBy α g)ᶜ = (MulAction.fixedBy α g)ᶜ
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofList_cons : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {k : α} {v : β} {tl : List (α × β)},
  Std.HashMap.ofList ((k, v) :: tl) = (∅.insert k v).insertMany tl
-- Mathlib.Topology.Semicontinuity.Basic
continuousAt_iff_lower_upperSemicontinuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ},
  ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.ne_of_disjoint_coe : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, Disjoint ↑I ↑J → I ≠ J
-- Init.Data.Format.Basic
/-- Converts a value to a `Format` object, with no expectation that the resulting string is valid
code.
 -/
Std.ToFormat.format : {α : Type u} → [self : Std.ToFormat α] → α → Std.Format
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac lhs s c₁ c₂) = 1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.atLeastTwo_eq_halfAdder : ∀ (lhsBit rhsBit carry : Bool), lhsBit.atLeastTwo rhsBit carry = ((lhsBit ^^ rhsBit) && carry || lhsBit && rhsBit)
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.mem_charPoly : ∀ {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}
  (f : BoundedContinuousFunction V ℂ),
  f ∈ BoundedContinuousFunction.charPoly he hL ↔ ∃ w, ⇑f = fun x => w.coeff.sum fun a z => z * ↑(e ((L x) a))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f g : (i : ι) → α i},
  (s.pi fun i => Set.Ioc (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)