mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addCommGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : Neg M₂]
  [inst_4 : Sub M₂] [inst_5 : SMul ℤ M₂] [inst_6 : AddCommGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Surjective.addCommGroup f hf one mul inv div npow zpow =
    { toAddGroup := Function.Surjective.addGroup f hf one mul inv div npow zpow, add_comm := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The function that sends `x : mixedSpace K` to `∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖`. It defines a
norm and it used to define `convexBodySum`.  -/
NumberField.mixedEmbedding.convexBodySumFun : {K : Type u_1} → [inst : Field K] → [NumberField K] → NumberField.mixedEmbedding.mixedSpace K → ℝ
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.colimit.whiskerLeft_ι_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F) (j : J) {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.desc F c)) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (c.ι.app j)
-- Batteries.Data.List.Basic
/-- Computes the partial products of the elements of a list.

Examples:

`[a, b, c].partialProds = [1, 1 * a, (1 * a) * b, ((1 * a) * b) * c]`
`[2, 3, 5].partialProds = [1, 2, 6, 30]`
 -/
List.partialProds : {α : Type u_1} → [Mul α] → [One α] → List α → List α
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat}
  (x : ↥((TopologicalSpace.Opens.map f.base).obj V)),
  CategoryTheory.CategoryStruct.comp (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩)
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op V)) (X.evaluation x)
-- Mathlib.Analysis.Complex.Norm
/-- The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.  -/
Complex.cauSeqIm : (CauSeq ℂ fun x => ‖x‖) → CauSeq ℝ abs
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.mk.injEq : ∀ {A : Type u_6} {B : Type u_7} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  (toMonoidHom : A →* B) (map_star' : ∀ (a : A), (↑toMonoidHom).toFun (star a) = star ((↑toMonoidHom).toFun a))
  (toMonoidHom_1 : A →* B) (map_star'_1 : ∀ (a : A), (↑toMonoidHom_1).toFun (star a) = star ((↑toMonoidHom_1).toFun a)),
  ({ toMonoidHom := toMonoidHom, map_star' := map_star' } =
      { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedRequest.default : {α : Type u} → [Inhabited α] → Lean.JsonRpc.Request α
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsIrreducible.connected : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R},
  A.IsIrreducible → Quiver.IsSStronglyConnected n
-- Mathlib.Algebra.Group.Defs
npowRec'.eq_3 : ∀ {M : Type u_2} [inst : One M] [inst_1 : Mul M] (x : M) (k : ℕ), npowRec' k.succ.succ x = npowRec' (k + 1) x * x
-- Mathlib.Algebra.Torsor.Basic
/-- Subtracting a point from the point `p` is an injective function.  -/
vsub_right_injective : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), Function.Injective fun x => p -ᵥ x
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_pos : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic], 0 < 𝒢.strictWidthInfty
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂AlgHom_X : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (g : σ → S₁) (i : σ), (MvPolynomial.eval₂AlgHom R g) (MvPolynomial.X i) = g i
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).Faithful
-- Mathlib.Data.ZMod.Basic
ZModModule.add_self : ∀ {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod 2) G] (x : G), x + x = 0
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      (obj : (U : C) → Set (F.obj U)) →
        (∀ {U V : C} (i : U ⟶ V), obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj V) →
          CategoryTheory.Subfunctor F
-- Mathlib.Data.Vector.Defs
/-- Appending of vectors corresponds under `toList` to appending of lists.  -/
List.Vector.toList_append : ∀ {α : Type u_1} {n m : ℕ} (v : List.Vector α n) (w : List.Vector α m), (v ++ w).toList = v.toList ++ w.toList
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.ι_left_coprodIsoSigma_inv : ∀ (X Y : AlgebraicGeometry.Scheme),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (fun i => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y)
        { down := CategoryTheory.Limits.WalkingPair.left })
      (AlgebraicGeometry.coprodIsoSigma X Y).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X₁ ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f)
        CategoryTheory.MonObj.mul) =
    f
-- Lean.Meta.Sym.Pattern
/-- Instance arguments that could not be synthesized, nor assigned while processing pending
constraints. `args` still holds a fresh, unassigned metavariable for each of them. A consumer that
splices `args` into a proof term (e.g. `BackwardRule.apply`) must treat a non-empty array as
failure; a purely structural matcher may ignore it.
 -/
Lean.Meta.Sym.MatchUnifyResult.unresolvedInsts : Lean.Meta.Sym.MatchUnifyResult → Array Lean.MVarId
-- Mathlib.Analysis.Polynomial.Basic
/-- If `Q(x) ∣ P(x)` at infinitely many integers `x` and `Q` is monic, `Q ∣ P`.  -/
Polynomial.dvd_of_infinite_eval_dvd_eval : ∀ {P Q : Polynomial ℤ}, Q.Monic → {a | Polynomial.eval a Q ∣ Polynomial.eval a P}.Infinite → Q ∣ P
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram `D` to `F` is limit of `F`
evaluated at `D`. This version is for contravariant diagrams, see `colimitYonedaHomIsoLimit` for a
covariant version.  -/
CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor Iᵒᵖ C) →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.yoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.rightOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (x_1 : ↑((smoothSheafCommRing IM I M R).presheaf.stalk x)),
  (CategoryTheory.ConcreteCategory.hom (smoothSheaf.evalHom IM I R x))
      ((CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.forgetStalk IM I M R x).hom) x_1) =
    (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalHom IM I M R x)) x_1
-- Init.Data.ToString.Basic
instToStringSigma : {α : Type u} → {β : α → Type v} → [ToString α] → [(x : α) → ToString (β x)] → ToString (Sigma β)
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.mk.inj : ∀ {w wn wr : ℕ} {q r : BitVec w} {wn_1 wr_1 : ℕ} {q_1 r_1 : BitVec w},
  { wn := wn, wr := wr, q := q, r := r } = { wn := wn_1, wr := wr_1, q := q_1, r := r_1 } →
    wn = wn_1 ∧ wr = wr_1 ∧ q = q_1 ∧ r = r_1
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_eq' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : SubtractionCommMonoid α],
  Function.Periodic f c → f (c - x) = f (-x)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransform_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)) (x : V),
  (Real.Lp.fourierTransform f) x = FourierTransform.fourier (↑↑f) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.instHasPullbackCompOfIsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (i : X' ⟶ X)
  [CategoryTheory.IsIso i] [CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp i f) g
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is faithful on `R`-bialgebras.  -/
AlgebraicGeometry.bialgSpec.instFaithful : ∀ {R : CommRingCat}, (AlgebraicGeometry.bialgSpec R).Faithful
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F]
  (x_1 : carrier ((X.restrict h).presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom)
      ((CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) x_1) =
    (CategoryTheory.ConcreteCategory.hom
        (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯))
      x_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.giMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f),
  AddSubsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.sub_self_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s → ∀ {a : α}, a ∈ s → MonotoneOn (variationOnFromTo f s a - f) s
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.affine_affine_hasPullback : ∀ {B C : CommRingCat} {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec C)
  (g : AlgebraicGeometry.Spec B ⟶ AlgebraicGeometry.Spec C), CategoryTheory.Limits.HasPullback f g
-- Lean.Compiler.InitAttr
/-- Returns the indices of modules in `env.header.modules` whose `regularInitAttr` has non-empty
entries. Computed at `--incr-(header-)save` time and consumed by `runInitAttrsForModules` on
`--incr-load`.
 -/
Lean.getRegularInitAttrModIdxs : Lean.Environment → Array ℕ
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toRingHom_eq_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), f.toRingHom = ↑f
-- Mathlib.AlgebraicGeometry.Scheme
/-- `Γ(X, U)` is notation for `X.presheaf.obj (op U)`.  -/
AlgebraicGeometry.«termΓ(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_smul_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (S : Set (Set α)) (t : Set β), ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_top : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.join P Lean.Order.top = Lean.Order.top
-- Mathlib.Order.SuccPred.Limit
/-- Successor limits don't cover any other elements.  -/
Order.IsSuccLimit.isSuccPrelimit : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Order.IsSuccLimit a → Order.IsSuccPrelimit a
-- Mathlib.Algebra.Ring.SumsOfSquares
NonUnitalSubsemiring.coe_sumSq : ∀ {T : Type u_2} [inst : NonUnitalCommSemiring T], ↑(NonUnitalSubsemiring.sumSq T) = {s | IsSumSq s}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_fst_app : ∀ {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 : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J J' : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} (F_1 : J ⟶ J') (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.map F_1).fst.app X_1 = (F_1.app X_1).fst
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_smul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] {M : Type u_3} [inst_1 : SMul M α] (m : M) (x : Shrink.{v, u_2} α),
  (equivShrink α).symm (m • x) = m • (equivShrink α).symm x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceAdd : Lean.Meta.Simp.DSimproc
-- Aesop.RuleSet
Aesop.GlobalRuleSet.mk.inj : ∀ {toBaseRuleSet : Aesop.BaseRuleSet} {simpTheorems : Lean.Meta.SimpTheorems} {simprocs : Lean.Meta.Simprocs}
  {toBaseRuleSet_1 : Aesop.BaseRuleSet} {simpTheorems_1 : Lean.Meta.SimpTheorems} {simprocs_1 : Lean.Meta.Simprocs},
  { toBaseRuleSet := toBaseRuleSet, simpTheorems := simpTheorems, simprocs := simprocs } =
      { toBaseRuleSet := toBaseRuleSet_1, simpTheorems := simpTheorems_1, simprocs := simprocs_1 } →
    toBaseRuleSet = toBaseRuleSet_1 ∧ simpTheorems = simpTheorems_1 ∧ simprocs = simprocs_1
-- Mathlib.Order.Preorder.Finsupp
Finsupp.instLE : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [LE M] → LE (ι →₀ M)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.total : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M},
  Module.DualBases e ε → ∀ {m₁ m₂ : M}, (∀ (i : ι), (ε i) m₁ = (ε i) m₂) → m₁ = m₂
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given an algebra map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map
`Aₐ →ₐ[R] Bₐ`.  -/
IsLocalization.Away.mapₐ : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_5} →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          {B : Type u_6} →
            [inst_3 : CommSemiring B] →
              [inst_4 : Algebra R B] →
                (Aₚ : Type u_7) →
                  [inst_5 : CommSemiring Aₚ] →
                    [inst_6 : Algebra A Aₚ] →
                      [inst_7 : Algebra R Aₚ] →
                        [IsScalarTower R A Aₚ] →
                          (Bₚ : Type u_8) →
                            [inst_9 : CommSemiring Bₚ] →
                              [inst_10 : Algebra B Bₚ] →
                                [inst_11 : Algebra R Bₚ] →
                                  [IsScalarTower R B Bₚ] →
                                    (f : A →ₐ[R] B) →
                                      (a : A) →
                                        [IsLocalization.Away a Aₚ] → [IsLocalization.Away (f a) Bₚ] → Aₚ →ₐ[R] Bₚ
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a Haar measure under right addition is again a Haar measure.  -/
MeasureTheory.Measure.isHaarMeasure_map_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [IsTopologicalAddGroup G] (g : G),
  (MeasureTheory.Measure.map (fun x => x + g) μ).IsAddHaarMeasure
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' : α},
  t.get? k = some k' → k' ∈ t
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.mk.injEq : ∀ (eNew eqProof : Lean.Expr) (mvarIds : List Lean.MVarId) (eNew_1 eqProof_1 : Lean.Expr) (mvarIds_1 : List Lean.MVarId),
  ({ eNew := eNew, eqProof := eqProof, mvarIds := mvarIds } =
      { eNew := eNew_1, eqProof := eqProof_1, mvarIds := mvarIds_1 }) =
    (eNew = eNew_1 ∧ eqProof = eqProof_1 ∧ mvarIds = mvarIds_1)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_left : ∀ {w : ℕ} (a b : BitVec w), (a == b + a) = (b == 0#w)
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
isLittleO_abs_log_rpow_rpow_nhdsGT_zero : ∀ {s : ℝ} (r : ℝ), s < 0 → (fun x => |Real.log x| ^ r) =o[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ s
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.Hom.mk.inj : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y Z : ContinuousGeneratedByCat X}
  {hom hom_1 : Topology.ContinuousMapGeneratedBy X ↑Y ↑Z}, { hom := hom } = { hom := hom_1 } → hom = hom_1
-- Mathlib.Analysis.Convex.Segment
right_mem_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : MulActionWithZero 𝕜 E] (x y : E), y ∈ segment 𝕜 x y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsFunctor_obj_d : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (i j : ℕ),
  ((groupHomology.chainsFunctor k G).obj A).d i j =
    ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun n => groupHomology.inhomogeneousChains.d A n) i
      j
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.instDecidableIsHermitianOfEqConjTranspose : {α : Type u_1} →
  {n : Type u_4} → [inst : Star α] → (A : Matrix n n α) → [Decidable (A.conjTranspose = A)] → Decidable A.IsHermitian
-- Mathlib.Data.EReal.Inv
EReal.max_neg_neg : ∀ (x y : EReal), max (-x) (-y) = -min x y
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- If `i : X ⟶ Y` is a monomorphism of simplicial sets and `d : ℕ`, this is
a coproduct of copies of `Δ[d]` indexed by the nondegenerate `d`-simplices of `Y`
not in the range of `i`.  -/
SSet.relativeCellComplexOfMono.sigmaStdSimplex : {X Y : SSet} → (X ⟶ Y) → ℕ → SSet
-- Aesop.Util.UnionFind
Aesop.UnionFind.sizes : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.UnionFind α → Array USize
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.treeMap : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.RiiSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Order.Bounded
Set.bounded_le_of_bounded_lt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  Set.Bounded (fun x1 x2 => x1 < x2) s → Set.Bounded (fun x1 x2 => x1 ≤ x2) s
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.SearchState.mk.injEq : ∀ (choiceStack : List Lean.Meta.Grind.EMatch.Choice) (instanceMap : Lean.Meta.Grind.EMatch.InstanceMap)
  (choiceStack_1 : List Lean.Meta.Grind.EMatch.Choice) (instanceMap_1 : Lean.Meta.Grind.EMatch.InstanceMap),
  ({ choiceStack := choiceStack, instanceMap := instanceMap } =
      { choiceStack := choiceStack_1, instanceMap := instanceMap_1 }) =
    (choiceStack = choiceStack_1 ∧ instanceMap = instanceMap_1)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.ext : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : Zero V] [inst_2 : SMul R V]
  (x y : HahnModule Γ R V), ((HahnModule.of R).symm x).coeff = ((HahnModule.of R).symm y).coeff → x = y
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.quoted.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Qq.Impl.ExprBackSubstResult.quoted e) = 1 + sizeOf e
-- Mathlib.Topology.MetricSpace.Holder
holderOnWith_empty : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (C r : NNReal)
  (f : X → Y), HolderOnWith C r f ∅
-- Init.GetElem
/-- `GetElem?.getElem?` succeeds when the validity predicate is satisfied and fails otherwise.  -/
LawfulGetElem.getElem?_def : ∀ {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)}
  {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] (c : cont) (i : idx)
  [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_map_C : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (p : Polynomial R),
  Polynomial.evalEval x y (Polynomial.map Polynomial.C p) = Polynomial.eval y p
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapDomainAddEquiv`. -/
MonoidAlgebra.mapDomainAddEquiv_apply : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (e : M ≃ N)
  (x : MonoidAlgebra R M), ((MonoidAlgebra.mapDomainAddEquiv R e) x).coeff = Finsupp.equivMapDomain e x.coeff
-- Mathlib.Analysis.Calculus.FDeriv.Const
HasCompactSupport.fderiv_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F},
  HasCompactSupport f → ∀ (v : E), HasCompactSupport fun x => (fderiv 𝕜 f x) v
-- Init.Sym.Simp.SimprocDSL
/-- Register a named `Sym.simp` variant.

```
register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite [thm1, thm2] with self
  maxSteps := 50000
```
 -/
Lean.Parser.Command.registerSymSimp : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctor_obj : ∀ (C : CategoryTheory.Cat), CategoryTheory.Cat.opFunctor.obj C = CategoryTheory.Cat.of (↑C)ᵒᵖ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.next_add' : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [c.TensorSigns] (p q : I),
  c.Rel q (c.next q) → c.next (p + q) = p + c.next q
-- Mathlib.Data.List.Basic
List.IsSuffix.idxOf_add_length_le : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁ <:+ l₂ → ∀ (a : α), List.idxOf a l₂ + l₁.length ≤ List.idxOf a l₁ + l₂.length
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.instOrdModuleKey : Ord Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_one : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : One α] [IsBotOneClass α], s.sup f = 1 ↔ ∀ i ∈ s, f i = 1