mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqEMatchTheoremConstraint : BEq Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.GroupTheory.OrderOfElement
/-- Elements of finite order are of finite order in submonoids.  -/
Submonoid.isOfFinOrder_coe : ∀ {G : Type u_1} [inst : Monoid G] {H : Submonoid G} {x : ↥H}, IsOfFinOrder ↑x ↔ IsOfFinOrder x
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.id_whiskerLeft_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv h))
-- Mathlib.Algebra.Module.RingHom
/-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`.
See note [reducible non-instances].  -/
RingHom.toModule : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → Module R S
-- Mathlib.Algebra.Lie.Basic
/-- Lie algebra equivalences are symmetric.  -/
LieEquiv.symm : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] → [inst_3 : LieAlgebra R L₁] → [inst_4 : LieAlgebra R L₂] → (L₁ ≃ₗ⁅R⁆ L₂) → L₂ ≃ₗ⁅R⁆ L₁
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.maximalIdeal.eq_1 : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A],
  IsDiscreteValuationRing.maximalIdeal A = { asIdeal := IsLocalRing.maximalIdeal A, isPrime := ⋯, ne_bot := ⋯ }
-- Mathlib.Algebra.Group.Defs
zpow_one : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G), a ^ 1 = a
-- Lean.Meta.Basic
/-- The name of the parameter.  -/
Lean.Meta.ExprParamInfo.name : Lean.Meta.ExprParamInfo → Lean.Name
-- Mathlib.Order.WithBot
WithBot.lt_unbot_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithBot α} (hx : x ≠ ⊥), a < x.unbot hx ↔ ↑a < x
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- A modular form is a cusp form if it lies in the cusp form submodule.  -/
ModularForm.IsCuspForm : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → [Γ.HasDetOne] → ModularForm Γ k → Prop
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.isStrictOrder : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : PartialOrder N],
  IsStrictOrder (Colex (α →₀ N)) fun x1 x2 => x1 < x2
-- Lean.LocalContext
Lean.LocalContext.findDeclRevM? : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → [Monad m] → Lean.LocalContext → (Lean.LocalDecl → m (Option β)) → m (Option β)
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.MemLp.meas_ge_lt_top : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {f : α → E},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → ∀ {ε : NNReal}, ε ≠ 0 → μ {x | ε ≤ ‖f x‖₊} < ⊤
-- Init.Data.Array.TakeDrop
Array.exists_of_uset : ∀ {α : Type u_1} {xs : Array α} {i : USize} {d : α} (h : i.toNat < xs.size),
  ∃ l₁ l₂, xs.toList = l₁ ++ xs[i] :: l₂ ∧ l₁.length = i.toNat ∧ (xs.uset i d h).toList = l₁ ++ d :: l₂
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis.cardinalMk_eq : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑I = Cardinal.mk ↑J
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.ofPred_exists`. -/
Set.setOf_exists : ∀ {β : Type u_2} {ι : Sort u_5} (p : ι → β → Prop), {x | ∃ i, p i x} = ⋃ i, {x | p i x}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.isIso_of_from_star : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C}
  (f : CategoryTheory.WithTerminal.star ⟶ X), CategoryTheory.IsIso f
-- Mathlib.Data.Part
Part.instUnion : {α : Type u_1} → [Union α] → Union (Part α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_eq_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, m.contains a = (Std.DHashMap.Const.get? m a).isSome
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.toLinearEquiv_smul : ∀ {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : SeminormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W] (e : V ≃ₗᵢ[𝕜] W)
  (α : ↥(unitary 𝕜)), (α • e).toLinearEquiv = Unitary.toUnits α • e.toLinearEquiv
-- Mathlib.NumberTheory.PellMatiyasevic
_private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.d.eq_1 : ∀ {a : ℕ} (_a1 : 1 < a), Pell.d✝ _a1 = a * a - 1
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The convolution of a Dirichlet character `χ` with the twist `χ * μ` is `δ`,
the indicator function of `{1}`.  -/
DirichletCharacter.convolution_mul_moebius : ∀ {n : ℕ} (χ : DirichletCharacter ℂ n),
  LSeries.convolution (fun n_1 => χ ↑n_1) ((fun n_1 => χ ↑n_1) * fun n => ↑(ArithmeticFunction.moebius n)) =
    LSeries.delta
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- Fraction free cardinality formula for the points of `ℙ k V` if `k` and `V` are finite
(for silly reasons the formula also holds when `k` and `V` are infinite).
See `Projectivization.card'` and `Projectivization.card''` for other spellings of the formula.  -/
Projectivization.card : ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V],
  Nat.card V - 1 = Nat.card (Projectivization k V) * (Nat.card k - 1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey? = t.keys.head?
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Cauchy–Schwarz inequality with norm  -/
abs_real_inner_le_norm : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), |inner ℝ x y| ≤ ‖x‖ * ‖y‖
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail.  -/
Std.DTreeMap.Internal.Impl.all : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ((a : α) → β a → Bool) → Bool
-- Init.Prelude
Nat.sub_le : ∀ (n m : ℕ), n - m ≤ n
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.cocone_ι_app : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (j : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.Types.Pushout.cocone f g).ι.app j =
    Option.rec
      (CategoryTheory.CategoryStruct.comp f
        (TypeCat.ofHom fun x => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x)))
      (fun val =>
        CategoryTheory.Limits.WalkingPair.rec
          (TypeCat.ofHom fun x => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x))
          (TypeCat.ofHom fun x => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inr x)) val)
      j
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The morphism from the domain to the scheme-theoretic image.  -/
AlgebraicGeometry.Scheme.Hom.toImage : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → X ⟶ AlgebraicGeometry.Scheme.Hom.image f
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (toArray : Array α)
  (toHashSet : Std.HashSet α),
  sizeOf { toArray := toArray, toHashSet := toHashSet } = 1 + sizeOf toArray + sizeOf toHashSet
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a localizer morphism induces a fully faithful functor on some choice of
localized categories, it will be so for any choice of localized categories.  -/
_private.Mathlib.CategoryTheory.Localization.LocalizerMorphism.0.CategoryTheory.LocalizerMorphism.fullyFaithfulImp : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [L₂.IsLocalization W₂] →
                              (G : CategoryTheory.Functor D₁ D₂) →
                                [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] →
                                  {D₁' : Type u₄'} →
                                    {D₂' : Type u₅'} →
                                      [inst_7 : CategoryTheory.Category.{v₄', u₄'} D₁'] →
                                        [inst_8 : CategoryTheory.Category.{v₅', u₅'} D₂'] →
                                          (L₁' : CategoryTheory.Functor C₁ D₁') →
                                            (L₂' : CategoryTheory.Functor C₂ D₂') →
                                              [L₁'.IsLocalization W₁] →
                                                [L₂'.IsLocalization W₂] →
                                                  (G' : CategoryTheory.Functor D₁' D₂') →
                                                    [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] →
                                                      G.FullyFaithful → G'.FullyFaithful
-- Lean.Compiler.LCNF.Types
Lean.Expr.isVoid : Lean.Expr → Bool
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_one : ∀ {α : Type u} (d : α), WithOne.unoneD d 1 = d
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.ext_iff : ∀ {P Q : AlgebraicGeometry.AffineTargetMorphismProperty},
  P = Q ↔ ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y], P f ↔ Q f
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_add : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] {p : ι → Prop} [inst_1 : DecidablePred p]
  (v v' : Π₀ (i : ι), β i), DFinsupp.subtypeDomain p (v + v') = DFinsupp.subtypeDomain p v + DFinsupp.subtypeDomain p v'
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.nnnorm_constOfIsEmpty : ∀ (𝕜 : Type u) (E : Type wE) {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (x : F),
  ‖ContinuousAlternatingMap.constOfIsEmpty 𝕜 E ι x‖₊ = ‖x‖₊
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq : ∀ (x : ℂ), Complex.cos x ≠ -1 → Complex.cos x = (1 - Complex.tan (x / 2) ^ 2) / (1 + Complex.tan (x / 2) ^ 2)
-- Batteries.Data.List.Basic
List.takeDTR.go.eq_3 : ∀ {α : Type u_1} (dflt : α) (a : ℕ) (a_1 : Array α),
  (a = 0 → False) → List.takeDTR.go dflt a [] a_1 = a_1.toListAppend (List.replicate a dflt)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_d_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.d = 0 → P.toPoly.degree = ⊥
-- Mathlib.Data.Set.MulAntidiagonal
Set.mulAntidiagonal.eq_1 : ∀ {α : Type u_1} [inst : Mul α] (s t : Set α) (a : α), s.mulAntidiagonal t a = {x | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a}
-- Mathlib.Data.Set.Prod
Set.prod_union : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β}, s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_bot_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ∈ ⊥.parts ↔ ∃ a ∈ s, {a} = t
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCoreAux.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E),
  balancedCoreAux 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- `A.toEuclideanLin` is positive if and only if `A` is positive semi-definite.  -/
Matrix.isPositive_toEuclideanLin_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  (Matrix.toEuclideanLin A).IsPositive ↔ A.PosSemidef
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkIso_inv_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom))
      CategoryTheory.Limits.CategoricalPullback.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w).inv.fst = eₗ.inv
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        (val : PresheafOfModules R.obj) → CategoryTheory.Presheaf.IsSheaf J val.presheaf → SheafOfModules R
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The Haar measure is sigma-finite in a second countable group.  -/
MeasureTheory.Measure.sigmaFinite_haarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G]
  {K₀ : TopologicalSpace.PositiveCompacts G}, MeasureTheory.SigmaFinite (MeasureTheory.Measure.haarMeasure K₀)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.isIntegralElem_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] (f : R →+* S) {x : R}, f.IsIntegralElem (f x)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.comp_autMap_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) {A B : C} [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) (a : (F.obj A).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.PreGaloisCategory.autMap f σ).hom))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) a) =
    (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (F.map σ.hom)) a)
-- Mathlib.Topology.Algebra.Module.EmbeddingOfLocal
LinearMap.isEmbedding_of_restrict_nhds_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜₁]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜₁ E]
  [inst_5 : Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} {f : E →ₛₗ[σ] F} [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F]
  [IsTopologicalAddGroup E] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] [RingHomIsometric σ]
  {V : Set E}, V ∈ nhds 0 → Topology.IsEmbedding (V.domRestrict ⇑f) → Topology.IsEmbedding ⇑f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
`RingHom.rangeS`.  -/
RingEquiv.ofLeftInverseS : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] → {g : S → R} → {f : R →+* S} → Function.LeftInverse g ⇑f → R ≃+* ↥f.rangeS
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.isOpen_ne_top : IsOpen {a | a ≠ ⊤}
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given `x y : R` and localizations `S`, `P` away from `x` and `x * y`
respectively, the homomorphism induced from `S` to `P`.  -/
IsLocalization.Away.awayToAwayRight : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (x : R) →
                [IsLocalization.Away x S] → (y : R) → [inst_5 : Algebra R P] → [IsLocalization.Away (x * y) P] → S →+* P
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).f = X.δ f g n₀ n₁ hn₁
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- A Gaussian distribution on `ℝ` with mean `μ` and variance `v`.  -/
ProbabilityTheory.gaussianReal : ℝ → NNReal → MeasureTheory.Measure ℝ
-- Batteries.Data.AssocList
Batteries.AssocList.findEntry?_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  Batteries.AssocList.findEntry? a l = List.find? (fun x => x.1 == a) l.toList
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.sup_toAddSubgroup : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of a function `f` w.r.t. a measure `μ`.

It is equal to `(μ.real univ)⁻¹ • ∫ x, f x ∂μ`, so it takes value zero if `f` is not integrable or
if `μ` is an infinite measure. If `μ` is a probability measure, then the average of any function is
equal to its integral.

For the average on a set, use `⨍ x in s, f x ∂μ`, defined as `⨍ x, f x ∂(μ.restrict s)`. For the
average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.«term⨍_,_∂_» : Lean.ParserDescr
-- Lean.CoreM
Lean.Core.throwMaxHeartbeat : Lean.Name → Lean.Name → ℕ → Lean.CoreM Unit
-- Init.Data.Nat.Dvd
Nat.dvd_add_iff_right : ∀ {k m n : ℕ}, k ∣ m → (k ∣ n ↔ k ∣ m + n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k fallback : α},
      k ∉ m → l.contains k = false → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat.eq_1 : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β),
  CauSeq.Completion.ofRat x = CauSeq.Completion.mk (CauSeq.const abv x)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {Z : D} (h : (F.leftDerived n).obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv
          (CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) h) =
        CategoryTheory.CategoryStruct.comp
          ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
          (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).inv h)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_mulRight : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  (MeasurableEquiv.mulRight g).toEquiv = Equiv.mulRight g
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The right inclusion of `G` into `coprod F G`.  -/
CategoryTheory.FunctorToTypes.coprod.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → G ⟶ CategoryTheory.FunctorToTypes.coprod F G
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A module is semisimple when every submodule has a complement, or equivalently, the module
is a direct sum of simple modules.  -/
IsSemisimpleModule : (R : Type u_2) → [inst : Ring R] → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Topology.CompactOpen
ContinuousWithinAt.compCM : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_6} [inst_4 : TopologicalSpace X'] {a : X'}
  {g : X' → C(Y, Z)} {f : X' → C(X, Y)} {s : Set X'},
  ContinuousWithinAt g s a → ContinuousWithinAt f s a → ContinuousWithinAt (fun x => (g x).comp (f x)) s a
-- Init.Core
/-- `IdempotentOp op` indicates `op` is an idempotent binary operation.
i.e. `a ∘ a = a`.
 -/
Std.IdempotentOp : {α : Sort u} → (α → α → α) → Prop
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.algEquivExtension.congr_simp : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n] (l : Type u_2) [inst_5 : Field l] [inst_6 : Algebra k l] (h : Module.finrank k l = n),
  FiniteField.algEquivExtension k p n l h = FiniteField.algEquivExtension k p n l h
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.Option.pmap_or.match_1.eq_2 : ∀ {α : Type u_1} {p : α → Prop} {o' : Option α}
  (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2) (a : α)
  (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) (h_1 : (h : ∀ (a : α), none.or o' = some a → p a) → motive none)
  (h_2 : (a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)),
  (match some a, h with
    | none, h => h_1 h
    | some a, h => h_2 a h) =
    h_2 a h
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- For `f` a morphism in `Arrow V`, this is a cokernel cofork of `(quotient V).map f`.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.cokernelCofork : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [CategoryTheory.Limits.HasBinaryBiproducts V] →
        {u v : CategoryTheory.Arrow V} →
          (f : u ⟶ v) → CategoryTheory.Limits.CokernelCofork ((CategoryTheory.Preadditive.RightFreyd.quotient V).map f)
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.mk.injEq : ∀ {α : Type u} (xs xs_1 : Subarray α), ({ xs := xs } = { xs := xs_1 }) = (xs = xs_1)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.type : Lean.Meta.Sym.Arith.Ring → Lean.Expr