mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.id_comp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Hom Q), f.comp (RootPairing.Hom.id P) = f
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instLinearMapClass : ∀ {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), LinearMapClass (ρ.IntertwiningMap σ) A V W
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- Two Gaussian measures are equal if and only if they have same mean and same covariance.  -/
ProbabilityTheory.IsGaussian.ext_iff_covarianceBilinDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : NormedSpace ℝ E]
  {ν : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [ProbabilityTheory.IsGaussian ν],
  μ = ν ↔
    ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧
      ProbabilityTheory.covarianceBilinDual μ = ProbabilityTheory.covarianceBilinDual ν
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.τ₁_ofEpiOfIsIsoOfMono_f' : ∀ {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) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).f' =
    h.f'
-- Init.System.IO
/-- Checks whether the current task's cancellation flag has been set by calling `IO.cancel` or by
dropping the last reference to the task.
 -/
IO.checkCanceled : BaseIO Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.b₂ = 1
-- Aesop.Tree.Data
Aesop.Iteration.instLE : LE Aesop.Iteration
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- The instances given by `fieldOfModelField` are compatible with the `Language.ring.Structure`
instance on `K`. This instance is to be used on models for the language of fields that do
not already have the ring operations on the Type.

Always add `fieldOfModelField` as a local instance first before using this instance.
 -/
FirstOrder.Field.compatibleRingOfModelField : (K : Type u_2) →
  [inst : FirstOrder.Language.ring.Structure K] →
    [inst_1 : K ⊨ FirstOrder.Language.Theory.field] → FirstOrder.Ring.CompatibleRing K
-- Init.Data.String.Slice
/-- Creates a new slice that contains the longest suffix of `s` for which `pat` matched
\(potentially repeatedly\).

Examples:

* `"red green blue".toSlice.dropEndWhile Char.isLower == "red green ".toSlice`

* `"red green blue".toSlice.dropEndWhile 'e' == "red green blu".toSlice`

* `"red green blue".toSlice.dropEndWhile (fun (_ : Char) => true) == "".toSlice`
 -/
String.Slice.dropEndWhile : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.NumberTheory.Chebyshev
/-- The sum of `ArithmeticFunction.vonMangoldt` over integers `n ≤ x`.  -/
Chebyshev.psi : ℝ → ℝ
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_real_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s →
    ∀ [inst_1 : DecidablePred fun x => x ∈ s],
      (ProbabilityTheory.bernoulliMeasure x y p).real s =
        if x ∈ s then if y ∈ s then 1 else ↑(unitInterval.toNNReal p)
        else if y ∈ s then ↑(unitInterval.toNNReal (unitInterval.symm p)) else 0
-- Init.Data.Array.Sort.Basic
_private.Init.Data.Array.Sort.Basic.0.Subarray.mergeSort.eq_def : ∀ {α : Type u_1} (xs : Subarray α) (le : α → α → Bool),
  xs.mergeSort le =
    if h : 1 < Std.Slice.size xs then
      have splitIdx := (Std.Slice.size xs + 1) / 2;
      have left := Std.Rio.Sliceable.mkSlice xs *...splitIdx;
      have right := Std.Rci.Sliceable.mkSlice xs splitIdx...*;
      Array.MergeSort.Internal.merge✝ (left.mergeSort le) (right.mergeSort le) le
    else Std.Slice.toArray xs
-- Batteries.Data.Fin.Lemmas
Fin.foldl_assoc : ∀ {α : Sort u_1} {n : ℕ} {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂ : α},
  Fin.foldl n (fun x i => op x (f i)) (op a₁ a₂) = op a₁ (Fin.foldl n (fun x i => op x (f i)) a₂)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_neg : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (f : X → E) (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  ∫ᵛ (x : X), (-f) x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instInfinitelyUpwardEnumerableInt : Std.PRange.InfinitelyUpwardEnumerable ℤ
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_neg : ∀ {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N), AlgebraicGeometry.tilde.map (-f) = -AlgebraicGeometry.tilde.map f
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mk_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (S : Set L)
  (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0)
  (h₃ :
    ∀ (c : R) {x : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {x y : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
          ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier),
  ↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S
-- Mathlib.Order.Max
NoMaxOrder.not_acc : ∀ {α : Type u_1} [inst : LT α] [NoMaxOrder α] (a : α), ¬Acc (fun x1 x2 => x2 < x1) a
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- A root system is a root pairing for which the roots and coroots span their ambient modules.  -/
RootPairing.IsRootSystem : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.Algebra.Ring.Defs
/-- A non-unital commutative semiring is a `NonUnitalSemiring` with commutative multiplication.
In other words, it is a type with the following structures: additive commutative monoid
(`AddCommMonoid`), commutative semigroup (`CommSemigroup`), distributive laws (`Distrib`), and
multiplication by zero law (`MulZeroClass`).  -/
NonUnitalCommSemiring : Type u → Type u
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U → ∀ {V : X.Opens} (x : ↥V), ↑x ∈ U → ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.one_div_nonneg' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ 1 / r
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_eq_bot : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = ⊥ → I = ⊥
-- Mathlib.RingTheory.Ideal.NatInt
Ideal.map_comap_natCastRingHom_int : ∀ {I : Ideal ℤ}, Ideal.map (Nat.castRingHom ℤ) (Ideal.comap (Nat.castRingHom ℤ) I) = I
-- Mathlib.Logic.Equiv.Sum
/-- `PSum` is equivalent to `Sum`.  -/
Equiv.psumEquivSum : (α : Type u_9) → (β : Type u_10) → α ⊕' β ≃ α ⊕ β
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of a semigroup hom to a subsemigroup of the domain.  -/
MulHom.domRestrict : {M : Type u_1} →
  {σ : Type u_4} →
    [inst : Mul M] →
      {N : Type u_5} →
        [inst_1 : Mul N] → [inst_2 : SetLike σ M] → [inst_3 : MulMemClass σ M] → (M →ₙ* N) → (S : σ) → ↥S →ₙ* N
-- Init.WFComputable
_private.Init.WFComputable.0.WellFounded.fixC.eq_def : ∀ {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x)
  (x : α), hwf.fixC F x = F x fun y x => hwf.fixC F y
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_eq_point_rev : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 1) (signs : Finset (Fin 2)) (i : Fin 2),
  s.touchpoint signs i = s.points i.rev
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_lt_add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LT α] [DenselyOrdered α] [AddLeftStrictMono α] {a b c : α},
  c < a + b → ∃ b' < b, c < a + b'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_union_le_size_add_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- `R` consists of a finite collection of arrows that together induce an isomorphism from the
coproduct of their sources.  -/
CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : C} {R : CategoryTheory.Presieve X}
  [self : R.Extensive],
  ∃ α,
    ∃ (_ : Finite α),
      ∃ Z π,
        R = CategoryTheory.Presieve.ofArrows Z π ∧
          Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshotInner.mk : {α : Type} →
  Lean.Language.Snapshot →
    Lean.Syntax →
      Option (Lean.Language.SnapshotTask α) →
        Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot →
          Lean.Elab.Tactic.TacticParsedSnapshotInner α
-- Mathlib.Algebra.BigOperators.Finprod
finprod_comp_equiv : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (e : α ≃ β) {f : β → M},
  ∏ᶠ (i : α), f (e i) = ∏ᶠ (i' : β), f i'
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.StdSimplex.join_join : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (f : Convexity.StdSimplex R (Convexity.StdSimplex R (Convexity.StdSimplex R M))),
  f.join.join = (Convexity.StdSimplex.map (fun x => x.join) f).join
-- Init.Data.Array.Subarray
Std.Slice.size.eq_1 : ∀ {γ : Type u_1} (s : Std.Slice γ) [inst : Std.Slice.SliceSize γ], s.size = Std.Slice.SliceSize.size s
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_iff_isSpectralMap : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}, AlgebraicGeometry.QuasiCompact f ↔ IsSpectralMap ⇑f
-- Mathlib.Algebra.CharP.IntermediateField
IntermediateField.expChar' : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  (p : ℕ) [ExpChar E p], ExpChar (↥L) p
-- Mathlib.Data.Nat.Digits.Defs
/-- `n` modulo `p^i` is like taking the least significant `i` digits of `n` in base `p`.
 -/
Nat.self_mod_pow_eq_ofDigits_take : ∀ {p : ℕ} (i n : ℕ), 2 ≤ p → n % p ^ i = Nat.ofDigits p (List.take i (p.digits n))
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.eq_def : ∀
  {motive :
    (R : Type u) →
      [inst : CommRing R] →
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsWeaklyRegular M rs → Sort u_7}
  (nil :
    (R : Type u) →
      [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive R M [] ⋯)
  (cons :
    {R : Type u} →
      [inst : CommRing R] →
        {M : Type v} →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              (r : R) →
                (rs : List R) →
                  (h1 : IsSMulRegular M r) →
                    (h2 :
                        RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
                      motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
                          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) h2 →
                        motive R M (r :: rs) ⋯)
  (x : Type u) (x_1 : CommRing x) (x_2 : Type v) (x_3 : AddCommGroup x_2) (x_4 : Module x x_2) (x_5 : List x)
  (x_6 : RingTheory.Sequence.IsWeaklyRegular x_2 x_5),
  RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing nil cons x_6 =
    match x, x_1, x_2, x_3, x_4, x_5, x_6 with
    | R, x, M, x_7, x_8, [], x_9 => nil R M
    | α, x, M, x_7, x_8, r :: rs, h =>
      match ⋯ with
      | ⋯ =>
        cons r rs h1 h2
          (RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing nil
            (fun {R} [CommRing R] {M} [AddCommGroup M] [Module R M] => cons) h2)
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftLeft_eq' : ∀ {m n : ℕ}, m.shiftLeft n = m <<< n
-- Init.Data.SInt.Lemmas
Int64.mul_two : ∀ {a : Int64}, a * 2 = a + a
-- Mathlib.Order.WellQuasiOrder
wellQuasiOrderedLE_def : ∀ (α : Type u_3) [inst : LE α], WellQuasiOrderedLE α ↔ WellQuasiOrdered fun x1 x2 => x1 ≤ x2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instHasLimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject C)
-- Init.Data.Vector.Lemmas
Vector.toArray_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (h : i < n), (xs.set i x h).toArray = xs.toArray.set i x ⋯
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_iff_indep : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instReflectsIsomorphismsComonadFunctorComonadToFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.comonadToFunctor C).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The adjoint triple `constantSheaf J A ⊣ Γ J A ⊣ coconstantSheaf J A` on any local site.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.constantΓCoconstantTriple : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_5 : CategoryTheory.Limits.HasProducts A] →
                  [inst_6 : CategoryTheory.HasWeakSheafify J A] →
                    CategoryTheory.Adjunction.Triple (CategoryTheory.constantSheaf J A) (CategoryTheory.Sheaf.Γ J A)
                      (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A)
-- Lean.Meta.IndPredBelow
/-- New local declarations that were added in the process of adding below discriminants to a matcher
with information on their purpose.
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl : Type
-- Init.Data.SInt.Basic
/-- Bitwise and for word-sized signed integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set,
according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.land : ISize → ISize → ISize
-- Lean.LocalContext
/-- Return `true` if all declarations in `lctx` satisfy `p`.  -/
Lean.LocalContext.all : Lean.LocalContext → (Lean.LocalDecl → Bool) → Bool
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.kerodon : Mathlib.CrossRef.Database
-- Lean.Message
Lean.instFromJsonMessageSeverity : Lean.FromJson Lean.MessageSeverity
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- For an `R`-algebra `S`, this asserts that the maps `algebraMap : R → S` and
`includeLeftSubRight R S : S → S ⊗[R] S` form an exact pair.
When `R` and `S` are commutative rings, this is true if and only if the inclusion
`im (algebraMap : R → S) → S` is an effective monomorphism in the category of commutative rings.  -/
Algebra.IsEffective : (R : Type u_1) → [inst : CommSemiring R] → (S : Type u_2) → [inst_1 : Ring S] → [Algebra R S] → Prop
-- Mathlib.Order.Atoms
/-- An order is simple iff it has exactly two elements, `⊥` and `⊤`.  -/
IsSimpleOrder : (α : Type u_4) → [inst : LE α] → [BoundedOrder α] → Prop
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_norm_rpow : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} {p : ENNReal},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p.toReal) μ
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℤ`.  -/
HurwitzZeta.hasSum_int_cosZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.cosZeta (↑a) s)
-- Mathlib.Algebra.Category.Grp.Limits
/-- The category of additive groups has all limits.  -/
AddGrpCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddGrpCat
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule_le_invtSubmodule_smul : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_3} {S : Type u_4} [inst_1 : Semiring R] [inst_2 : Semiring S]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : DistribSMul S R] [inst_6 : SMulCommClass R S M]
  [IsScalarTower S R M] (f : Module.End R M) (c : S), f.invtSubmodule ≤ (c • f).invtSubmodule
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_mul : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I J : FractionalIdeal M K),
  FractionalIdeal.extended L hf (I * J) = FractionalIdeal.extended L hf I * FractionalIdeal.extended L hf J
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`,
`NormedSpace.exp (x+y) = (NormedSpace.exp x) * (NormedSpace.exp y)`.  -/
NormedSpace.exp_add : ∀ {𝔸 : Type u_2} [inst : NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {x y : 𝔸},
  NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `get_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.get_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → Option γ} {k : α} {h : k ∈ Std.DHashMap.filterMap f m},
  Std.DHashMap.Const.get (Std.DHashMap.filterMap f m) k h = (f k (Std.DHashMap.Const.get m k ⋯)).get ⋯
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.run : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → {σ : Type} → Lean.MonadStateCacheT α β m σ → m σ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.fundamentalDomain_integerLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.IsAddFundamentalDomain (↥(NumberField.mixedEmbedding.integerLattice K))
    (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K)) MeasureTheory.volume
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.fvar : Lean.FVarId → ℕ → Lean.Meta.LazyDiscrTree.Key
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.expandOptLocation : Lean.Syntax → Lean.Elab.Tactic.Location
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → (m.isEmpty = true ↔ ∀ (a : α), a ∉ m)
-- Std.Http.Data.URI.Basic
/-- Removes all occurrences of a query parameter by raw key string. The key is percent-encoded before matching.
 -/
Std.Http.URI.Query.erase : Std.Http.URI.Query → String → Std.Http.URI.Query
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.finsetSum_apply : ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
  (g : α → Π₀ (i : ι), β i) (i : ι), (∑ a ∈ s, g a) i = ∑ a ∈ s, (g a) i
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.algebraMap_self_map : ∀ (R : Type u) [inst : CommRing R] (U V : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ)
  (i : V ⟶ U),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj V)))
      ((AlgebraicGeometry.Spec.structureSheaf R).obj.map i) =
    CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj U))
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.instToStringError : ToString Std.Http.Protocol.H1.Error
-- Mathlib.Analysis.Normed.Group.Basic
ball_zero_eq : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (r : ℝ), Metric.ball 0 r = {x | ‖x‖ < r}
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instInf : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Min (L.DefinableSet A α)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.rankGT.of_le : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {n n' : ℕ}, s.rankGT n → n' ≤ n → s.rankGT n'
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinf_X₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).X₂ = groupHomology.H1 A
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_empty : ∀ {α : Type u_1} {β : Type u_2} (t : α → Finset β), ∅.disjiUnion t ⋯ = ∅
-- Mathlib.Topology.Category.Profinite.Basic
FintypeCat.toProfinite_map_hom_hom_apply : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : X.obj),
  (TopCat.Hom.hom (FintypeCat.toProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a