mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.exists_compl : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  l.MemBaseSet I c r π → l.bDistortion = true → ∃ π', π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_mem_openSegment_compl_self : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → E} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    μ s ≠ 0 →
      μ sᶜ ≠ 0 →
        MeasureTheory.Integrable f μ →
          ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.quotientRel.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  p.quotientRel = QuotientAddGroup.leftRel p.toAddSubgroup
-- Mathlib.Analysis.Normed.MulAction
ENormSMulClass.enorm_smul : ∀ {α : Type u_3} {β : Type u_4} {inst : ENorm α} {inst_1 : ENorm β} {inst_2 : SMul α β} [self : ENormSMulClass α β]
  (r : α) (x : β), ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ
-- Init.Core
Std.LawfulIdentity.toLawfulRightIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [self : Std.LawfulIdentity op o], Std.LawfulRightIdentity op o
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → Filter.Tendsto f (MeasureTheory.ae μa) (MeasureTheory.ae μb)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.homEquiv_apply_coe : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (f : P.Ring →ₐ[R] S), ↑(P.homEquiv f) = f P.X
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.quotientEquivOfIsTopCompl_comp_mkQL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  ↑(p.quotientEquivOfIsTopCompl q h) ∘SL p.mkQL = q.projectionOntoL p ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Two
/-- Variant of `twoδ₁Toδ₀` for preorders.  -/
CategoryTheory.ComposableArrows.twoδ₁Toδ₀' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯) ⟶
            CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₁₂)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_sub : ∀ (x y : ℂ), Complex.sinh (x - y) = Complex.sinh x * Complex.cosh y - Complex.cosh x * Complex.sinh y
-- Mathlib.Order.Sublattice
/-- The underlying set of a sublattice. **Do not use directly**. Instead, use the coercion
`Sublattice α → Set α`, which Lean should automatically insert for you in most cases.  -/
Sublattice.carrier : {α : Type u_2} → [inst : Lattice α] → Sublattice α → Set α
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), (FreeCommRing.map f) (FreeCommRing.of x) = FreeCommRing.of (f x)
-- Mathlib.Order.SetAccumulate
Set.monotone_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], Monotone (Set.accumulate s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_maxKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β}, cmp (Std.DTreeMap.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.Algebra.Order.Field.Basic
strictMono_div_right_of_pos : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α},
  0 < a → StrictMono fun x => x / a
-- Mathlib.RingTheory.Etale.Finite
/-- The object property of finite `R`-algebras.  -/
CommAlgCat.finite : (R : Type u) → [inst : CommRing R] → CategoryTheory.ObjectProperty (CommAlgCat R)
-- Mathlib.Data.List.Sort
List.sortedLT_iff_isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT ↔ List.IsChain (fun x1 x2 => x1 < x2) l
-- Mathlib.GroupTheory.Exponent
AddMonoid.exists_addOrderOf_eq_exponent : ∀ {G : Type u} [inst : AddCommMonoid G], AddMonoid.ExponentExists G → ∃ g, addOrderOf g = AddMonoid.exponent G
-- Mathlib.Topology.Inseparable
specializes_iff_forall_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapMap_comp_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y Z : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [inst_1 : X.HasMap p]
  [inst_2 : Y.HasMap p] [inst_3 : Z.HasMap p] {Z_1 : CategoryTheory.GradedObject J C} (h : Z.mapObj p ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.comp φ ψ) p) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap ψ p) h)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.tendsto_left_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β}
  {f : α → β}, la.HasBasis pa sa → (Filter.Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ Set.MapsTo f (sa i) t)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.list_cycles_perm_list_cycles : ∀ {α : Type u_4} [Finite α] {l₁ l₂ : List (Equiv.Perm α)},
  l₁.prod = l₂.prod →
    (∀ σ ∈ l₁, σ.IsCycle) →
      (∀ σ ∈ l₂, σ.IsCycle) → List.Pairwise Equiv.Perm.Disjoint l₁ → List.Pairwise Equiv.Perm.Disjoint l₂ → l₁.Perm l₂
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.surj : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N) (r : R)
  [IsLocalizedModule.Away r f] (y : N), ∃ n x, r ^ n • y = f x
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuousOn_mkD_of_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {T : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace T] {s : Set T} (f : T → X → Y) (g : C(X, Y)),
  ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) → ContinuousOn (fun x => ContinuousMap.mkD (f x) g) s
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ZMod q` is a unit, then there are infinitely many prime numbers `p`
such that `(p : ZMod q) = a`.  -/
Nat.infinite_setOfPred_prime_and_eq_mod : ∀ {q : ℕ} [NeZero q] {a : ZMod q}, IsUnit a → {p | Nat.Prime p ∧ ↑p = a}.Infinite
-- Mathlib.Analysis.Complex.Poisson
/-- The Poisson kernel of integration.
 -/
poissonKernel : ℂ → ℂ → ℂ → ℝ
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.mk.injEq : ∀ (variant : Lean.Name) (args : Lean.Elab.Tactic.Grind.DSimpArgs) (variant_1 : Lean.Name)
  (args_1 : Lean.Elab.Tactic.Grind.DSimpArgs),
  ({ variant := variant, args := args } = { variant := variant_1, args := args_1 }) =
    (variant = variant_1 ∧ args = args_1)
-- ProofWidgets.Component.Basic
ProofWidgets.instRpcEncodableInteractiveCodeProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveCodeProps
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_last : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)), SimplexCategory.II.map' f (Fin.last (m + 1)) = Fin.last (n + 1)
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- The **Sauer-Shelah lemma**.  -/
Finset.card_shatterer_le_sum_vcDim : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} [inst_1 : Fintype α],
  𝒜.shatterer.card ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitor_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.f = CategoryTheory.Limits.prod.snd
-- Mathlib.Algebra.BigOperators.Pi
sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Analysis.Polynomial.Order
Polynomial.negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos : ∀ {P : Polynomial ℝ} {x : ℝ},
  (∀ (y : ℝ), P.IsRoot y → x < y) → P.leadingCoeff ≤ 0 → ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P < 0
-- Mathlib.Analysis.Normed.Operator.Basic
/-- Continuous linear maps form a seminormed ring with respect to the operator norm.  -/
ContinuousLinearMap.toSeminormedRing : {𝕜 : Type u_1} →
  {E : Type u_4} →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : NontriviallyNormedField 𝕜] → [inst_2 : NormedSpace 𝕜 E] → SeminormedRing (E →L[𝕜] E)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafification_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D],
  CategoryTheory.IsIso (CategoryTheory.sheafificationAdjunction J D).counit
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
/-- The submodule of a tensor product corresponding to a decomposition on the left.  -/
DirectSum.decomposeTensor : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (ι → Submodule R M) →
              (N : Type u_5) →
                [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → ι → Submodule R (TensorProduct R M N)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- The canonical isomorphism `(X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃)`.  -/
CategoryTheory.Limits.pullbackAssoc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄] →
                    [inst_4 :
                        CategoryTheory.Limits.HasPullback f₁
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] →
                      CategoryTheory.Limits.pullback
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄ ≅
                        CategoryTheory.Limits.pullback f₁
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)
-- Mathlib.Data.Finset.Piecewise
Finset.update_eq_piecewise : ∀ {ι : Type u_1} {β : Type u_3} [inst : DecidableEq ι] (f : ι → β) (i : ι) (v : β),
  Function.update f i v = {i}.piecewise (fun x => v) f
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (n • b) ((n + 1) • b))
-- Mathlib.RingTheory.Etale.Finite
/-- If `S` is an `R`-algebra, this is the base change functor `A ↦ S ⊗[R] A`.  -/
CommAlgCat.FiniteEtale.baseChange : (R : Type u) →
  [inst : CommRing R] →
    (S : Type w) →
      [inst_1 : CommRing S] →
        [Algebra R S] → CategoryTheory.Functor (CommAlgCat.FiniteEtale R) (CommAlgCat.FiniteEtale S)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_div_self' : ∀ {x : ℝ}, √x / x = 1 / √x
-- Mathlib.Algebra.Ring.Idempotent
/-- `a + b` is idempotent if and only if `a` and `b` anti-commute.  -/
IsIdempotentElem.add_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [IsCancelAdd R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → (IsIdempotentElem (a + b) ↔ a * b + b * a = 0)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionParams.fromJson : Lean.Json → Except String Lean.Lsp.CompletionParams
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G},
  K ≤ L → (H.addSubgroupOf L).relIndex (K.addSubgroupOf L) = H.relIndex K
-- Mathlib.Algebra.Order.Hom.Basic
map_pos_of_ne_one : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [GroupNormClass F α β] (f : F) {x : α}, x ≠ 1 → 0 < f x
-- Lean.Util.MonadCache
/-- Interface for caching results.   -/
Lean.MonadCache : Type → Type → (Type → Type) → Type
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instSMulOfSMulCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : SMul M X] → [inst_1 : SMul N Y] → [inst_2 : SMul R Y] → [SMulCommClass N R Y] → SMul R (X →ₑ[σ] Y)
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.exists_inter_eq_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  𝒜.Shatters s → a ∈ s → ∃ t ∈ 𝒜, s ∩ t = {a}
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- The left homotopy relation on morphisms in a category with weak equivalences.  -/
HomotopicalAlgebra.LeftHomotopyRel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → HomRel C
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instAddHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → Add (M ⟶ N)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.unary.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.setGoals : List Lean.Meta.Grind.Goal → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.commSemiring : {R : Type u_1} → {M : Type u_4} → [inst : CommSemiring R] → [AddCommMonoid M] → CommSemiring (AddMonoidAlgebra R M)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.max!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.max! = t₂.max!
-- Init.Core
/-- An asymmetric relation satisfies `r a b → ¬ r b a`.  -/
Std.Asymm.asymm : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Asymm r] (a b : α), r a b → ¬r b a
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.isCardinalPresentable : ∀ {X : Type u} {κ : Cardinal.{u}},
  HasCardinalLT X κ → ∀ [inst : Fact κ.IsRegular], CategoryTheory.IsCardinalPresentable X κ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.Unsat : Std.Tactic.BVDecide.BVLogicalExpr → Prop
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.isBigOTVS : ∀ {α : 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 =Θ[𝕜; l] g → f =O[𝕜; l] g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey ⋯
-- Init.Data.Vector.Attach
Vector.attach_empty : ∀ {α : Type u_1}, #v[].attach = #v[]
-- Std.Time.Zoned.Database
/-- Gets the zone rules for a specific time zone identifier, handling Windows and non-Windows platforms.
In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
files.
 -/
Std.Time.Database.defaultGetZoneRules : String → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.probCharDual_zero : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedSpace ℝ F],
  BoundedContinuousFunction.probCharDual 0 = 1
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGTD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_le : ∀ {p q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], ↑p ≤ ↑q ↔ p ≤ q
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- Given a directed system of `R`-modules, tensoring it on the left gives a directed system  -/
DirectedSystem.lTensor : ∀ (R : Type u) (M : Type u_1) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Preorder ι] {F : ι → Type u_4} [inst_4 : (i : ι) → AddCommMonoid (F i)] [inst_5 : (i : ι) → Module R (F i)]
  {f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j},
  (DirectedSystem F fun x x_1 h => ⇑(f h)) →
    DirectedSystem (fun i => TensorProduct R M (F i)) fun x x_1 h => ⇑(LinearMap.lTensor M (f h))
-- Mathlib.RingTheory.EssentialFiniteness
/-- Let `S` be an `R`-algebra essentially of finite type, this is a choice of a finset `s ⊆ S`
such that `S` is the localization of `R[s]`.  -/
Algebra.EssFiniteType.finset : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [h : Algebra.EssFiniteType R S] → Finset S
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.restrictScalars_zero : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A], ContinuousLinearMap.restrictScalars R 0 = 0
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hasForgetToCommBialgCat : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (CommHopfAlgCat R) (CommBialgCat R)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates colimits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C Dᵒᵖ) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesLimitsOfShape J F.leftOp
-- Std.Do.Triple.SpecLemmas
/-- The elements starting at the current position. If the position is after the last element of the
list, then the suffix is empty; otherwise, the first element of the suffix is the current element
that the cursor points to.
 -/
List.Cursor.suffix : {α : Type u} → {l : List α} → l.Cursor → List α
-- Lean.Data.Lsp.Utf16
/-- Starting at `utf8pos`, finds the UTF-8 offset of the `p`-th codepoint.  -/
Lean.String.codepointPosToUtf8PosFrom : String → String.Pos.Raw → ℕ → String.Pos.Raw
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a k : α}
  {v : β},
  Std.DTreeMap.Const.get? (t.insert k v) a = if cmp k a = Ordering.eq then some v else Std.DTreeMap.Const.get? t a
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.equivEquivIso_apply_hom : ∀ {A B : FintypeCat} (e : A.obj ≃ B.obj), (FintypeCat.equivEquivIso e).hom = FintypeCat.homMk ⇑e
-- Mathlib.Algebra.Squarefree.Basic
/-- An element of a monoid is squarefree if the only squares that
divide it are the squares of units.  -/
Squarefree : {R : Type u_1} → [Monoid R] → R → Prop
-- Mathlib.Order.Interval.Basic
Interval.coe_pure : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), ↑(Interval.pure a) = {a}
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_strictAnti₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < b → b < a → a⁻¹ < b⁻¹
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH0_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (groupCohomology.shortComplexH0 A).Exact
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.decidable_good : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → DecidablePred (Encodable.good✝ p)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.ofAlgHom_toRingHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f : P.Ring →ₐ[R] P'.Ring)
  (H :
    (IsScalarTower.toAlgHom R P'.Ring S').comp f =
      (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)),
  (Algebra.Extension.Hom.ofAlgHom f H).toRingHom = f.toRingHom
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.terminal : Lean.Elab.Tactic.Try.Ctx → Bool
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.sub : ∀ {α : Type u_1} {n : Type u_4} [inst : SubtractionMonoid α] {A B : Matrix n n α}, A.IsDiag → B.IsDiag → (A - B).IsDiag
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsFiniteOfIsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.Presentation) [σ.IsFinite],
  (SheafOfModules.Presentation.ofIsIso f σ).IsFinite
-- Mathlib.RingTheory.NormalClosure
Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S],
  FiniteDimensional (FractionRing S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.inr_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : B), (ContinuousAddMonoidHom.inr A B) i = (0, i)
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- The complete lattice structure on pretopologies. This is induced by the `InfSet` instance, but
with good definitional equalities for `⊥`, `⊤` and `⊓`.  -/
CategoryTheory.Pretopology.instCompleteLattice : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → CompleteLattice (CategoryTheory.Pretopology C)