mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Semantics
/-- The complete theory of a structure `M` is the set of all sentences `M` satisfies.  -/
FirstOrder.Language.completeTheory : (L : FirstOrder.Language) → (M : Type w) → [L.Structure M] → L.Theory
-- Mathlib.Order.MinMax
max_left_commutative : ∀ {α : Type u} [inst : LinearOrder α], LeftCommutative max
-- Mathlib.Algebra.Group.Defs
CommGroup.toDivisionCommMonoid.eq_1 : ∀ {G : Type u_1} [inst : CommGroup G],
  CommGroup.toDivisionCommMonoid =
    { toDivInvMonoid := inst.toDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯, mul_comm := ⋯ }
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.RootOrdered.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (x : α)
  (parent : RBTree.RBNode.Path α) (v : α) (h_1 : (x : α) → motive RBTree.RBNode.Path.root x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (x : α) → (r : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.Path.left c parent x r) v)
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → (v : α) → motive (RBTree.RBNode.Path.right c l x parent) v),
  (match RBTree.RBNode.Path.right c l x parent, v with
    | RBTree.RBNode.Path.root, x => h_1 x
    | RBTree.RBNode.Path.left c parent x r, v => h_2 c parent x r v
    | RBTree.RBNode.Path.right c l x parent, v => h_3 c l x parent v) =
    h_3 c l x parent v
-- Lean.Meta.Hint
Lean.Meta.Hint.Suggestion.mk.sizeOf_spec : ∀ (toTryThisSuggestion : Lean.Meta.Tactic.TryThis.Suggestion) (span? previewSpan? : Option Lean.Syntax)
  (diffGranularity : Lean.Meta.Hint.DiffGranularity),
  sizeOf
      { toTryThisSuggestion := toTryThisSuggestion, span? := span?, previewSpan? := previewSpan?,
        diffGranularity := diffGranularity } =
    1 + sizeOf toTryThisSuggestion + sizeOf span? + sizeOf previewSpan? + sizeOf diffGranularity
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The global sections of an affine scheme over `Spec R` are a `R`-algebra.  -/
AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfOverSpecOfIsAffine : {R : CommRingCat} →
  {X : AlgebraicGeometry.Scheme} →
    [X.Over (AlgebraicGeometry.Spec R)] → [AlgebraicGeometry.IsAffine X] → Algebra ↑R ↑(X.presheaf.obj (Opposite.op ⊤))
-- Lean.Elab.PreDefinition.TerminationHint
/-- A single `termination_by` clause  -/
Lean.Elab.TerminationBy : Type
-- Mathlib.Analysis.Normed.Group.InfiniteSum
cauchySeq_finset_iff_vanishing_norm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
  (CauchySeq fun s => ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
-- Mathlib.RingTheory.Smooth.Locus
Algebra.IsSmoothAt.exists_notMem_smooth : ∀ (R : Type u_1) {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] (p : Ideal A) [inst_4 : p.IsPrime] [Algebra.IsSmoothAt R p],
  ∃ f ∉ p, Algebra.Smooth R (Localization.Away f)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.String.0.String.reduceBoolPred : Lean.Name → ℕ → (String → String → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  [LieModule.IsNilpotent L M], ⨅ k, LieModule.lowerCentralSeries R L M k = ⊥
-- Mathlib.Algebra.Group.Units.Defs
/-- Partial division, denoted `a /ₚ u`. It is defined when the
second argument is invertible, and unlike the division operator
in `DivisionRing` it is not totalized at zero.  -/
«term_/ₚ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.starPullbackIsoStar_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Over.starPullbackIsoStar f).inv.app X_1).left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f X_1).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).inv
        (CategoryTheory.Limits.pullback.map CategoryTheory.Limits.prod.fst f
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
              (CategoryTheory.CategoryStruct.id (Y ⨯ X_1)))
            CategoryTheory.Limits.prod.fst)
          f (CategoryTheory.CategoryStruct.id (Y ⨯ X_1)) (CategoryTheory.CategoryStruct.id X)
          (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯))
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.perfectRing : ∀ (k : Type u) [inst : Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [IsAlgClosed k], PerfectRing k p
-- Mathlib.Topology.Continuous
/-- Composition of a continuous map with dense range and a function with dense range has dense
range.  -/
DenseRange.comp : ∀ {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {α : Type u_4} {g : Y → Z}
  {f : α → Y}, DenseRange g → DenseRange f → Continuous g → DenseRange (g ∘ f)
-- Std.Time.Format.Basic
/-- The format parses any timezone.  -/
Std.Time.Awareness.any : Std.Time.Awareness
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.map₂_coe_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] (a : α) (b : β) (f : α → β → γ),
  UniformContinuous₂ f → UniformSpace.Completion.map₂ f ↑a ↑b = ↑(f a b)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The operation `lift` is natural.  -/
CategoryTheory.FreeGroupoid.mapCompLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        {E : Type u₂} →
          [inst_2 : CategoryTheory.Groupoid E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                (CategoryTheory.FreeGroupoid.map F).comp (CategoryTheory.FreeGroupoid.lift G) ≅
                  CategoryTheory.FreeGroupoid.lift (F.comp G)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.comap_incl_self : ∀ {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), LieSubmodule.comap N.incl N = ⊤
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_empty : ∀ {α : Type u_1} {i : ℕ} {a : α}, #v[].setIfInBounds i a = #v[]
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM.inj : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {inst : Semiring 𝕜₁} {inst_1 : Semiring 𝕜₂} {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} {inst_2 : AddCommGroup E} {inst_3 : TopologicalSpace E} {inst_4 : Module 𝕜₁ E}
  {inst_5 : AddCommGroup F} {inst_6 : TopologicalSpace F} {inst_7 : Module 𝕜₂ F} {toCLM toCLM_1 : E →SL[σ] F},
  ContinuousLinearMapWOT.ofCLM toCLM = ContinuousLinearMapWOT.ofCLM toCLM_1 → toCLM = toCLM_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isSome_get?_iff_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.Algebra.Quaternion
Quaternion.algebraMap_def : ∀ {R : Type u_3} [inst : CommRing R], ⇑(algebraMap R (Quaternion R)) = Quaternion.coe
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_eq_zero : ∀ {x : ℕ}, ArithmeticFunction.zeta x = 0 ↔ x = 0
-- Init.Data.Option.Lemmas
Option.eq_some_of_pfilter_eq_some : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {a : α}, o.pfilter p = some a → o = some a
-- Mathlib.RepresentationTheory.Basic
Representation.tprod_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρV : Representation k G V) (ρW : Representation k G W) (g : G), (ρV.tprod ρW) g = TensorProduct.map (ρV g) (ρW g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.mk.sizeOf_spec : ∀ (triggerCharacters? allCommitCharacters? : Option (Array String)) (resolveProvider : Bool),
  sizeOf
      { triggerCharacters? := triggerCharacters?, allCommitCharacters? := allCommitCharacters?,
        resolveProvider := resolveProvider } =
    1 + sizeOf triggerCharacters? + sizeOf allCommitCharacters? + sizeOf resolveProvider
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isGround.injEq : ∀ (bvarIdx bvarIdx_1 : ℕ),
  (Lean.Meta.Grind.EMatchTheoremConstraint.isGround bvarIdx =
      Lean.Meta.Grind.EMatchTheoremConstraint.isGround bvarIdx_1) =
    (bvarIdx = bvarIdx_1)
-- Batteries.Recycling.RBTree.Basic
RBTree.instReprRBNode : {α : Type u_1} → [Repr α] → Repr (RBTree.RBNode α)
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- An equicontinuous family of functions defined on a compact uniform space is automatically
uniformly equicontinuous.  -/
CompactSpace.uniformEquicontinuous_of_equicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι : Type u_4} {F : ι → β → α}
  [CompactSpace β], Equicontinuous F → UniformEquicontinuous F
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.qaryEntropy_two : Real.qaryEntropy 2 = Real.binEntropy
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- `S (p + 1) i` can be written as the image of a `biUnion`  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.S_succ_eq_biUnion : ∀ {n p : ℕ} (i : Fin n),
  BirdDet.S✝ (p + 1) i = (Finset.Ioi i).biUnion fun k => Finset.image (Fin.cons k) (BirdDet.S✝ p k)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instIsCharPInt16HPowNatOfNat : Lean.Grind.IsCharP Int16 (2 ^ 16)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.IsMinimalPrime.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (I p : Ideal R), I.IsMinimalPrime p = Minimal (fun q => q.IsPrime ∧ I ≤ q) p
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_of_mem_val_ofUnits : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {y : Mˣ}, ↑y ∈ S.ofUnits → y ∈ S
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- For a point inside or on the sphere, the product of distances to two intersection
points on a line through the point equals the negative of the power of the point.  -/
EuclideanGeometry.Sphere.mul_dist_eq_neg_power_of_dist_center_le_radius : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p a b : P},
  0 ≤ s.radius → p ∈ line[ℝ, a, b] → a ∈ s → b ∈ s → dist p s.center ≤ s.radius → dist p a * dist p b = -s.power p
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.instMonadPrettyFormatStateMTaggedState : Std.Format.MonadPrettyFormat (StateM Lean.Widget.TaggedText.TaggedState✝)
-- Mathlib.Algebra.Module.Injective
Module.Baer.iff_surjective : ∀ {M : Type u_1} [inst : AddCommGroup M] {R : Type u} [inst_1 : CommRing R] [inst_2 : Module R M],
  Module.Baer R M ↔ ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.max?.isSome = !t.isEmpty
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_sup_left : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  a ≤ a ⊔ b
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F =
    CategoryTheory.preadditiveCoyonedaObj
      (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator✝ F)
-- Mathlib.Logic.Basic
mem_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a : α} {s t : β},
  (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t)
-- Mathlib.Topology.NhdsWithin
nhds_bind_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α},
  ((nhds a).bind fun x => nhdsWithin x s) = nhdsWithin a s
-- Mathlib.Algebra.Ring.Divisibility.Basic
dvd_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Semigroup α] [LeftDistribClass α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b + c
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.lift.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f f_1 : { a // a ≠ 0 } → α) (e_f : f = f_1)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ = FiniteArchimedeanClass.mk ↑b ⋯ → f a = f b)
  (a a_1 : FiniteArchimedeanClass M),
  a = a_1 → FiniteArchimedeanClass.lift f h a = FiniteArchimedeanClass.lift f_1 ⋯ a_1
-- Init.Data.Rat.Basic
/-- The ceiling of a rational number `a` is the smallest integer greater than or equal to `a`.  -/
Rat.ceil : ℚ → ℤ
-- Init.Grind.Config
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`.  -/
Lean.Grind.Config.ext : Lean.Grind.Config → Bool
-- Mathlib.Algebra.Group.Center
IsAddCentral.right_comm : ∀ {M : Type u_1} {c : M} [inst : Add M], IsAddCentral c → ∀ (a b : M), a + b + c = a + c + b
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.leftUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.OplaxTrans.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.Data.Finset.Grade
Finset.covBy_iff_card_sdiff_eq_one : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1
-- Mathlib.RingTheory.Derivation.Basic
/-- `coeFn` as an `AddMonoidHom`.  -/
Derivation.coeFnAddMonoidHom : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Derivation R A M →+ A → M
-- Mathlib.Data.Multiset.MapFold
Multiset.map_pmap : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α)
  (H : ∀ a ∈ s, p a), Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_zero : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)],
  (LinearMap.pi fun x => 0) = 0
-- Init.Data.Dyadic.Basic
Dyadic.toRat_inj : ∀ {x y : Dyadic}, x.toRat = y.toRat ↔ x = y
-- Mathlib.Order.RelIso.Basic
/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the sum.
 -/
RelIso.sumLexCongr : {α₁ : Type u_5} →
  {α₂ : Type u_6} →
    {β₁ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {r₂ : α₂ → α₂ → Prop} →
            {s₁ : β₁ → β₁ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r s₁ → r₂ ≃r s₂ → Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- The stream of `IntFractPair`s of an integer stops after the first term.
 -/
GenContFract.IntFractPair.stream_succ_of_int : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] (a : ℤ)
  (n : ℕ), GenContFract.IntFractPair.stream (↑a) (n + 1) = none
-- Mathlib.Data.Finite.Defs
instInfinitePLift : ∀ {α : Sort u_1} [Infinite α], Infinite (PLift α)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `MultipliableUniformly f` means that there is some infinite product to which
`f` converges uniformly. Use `fun x ↦ ∏' i, f i x` to get the product function.  -/
MultipliableUniformly : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → [UniformSpace α] → Prop
-- Init.Data.String.Pattern.Basic
/-- Provides a conversion from a pattern to an iterator of `SearchStep` searching for matches of
the pattern from the end towards the start of a `Slice`.

While these operations can be implemented on top of `BackwardPattern`, some patterns allow
for more efficient implementations. For example, a searcher for `String` patterns derived
from the `BackwardPattern` instance on strings would try to match the pattern at every
position in the string, but more efficient string matching routines are known. Indeed, the Lean
standard library uses the Knuth-Morris-Pratt algorithm. See the module
`Init.Data.String.Pattern.String` for the implementation.

This class can be used to provide such an efficient implementation. If there is no
need to specialize in this fashion, then
`ToBackwardSearcher.defaultImplementation` can be
used to automatically derive an instance.
 -/
String.Slice.Pattern.ToBackwardSearcher : {ρ : Type} → ρ → outParam (String.Slice → Type) → Type
-- Mathlib.Order.Minimal
/-- **Alias** of `image_antitone_setOfPred_minimal_mem`. -/
image_antitone_setOf_minimal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) →
    f '' {x | Minimal (fun x => x ∈ s) x} = {x | Maximal (fun x => x ∈ f '' s) x}
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.map_r_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) (F : CategoryTheory.Functor C D),
  (h.map F).r.left = F.map (CategoryTheory.Arrow.Hom.left h.r)
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B) (a : A),
  (MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a = if h : f a = 0 then 0 else ↑⟨Units.mk0 (f a) h, ⋯⟩
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.unit_naturality : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₁.obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app X) (α.r.toFunctor.map (α.l.toFunctor.map f)) =
    CategoryTheory.CategoryStruct.comp f (α.adj.unit.toNatTrans.app Y)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_7 : ∀ (cf cg : Nat.Partrec.Code),
  (cf.prec cg).eval =
    Nat.unpaired fun a n =>
      Nat.rec (cf.eval a)
        (fun y IH => do
          let i ← IH
          cg.eval (Nat.pair a (Nat.pair y i)))
        n
-- Mathlib.Topology.Separation.Basic
R0Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X], Std.Symm Specializes → R0Space X
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_push_iff : ∀ {α : Type u_1} {β : Type u_2} {ys : Array β} {xs : Array α} {b : β} {f : (i : ℕ) → α → i < xs.size → β},
  xs.mapFinIdx f = ys.push b ↔
    ∃ zs a, ∃ (w : xs = zs.push a), (zs.mapFinIdx fun i a_1 h => f i a_1 ⋯) = ys ∧ b = f (xs.size - 1) a ⋯
-- Mathlib.Topology.UnitInterval
unitInterval.eq_closedBall : unitInterval = Metric.closedBall 2⁻¹ 2⁻¹
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' : ∀ (n : ℕ), Real.eulerMascheroniConstant < Real.eulerMascheroniSeq' n
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The unit of the constructed pointwise left Kan extension when
`HasPointwiseLeftKanExtension L F` holds.  -/
CategoryTheory.Functor.pointwiseLeftKanExtensionUnit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] → F ⟶ L.comp (L.pointwiseLeftKanExtension F)
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.ext : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsContPerfPair}, x = y
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_inf : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b c : CauSeq α abs},
  a < b → a < c → a < b ⊓ c
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.comp_mapMon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.MonObj.one)
-- Mathlib.Topology.Instances.Rat
Nat.dist_cast_rat : ∀ (x y : ℕ), dist ↑x ↑y = dist x y
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- The `AugmentedSimplexCategory` is the category obtained from `SimplexCategory` by adjoining an
initial object.  -/
AugmentedSimplexCategory : Type
-- Mathlib.MeasureTheory.Measure.Restrict
/-- In a measure space, one can restrict the measure to a subtype to get a new measure space.
Not registered as an instance, as there are other natural choices such as the normalized restriction
for a probability measure, or the subspace measure when restricting to a vector subspace. Enable
locally if needed with `attribute [local instance] Measure.Subtype.measureSpace`.  -/
MeasureTheory.Measure.Subtype.measureSpace : {δ : Type u_4} → [MeasureTheory.MeasureSpace δ] → {p : δ → Prop} → MeasureTheory.MeasureSpace (Subtype p)
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort.eq_2 : ∀ (x : Lean.Grind.AC.Var) (s_2 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s_2).sort = s_2.sort' (Lean.Grind.AC.Seq.var x)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_ofReal_of_neg : ∀ {x : ℝ}, x < 0 → (↑x).arg = Real.pi
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`.  -/
BitVec.reduceGetLsb : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.coe_splitUpper : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, ↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivWithinAt.neg` -/
HasDerivWithinAt.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun i => -f i) (-f') s x