mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.String.Matcher
/-- Find the first substring of `s` matching `m.pattern`, or `none` if no such substring exists.  -/
String.Matcher.find? : String.Matcher → Substring.Raw → Option Substring.Raw
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The tensor product of two linear isometry equivalences is a linear isometry equivalence.
In particular, this is the linear isometry equivalence version of `TensorProduct.congr f g` when `f`
and `g` are linear isometry equivalences.  -/
TensorProduct.congrIsometry : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        {H : Type u_5} →
          [inst : RCLike 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : InnerProductSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : InnerProductSpace 𝕜 F] →
                    [inst_5 : NormedAddCommGroup G] →
                      [inst_6 : InnerProductSpace 𝕜 G] →
                        [inst_7 : NormedAddCommGroup H] →
                          [inst_8 : InnerProductSpace 𝕜 H] →
                            (E ≃ₗᵢ[𝕜] G) → (F ≃ₗᵢ[𝕜] H) → TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 G H
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom h)
-- Std.Http.Transport
/-- Tries to receive data without blocking, joining all immediately available chunks. Returns `none` if no
data is available.
 -/
Std.Http.Internal.Mock.Server.tryRecv? : Std.Http.Internal.Mock.Server → optParam UInt64 0 → BaseIO (Option ByteArray)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.of_neg : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R (-x) → IsIntegral R x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.updateCell.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k))
  (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced),
  Std.DTreeMap.Internal.Impl.updateCell k f l hl =
    match l, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      match (f Std.DTreeMap.Internal.Cell.empty).inner with
      | none =>
        { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some ⟨k', v'⟩ =>
        {
          impl :=
            Std.DTreeMap.Internal.Impl.inner 1 k' v' Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
          balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl =>
      match h : compare k ky with
      | Ordering.lt =>
        match Std.DTreeMap.Internal.Impl.updateCell k f l ⋯ with
        | { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance ky y newL r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.eq =>
        match (f (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)).inner with
        | none => { impl := l.glue r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
        | some ⟨ky', y'⟩ =>
          { impl := Std.DTreeMap.Internal.Impl.inner sz ky' y' l r, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.gt =>
        match Std.DTreeMap.Internal.Impl.updateCell k f r ⋯ with
        | { impl := newR, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance ky y l newR ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.ext : ∀ {α : Type u_1} {x y : Quiver.SingleObj α}, x = y
-- Mathlib.Order.Directed
/-- **Alias** of the reverse direction of `directed_comp_iff_of_surjective`. -/
Directed.comp_of_surjective : ∀ {α : Type u_1} {ι : Sort u_3} {κ : Sort u_4} {r : α → α → Prop} {f : ι → κ},
  Function.Surjective f → ∀ {g : κ → α}, Directed r g → Directed r (g ∘ f)
-- Init.Data.List.Sublist
List.Sublist.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Sublist l₂ → l₂.Sublist l₃ → l₁.Sublist l₃
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_eq_of_row_eq_zero : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  {A : Matrix n n R} {p : n}, A.row p = 0 → Matrix.detp s A = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism.  -/
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y},
  f = g → ∀ {c : CategoryTheory.Limits.Cofork f g} (h : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsIso c.π
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {l : Filter β}
  {u : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l u
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.neBot_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (l.NeBot ↔ ∀ {i : ι}, p i → (s i).Nonempty)
-- Std.Time.Time.Unit.Second
Std.Time.Second.instOrdOffset : Ord Std.Time.Second.Offset
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff_cancel_left : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → t \ (t \ s) = s
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Ioi : ∀ (x : ℝ), Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.mono_set : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f t μ → s ⊆ t → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.equiv_mapSubmodule.eq_1 : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (p : Submodule R M) (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule),
  Module.AEval.equiv_mapSubmodule a p hp =
    { toFun := fun x => ⟨(Module.AEval.of R M a) ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯,
      invFun := fun x => ⟨(Module.AEval.of R M a).symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_mk_iff_isUnmixed : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔ NumberField.ComplexEmbedding.IsUnmixed k φ
-- Mathlib.Order.WithBot
WithTop.map_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {v : WithTop α}, WithTop.map f v = ↑y ↔ ∃ x, v = ↑x ∧ f x = y
-- Mathlib.Algebra.Regular.SMul
/-- Right-regular multiplication on `R` is equivalent to `Rᵐᵒᵖ`-regularity of `R` itself.  -/
isRightRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (T T_1 : ℕ → ℝ),
  T = T_1 →
    ∀ (g g_1 : ℝ → ℝ),
      g = g_1 →
        ∀ (a a_1 : α → ℝ),
          a = a_1 →
            ∀ (b b_1 : α → ℝ),
              b = b_1 →
                ∀ (r r_1 : α → ℕ → ℕ), r = r_1 → AkraBazziRecurrence T g a b r = AkraBazziRecurrence T_1 g_1 a_1 b_1 r_1
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_finsetSum_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ},
  (∀ i ∈ s, (f i).totalDegree ≤ d) → (s.sum f).totalDegree ≤ d
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier : Type
-- Init.Data.Order.LemmasExtra
/-- Derives an `Ord α` instance from an `LE α` instance. Because all elements are comparable with
`compare`, the resulting `Ord α` instance only makes sense if `LE α` is total.
 -/
Classical.Order.instOrd : {α : Type u} → [LE α] → Ord α
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
/-- A subset of the triangles constructed in a weird way to make them easy to count.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.triangle_split_helper : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α} [inst_1 : DecidableEq α],
  ((s \ (SimpleGraph.badVertices✝ G ε s t ∪ SimpleGraph.badVertices✝ G ε s u)).biUnion fun x =>
      Finset.image (fun x_1 => (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z}
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_le_of_right_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidablePred fun x => b ≤ x],
  Multiset.filter (fun x => b ≤ x) (Multiset.Ico a b) = ∅
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.mk : Lean.Syntax → Lean.Level → Lean.Level → Option Lean.Meta.DefEqContext → Lean.Meta.PostponedEntry
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
/-- An explicit upper bound for `‖jacobiTheta τ - 1‖`.  -/
norm_jacobiTheta_sub_one_le : ∀ {τ : ℂ}, 0 < τ.im → ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * τ.im)) * Real.exp (-Real.pi * τ.im)
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.not_isSimple_of_subsingleton : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Subsingleton L],
  ¬LieAlgebra.IsSimple R L
-- Init.Data.BitVec.Bootstrap
BitVec.getLsbD.eq_1 : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getLsbD i = x.toNat.testBit i
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `declName` priority for E-matching pattern inference in `s`.  -/
Lean.Meta.Grind.SymbolPriorities.getPrio : Lean.Meta.Grind.SymbolPriorities → Lean.Name → ℕ
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.instCoePointedCone : {R : Type u_2} →
  {E : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] → [inst_5 : Module R E] → Coe (ProperCone R E) (PointedCone R E)