mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nsmul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α],
  Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (n • c)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} {Y X : CategoryTheory.Limits.Cone F.rightOp} (f : Y ⟶ X),
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKey! k' =
    if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fourier integral of the `n`-th derivative of a function is obtained by multiplying the
Fourier integral of the original function by `(2πI L w ⬝ )^n`.  -/
Real.fourier_iteratedFDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E} {N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) MeasureTheory.volume) →
      ∀ {n : ℕ},
        ↑n ≤ N →
          FourierTransform.fourier (iteratedFDeriv ℝ n f) = fun w =>
            VectorFourier.fourierPowSMulRight (-innerSL ℝ) (FourierTransform.fourier f) w n
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.nndist_eq : ∀ (x y : ℝ), nndist x y = Real.nnabs (x - y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.leftUnitor_hom_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).hom.app j =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj j)).hom
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.linearEquivConj_mulLeft : ∀ {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₂] (f : A₁ ≃ₐ[R] A₂) (x : A₁),
  (↑f).conj (LinearMap.mulLeft R x) = LinearMap.mulLeft R (f x)
-- Mathlib.Data.Nat.Basic
Nat.pow_sub_one : ∀ {x a : ℕ}, x ≠ 0 → a ≠ 0 → x ^ (a - 1) = x ^ a / x
-- Init.Data.Ord.Basic
/-- Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.eq`.
 -/
beqOfOrd : {α : Type u_1} → [Ord α] → BEq α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is zero if and only if they are on the same ray.  -/
Orientation.oangle_eq_zero_iff_sameRay : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = 0 ↔ SameRay ℝ x y
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_one : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M],
  UniqueFactorizationMonoid.primeFactors 1 = ∅
-- Init.Data.List.Sublist
List.drop_suffix_drop_left : ∀ {α : Type u_1} (l : List α) {i j : ℕ}, i ≤ j → List.drop j l <:+ List.drop i l
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft.sizeOf_spec : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η) =
    1 + sizeOf e + sizeOf f + sizeOf g + sizeOf h + sizeOf η
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedSimprocDecl.default : Lean.Meta.Simp.SimprocDecl
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNontrivial : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [Nonempty ι]
  [inst_5 : (i : ι) → MulZeroOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  [∀ (i : ι), Nontrivial (G i)], Nontrivial (DirectLimit G f)
-- Mathlib.Data.Set.Basic
Set.mem_sep_iff : ∀ {α : Type u} {s : Set α} {p : α → Prop} {x : α}, x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ s ∧ p x
-- Std.Time.Date.Basic
/-- Convert `Week.Offset` into `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Hour.Offset
-- Mathlib.Algebra.Module.MinimalAxioms
/-- Define a `Module` structure on a Type by proving a minimized set of axioms.  -/
Module.ofMinimalAxioms : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : SMul R M] →
          (∀ (r : R) (x y : M), r • (x + y) = r • x + r • y) →
            (∀ (r s : R) (x : M), (r + s) • x = r • x + s • x) →
              (∀ (r s : R) (x : M), (r * s) • x = r • s • x) → (∀ (x : M), 1 • x = x) → Module R M
-- Mathlib.Data.List.Duplicate
List.Duplicate.ne_singleton : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → ∀ (y : α), l ≠ [y]
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The equivalence `RightExtension L F ≌ RightExtension L' F` induced by
a natural isomorphism `L ≅ L'`.  -/
CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            {L L' : CategoryTheory.Functor C D} →
              (L ≅ L') → (F : CategoryTheory.Functor C H) → L.RightExtension F ≌ L'.RightExtension F
-- Mathlib.RingTheory.KrullDimension.Regular
Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] {x : R},
  x ∈ (Module.annihilator R M).jacobson → Module.supportDim R M ≤ Module.supportDim R (QuotSMulTop x M) + 1
-- Mathlib.Logic.Equiv.Basic
Equiv.instCanLiftForallCoeBijective : ∀ {α : Sort u_1} {β : Sort u_4}, CanLift (α → β) (α ≃ β) DFunLike.coe Function.Bijective
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (x y : Associates R),
  ↑((Ideal.associatesEquivIsPrincipal R) (x * y)) =
    ↑((Ideal.associatesEquivIsPrincipal R) x) * ↑((Ideal.associatesEquivIsPrincipal R) y)
-- Mathlib.Data.Sym.Card
/-- The `offDiag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s.offDiag / 2`.
This is because every element `s(x, y)` of `Sym2 α` not on the diagonal comes from exactly two
pairs: `(x, y)` and `(y, x)`.  -/
Sym2.card_image_offDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α),
  (Finset.image (Function.uncurry Sym2.mk) s.offDiag).card = s.card.choose 2
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_apply_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X}
  {g : Z ⟶ X}, R g → CategoryTheory.Presieve.pushforward f R (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_rotate : ∀ {α : Type u} (l : List α) (k : ℕ), (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
-- Mathlib.CategoryTheory.Equivalence
/-- Compatibility of `changeFunctor` with the composition of isomorphisms of functors  -/
CategoryTheory.Equivalence.changeFunctor_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G G' : CategoryTheory.Functor C D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G'),
  (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.add_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : ContinuousAdd M₃]
  (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂), (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.basisFun_inner : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] [inst_1 : Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι),
  inner 𝕜 ((EuclideanSpace.basisFun ι 𝕜) i) x = x.ofLp i
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.warnRedundantEMatchArg : Lean.Meta.Grind.ExtensionStateArray → Lean.Name → Lean.MetaM Unit
-- Init.Conv
/-- `try tac` runs `tac` and succeeds even if `tac` failed.  -/
Lean.Parser.Tactic.Conv.convTry_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] [inst_2 : CategoryTheory.LocallySmall.{max w' w, v₁, u₁} C]
  {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w w'))}
  (h : (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X).comp CategoryTheory.uliftFunctor.{w', w} ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι
          CategoryTheory.uliftFunctor.{w', w})
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{max w' w, v₁, u₁} S).ι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaUliftFunctorIso.inv.app X) h)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stWrite.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.pop f) = l.tail
-- Mathlib.Topology.Category.Born
Born.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : Bornology carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_uInt32ToNat : ∀ (n : UInt32), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given two points on a circle, the radius of that circle may be expressed explicitly as half
the distance between those two points divided by the cosine of the angle between the chord and
the radius at one of those points.  -/
EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₁ s.center).cos / 2 = s.radius
-- Mathlib.Data.NNRat.Defs
/-- `toNNRat` and `(↑) : ℚ≥0 → ℚ` form a Galois insertion.  -/
NNRat.gi : GaloisInsertion Rat.toNNRat NNRat.cast
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.map_univ_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {f : β ↪ α},
  Function.Surjective ⇑f → Finset.map f Finset.univ = Finset.univ
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.instForMTotalOfIteratorLoopOfMonadOfMonadLiftTOfFinite : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [Monad n] → [MonadLiftT m n] → [Std.Iterators.Finite α m] → ForM n (Std.IterM.Total m β) β
-- Mathlib.RingTheory.Ideal.Span
Ideal.subset_span : ∀ {α : Type u} [inst : Semiring α] {s : Set α}, s ⊆ ↑(Ideal.span s)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- Attempt to parse a `NatOffset` from an expression -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.asOffset : Lean.Expr → Lean.Meta.SimpM (Option (Lean.Expr × ℕ))
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sum_repr : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) (u : M), ∑ i, (b.repr u) i • b i = u
-- Lean.Elab.Binders
/-- The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
If `config.postponeValue == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`.
If `config.generalize == true`, then the value is abstracted from the expected type when elaborating the body.
 -/
Lean.Elab.Term.elabLetDeclAux : Lean.Syntax →
  Array Lean.Syntax →
    Lean.Syntax →
      Lean.Syntax → Lean.Syntax → Option Lean.Expr → Lean.Elab.Term.LetConfig → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.congr_equiv : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} {ι' : Type u_10} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E],
  WithSeminorms p → ∀ (e : ι' ≃ ι), WithSeminorms (p ∘ ⇑e)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruImage f))
      (CategoryTheory.Abelian.PreservesImage.iso F f).hom =
    CategoryTheory.Abelian.factorThruImage (F.map f)
-- Aesop.Script.Step
Aesop.Script.LazyStep.toStep : Aesop.Script.LazyStep → Lean.MetaM Aesop.Script.Step
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.sInf_apply_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)},
  e ∈ s → (∀ j > i, e j = sInf s j) → sInf s i ≤ e i
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.efixedPoint_eq_of_edist_lt_top : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤) {y : α} (hy : edist y (f y) ≠ ⊤),
  edist x y ≠ ⊤ → ContractingWith.efixedPoint f hf x hx = ContractingWith.efixedPoint f hf y hy
-- Mathlib.Tactic.DepRewrite
/-- `ReaderT` context for `M`.  -/
Mathlib.Tactic.DepRewrite.Context : Type
-- Mathlib.Algebra.Order.AddGroupWithTop
add_right_strictMono_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {b : α}, b ≠ ⊤ → StrictMono fun x => b + x
-- Std.Data.TreeSet.AdditionalOperations
/-- Given a proof that such an element exists, retrieves the smallest element that is
greater than or equal to the given element.
 -/
Std.TreeSet.getGE : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → (t : Std.TreeSet α cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Mathlib.Probability.Distributions.Geometric
/-- If a function is integrable with respect to `geometricMeasure p`, then its integral
against this measure is given by its sum weighted by `(1 - p) ^ n * p`.

See `integral_geometricMeasure` for a version where the codomain is finite-dimensional
and does not require the integrability hypothesis.  -/
ProbabilityTheory.integral_geometricMeasure' : ∀ {p : ↑unitInterval} {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℕ → E} [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  p ≠ 0 →
    MeasureTheory.Integrable f (ProbabilityTheory.geometricMeasure p) →
      ∫ (n : ℕ), f n ∂ProbabilityTheory.geometricMeasure p = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSlice.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → ℕ → List α → Sort u_2) (m : ℕ) (xs : List α) (h_1 : (x x_1 : ℕ) → motive x x_1 [])
  (h_2 : (m : ℕ) → (xs : List α) → motive 0 m xs)
  (h_3 : (n m : ℕ) → (x : α) → (xs : List α) → motive n.succ m (x :: xs)),
  (xs = [] → False) →
    (match 0, m, xs with
      | x, x_1, [] => h_1 x x_1
      | 0, m, xs => h_2 m xs
      | n.succ, m, x :: xs => h_3 n m x xs) =
      h_2 m xs
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to a `USize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toUSize : Float.Model.UnpackedFloat → USize
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- We say that a functor creates finite limits if it creates all limits of shape `J` where
`J : Type` is a finite category.  -/
CategoryTheory.Limits.CreatesFiniteCoproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
-- Batteries.Data.AssocList
Batteries.AssocList.length_replace : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : Batteries.AssocList α β} [inst : BEq α] {a : α},
  (Batteries.AssocList.replace a b l).length = l.length
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.arrayLit.sizeOf_spec : ∀ (a : List Lean.Meta.Match.Example), sizeOf (Lean.Meta.Match.Example.arrayLit a) = 1 + sizeOf a
-- Mathlib.Topology.Order.Basic
ge_mem_nhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a b : α},
  b < a → ∀ᶠ (x : α) in nhds b, x ≤ a
-- Mathlib.Computability.Primrec.Basic
Primrec.dom_bool : ∀ {α : Type u_1} [inst : Primcodable α] (f : Bool → α), Primrec f
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_keys_unit_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α Unit}, m₁.keys.Perm m₂.keys → m₁.Equiv m₂
-- Mathlib.Data.Fintype.Order
Finite.exists_le : ∀ {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] (f : ι → α),
  ∃ M, ∀ (i : ι), f i ≤ M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}
  {fallback : β}, Std.ExtDHashMap.Const.getD ∅ a fallback = fallback
-- Mathlib.Order.Category.Semilat
/-- Construct a bundled `SemilatSupCat` from a `SemilatticeSup`.  -/
SemilatSupCat.of : (X : Type u) → [isSemilatticeSup : SemilatticeSup X] → [isOrderBot : OrderBot X] → SemilatSupCat
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_limit : ∀ {o : Ordinal.{u_1}}, Order.IsSuccPrelimit o → Cardinal.preAleph o = ⨆ a, Cardinal.preAleph ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The second inclusion of a pushout cocone.  -/
CategoryTheory.Limits.PushoutCocone.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Y} → {g : X ⟶ Z} → (t : CategoryTheory.Limits.PushoutCocone f g) → Z ⟶ t.pt
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.instMembershipOfLEOfLT : {α : Type u} → [LE α] → [LT α] → Membership α (Std.Rco α)
-- Mathlib.MeasureTheory.PiSystem
/-- A Dynkin system is a collection of subsets of a type `α` that contains the empty set,
is closed under complementation and under countable union of pairwise disjoint sets.
The disjointness condition is the only difference with `σ`-algebras.

The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras
generated by a collection of sets which is stable under intersection.

A Dynkin system is also known as a "λ-system" or a "d-system".
 -/
MeasurableSpace.DynkinSystem : Type u_4 → Type u_4
-- Mathlib.RepresentationTheory.Intertwining
/-- The left inclusion of a product representation is an intertwining map.  -/
Representation.IntertwiningMap.inl : (A : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → ρ.IntertwiningMap (ρ.prod σ)
-- Mathlib.Order.DirectedInverseSystem
/-- A natural family of bijections below a limit ordinal
induces a bijection at the limit ordinal.  -/
InverseSystem.invLimEquiv : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
            {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j} →
              InverseSystem.IsNatEquiv f equiv →
                ↑(InverseSystem.limit f i) ≃ ↑(InverseSystem.limit InverseSystem.piLTProj i)
-- Mathlib.Probability.ConditionalProbability
/-- Unexpander for `μ[|s]` notation.  -/
ProbabilityTheory.condUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
ContinuousLinearMap.antilipschitz_of_bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal}, (∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.MakesOverArrow.app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {u : F.obj (Opposite.op X)},
  CategoryTheory.OverPresheafAux.MakesOverArrow η s u →
    (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) u = CategoryTheory.yonedaEquiv s
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- We say that an `R`-algebra `S` is quasi-finite
if `κ(p) ⊗[R] S` is finite-dimensional over `κ(p)` for all primes `p` of `R`.

This is slightly different from the
[stacks projects definition](https://stacks.math.columbia.edu/tag/00PL),
which requires `S` to be of finite type over `R`.

Also see `Algebra.QuasiFinite.iff_finite_comap_preimage_singleton` that
this is equivalent to having finite fibers for finite-type algebras.
 -/
Algebra.QuasiFinite : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_a₄_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).a₄ = W.a₄