mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mdifferentiableAt : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (s : ContMDiffSection I F (↑⊤) V) {x : M},
  (MDiffAt fun x => ⟨x, s x⟩) x
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₂_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
-- Mathlib.Topology.Category.UniformSpace
/-- The concrete category instance on `CpltSepUniformSpace`.  -/
CpltSepUniformSpace.concreteCategory : CategoryTheory.ConcreteCategory CpltSepUniformSpace fun x1 x2 => { f // UniformContinuous f }
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
AlgEquiv.toLinearMap.eq_1 : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.toLinearMap = ↑↑e
-- Init.Data.Vector.Lemmas
Vector.all_flatten : ∀ {α : Type u_1} {n m : ℕ} {f : α → Bool} {xss : Vector (Vector α n) m}, xss.flatten.all f = xss.all fun x => x.all f
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.con_subgroup : ∀ {G : Type u_1} [inst : Group G] (c : Con G), QuotientGroup.con c.subgroup = c
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.injective_distDenseSeq : ∀ {X : Type u_3} [inst : MetricSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] (x y : X),
  x ≠ y → ∃ n, Metric.PiNatEmbed.distDenseSeq X n x ≠ Metric.PiNatEmbed.distDenseSeq X n y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.copy_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- The extended diameter is the greatest distance between any two vertices, with the value `⊤` in
case the distances are not bounded above, or the graph is not connected.
 -/
SimpleGraph.ediam : {α : Type u_1} → SimpleGraph α → ℕ∞
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instConcreteCategoryContinuousMapGeneratedByCarrier : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.ConcreteCategory (ContinuousGeneratedByCat X) fun Y Z => Topology.ContinuousMapGeneratedBy X ↑Y ↑Z
-- Mathlib.Data.Set.Card
/-- The cardinality of a set as a term in `ℕ∞`  -/
Set.encard : {α : Type u_1} → Set α → ℕ∞
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
can avoid the "motive is not type correct" error.
 -/
CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F)
  (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) =
    J.yonedaEquiv (CategoryTheory.CategoryStruct.comp (J.yoneda.map g.unop) f)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutCongr.eq_1 : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] {g : X ⟶ Y} (h : f = g),
  CategoryTheory.MorphismProperty.Under.pushoutCongr h =
    CategoryTheory.NatIso.ofComponents
      (fun X_1 => CategoryTheory.MorphismProperty.Under.isoMk (CategoryTheory.Limits.pushout.congrHom ⋯ h) ⋯) ⋯
-- Init.Data.Float.Model.Unpacked.Round
/-- If the target exponent is smaller than the given exponent, decreases the exponent of the mantissa to
the target exponent; otherwise does nothing.
 -/
Float.Model.UnpackedFloat.decreaseExponent : ℕ → ℤ → ℤ → ℕ × ℤ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomialY_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, Polynomial.evalEval 0 0 W.polynomialY = W.a₃
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The equivalence map for the representation as a product.  -/
RegularWreathProduct.equivProd : (D : Type u_3) → (Q : Type u_4) → D ≀ᵣ Q ≃ (Q → D) × Q
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_sub_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], Int.fract (a - OfNat.ofNat n) = Int.fract a
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.mkInitial : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → IO (Lean.ScopedEnvExtension.StateStack α β σ)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instNormMulClass : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], NormMulClass ℤ_[p]
-- Mathlib.RingTheory.DividedPowers.Basic
/-- A “multinomial” theorem for divided powers — without multinomial coefficients.  -/
DividedPowers.dpow_sum : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {ι : Type u_2} [inst_1 : DecidableEq ι]
  {s : Finset ι} {x : ι → A},
  (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, hI.dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, hI.dpow (Multiset.count i ↑k) (x i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : β → β},
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.modify t k f) k' fallback =
        if cmp k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
        else Std.DTreeMap.Raw.Const.getD t k' fallback
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.mk.sizeOf_spec : ∀ (options : Lean.Options) (table : Lean.Parser.TokenTable),
  sizeOf { options := options, table := table } = 1 + sizeOf options + sizeOf table
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfExample : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.DefView
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of `F⟮α⟯ / F` is smaller than the degree of `F⟮α⟯ / F` if `α` is
algebraic over `F`.  -/
IntermediateField.finSepDegree_adjoin_simple_le_finrank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsAlgebraic F α → Field.finSepDegree F ↥F⟮α⟯ ≤ Module.finrank F ↥F⟮α⟯
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- When `b < sSup s`, there is an element `a` in `s` with `b < a`, if `s` is nonempty and the order
is a linear order.  -/
exists_lt_of_lt_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α},
  s.Nonempty → b < sSup s → ∃ a ∈ s, b < a
-- Mathlib.Order.Minimal
minimal_iff_forall_lt : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y
-- Init.Data.Fin.Lemmas
Fin.castSucc_lt_iff_succ_le : ∀ {n : ℕ} {i : Fin n} {j : Fin (n + 1)}, i.castSucc < j ↔ i.succ ≤ j
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.infinite : ∀ {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Nonempty ι], Infinite (EuclideanSpace 𝕜 ι)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.notMem₂ : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (s : self.ι),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index s))) (self.simplex s) ∉
    A.obj (Opposite.op { len := self.dim s })
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.ordConnected_setOfPred_closedEBall_subset`. -/
EMetric.ordConnected_setOf_closedBall_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.closedEBall x r ⊆ s}.OrdConnected
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_succ_symm_apply : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), (Equiv.symm (finRotate n)) i = i - 1
-- Lean.Expr
/-- During elaboration expressions corresponding to pattern matching terms
are annotated with `Syntax` objects. This function returns `some (stx, p')` if
`p` is the pattern `p'` annotated with `stx`
 -/
Lean.patternWithRef? : Lean.Expr → Option (Lean.Syntax × Lean.Expr)
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.visitLevel : Lean.Level → Lean.CollectLevelMVars.Visitor
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.Repr.induced_index : ∀ {R : Type u} {A : Type v} {B : Type w} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A]
  [inst_6 : Coalgebra R B] {a : A} (repr : Coalgebra.Repr R a ι) {F : Type u_2} [inst_7 : FunLike F A B]
  [inst_8 : CoalgHomClass F R A B] (φ : F), (repr.induced φ).index = repr.index
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsFunctor_hom_ext_iff : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A : Rep.{w, u, v} k G} {M : ModuleCat k}
  {f g : (Rep.coinvariantsFunctor k G).obj A ⟶ M},
  f = g ↔
    CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) f =
      CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) g
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.appendResults : {α : Type} → Lean.Meta.LazyDiscrTree.MatchResult α → Array α → Array α
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.left.Step → Sort u_3) (it₁' : Std.IterM m β₁)
  (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) →
        (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out)) →
          motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) →
      (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it.internalState.left.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.skip it₁', 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_2 it₁' hp
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y i i_1 : ℤ),
  ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom.f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i)).obj (K₂.X (i_1 + y)))
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f₀ : S₁.L₀ ⟶ S₂.L₀) (f₁ : S₁.L₁ ⟶ S₂.L₁) (f₂ : S₁.L₂ ⟶ S₂.L₂)
  (f₃ : S₁.L₃ ⟶ S₂.L₃)
  (comm₀₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam)
  (f₀_1 : S₁.L₀ ⟶ S₂.L₀) (f₁_1 : S₁.L₁ ⟶ S₂.L₁) (f₂_1 : S₁.L₂ ⟶ S₂.L₂) (f₃_1 : S₁.L₃ ⟶ S₂.L₃)
  (comm₀₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₀_1 S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam)
  (comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₁_1 S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam)
  (comm₂₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₂_1 S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam),
  ({ f₀ := f₀, f₁ := f₁, f₂ := f₂, f₃ := f₃, comm₀₁ := comm₀₁, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
      { f₀ := f₀_1, f₁ := f₁_1, f₂ := f₂_1, f₃ := f₃_1, comm₀₁ := comm₀₁_1, comm₁₂ := comm₁₂_1, comm₂₃ := comm₂₃_1 }) =
    (f₀ = f₀_1 ∧ f₁ = f₁_1 ∧ f₂ = f₂_1 ∧ f₃ = f₃_1)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- A unit-distance embedding of a graph into a metric space is a vertex embedding
such that adjacent vertices are at distance 1 from each other.  -/
SimpleGraph.UnitDistEmbedding : {V : Type u_1} → SimpleGraph V → (E : Type u_3) → [MetricSpace E] → Type (max u_1 u_3)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.initial : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → σ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The inclusion of ideal sheaf induces an inclusion of subschemes  -/
AlgebraicGeometry.Scheme.IdealSheafData.inclusion : {X : AlgebraicGeometry.Scheme} → {I J : X.IdealSheafData} → I ≤ J → (J.subscheme ⟶ I.subscheme)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- See `MvPolynomial.IsHomogeneous.funext`
for a version that assumes `Infinite R`.  -/
MvPolynomial.IsHomogeneous.funext_of_le_card : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] [IsDomain R] {F G : MvPolynomial σ R} {n : ℕ},
  F.IsHomogeneous n →
    G.IsHomogeneous n → (∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) → ↑n ≤ Cardinal.mk R → F = G
-- Mathlib.Topology.NhdsWithin
sdiff_mem_nhdsWithin_sdiff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s t : Set α},
  s ∈ nhdsWithin x t → ∀ (t' : Set α), s \ t' ∈ nhdsWithin x (t \ t')
-- Mathlib.Algebra.Group.Hom.Defs
instOneMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOneClass N],
  instOneMonoidHom = { one := { toFun := fun x => 1, map_one' := ⋯, map_mul' := ⋯ } }
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `SemimoduleCat R`.  -/
SemimoduleCat.of : (R : Type u) → [inst : Semiring R] → (X : Type v) → [inst_1 : AddCommMonoid X] → [Module R X] → SemimoduleCat R
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap : Lean.Grind.IntInterval → ℤ → ℤ
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.sub : ∀ {α : Type u_2} [inst : AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_5} [inst_1 : SubtractionCommMonoid β]
  {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  IsAddFreimanHom n A B₁ f₁ → IsAddFreimanHom n A B₂ f₂ → IsAddFreimanHom n A (B₁ - B₂) (f₁ - f₂)
-- Init.Data.String.Basic
String.Pos.ofSlice_slice : ∀ {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁}, String.Pos.ofSlice (pos.slice p₀ p₁ h₁ h₂) = pos
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- A cases eliminator that makes `cases z` use `UnitDisc.mk` instead of `Subtype.mk`.  -/
Complex.UnitDisc.casesOn : {motive : Complex.UnitDisc → Sort u_1} →
  ((z : ℂ) → (hz : ‖z‖ < 1) → motive (Complex.UnitDisc.mk z hz)) → (z : Complex.UnitDisc) → motive z
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.G : List (List (Option ℕ)) → Option (List (Option ℕ))
-- Mathlib.RingTheory.Valuation.Basic
Valuation.val_le_one_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x : K}, x ≠ 0 → (v x ≤ 1 ↔ 1 ≤ v x⁻¹)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sSup s = 0` when `s` is a set of reals that's either empty or unbounded above,
it suffices to show that all elements of `s` are nonnegative to show that `0 ≤ sSup s`.  -/
Real.sSup_nonneg : ∀ {s : Set ℝ}, (∀ x ∈ s, 0 ≤ x) → 0 ≤ sSup s
-- Mathlib.Analysis.Calculus.FDeriv.Basic
UniqueDiffOn.eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' f₁' : E →L[𝕜] F} {x : E} {s : Set E} [T2Space F],
  UniqueDiffOn 𝕜 s → x ∈ s → HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f₁' s x → f' = f₁'
-- Mathlib.Combinatorics.Matroid.Loop
/-- A coloop is a loop of the dual matroid.
See `Matroid.isColoop_tfae` for a number of equivalent definitions.  -/
Matroid.IsColoop : {α : Type u_1} → Matroid α → α → Prop
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : Fintype ι] [inst_5 : InnerProductSpace ℝ E],
  (∀ (i : ι), AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) P) =
        ∏ i, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.mk.sizeOf_spec : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] [inst_9 : SizeOf K] [inst_10 : SizeOf M]
  (stratum : FiniteArchimedeanClass M → Submodule K M)
  (disjoint_ball_stratum : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum c))
  (ball_sup_stratum_eq :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum c = FiniteArchimedeanClass.closedBall K c),
  sizeOf
      { stratum := stratum, disjoint_ball_stratum := disjoint_ball_stratum,
        ball_sup_stratum_eq := ball_sup_stratum_eq } =
    1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x : R} {s : ↥(ValuativeRel.posSubmonoid R)},
  0 < ValuativeRel.ValueGroupWithZero.mk x s ↔ 0 <ᵥ x
-- Lean.Server.Requests
Lean.Server.RequestError.toLspResponseError : Lean.JsonRpc.RequestID → Lean.Server.RequestError → Lean.JsonRpc.ResponseError Unit
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Functional equation for the even Hurwitz zeta function.  -/
HurwitzZeta.completedHurwitzZetaEven_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaEven a (1 - s) = HurwitzZeta.completedCosZeta a s
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.eq_of_dep_subset : ∀ {α : Type u_1} {M : Matroid α} {C X : Set α}, M.IsCircuit C → M.Dep X → X ⊆ C → X = C
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The index type `ι`  -/
CategoryTheory.Mat_.ι : {C : Type u₁} → CategoryTheory.Mat_ C → Type
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrp_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.Grp C),
  CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj X = GrpCat.shrinkFunctor.{w, v, v, u} (CategoryTheory.yonedaGrp.obj X)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.smul_mem_of_set_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {g : G},
  s ∈ MulAction.fixedBy (Set α) g → ∀ {x : α}, g • x ∈ s ↔ x ∈ s
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_natCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ), QuadraticAlgebra.C ↑n = ↑n
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_toMatrix_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂} (b : Module.Basis ι R₂ M₂),
  ((LinearMap.BilinForm.toMatrix b) B).Nondegenerate ↔ B.Nondegenerate
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.instInhabitedKind : Inhabited Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.measure_sdiff_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → μ (s \ t) = μ s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_alter_of_beq_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Mathlib.Topology.Order.Completion
Order.Fill.some.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α],
  Order.Fill.some = { toFun := fun x => ⟨toLex (x, 0), ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `OrderedAdd` instance with `IsPreorder` if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.orderedAddInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.toSubsemiring_strictMono : ∀ {R : Type u_1} [inst : CommRing R], StrictMono RingPreordering.toSubsemiring
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instCoeAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → Coe (FiniteIndexNormalAddSubgroup G) (AddSubgroup G)
-- Mathlib.RingTheory.Binomial
Ring.choose_neg' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ),
  Ring.choose (-r) n = (↑n).negOnePow • Ring.multichoose r n
-- Mathlib.Topology.Constructions
Continuous.subtype_mk : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  Continuous f → ∀ (hp : ∀ (x : Y), p (f x)), Continuous fun x => ⟨f x, ⋯⟩
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isRegular_cons_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (rs : List R),
  RingTheory.Sequence.IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs