mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite =
  { hom := fun {X Y} f => f.hom', ofHom := fun {X Y} f => { hom' := f },
    hom_ofHom :=
      @instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_1,
    ofHom_hom :=
      @instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_2,
    id_apply :=
      @instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_3,
    comp_apply :=
      @instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_4 }
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.smul_def : ∀ {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.MonoidalLeftAction C D]
  (X : D), CategoryTheory.ModObj.smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_top_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⊤.relIndex H = 1
-- Mathlib.Order.Closure
ClosureOperator.isClosed_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] (c : ClosureOperator α), c.IsClosed ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.strongMonoCategory_of_regularMonoCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsRegularMonoCategory C],
  CategoryTheory.StrongMonoCategory C
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gt`. -/
Polynomial.abs_div_tendsto_atTop_of_degree_gt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    Q ≠ 0 → Filter.Tendsto (fun x => |Polynomial.eval x P / Polynomial.eval x Q|) Filter.atTop Filter.atTop
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax.inj : ∀ {kind : Lean.SyntaxNodeKind} {a : Lean.TSyntax kind} {kind_1 : Lean.SyntaxNodeKind} {a_1 : Lean.TSyntax kind_1},
  Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a = Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a_1 →
    kind = kind_1 ∧ a ≍ a_1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_add_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree g) < m.toSyn (m.degree f) → m.leadingCoeff (f + g) = m.leadingCoeff f
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The equivalence of categories
`(Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              (X₂ : C₂) → (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] (e : E ≃L[𝕜] E') (x : M),
  ↑(extChartAt (I.transContinuousLinearEquiv e) x) = ⇑e ∘ ↑(extChartAt I x)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.instStrongHomClassOfIsAlgebraic : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] [L.IsAlgebraic],
  L.StrongHomClass (L.Hom M N) M N
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.TreeMap.getEntryGE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option (α × β)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- The filter on the collection of all the finite sequences of `uIoc` intervals induced by the
function that maps the finite sequence of the intervals to the total length of the intervals.
Details:
1. Technically the filter is on `ℕ × (ℕ → X × X)`. A finite sequence `uIoc (a i) (b i)`, `i < n`
   is represented by any `E : ℕ × (ℕ → X × X)` which satisfies `E.1 = n` and `E.2 i = (a i, b i)`
   for `i < n`. Its total length is `∑ i ∈ Finset.range n, dist (a i) (b i)`.
2. For a sequence `G : ℕ → ℕ × (ℕ → X × X)`, convergence of `G` along `totalLengthFilter` means that
   the total length of `G j`, i.e., `∑ i ∈ Finset.range (G j).1, dist ((G j).2 i).1 ((G j).2 i).2)`,
   tends to `0` as `j` tends to infinity.
 -/
AbsolutelyContinuousOnInterval.totalLengthFilter : {X : Type u_1} → [PseudoMetricSpace X] → Filter (ℕ × (ℕ → X × X))
-- Mathlib.Data.Sum.Order
Sum.instLESum : {α : Type u_1} → {β : Type u_2} → [LE α] → [LE β] → LE (α ⊕ β)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₂_hom_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑(groupHomology.cycles A 2)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesMap f φ 2)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).hom) x)
-- Mathlib.Order.WellFoundedSet
/-- This indicates that every bad sequence `g` that agrees with `f` on the first `n`
terms has `rk (f n) ≤ rk (g n)`.  -/
Set.PartiallyWellOrderedOn.IsMinBadSeq : {α : Type u_2} → (α → α → Prop) → (α → ℕ) → Set α → ℕ → (ℕ → α) → Prop
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.image_Ioi_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictAntiOn f (Set.Ici a) → f '' Set.Ioi a ⊆ Set.Iio (f a)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.instCoeOutMatroidᵣ : {α : Type u_2} → CoeOut (Matroid.Matroidᵣ α) (Matroid α)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.hole.injEq : ∀ (name name_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MRefinePat.hole name = Lean.Parser.Tactic.MRefinePat.hole name_1) = (name = name_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_sum : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R),
  (∑ i ∈ s, f i).toFinsupp = ∑ i ∈ s, (f i).toFinsupp
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.WeakEquivalence.mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} [self : HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.weakEquivalences C f
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Continuous constant functions as a `RingHom`.  -/
ContinuousMap.C : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] → [Algebra R A] → [inst_5 : IsTopologicalSemiring A] → R →+* C(α, A)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGTD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  Std.DTreeMap.Internal.Impl.getKeyGTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGT? k t).getD fallback
-- Mathlib.Data.Part
Part.instCoeOption : {α : Type u_1} → Coe (Option α) (Part α)
-- Init.Data.Nat.Gcd
Nat.gcd_zero_right : ∀ (n : ℕ), n.gcd 0 = n
-- Aesop.Stats.Basic
Aesop.Stats.script : Aesop.Stats → Aesop.Nanos
-- Std.Time.Format
/-- Formats a `DateTime` using a specific format.
 -/
Std.Time.DateTime.format : Std.Time.DateTime → String → String
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseₘaux.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.eraseₘaux a =
    ⟨{ size := (↑m).size - 1,
        buckets :=
          Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.erase a l },
      ⋯⟩
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A strongly measurable function is almost everywhere measurable.  -/
MeasureTheory.StronglyMeasurable.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α},
  MeasureTheory.StronglyMeasurable f → AEMeasurable f μ
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The isomorphism `S.cycles ≅ h.K` induced by a left homology data `h` for a
short complex `S`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h : S.LeftHomologyData) → [inst_2 : S.HasLeftHomology] → S.cycles ≅ h.K
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.isBotZeroClass : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)], IsBotZeroClass (Colex (Π₀ (i : ι), α i))
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- The morphism in the fiber over `S` corresponding to a morphism in `𝒳` lifting `𝟙 S`.  -/
CategoryTheory.Functor.Fiber.homMk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          (S : 𝒮) →
            {a b : 𝒳} →
              (φ : a ⟶ b) →
                [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ] →
                  CategoryTheory.Functor.Fiber.mk ⋯ ⟶ CategoryTheory.Functor.Fiber.mk ⋯
-- Std.Http.Protocol.H1
/-- Processes connection-close body output (HTTP/1.0 server, unknown body length).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processClosingFrameBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.mk.injEq : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (carrier : IntermediateField F E) (emb : ↥carrier →ₐ[F] K)
  (carrier_1 : IntermediateField F E) (emb_1 : ↥carrier_1 →ₐ[F] K),
  ({ carrier := carrier, emb := emb } = { carrier := carrier_1, emb := emb_1 }) = (carrier = carrier_1 ∧ emb ≍ emb_1)
-- Mathlib.RingTheory.Int.Basic
Int.prime_iff_natAbs_prime : ∀ {k : ℤ}, Prime k ↔ Nat.Prime k.natAbs
-- Mathlib.Algebra.Algebra.Tower
Submodule.span_algebraMap_image_of_tower : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_1} {T : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Module R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (a : Set S),
  Submodule.span R (⇑(algebraMap S T) '' a) = Submodule.map (↑R (Algebra.linearMap S T)) (Submodule.span R a)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_subset_add : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s → a +ᵥ t ⊆ s + t
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_lt_aleph_one : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c < Cardinal.aleph 1 ↔ c < Cardinal.aleph 1
-- Mathlib.CategoryTheory.Action.Basic
Action.id_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (M : Action V G),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.V
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.getSparseCasesOnInfo : Lean.Name → Lean.CoreM (Option Lean.Meta.SparseCasesOnInfo)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_dvd_iff : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] {r : R} {z : QuadraticAlgebra R a b},
  (algebraMap R (QuadraticAlgebra R a b)) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V] {N : WithTop ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ) →
    MeasureTheory.AEStronglyMeasurable f μ →
      HasFTaylorSeriesUpTo N (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
        fun w n =>
        VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
          (fun v => VectorFourier.fourierPowSMulRight L f v n) w
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_inverse : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (TopCat.Presheaf.generateEquivalenceOpensLe U hY).inverse = TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY
-- Init.Data.Vector.Range
Vector.range'_eq_append_iff : ∀ {s n m : ℕ} {xs : Vector ℕ n} {ys : Vector ℕ m},
  Vector.range' s (n + m) = xs ++ ys ↔ xs = Vector.range' s n ∧ ys = Vector.range' (s + n) m
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`.  -/
CategoryTheory.Limits.Fan : {β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Type (max (max w u) v)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.literal.inj : ∀ {α : Type} {a a_1 : α}, Std.Tactic.BVDecide.BoolExpr.literal a = Std.Tactic.BVDecide.BoolExpr.literal a_1 → a = a_1
-- Mathlib.NumberTheory.Divisors
/-- The `Finset` and `List` versions agree by definition.  -/
Nat.val_divisorsAntidiagonal : ∀ (n : ℕ), n.divisorsAntidiagonal.val = ↑n.divisorsAntidiagonalList
-- Lean.Syntax
Lean.Syntax.asNode : Lean.Syntax → Lean.SyntaxNode
-- Init.Data.List.Basic
List.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), List.map f [] = []
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt32
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_1.eq_3 : ∀ {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ Id β₁] {it₁ : Std.Iter β₁} (motive : it₁.Step → Sort u_2)
  (hp : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.Iter β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.Iter β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.done, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_3 hp
-- Init.Data.String.Slice
/-- Removes trailing whitespace from a slice by moving its end position to the last non-whitespace
character, or to its start position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".toSlice.trimAsciiEnd == "abc".toSlice`

* `"   abc".toSlice.trimAsciiEnd == "   abc".toSlice`

* `"abc \t  ".toSlice.trimAsciiEnd == "abc".toSlice`

* `"  abc   ".toSlice.trimAsciiEnd == "  abc".toSlice`

* `"abc\ndef\n".toSlice.trimAsciiEnd == "abc\ndef".toSlice`
 -/
String.Slice.trimAsciiEnd : String.Slice → String.Slice
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The morphism that is part of a morphism of costructured arrows.  -/
CategoryTheory.CostructuredArrow.Hom.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} → {X Y : CategoryTheory.CostructuredArrow S T} → (X ⟶ Y) → (X.left ⟶ Y.left)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Evaluate the `Trie α` at index `trie`,
replacing it with the evaluated value,
and returning the `Trie α`.

Performance note: In the `apply` search discrimination tree, after root node `⟨Eq, 3⟩`,
there are about `150,000` entries in the `pending` array.
To deal with this smoothly, we parallelize the computation into chunks of `5000` entries.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.evalNode : {α : Type} →
  Lean.Meta.RefinedDiscrTree.TrieIndex → Lean.Meta.RefinedDiscrTree.TreeM✝ α (Lean.Meta.RefinedDiscrTree.Trie α)
-- Init.Data.Array.Lemmas
Array.contains_eq_true_of_mem : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a : α} {as : Array α}, a ∈ as → as.contains a = true
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.tsumNormRPowBound_spec : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  (L : Submodule ℤ E) [inst_3 : DiscreteTopology ↥L],
  ∀ r < -↑(Module.finrank ℤ ↥L),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ ZLattice.tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.newArg? : Lean.Elab.DeprecatedArgEntry → Option Lean.Name
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.so.eq_1 : ∀ (n : Type u_1) (R : Type u₂) [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LieAlgebra.Orthogonal.so n R = skewAdjointMatricesLieSubalgebra 1
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.smul_comp : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Zero A] [inst_1 : Zero B] [inst_2 : Zero C]
  [inst_3 : SMulZeroClass M C] (m : M) (g : ZeroHom B C) (f : ZeroHom A B), (m • g).comp f = m • g.comp f
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.lineDifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E}, LineDifferentiableAt 𝕜 f x v → LineDifferentiableWithinAt 𝕜 f s x v
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_functor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (self : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.obj self = self.unmop
-- Mathlib.Algebra.Group.Ext
Group.toDivInvMonoid_injective : ∀ {G : Type u_1}, Function.Injective (@Group.toDivInvMonoid G)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E}, DifferentiableAt 𝕜 f x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_self : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] (v : Projectivization F (Fin 3 → F)), v.cross v = v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGED.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.getEntryGED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGE? k t).getD fallback
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult : Type
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction.parseDelete : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Mathlib.Topology.Compactification.StoneCech
/-- The basic open sets for the topology on ultrafilters are also closed.  -/
ultrafilter_isClosed_basic : ∀ {α : Type u} (s : Set α), IsClosed {u | s ∈ u}
-- Init.Data.Iterators.Basic
Std.Iter.step_eq : ∀ {α β : Type u_1} {IsPlausibleStep : Std.IterM Id β → Std.IterStep (Std.IterM Id β) β → Prop}
  {step : (it : Std.IterM Id β) → Id (Std.Shrink (Std.PlausibleIterStep (IsPlausibleStep it)))} {it : Std.Iter β},
  it.step = Std.IterM.Step.toPure (step it.toIterM).run.inflate
-- Mathlib.Algebra.Star.Center
Set.star_centralizer : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {s : Set R}, star s.centralizer = (star s).centralizer
-- Mathlib.Data.Set.Insert
Set.inter_singleton_eq_empty : ∀ {α : Type u_1} {s : Set α} {a : α}, s ∩ {a} = ∅ ↔ a ∉ s
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow_iff : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {m n : ℕ}, 0 < m → 0 < n → (IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y)
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.extendRCLikeL_symm_apply_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : WeakDual 𝕜 F) (x : F), (WeakDual.extendRCLikeL.symm f) x = RCLike.re (f x)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.farFromTriangleFree_iff : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {G : SimpleGraph α} {ε : 𝕜}
  [inst_2 : Fintype α] [inst_3 : DecidableRel G.Adj],
  G.FarFromTriangleFree ε ↔
    ∀ ⦃H : SimpleGraph α⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
-- Mathlib.Logic.Equiv.Finset
/-- If `α` is encodable, then so is `Finset α`.  -/
Finset.encodable : {α : Type u_1} → [Encodable α] → Encodable (Finset α)
-- Init.Data.UInt.Bitwise
UInt8.toNat_or : ∀ (a b : UInt8), (a ||| b).toNat = a.toNat ||| b.toNat
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, a ∈ t)
-- Mathlib.Combinatorics.Graph.Basic
/-- A graph with one vertex and loops at that vertex. This is an abbreviation for the special case
of `banana` where the two vertices are the same. Most lemmas about `bouquet` should instead be
proved using `banana` instead.  -/
Graph.bouquet : {α : Type u_1} → {β : Type u_2} → α → Set β → Graph α β