mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfShape_finite_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeSup α]
  [inst_2 : OrderBot α] [inst_3 : SemilatticeSup β] [inst_4 : OrderBot β] [inst_5 : SupBotHomClass F α β] {J : Type w}
  [inst_6 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesColimitsOfShape J (↑f).toFunctor
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.comp' : ∀ {n m : ℕ} {f : List.Vector ℕ m →. ℕ} {g : List.Vector ℕ n → List.Vector ℕ m},
  Nat.Partrec' f → Nat.Partrec'.Vec g → Nat.Partrec' fun v => f (g v)
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.le_triangEnvelope : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P ≤ P.triangEnvelope
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Restating the definition of a limit cone in terms of the ∃! operator.  -/
CategoryTheory.Limits.IsLimit.existsUnique : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F), ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.mk : Lean.Syntax → Bool → Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole] → Lean.Term → Bool → Lean.Elab.TerminationBy
-- Mathlib.Analysis.LocallyConvex.Basic
Absorbent.subset_range_iff_surjective : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {F : Type u_8} {𝕜₂ : Type u_9} [inst_3 : Semiring 𝕜₂] {σ : 𝕜₂ →+* 𝕜} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : RingHomSurjective σ] {f : F →ₛₗ[σ] E} {s : Set E}, Absorbent 𝕜 s → (s ⊆ ↑f.range ↔ Function.Surjective ⇑f)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.addEquiv_coe_eq : ∀ {X Y : Type u_1} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (e : X ≃+ Y),
  AddSemigrp.Hom.hom (AddSemigrp.ofHom ↑e) = ↑e
-- Mathlib.Topology.Continuous
ContinuousAt.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {x : X} {g : Y → Z},
  ContinuousAt g (f x) → ContinuousAt f x → ContinuousAt (g ∘ f) x
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul.toMeasurableConstSMul : ∀ {M : Type u_2} {α : Type u_3} {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableSMul M α], MeasurableConstSMul M α
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instContinuousAdd : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  ContinuousAdd (WeakDual 𝕜 E)
-- Init.Data.UInt.Lemmas
USize.toNat_one : USize.toNat 1 = 1
-- Lean.DocString.Parser
/-- Parses an argument to a role, directive, command, or code block, which may be named or positional or
a flag.
 -/
Lean.Doc.Parser.arg : Lean.Parser.ParserFn
-- Mathlib.Order.Category.BddOrd
BddOrd.mk.inj : ∀ {toPartOrd : PartOrd} {isBoundedOrder : BoundedOrder ↑toPartOrd} {toPartOrd_1 : PartOrd}
  {isBoundedOrder_1 : BoundedOrder ↑toPartOrd_1},
  { toPartOrd := toPartOrd, isBoundedOrder := isBoundedOrder } =
      { toPartOrd := toPartOrd_1, isBoundedOrder := isBoundedOrder_1 } →
    toPartOrd = toPartOrd_1 ∧ isBoundedOrder ≍ isBoundedOrder_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Computability.NFA
NFA.mk.inj : ∀ {α : Type u} {σ : Type v} {step : σ → α → Set σ} {start accept : Set σ} {step_1 : σ → α → Set σ}
  {start_1 accept_1 : Set σ},
  { step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 } →
    step = step_1 ∧ start = start_1 ∧ accept = accept_1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.integrable_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  MeasureTheory.Integrable (s.rnDeriv μ) μ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If `f : M → M'` has injective differential at `x`, it is `MDifferentiable` at `x`.  -/
mdifferentiableAt_of_mfderiv_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M} {f : M → M'},
  Function.Injective ⇑(mfderiv% f x) → MDiffAt f x
-- Init.Data.List.SplitOn.Lemmas
List.splitOn_nil : ∀ {α : Type u_1} [inst : BEq α] (a : α), List.splitOn a [] = [[]]
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- If `I : InjectiveResolution Z` and `F : C ⥤ D` is an additive functor, this is
an isomorphism between `F.rightDerivedToHomotopyCategory.obj X` and the complex
obtained by applying `F` to `I.cocomplex`.  -/
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {X : C} →
                (I : CategoryTheory.InjectiveResolution X) →
                  (F : CategoryTheory.Functor C D) →
                    [inst_5 : F.Additive] →
                      F.rightDerivedToHomotopyCategory.obj X ≅
                        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
                              (HomotopyCategory.quotient D (ComplexShape.up ℕ))).obj
                          I.cocomplex
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftEquiv_symm_apply : ∀ {ι : Type u_1} [inst : Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (l : (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] F),
  (PiTensorProduct.liftEquiv 𝕜 E F).symm l = (PiTensorProduct.lift.symm ↑l).mkContinuous ‖l‖ ⋯
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- **Alias** of `Real.nullSingletonClass_volume`. -/
Real.noAtoms_volume : MeasureTheory.NullSingletonClass MeasureTheory.volume
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- Given a bicategory `B`, `Pith B` is the bicategory obtained by discarding the non-invertible
2-cells from `B`. We implement this as a wrapper type for `B`, and use `CategoryTheory.Core`
to discard the non-invertible morphisms.  -/
CategoryTheory.Bicategory.Pith : Type u₁ → Type u₁
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toSkeleton_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : CategoryTheory.Skeleton C},
  CategoryTheory.toSkeleton X = Y ↔ Nonempty (X ≅ (CategoryTheory.fromSkeleton C).obj Y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.one_sub_sq_div_two_lt_cos : ∀ {x : ℝ}, x ≠ 0 → 1 - x ^ 2 / 2 < Real.cos x
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is closed in the valuative topology.  -/
Valuation.isClosed_closedBall : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsClosed {x | v.restrict x ≤ r}
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of the forward direction of `ZFSet.IsOrdinal.subset_iff_eq_or_mem`. -/
ZFSet.IsOrdinal.eq_or_mem_of_subset : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → x ⊆ y → x = y ∨ x ∈ y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The addition-preserving equivalence between the type of nonsingular projective points on a
Weierstrass curve `W` and the type of nonsingular points in affine coordinates.  -/
WeierstrassCurve.Projective.Point.toAffineAddEquiv : {F : Type u} →
  [inst : Field F] → (W : WeierstrassCurve.Projective F) → [inst_1 : DecidableEq F] → W.Point ≃+ W.toAffine.Point
-- Mathlib.Algebra.Homology.Single
/-- Morphisms to a single object cochain complex with `X` concentrated in degree 0
to an `ℕ`-indexed cochain complex `C` are the same as morphisms `f : C.X 0 ⟶ X`.
 -/
CochainComplex.toSingle₀Equiv : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : CochainComplex V ℕ) → (X : V) → (C ⟶ (CochainComplex.single₀ V).obj X) ≃ (C.X 0 ⟶ X)
-- Init.Data.Int.Order
Int.sub_nonneg_of_le : ∀ {a b : ℤ}, b ≤ a → 0 ≤ a - b
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_neg_I : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], RCLike.sqrt (-RCLike.I) = ↑√2⁻¹ * (1 + RCLike.I) * -RCLike.I
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.PositiveCompacts α)
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- **Roth's theorem** for `ℕ` as an asymptotic statement.

The maximum density of a 3AP-free set in `{1, ..., n}` goes to zero as `n` tends to infinity.  -/
rothNumberNat_isLittleO_id : (fun N => ↑(rothNumberNat N)) =o[Filter.atTop] fun N => ↑N
-- Init.Data.Nat.Div.Basic
Nat.pos_of_div_pos : ∀ {a b : ℕ}, 0 < a / b → 0 < a
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R),
  CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyLift γ hR) =
    J.sheafifyLift (CategoryTheory.CategoryStruct.comp η γ) hR
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Icc : ∀ (x y : ℝ), Real.toEReal ⁻¹' Set.Icc ↑x ↑y = Set.Icc x y
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
AddMonoidHom.isUniformEmbedding_of_isEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {Hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] [inst_6 : FunLike Hom α β]
  [AddMonoidHomClass Hom α β] {f : Hom}, Topology.IsEmbedding ⇑f → IsUniformEmbedding ⇑f
-- Init.SizeOfLemmas
BitVec.sizeOf : ∀ {w : ℕ} (a : BitVec w), sizeOf a = sizeOf a.toFin + 1
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.automorphismGroup : {R : Type u_1} →
  {M : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Group (M ≃ₗ[R] M)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_mono : ∀ {α : Type u_1} {β : Type v} (f : α → β), Monotone (Multiset.map f)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Bool × Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Data.Set.Lattice.Image
Set.image_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β) (s : (i : ι) → κ i → Set α),
  f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_mul_comm : ∀ {f : ArithmeticFunction ℕ}, ArithmeticFunction.zeta * f = f * ArithmeticFunction.zeta
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.mk.injEq : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1}
  (inner : Std.DTreeMap.Internal.Impl α β) (wf : inner.WF) (inner_1 : Std.DTreeMap.Internal.Impl α β)
  (wf_1 : inner_1.WF), ({ inner := inner, wf := wf } = { inner := inner_1, wf := wf_1 }) = (inner = inner_1)
-- Init.Control.Lawful.Basic
map_congr : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Functor m] {x : m α} {f g : α → β},
  (∀ (a : α), f a = g a) → f <$> x = g <$> x
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.comp_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesColimit G H],
  CategoryTheory.Limits.PreservesColimit (F.comp G) H
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instAlgHomClass : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  AlgHomClass (A →A[R] B) R A B
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜},
  iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_iso : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  IsJacobsonRing R ↔ IsJacobsonRing S
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.mk : (s : String.Slice) → (offset : String.Pos.Raw) → offset ≤ s.rawEndPos → String.Slice.RevByteIterator
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_6.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_7 t ×' Lean.Elab.Term.Do.Code.below_6 t
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.exists_eq_singleton_append : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.endPos),
  p.Splits t₁ t₂ → ∃ t₂', t₂ = String.singleton (p.get hp) ++ t₂'
-- Mathlib.CategoryTheory.Filtered.Final
/-- `CostructuredArrow.post T S X` is initial if `T` and `S` are initial and the domain of `T` is
cofiltered.  -/
CategoryTheory.CostructuredArrow.initial_post : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] (X : D)
  (T : CategoryTheory.Functor C D) [T.Initial] (S : CategoryTheory.Functor D E) [S.Initial],
  (CategoryTheory.CostructuredArrow.post T S X).Initial
-- Mathlib.RingTheory.Coalgebra.Basic
/-- the first coordinate of a representation of `comul a`  -/
Coalgebra.Repr.left : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → {a : A} → {ι : Type u_1} → Coalgebra.Repr R a ι → ι → A
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.cofanInl_of_binaryCoproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, Q 2 = 0 → WeierstrassCurve.Jacobian.addZ P Q = -(Q 0 * P 2) * P 2
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.instNonemptyRankFunctionNat : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], Nonempty (P.RankFunction ℕ)
-- Mathlib.GroupTheory.HNNExtension
/-- Every element `g : G` in the list is the chosen element of its coset  -/
HNNExtension.NormalWord.mem_set : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  (self : HNNExtension.NormalWord d) (u : ℤˣ) (g : G), (u, g) ∈ self.toList → g ∈ d.set u
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- The embedding of `H` into `G ⊕g H`.  -/
SimpleGraph.Embedding.sumInr : {V : Type u_3} → {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → H ↪g G ⊕g H
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- Power series expansion of the logarithm around `1`.  -/
Real.hasSum_pow_div_log_of_abs_lt_one : ∀ {x : ℝ}, |x| < 1 → HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-Real.log (1 - x))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSemilatticeInf : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [SemilatticeInf β] → SemilatticeInf (MeasureTheory.SimpleFunc α β)
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Over X))
  [i : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Over.forget X))], CategoryTheory.Limits.HasColimit F
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.mk : Lean.SMap Lean.Name Lean.Meta.MatcherInfo → Lean.Meta.Match.Extension.State
-- Mathlib.Data.Fintype.Shrink
Shrink.instFinite : ∀ {α : Type u} [inst : Finite α], Finite (Shrink.{v, u} α)
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s` and an element `a ∉ s`, the sum of `f i` over `i ∈ insert a s`
equals `f a` plus the sum of `f i` over `i ∈ s`.  -/
finsum_mem_insert : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {a : α} {s : Set α} (f : α → M),
  a ∉ s → s.Finite → ∑ᶠ (i : α) (_ : i ∈ insert a s), f i = f a + ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instLinearOrder : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → LinearOrder (ArchimedeanClass M)
-- Mathlib.Order.Bounded
Set.bounded_le_Iio : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Iio a)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
_private.Mathlib.NumberTheory.LSeries.HurwitzZetaEven.0.HurwitzZeta.tendsto_div_two_punctured_nhds : ∀ (a : ℂ), Filter.Tendsto (fun s => s / 2) (nhdsWithin a {a}ᶜ) (nhdsWithin (a / 2) {a / 2}ᶜ)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.yieldLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)},
  it.internalState.memoizedLeft = none →
    ∀ {it' : Std.IterM m β₁} {out : β₁} (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it' out)),
      Std.Iterators.Types.Zip.PlausibleStep it
        (Std.IterStep.skip
          { internalState := { left := it', memoizedLeft := some ⟨out, ⋯⟩, right := it.internalState.right } })
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.card_nsmul_le_sum : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s : Multiset α} {a : α} [AddLeftMono α],
  (∀ x ∈ s, a ≤ x) → s.card • a ≤ s.sum
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.uliftYonedaAdjunction.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α α_1 : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) (e_α : α = α_1) [inst_3 : L.IsLeftKanExtension α],
  CategoryTheory.Presheaf.uliftYonedaAdjunction L α = CategoryTheory.Presheaf.uliftYonedaAdjunction L α_1
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.M : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Month.Ordinal
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.pow_dvd_pow_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsIntegrallyClosed R] {n : ℕ},
  n ≠ 0 → ∀ {a b : R}, a ^ n ∣ b ^ n ↔ a ∣ b
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.map_mono : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ), Monotone (HomogeneousIdeal.map f)
-- Mathlib.Order.CompleteLattice.Defs
toDual_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : ι → α), OrderDual.toDual (⨆ i, f i) = ⨅ i, OrderDual.toDual (f i)