mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localAlgEquiv'_apply : ∀ {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] (I : Ideal R) [hI : I.IsPrime] [inst_4 : Algebra R P] (J : Ideal S) (K : Ideal P)
  [inst_5 : J.IsPrime] [inst_6 : K.IsPrime] [inst_7 : J.LiesOver I]
  [inst_8 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_9 : Localization.AtPrime.IsLiesOverAlgebra I J] [inst_10 : K.LiesOver I]
  [inst_11 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)]
  [inst_12 : Localization.AtPrime.IsLiesOverAlgebra I K] (f : S ≃ₐ[R] P) (h : J = Ideal.comap f K)
  (a : Localization.AtPrime J), (Localization.localAlgEquiv' I J K f h) a = (Localization.localRingHom J K (↑f) h) a
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.eventually_lt : ∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {l : Filter γ}
  {f g : γ → α} {y z : α},
  Filter.Tendsto f l (nhds y) → Filter.Tendsto g l (nhds z) → y < z → ∀ᶠ (x : γ) in l, f x < g x
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.addCommGroup : {R : Type u} →
  {M : Type v} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → {module_M : Module R M} → (p : Submodule R M) → AddCommGroup ↥p
-- Std.Time.Internal.Bounded
/-- Adds two `Bounded` and adjust the boundaries.
 -/
Std.Time.Internal.Bounded.LE.subBounds : {n m i j : ℤ} →
  Std.Time.Internal.Bounded.LE n m → Std.Time.Internal.Bounded.LE i j → Std.Time.Internal.Bounded.LE (n - j) (m - i)
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- If `a ≠ 0` then the exponential zeta function is analytic everywhere.  -/
HurwitzZeta.differentiable_expZeta_of_ne_zero : ∀ {a : UnitAddCircle}, a ≠ 0 → Differentiable ℂ (HurwitzZeta.expZeta a)
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- If the relation given by $(f_i)_{i \in \iota}$ and $(x_i)_{i \in \iota}$ is trivial, then
$\sum_i f_i x_i$ is actually equal to $0$.  -/
Module.sum_smul_eq_zero_of_isTrivialRelation : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Fintype ι] {f : ι → R} {x : ι → M}, Module.IsTrivialRelation f x → ∑ i, f i • x i = 0
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The composition of the left maps in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPost' F)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Init.Data.List.Find
List.find?_flatMap_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool},
  List.find? p (List.flatMap f xs) = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, (!p y) = true
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_comm : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁ → Sort u_10} {κ₂ : ι₂ → Sort u_11}
  (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α),
  ⨅ i₁, ⨅ j₁, ⨅ i₂, ⨅ j₂, f i₁ j₁ i₂ j₂ = ⨅ i₂, ⨅ j₂, ⨅ i₁, ⨅ j₁, f i₁ j₁ i₂ j₂
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- If `e : V ≃ₗ[K] V` is such that `e.fixedReduce = 1`, then `e` is the product of
at most `finrank K (V ⧸ e.fixedSubmodule) - 1` transvections and one dilatransvection.

This is the first non-exceptional case in Dieudonné's theorem.  -/
LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V},
  e.fixedReduce = 1 →
    e ∈
      LinearEquiv.transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) *
        LinearEquiv.dilatransvections K V
-- Init.Tactics
/-- If true, use `grind` as a discharger for subgoals that cannot be closed
by `solve_by_elim` alone.  -/
Lean.Parser.Tactic.LibrarySearchConfig.grind : Lean.Parser.Tactic.LibrarySearchConfig → Bool
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_eq_sInf_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.inf f = sInf (f '' ↑s)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.continuousOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → ContinuousOn f s
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.p_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp P.p₀ h
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.mul_scaleRoots_of_noZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R) [NoZeroDivisors R],
  (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.toIsCompletelyMetrizableSpace : ∀ {α : Type u_3} {h : TopologicalSpace α} [self : PolishSpace α], TopologicalSpace.IsCompletelyMetrizableSpace α
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M) (a : α),
  (Finsupp.filter p f) a = if p a then f a else 0
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.comp.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : AddMonoid A] [inst_4 : DistribMulAction M A] {B : Type u_5}
  [inst_5 : AddMonoid B] [inst_6 : DistribMulAction N B] {C : Type u_7} [inst_7 : AddMonoid C]
  [inst_8 : DistribMulAction P C] [κ : φ.CompTriple ψ χ] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B),
  g.comp f = { toMulActionHom := (↑g).comp ↑f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Convex.Segment
Pi.image_update_segment : ∀ {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] [inst_4 : DecidableEq ι] (i : ι)
  (x₁ x₂ : M i) (y : (i : ι) → M i),
  Function.update y i '' segment 𝕜 x₁ x₂ = segment 𝕜 (Function.update y i x₁) (Function.update y i x₂)
-- Lean.Compiler.IR.CompilerM
Lean.IR.findEnvDecl : Lean.Environment → Lean.Name → Option Lean.IR.Decl
-- Mathlib.Tactic.DeriveTraversable
/-- `nestedMap f α (List (Array (List α)))` synthesizes the expression
`Functor.map (Functor.map (Functor.map f))`. `nestedMap` assumes that `α` appears in
`(List (Array (List α)))`.

(Similar to `nestedTraverse` but for `Functor`.)  -/
Mathlib.Deriving.Traversable.nestedMap : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.List.Defs
List.permutations'Aux.eq_2 : ∀ {α : Type u_1} (t a : α) (tail : List α),
  List.permutations'Aux t (a :: tail) = (t :: a :: tail) :: List.map (List.cons a) (List.permutations'Aux t tail)
-- Mathlib.Topology.Separation.Hausdorff
/-- The largest T2 quotient of a topological space. This construction is left-adjoint to the
inclusion of T2 spaces into all topological spaces.  -/
T2Quotient : (X : Type u_1) → [TopologicalSpace X] → Type u_1
-- Mathlib.Analysis.Analytic.Basic
/-- Analogue of `HasFPowerSeriesAt` where convergence is required only on a set `s`.  -/
HasFPowerSeriesWithinAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → FormalMultilinearSeries 𝕜 E F → Set E → E → Prop
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The set of roots whose root space is contained in a given Lie ideal.  -/
LieIdeal.rootSet : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra K L] →
          [inst_3 : FiniteDimensional K L] →
            {H : LieSubalgebra K L} → [inst_4 : H.IsCartanSubalgebra] → LieIdeal K L → Set ↥LieSubalgebra.root
-- Init.Data.SInt.Lemmas
Int16.ofIntTruncate_toInt : ∀ (x : Int16), Int16.ofIntClamp x.toInt = x
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj : ∀ (X : AlgebraicGeometry.Scheme) (U : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).obj U = U.toOpens
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).get? k = Option.map f (t.get? k)
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
smaller than the order of the power series.  -/
MvPowerSeries.coeff_of_lt_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {d : σ →₀ ℕ},
  ↑(Finsupp.degree d) < f.order → (MvPowerSeries.coeff d) f = 0
-- Mathlib.RepresentationTheory.Tannaka
/-- The group homomorphism `G →* Aut (forget k G)` shown to be an isomorphism.  -/
TannakaDuality.FiniteGroup.equivHom : (k G : Type u) →
  [inst : CommRing k] → [inst_1 : Group G] → G →* CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)
-- Std.Async.System
/-- Gets information about the operating system.
 -/
Std.Async.System.getSystemInfo : IO Std.Async.System.OSInfo
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicateTR.loop.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (as : List α) (h_1 : (as : List α) → motive 0 as)
  (h_2 : (n : ℕ) → (as : List α) → motive n.succ as),
  (match n.succ, as with
    | 0, as => h_1 as
    | n.succ, as => h_2 n as) =
    h_2 n as
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedUsedSimps.default : Lean.Meta.Simp.UsedSimps
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.op_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.op.inl = c.fst.op
-- Mathlib.Data.Nat.Cast.Defs
AddCommMonoidWithOne.toAddCommMonoid : {R : Type u_2} → [self : AddCommMonoidWithOne R] → AddCommMonoid R
-- Lean.Parser.Term
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term.  -/
Lean.Parser.Term.letI : Lean.Parser.Parser
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Congr!.Config
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instDistribMulAction : (p : ENNReal) →
  (K : Type u_1) →
    (V : Type u_4) →
      [inst : Monoid K] → [inst_1 : AddCommGroup V] → [DistribMulAction K V] → DistribMulAction K (WithLp p V)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.coe_nil : ∀ {α : Type u_1}, ↑[] = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.toLinearMap_projectionOntoL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q),
  ↑(p.projectionOntoL q h) = p.projectionOnto q ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map₁_one : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (φ : Rep.res 1 A ⟶ B), groupCohomology.map 1 φ 1 = 0
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.successProbability : Aesop.UnsafeQueueEntry → Aesop.Percent
-- Mathlib.RingTheory.Unramified.LocalStructure
HasStandardEtaleSurjectionOn.mk : ∀ {R : Type u_1} {A : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [Algebra.IsStandardEtale R A] {Sf : Type u_4} [inst_6 : CommRing Sf]
  [inst_7 : Algebra R Sf] [inst_8 : Algebra S Sf] [IsScalarTower R S Sf] {f : S} [IsLocalization.Away f Sf]
  (φ : A →ₐ[R] Sf), Function.Surjective ⇑φ → HasStandardEtaleSurjectionOn R f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany! l) =
        (Std.DTreeMap.Internal.Impl.contains k t || (List.map Sigma.fst l).contains k)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_zero_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (m : Fin 0 → E), (iteratedFDeriv 𝕜 0 f x) m = f x
-- Lean.Expr
/-- Lower the loose bound variables `>= s` in `e` by `d`.
That is, a loose bound variable `bvar i` with `i >= s` is mapped to `bvar (i-d)`.

Remark: if `s < d`, then the result is `e`.
 -/
Lean.Expr.lowerLooseBVars : Lean.Expr → ℕ → ℕ → Lean.Expr
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.trans_left : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  t₁.Bounded o₁ ↑x → Ordnode.Valid' (↑x) t₂ o₂ → Ordnode.Valid' o₁ t₂ o₂
-- Init.Data.List.Scan.Lemmas
List.scanl_iff_nil : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (c : β), List.scanl f b l = [c] ↔ c = b ∧ l = []
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_forall_eq : ∀ {α : Type u} {s : Set α} (a : α), (∀ b ∈ s, b = a) → s.Subsingleton
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N),
  AddSubmonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }
-- Init.Data.Array.Erase
Array.eraseIdx_append_of_size_le : ∀ {α : Type u_1} {xs : Array α} {k : ℕ} (hk : xs.size ≤ k) (ys : Array α) (h : k < (xs ++ ys).size),
  (xs ++ ys).eraseIdx k h = xs ++ ys.eraseIdx (k - xs.size) ⋯
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.inhabited : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Inhabited α] → Inhabited (Matrix m n α)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιNatTrans_app_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C}
  (f : X ⟶ Y) (d : ↑(F.obj X)), ((CategoryTheory.Grothendieck.ιNatTrans f).app d).base = f
-- Mathlib.Topology.FiberBundle.Constructions
inducing_pullbackTotalSpaceEmbedding : ∀ {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B),
  Topology.IsInducing (Bundle.pullbackTotalSpaceEmbedding f)
-- Mathlib.MeasureTheory.Group.LIntegral
/-- Translating a function by right-multiplication does not change its Lebesgue integral
with respect to a right-invariant measure.  -/
MeasureTheory.lintegral_mul_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G] [MeasurableMul G]
  [μ.IsMulRightInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenIsoAway_hom : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  (AlgebraicGeometry.Proj.basicOpenIsoAway 𝒜 f f_deg hm).hom = AlgebraicGeometry.Proj.awayToSection 𝒜 f
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_one : ∀ {M : Type u_4} [inst : CommMonoid M] (f : ℕ → M), ∏ k ∈ Finset.range 1, f k = f 0
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C)
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType X₁ × CategoryTheory.ToType X₂),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)
      ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) =
    x.1
-- Batteries.Data.HashMap.Basic
/-- Combines two hashmaps using a monadic function `f` to combine two values at a key.
```
def map1 := ofList [("one", 1), ("two", 2)]
def map2 := ofList [("two", 2), ("three", 3)]
def map3 := ofList [("two", 3), ("three", 3)]
def mergeIfNoConflict? (_ : String) (v₁ v₂ : Nat) : Option Nat :=
  if v₁ != v₂ then none else some v₁


mergeWithM mergeIfNoConflict? map1 map2 = some {"one" => 1, "two" => 2, "three" => 3}
mergeWithM mergeIfNoConflict? map1 map3 = none
```
 -/
Batteries.HashMap.mergeWithM : {α : Type u_1} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {m : Type (max u_2 u_1) → Type u_3} →
        {β : Type (max u_2 u_1)} →
          [Monad m] → (α → β → β → m β) → Batteries.HashMap α β → Batteries.HashMap α β → m (Batteries.HashMap α β)
-- Mathlib.Data.Set.Pairwise.Basic
/-- A function `f : α → ι` with nonempty codomain takes pairwise equal values on a set `s` if and
only if for some `z` in the codomain, `f` takes value `z` on all `x ∈ s`. See also
`Set.Nonempty.pairwise_eq_iff_exists_eq` for a version that assumes `Set.Nonempty s` instead of
`[Nonempty ι]`.  -/
Set.pairwise_eq_iff_exists_eq : ∀ {α : Type u_1} {ι : Type u_4} [Nonempty ι] (s : Set α) (f : α → ι),
  (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
-- Mathlib.Order.Category.Frm
Frm.of.inj : ∀ {carrier : Type u_1} {str : Order.Frame carrier} {carrier_1 : Type u_1} {str_1 : Order.Frame carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.RingTheory.Ideal.Maps
Ideal.isMaximal_map_iff_of_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Bijective ⇑f → ∀ {I : Ideal R}, (Ideal.map f I).IsMaximal ↔ I.IsMaximal
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIsoClass.toOrderAddMonoidIso.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : EquivLike F α β] [inst_5 : OrderIsoClass F α β] [inst_6 : AddEquivClass F α β]
  (f : F), ↑f = { toAddEquiv := ↑f, map_le_map_iff' := ⋯ }
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.mk : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstrProof → ℕ → Lean.Meta.Grind.AC.EqCnstr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ),
  Turing.TM1.stepAux Turing.TM1.Stmt.halt x x_1 = { l := none, var := x, Tape := x_1 }
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup.eq_1 : ∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] (u : ℕ → R),
  LinearGrowth.linearGrowthSup u = Filter.limsup (fun n => u n / ↑n) Filter.atTop
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IteratorAccess.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        ((it : Std.IterM m β) → (n : ℕ) → m (Std.PlausibleIterStep (Std.IterM.IsPlausibleNthOutputStep n it))) →
          Std.IteratorAccess α m
-- Mathlib.Tactic.FunProp.FunctionData
/-- main variable  -/
Mathlib.Meta.FunProp.FunctionData.mainVar : Mathlib.Meta.FunProp.FunctionData → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- (An auxiliary definition for `functorCategoryMonoidal`.)  -/
CategoryTheory.Monoidal.FunctorCategory.whiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          {F' G' : CategoryTheory.Functor C D} →
            (F : CategoryTheory.Functor C D) →
              (F' ⟶ G') →
                (CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶
                  CategoryTheory.Monoidal.FunctorCategory.tensorObj F G')
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions : Type
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslationInfo.mk.sizeOf_spec : ∀ (translation : Lean.Name) (reorder : Mathlib.Tactic.Translate.Reorder)
  (relevantArg : Mathlib.Tactic.Translate.RelevantArg),
  sizeOf { translation := translation, reorder := reorder, relevantArg := relevantArg } =
    1 + sizeOf translation + sizeOf reorder + sizeOf relevantArg
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.associates_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  Irreducible (Associates.mk v.asIdeal)
-- Init.Data.List.Lemmas
List.length_pos_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → 0 < l.length
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.toFreeMonoid_mk_eq_cons : ∀ {α : Type u_1} (x : α) (xs : List α),
  FreeSemigroup.toFreeMonoid { head := x, tail := xs } = FreeMonoid.ofList (x :: xs)
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.indexing_mode : Lean.Parser.Category
-- Lean.Elab.App
/-- A weak version of forallTelescopeReducing that only uses whnfCore, to avoid unfolding definitions except by `unfoldDefinition?` below.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveDottedIdentFn.withForallBody : {α : Type} → Lean.Expr → (Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Color `G ⊕g H` with colorings of `G` and `H`  -/
SimpleGraph.Coloring.sum : {V : Type u_3} →
  {W : Type u_5} →
    {γ : Type u_7} → {G : SimpleGraph V} → {H : SimpleGraph W} → G.Coloring γ → H.Coloring γ → (G ⊕g H).Coloring γ