mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instTop : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → Top ↥L
-- Mathlib.Order.Basic
LinearOrder.ext : ∀ {α : Type u_2} {A B : LinearOrder α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- Auxiliary definition for `FunctorialFactorizationData.functorCategory`.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      W₁.FunctorialFactorizationData W₂ →
        (J : Type u_3) →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} J] →
            CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Functor J C)) (CategoryTheory.Functor J C)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_fderivWithin_iteratedFDerivWithin : ∀ {𝕜 : 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 : E → F} {x : E} {n : ℕ},
  ‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
CochainComplex.instFullIntSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ), (CochainComplex.singleFunctor C n).Full
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_d20 : 3.14159265358979323846 < Real.pi
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_intermediateDropWhileM : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] {it : Std.IterM m β} {P : β → m (ULift.{u_1, 0} Bool)} {dropping : Bool},
  (Std.IterM.Intermediate.dropWhileM P dropping it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        if h' : dropping = true then do
          let __do_lift ← MonadAttach.attach (P out)
          match __do_lift with
            | ⟨{ down := true }, hP⟩ =>
              pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileM P true it') ⋯))
            | ⟨{ down := false }, hP⟩ =>
              pure
                (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileM P false it') out ⋯))
        else
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileM P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileM P dropping it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Init.Data.SInt.Bitwise
instAssociativeInt32HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.RingTheory.IsTensorProduct
/-- If `M` is the tensor product of `M₁` and `M₂`, we may lift a bilinear map `M₁ →ₗ[R] M₂ →ₗ[R] M'`
to a `M →ₗ[R] M'`.  -/
IsTensorProduct.lift : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M₁ : Type u_2} →
      {M₂ : Type u_3} →
        {M : Type u_4} →
          {M' : Type u_5} →
            [inst_1 : AddCommMonoid M₁] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : AddCommMonoid M'] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M] →
                          [inst_8 : Module R M'] →
                            {f : M₁ →ₗ[R] M₂ →ₗ[R] M} → IsTensorProduct f → (M₁ →ₗ[R] M₂ →ₗ[R] M') → M →ₗ[R] M'
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.refl_prod_refl : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (OpenPartialHomeomorph.refl X).prod (OpenPartialHomeomorph.refl Y) = OpenPartialHomeomorph.refl (X × Y)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.IsSplitMono f], CategoryTheory.Limits.IsZero X ↔ f = 0
-- Mathlib.Order.Directed
isBot_or_exists_lt : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] (a : α), IsBot a ∨ ∃ b, b < a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  (CategoryTheory.ShortComplex.homologyMap φ).op =
    CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.homologyOpIso.hom)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of an antitone function and a strictly antitone function is
strictly antitone.  -/
AntitoneOn.add_strictAnti : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
  [AddLeftStrictMono α] [AddRightMono α] {f g : β → α},
  AntitoneOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x + g x) s
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixingSubgroup_le_of_le : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F F' : IntermediateField K L),
  F ≤ F' → fixingSubgroup G ↑F' ≤ fixingSubgroup G ↑F
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A sesquilinear form `B` is **nonnegative** if for any `x` we have `0 ≤ B x x`.  -/
LinearMap.IsNonneg : {R : Type u_1} →
  {M : Type u_5} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {I₁ I₂ : R →+* R} → [LE R] → (M →ₛₗ[I₁] M →ₛₗ[I₂] R) → Prop
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivWithinAt_add_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt (fun x => f x + c) f' s x ↔ HasDerivWithinAt f f' s x
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} {x y : CategoryTheory.Kleisli T}
  {f g : x ⟶ y}, f.of = g.of → f = g
-- Mathlib.ModelTheory.Types
/-- **Alias** of `FirstOrder.Language.Theory.CompleteType.setOfPred_mem_eq_univ_iff`. -/
FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : (L.withConstants α).Sentence),
  {p | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
_private.Mathlib.Algebra.ContinuedFractions.Computation.Translations.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_comp : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {ξ : MeasureTheory.Measure γ} (g : γ →ₘ[ξ] δ) {f : β → γ}
  (hf : MeasureTheory.MeasurePreserving f ν ξ) {f' : α → β} (hf' : MeasureTheory.MeasurePreserving f' μ ν),
  g.compMeasurePreserving (f ∘ f') ⋯ = (g.compMeasurePreserving f hf).compMeasurePreserving f' hf'
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.mem_torsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ},
  x ∈ NumberField.Units.torsion K ↔
    ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1
-- Mathlib.Logic.ExistsUnique
ExistsUnique.exists₂ : ∀ {α : Sort u_1} {p : α → Sort u_2} {q : (x : α) → p x → Prop}, (∃! x, ∃! hx, q x hx) → ∃ x hx, q x hx
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₃_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 3),
  ∃ X₀ X₁ X₂ X₃ f₀ f₁ f₂, X = CategoryTheory.ComposableArrows.mk₃ f₀ f₁ f₂
-- Mathlib.CategoryTheory.Countable
/-- Applying `ULift` to morphisms and objects of a category preserves countability.  -/
CategoryTheory.countableCategoryUlift : ∀ {J : Type v} [inst : CategoryTheory.Category.{v, v} J] [CategoryTheory.CountableCategory J],
  CategoryTheory.CountableCategory (CategoryTheory.ULiftHom (ULift.{w, v} J))
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_neg : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {f : M →ₗ[R] M₂} {p : Submodule R M₂},
  Submodule.comap (-f) p = Submodule.comap f p
-- Lean.Expr
Lean.instReprLiteral.repr : Lean.Literal → ℕ → Std.Format
-- Init.SimpLemmas
or_self : ∀ (p : Prop), (p ∨ p) = p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_iso_hom_app : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).iso.hom.app X_1 = (J.obj X_1).iso.hom
-- Mathlib.Computability.RecursiveIn
/-- Monotonicity of `RecursiveIn` with respect to oracle sets.  -/
RecursiveIn.mono : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {O₁ O₂ : Set (ℕ →. ℕ)},
  O₁ ⊆ O₂ → RecursiveIn O₁ f → RecursiveIn O₂ f
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions : ∀ {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)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B),
  J.PreservesSheafification F ↔
    ∀ (P : CategoryTheory.Functor Cᵒᵖ A),
      CategoryTheory.IsIso (G₂.map (CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F))
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_self : ∀ {a : ℤ}, a.tmod a = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instModule_1 : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [Module R M] → Module (ArithmeticFunction R) (ArithmeticFunction M)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.coe_toOrthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : HilbertBasis ι 𝕜 E), ⇑b.toOrthonormalBasis = ⇑b
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fx : γ) → motive (some fx)) → motive __do_lift
-- Lean.Util.CollectMVars
Lean.CollectMVars.instInhabitedState : Inhabited Lean.CollectMVars.State
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.toMatrix_lsmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x : R),
  (LinearMap.toMatrix b b) ((Algebra.lsmul R R S) x) = Matrix.diagonal fun x_1 => x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Finset`. See note [pointwise nat action].  -/
Finset.zpow : {α : Type u_2} → [DecidableEq α] → [One α] → [Mul α] → [Inv α] → Pow (Finset α) ℤ
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom)
-- Mathlib.Data.Finset.SDiff
Finset.mem_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s \ t ↔ a ∈ s ∧ a ∉ t
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_mapWithPostcondition_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {δ : Type w} [inst_1 : Monad m] [LawfulMonad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ}
  {g : γ → Std.Iterators.PostconditionT n δ},
  (Std.IterM.mapWithPostcondition g (Std.Iter.mapWithPostcondition f it)).toArray =
    (Std.Iter.mapWithPostcondition (fun b => liftM (f b) >>= g) it).toArray
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_left_eq_Ioc_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert a (Set.Ioc a b) = Set.Ioc (a - 1) b
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x),
  h.uliftYonedaIso.hom = CategoryTheory.uliftYonedaEquiv.symm { down := x }
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω},
  MeasurableSet s →
    (μ.tilted fun x => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a) / ProbabilityTheory.mgf X μ t ∂μ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  l.length ≤ (Std.Internal.List.eraseKey k l).length + 1
-- Lean.Elab.App
/-- This method executes after all application arguments have been processed.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.finalize : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.RingTheory.Nilpotent.Basic
isNilpotent_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R},
  (∀ i ∈ s, IsNilpotent (f i)) → IsNilpotent (∑ i ∈ s, f i)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_eq_two : ∀ {α : Type u_1} {v : FreeAddMonoid α}, v.length = 2 ↔ ∃ c d, v = FreeAddMonoid.of c + FreeAddMonoid.of d
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_mul_iff_left : ∀ {a b c : ℤ}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- If `s : Set 𝕜` with `RCLike 𝕜` is compact and contains `0`, then the non-unital star subalgebra
generated by the identity function in `C(s, 𝕜)₀` is dense. This can be seen as a version of the
Weierstrass approximation theorem.  -/
ContinuousMapZero.adjoin_id_dense : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : Fact (0 ∈ s)] [CompactSpace ↑s],
  Dense ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id s})
-- Init.Data.String.TakeDrop
/-- Returns a `String.Slice` obtained by removing the specified number of characters \(Unicode code
points\) from the end of the string.

If `n` is greater than `s.toList.length`, returns an empty slice.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

Examples:

* `"red green blue".dropEnd 5 == "red green".toSlice`

* `"red green blue".dropEnd 11 == "red".toSlice`

* `"red green blue".dropEnd 50 == "".toSlice`

* `"مرحبا بالعالم".dropEnd 3 == "مرحبا بالع".toSlice`
 -/
String.dropEnd : String → ℕ → String.Slice
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_1.go : {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
    {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
      {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
        (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
          ((t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t) →
            ((t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t) →
              ((t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                  Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t) →
                ((t : String × Lean.Elab.ConfigEval.HandlerTrie✝) →
                    Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t) →
                  motive_2 t ×' Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t
-- Std.Time.Time.Unit.Second
Std.Time.Second.instSubOffset : Sub Std.Time.Second.Offset
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.le_toOuterMeasure_caratheodory : ∀ {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α), ms ≤ μ.caratheodory
-- Init.Data.SInt.Basic
instHashableInt16 : Hashable Int16
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomSurjective.mk : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂},
  Function.Surjective ⇑σ → RingHomSurjective σ
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.hasToJson : Lean.ToJson Lean.Lsp.TextDocumentContentChangeEvent
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Create a semilinear map between Schwartz spaces.

Note: This is a helper definition for `mkCLM`.  -/
SchwartzMap.mkLM : {𝕜 : Type u_2} →
  {𝕜' : Type u_3} →
    {D : Type u_4} →
      {E : Type u_5} →
        {F : Type u_6} →
          {G : Type u_7} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedSpace ℝ E] →
                [inst_2 : NormedAddCommGroup F] →
                  [inst_3 : NormedSpace ℝ F] →
                    [inst_4 : NormedField 𝕜] →
                      [inst_5 : NormedField 𝕜'] →
                        [inst_6 : NormedAddCommGroup D] →
                          [inst_7 : NormedSpace ℝ D] →
                            [inst_8 : NormedSpace 𝕜 E] →
                              [inst_9 : SMulCommClass ℝ 𝕜 E] →
                                [inst_10 : NormedAddCommGroup G] →
                                  [inst_11 : NormedSpace ℝ G] →
                                    [inst_12 : NormedSpace 𝕜' G] →
                                      [inst_13 : SMulCommClass ℝ 𝕜' G] →
                                        {σ : 𝕜 →+* 𝕜'} →
                                          (A : SchwartzMap D E → F → G) →
                                            (∀ (f g : SchwartzMap D E) (x : F), A (f + g) x = A f x + A g x) →
                                              (∀ (a : 𝕜) (f : SchwartzMap D E) (x : F), A (a • f) x = σ a • A f x) →
                                                (∀ (f : SchwartzMap D E), ContDiff ℝ (↑⊤) (A f)) →
                                                  (∀ (n : ℕ × ℕ),
                                                      ∃ s C,
                                                        0 ≤ C ∧
                                                          ∀ (f : SchwartzMap D E) (x : F),
                                                            ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤
                                                              C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f) →
                                                    SchwartzMap D E →ₛₗ[σ] SchwartzMap F G
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mul_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : AddCommMonoid 𝕜]
  [inst_3 : Mul 𝕜] (f g : IncidenceAlgebra 𝕜 α) (a b : α), (f * g) a b = ∑ x ∈ Finset.Icc a b, f a x * g x b
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- the underlying object of a (pre)cylinder  -/
HomotopicalAlgebra.Precylinder.I : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {A : C} → HomotopicalAlgebra.Precylinder A → C
-- Lean.Environment
/-- Maps `Visibility` to `α`.  -/
_private.Lean.Environment.0.Lean.VisibilityMap : Type → Type
-- Init.Grind.ToInt
Lean.Grind.IntInterval.ci.injEq : ∀ (lo lo_1 : ℤ), (Lean.Grind.IntInterval.ci lo = Lean.Grind.IntInterval.ci lo_1) = (lo = lo_1)
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is an `AddCommSemigroup` under pointwise operations if `α` is.  -/
Filter.addCommSemigroup : {α : Type u_2} → [AddCommSemigroup α] → AddCommSemigroup (Filter α)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_succ_dist : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  ‖newton_seq_gen✝ hnorm (n + 1) - newton_seq_gen✝ hnorm n‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen✝ p F a ^ 2 ^ n
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `(∅ ⟶ W) □ X ≅ W ◁ X` in a braided CCC with pushouts and
an initial object.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          [CategoryTheory.BraidedCategory C] →
            (X : CategoryTheory.Arrow C) →
              {I : C} →
                (i : CategoryTheory.Limits.IsInitial I) →
                  {W : C} →
                    (CategoryTheory.Arrow.mk (i.to W) □ X) ≅
                      CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W X.hom)
-- Init.Data.String.Decode
String.length_utf8EncodeChar : ∀ (c : Char), (String.utf8EncodeChar c).length = c.utf8Size