mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Content
/-- The inner content of a union of sets is at most the sum of the individual inner contents.
This is the "unbundled" version of `innerContent_iSup_nat`.
It is required for the API of `inducedOuterMeasure`.  -/
MeasureTheory.Content.innerContent_iUnion_nat : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] ⦃U : ℕ → Set G⦄
  (hU : ∀ (i : ℕ), IsOpen (U i)),
  μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Module.Basis.continuous_toMatrix : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [inst : NontriviallyNormedField R] [CompleteSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [inst_6 : Module R M]
  [ContinuousSMul R M] (B : Module.Basis ι R M), Continuous fun v => B.toMatrix v
-- Mathlib.MeasureTheory.Measure.AddContent
/-- The additive content on the set of open-closed intervals, associating to an interval `Ioc u v`
the difference `f v - f u`.  -/
MeasureTheory.AddContent.onIoc : {α : Type u_1} →
  [inst : LinearOrder α] →
    {G : Type u_3} →
      [inst_1 : AddCommGroup G] → (α → G) → MeasureTheory.AddContent G {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.coeff_mul_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
  (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun x x_1 => x_1 ^ 2
-- Mathlib.Order.Monotone.Defs
Antitone.antitoneOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ (s : Set α), AntitoneOn f s
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ofHom_apply : ∀ {X Y : Type u} [inst : BooleanAlgebra X] [inst_1 : BooleanAlgebra Y] (f : BoundedLatticeHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (BoolAlg.ofHom f)) x = f x
-- Init.Data.Order.Ord
Std.instOrientedCmpCompareOnOfOrientedOrd : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Ord β] [Std.OrientedOrd β], Std.OrientedCmp (compareOn f)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.disjoint_span_image : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v →
    ∀ {s t : Set ι}, Disjoint s t → Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.one_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
  ↑1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_inter : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  (m₁ m₂ : Std.DTreeMap.Internal.Impl α β) (hm₁ : m₁.WF),
  m₂.WF →
    (m₁.inter m₂ ⋯).toListModel.Perm
      (List.filter (fun p => Std.Internal.List.containsKey p.fst m₂.toListModel) m₁.toListModel)
-- Lean.Server.References
Lean.Server.LoadedILean.mk.inj : ∀ {moduleUri : Lean.Lsp.DocumentUri} {ileanPath : System.FilePath} {directImports : Lean.Server.DirectImports}
  {refs : Lean.Lsp.ModuleRefs} {decls : Lean.Lsp.Decls} {moduleUri_1 : Lean.Lsp.DocumentUri}
  {ileanPath_1 : System.FilePath} {directImports_1 : Lean.Server.DirectImports} {refs_1 : Lean.Lsp.ModuleRefs}
  {decls_1 : Lean.Lsp.Decls},
  { moduleUri := moduleUri, ileanPath := ileanPath, directImports := directImports, refs := refs, decls := decls } =
      { moduleUri := moduleUri_1, ileanPath := ileanPath_1, directImports := directImports_1, refs := refs_1,
        decls := decls_1 } →
    moduleUri = moduleUri_1 ∧
      ileanPath = ileanPath_1 ∧ directImports = directImports_1 ∧ refs = refs_1 ∧ decls = decls_1
-- Mathlib.Tactic.Constructor
/-- `fconstructor`, on a goal which is an inductive type, solves it by applying the first matching
constructor, creating new goals for all arguments to the constructor in the same order.
This is like `constructor` except the goals are not reordered.
 -/
tacticFconstructor : Lean.ParserDescr
-- Mathlib.Data.Rat.Cast.Defs
/-- Any two ring homomorphisms from `ℚ` to a semiring are equal. If the codomain is a division ring,
then this lemma follows from `eq_ratCast`.  -/
RingHom.ext_rat : ∀ {F : Type u_1} {R : Type u_5} [inst : Semiring R] [inst_1 : FunLike F ℚ R] [RingHomClass F ℚ R] (f g : F), f = g
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.N : {R : Type u_1} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type u_3} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → I.Filtration M → ℕ → Submodule R M
-- Init.Data.Array.Lemmas
Array.exists_of_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : α → Array β}, b ∈ Array.flatMap f xs → ∃ a ∈ xs, b ∈ f a
-- Mathlib.SetTheory.Cardinal.Defs
/-- Lift a binary operation `Type* → Type* → Type*` to a binary operation on `Cardinal`s.  -/
Cardinal.map₂ : (f : Type u → Type v → Type w) →
  ((α β : Type u) → (γ δ : Type v) → α ≃ β → γ ≃ δ → f α γ ≃ f β δ) → Cardinal.{u} → Cardinal.{v} → Cardinal.{w}
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgEquiv.toCoalgIso_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] [inst_5 : Coalgebra R X] [inst_6 : Coalgebra R Y] (e : X ≃ₗc[R] Y),
  e.symm.toCoalgIso = e.toCoalgIso.symm
-- Mathlib.Algebra.Group.End
Equiv.Perm.mul_apply : ∀ {α : Type u_4} (f g : Equiv.Perm α) (x : α), (f * g) x = f (g x)
-- Mathlib.Topology.EMetricSpace.Defs
/-- A weak extended metric space extends a `WeakPseudoEMetricSpace` with the condition
`edist x y = 0 ↔ x = y`.  -/
WeakEMetricSpace : (α : Type u) → [TopologicalSpace α] → Type u
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j),
  (Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j)) (Φ.iterationFunctorObjSuccIso j hj).inv
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
  (π π_1 : (a : α) → X a ⟶ B) (e_π : π = π_1) [inst_1 : CategoryTheory.EffectiveEpiFamily X π]
  (e e_1 : (a : α) → X a ⟶ W) (e_e : e = e_1)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)),
  CategoryTheory.EffectiveEpiFamily.desc X π e h = CategoryTheory.EffectiveEpiFamily.desc X π_1 e_1 ⋯
-- Mathlib.Computability.PartrecCode
/-- An encoding of a `Nat.Partrec.Code` as a ℕ.  -/
Nat.Partrec.Code.encodeCode : Nat.Partrec.Code → ℕ
-- Init.Data.Fin.Basic
/-- Replaces the bound with another that is suitable for the value.

The proof embedded in `i` can be used to cast to a larger bound even if the concrete value is not
known.

Examples:
```lean example
example : Fin 12 := (7 : Fin 10).castLT (by decide : 7 < 12)
```
```lean example
example (i : Fin 10) : Fin 12 :=
  i.castLT <| by
    cases i; simp; omega
```
 -/
Fin.castLT : {n m : ℕ} → (i : Fin m) → ↑i < n → Fin n
-- Init.Data.List.Lemmas
List.tail_append : ∀ {α : Type u_1} {l l' : List α}, (l ++ l').tail = if l.isEmpty = true then l'.tail else l.tail ++ l'
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.tower_top_intermediateField : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  [IsGalois F E], IsGalois (↥K) E
-- Mathlib.Algebra.Regular.Basic
/-- In a semigroup, the product of right-regular elements is right-regular.  -/
IsRightRegular.mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRightRegular a → IsRightRegular b → IsRightRegular (a * b)
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.HasBasis.cauchy_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s →
    ∀ {f : Filter α}, Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.isStrictMinor_irrefl : ∀ {α : Type u_1} (M : Matroid α), ¬M <m M
-- Mathlib.MeasureTheory.PiSystem
le_generateFrom_piiUnionInter : ∀ {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} (S : Set ι) {x : ι},
  x ∈ S → MeasurableSpace.generateFrom (π x) ≤ MeasurableSpace.generateFrom (piiUnionInter π S)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.OfSurjective.isDPMorphism : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {f : A →+* B} {J : Ideal B} (hf : Function.Surjective ⇑f) (hIJ : J = Ideal.map f I)
  (hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)),
  hI.IsDPMorphism (DividedPowers.Quotient.OfSurjective.dividedPowers hI hf hIJ hIf) f
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_neg_linearMap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M), ↑(-D) = -↑D
-- Mathlib.Data.Nat.Fib.Basic
Nat.isDvdSequence_fib : IsDvdSequence Nat.fib
-- Init.PropLemmas
or_left_comm : ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.ext_iff : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {rels : Set (FreeGroup α)} {φ ψ : PresentedGroup rels →* G},
  φ = ψ ↔ ∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of a family equicontinuous at `x₀` within `S` is continuous at `x₀` within `S`.  -/
EquicontinuousWithinAt.continuousWithinAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X} {x₀ : X}, EquicontinuousWithinAt F S x₀ → ∀ (i : ι), ContinuousWithinAt (F i) S x₀
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBoolAt : Lean.Name → Lean.SubExpr.Pos → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h],
  CategoryTheory.Limits.imageSubobjectCompIso f h = CategoryTheory.Limits.imageSubobjectCompIso f h
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.balanced_of_strongMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.StrongMonoCategory C],
  CategoryTheory.Balanced C
-- Mathlib.Data.Finset.Interval
/-- `LocallyFiniteOrder` instance for `Finset α`.

We provide an optimized definition for `Finset.Icc (s : Finset α) t`,
then define the other intervals based on `Icc`.

We do not define, e.g., `Finset.Ico` based on `Finset.ssubsets`,
because it would require more code without performance gain.
 -/
Finset.instLocallyFiniteOrder : {α : Type u_1} → [DecidableEq α] → LocallyFiniteOrder (Finset α)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_norm_rpow' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β} {p : ENNReal},
  MeasureTheory.MemLp f p μ → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p.toReal) μ
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- `Codiscrete α` is equivalent to the original type `α`.  -/
CategoryTheory.codiscreteEquiv : {α : Type u} → CategoryTheory.Codiscrete α ≃ α
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- An isomorphism of graphs gives rise to an embedding of graphs.  -/
SimpleGraph.Iso.toEmbedding : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ≃g G' → G ↪g G'
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  {γ₁ γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂}, γ₁ = γ₂ → γ₁.φH = γ₂.φH
-- Init.Data.Int.Lemmas
Int.mul_zero : ∀ (a : ℤ), a * 0 = 0
-- Mathlib.Algebra.Ring.ULift
ULift.instIntCast : {R : Type u} → [IntCast R] → IntCast (ULift.{u_1, u} R)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc`. -/
CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.extrinsicFix₂.eq_1 : ∀ {α : Sort u_1} {β : α → Sort u_2} {C₂ : (a : α) → β a → Sort u_3} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
  (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) (a : α) (b : β a),
  WellFounded.extrinsicFix₂ R F a b = WellFounded.extrinsicFix R (fun x G => F x.fst x.snd fun a b => G ⟨a, b⟩) ⟨a, b⟩
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurry0_norm : ∀ (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (x : G'),
  ‖ContinuousMultilinearMap.uncurry0 𝕜 G x‖ = ‖x‖
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_injective : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R], Function.Injective Nat.cast
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open right half-plane and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right half-plane
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant on the imaginary axis;
* `f x`, `x : ℝ`, tends to zero superexponentially fast as `x → ∞`:
  for any natural `n`, `exp (n * x) * ‖f x‖` tends to zero as `x → ∞`.

Then `f` is equal to zero on the closed right half-plane.  -/
PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f {z | 0 < z.re} →
    (∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun x => ‖f ↑x‖) →
        (∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → Set.EqOn f 0 {z | 0 ≤ z.re}
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.dense_setOfPred_finite : ∀ {α : Type u_1} [inst : TopologicalSpace α], Dense {K | (↑K).Finite}
-- Mathlib.Algebra.Group.Defs
/-- Commutative version of `AddCancelMonoid`.  -/
AddCancelCommMonoid : Type u → Type u
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_singleton : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] {r : S}, Ideal.spanNorm R (Ideal.span {r}) = Ideal.span {(Algebra.intNorm R S) r}
-- Mathlib.Order.Filter.Basic
Filter.principal_sdiff_principal : ∀ {α : Type u} {s t : Set α}, Filter.principal s \ Filter.principal t = Filter.principal (s \ t)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β),
  l.minEntry?ₘ = Std.DTreeMap.Internal.Impl.applyPartition (fun x => Ordering.lt) l fun x x_1 x_2 r => r.head?
-- Init.Data.Fin.Basic
/-- Subtraction modulo `n`, usually invoked via the `-` operator.

Examples:
* `(5 : Fin 11) - (3 : Fin 11) = (2 : Fin 11)`
* `(3 : Fin 11) - (5 : Fin 11) = (9 : Fin 11)`
 -/
Fin.sub : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.Analysis.PSeries
Finset.sum_condensed_le : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
    ∀ (n : ℕ), ∑ k ∈ Finset.range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Finset.Ico 2 (2 ^ n + 1), f k
-- Plausible.Testable
Plausible.LT.printableProp : {α : Type u_1} → [Repr α] → [inst : LT α] → {x y : α} → Plausible.PrintableProp (x < y)
-- Std.Sync.RecursiveMutex
/-- Recursive (or reentrant) exclusion primitive.

If you want to guard shared state, use `RecursiveMutex α` instead.
 -/
Std.BaseRecursiveMutex : Type
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map : ∀ {X Y : AlgebraicGeometry.Scheme} {M : X.Modules} (f : X ⟶ Y) {U V : Y.Opens} (i : U ⟶ V),
  ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M).presheaf.map i.op =
    M.presheaf.map ((TopologicalSpace.Opens.map f.base).map i).op
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
instModuleMatrixFinOfNatNatProd : {R : Type u_1} → [inst : Semiring R] → Module (Matrix (Fin 2) (Fin 2) R) (R × R)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.y_mul_dvd : ∀ {a : ℕ} (a1 : 1 < a) (n k : ℕ), Pell.yn a1 n ∣ Pell.yn a1 (n * k)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
/-- Let `X` and `Y` be R₁ topological spaces
with Borel σ-algebras and measures `μ` and `ν`, respectively.
Suppose that `μ` is inner regular for finite measure sets with respect to compact sets
and `ν` is a locally finite measure.
Let `1 ≤ p < ∞` be an extended nonnegative real number.
Then the composition of a function `g : Lp E p ν`
and a measure-preserving continuous function `f : C(X, Y)`
is continuous in both variables.  -/
MeasureTheory.Lp.compMeasurePreserving_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] (μ : MeasureTheory.Measure X)
  (ν : MeasureTheory.Measure Y) [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] (E : Type u_3)
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)],
  p ≠ ⊤ → Continuous fun gf => (MeasureTheory.Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
-- Init.Data.List.Attach
List.pmap_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a},
  List.pmap f l H = [] ↔ l = []
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The `q`-expansion of `f` is an `FPowerSeries` representing `cuspFunction n f`.  -/
UpperHalfPlane.hasFPowerSeries_cuspFunction : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) {c : ℕ → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0 →
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        HasFPowerSeriesOnBall (UpperHalfPlane.cuspFunction h ⇑f) (UpperHalfPlane.qExpansionFormalMultilinearSeries h f)
          0 1
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel κ.fst
-- Mathlib.Order.KrullDimension
Order.height_ofDual : ∀ {α : Type u_1} [inst : Preorder α] (x : αᵒᵈ), Order.height (OrderDual.ofDual x) = Order.coheight x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.val_mul : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  (x y : ArchimedeanClass.FiniteElement K), ↑(x * y) = ↑x * ↑y
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.mul_klFun_le_toReal_klDiv : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ν.real Set.univ * InformationTheory.klFun (μ.real Set.univ / ν.real Set.univ) ≤
        (InformationTheory.klDiv μ ν).toReal
-- Mathlib.Algebra.Notation.Support
Pi.support_single_disjoint : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i j : ι} {a b : M},
  a ≠ 0 → b ≠ 0 → (Disjoint (Function.support (Pi.single i a)) (Function.support (Pi.single j b)) ↔ i ≠ j)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i)
-- Batteries.Lean.Json
instToJsonFloat_batteries : Lean.ToJson Float
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.mul_fromLeftInv : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : ↥S.leftInv), ↑x * ↑(S.fromLeftInv x) = 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt.sizeOf_spec : ∀ (a b toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt a b toIntThm lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf toIntThm + sizeOf lhs + sizeOf rhs
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
  [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E}, AnalyticOn 𝕜' f s → AnalyticOn 𝕜 f s
-- Mathlib.FieldTheory.AxGrothendieck
/-- Any injective polynomial map over an algebraic extension of a finite field is surjective.  -/
ax_grothendieck_of_locally_finite : ∀ {ι : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field K] [Finite K] [inst_2 : CommRing R] [Finite ι]
  [inst_4 : Algebra K R] [alg : Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R) (S : Set (ι → R)),
  Set.MapsTo (fun v i => (MvPolynomial.eval v) (ps i)) S S →
    Set.InjOn (fun v i => (MvPolynomial.eval v) (ps i)) S → Set.SurjOn (fun v i => (MvPolynomial.eval v) (ps i)) S S
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_mul_pow_sub_le_factorial : ∀ {n m : ℕ}, n ≤ m → n.factorial * n ^ (m - n) ≤ m.factorial
-- Batteries.Data.ByteArray
ByteArray.set_set : ∀ (a : ByteArray) (i : Fin a.size) (v v' : UInt8), (a.set (↑i) v ⋯).set (↑i) v' ⋯ = a.set (↑i) v' ⋯
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.toStringWithToken.maybePseudoSyntax : Lean.Name → Bool