mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.comp_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {a b c : CategoryTheory.Quotient r}
  (f : a.as ⟶ b.as) (g : b.as ⟶ c.as),
  CategoryTheory.Quotient.comp r (Quot.mk (CategoryTheory.HomRel.CompClosure r) f)
      (Quot.mk (CategoryTheory.HomRel.CompClosure r) g) =
    Quot.mk (CategoryTheory.HomRel.CompClosure r) (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Shifting a configuration commutes with occurrences of a pattern.

Formally: a pattern `p` occurs in the shifted configuration `mulShift h x` at
position `g` if and only if it occurs in the original configuration `x` at
position `g * h`.  -/
SymbolicDynamics.FullShift.Pattern.mulOccursInAt_mulShift : ∀ {A : Type u_3} {G : Type u_4} [inst : Inhabited A] [inst_1 : Monoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (x : G → A) (g h : G), p.mulOccursInAt (SymbolicDynamics.FullShift.mulShift g x) h ↔ p.mulOccursInAt x (g * h)
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
/-- **Frullani's integral**, limit form, for functions valued in a complete normed space.
If `f` is locally integrable on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
and `0 < a` and `0 < b`, then `∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x)) → log (b / a) • (L - R)`
as `ε → 0⁺` and `r → +∞`.  -/
Frullani.tendsto_intervalIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L R : E}
  [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L) →
          Filter.Tendsto f Filter.atTop (nhds R) →
            Filter.Tendsto (fun p => ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x)))
              (nhdsWithin 0 (Set.Ioi 0) ×ˢ Filter.atTop) (nhds (Real.log (b / a) • (L - R)))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.commMonoid.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.IsCommMonObj M],
  CategoryTheory.Hom.commMonoid = { toMonoid := CategoryTheory.Hom.monoid, mul_comm := ⋯ }
-- Mathlib.Topology.Sheaves.Skyscraper
/-- Taking skyscraper presheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
`p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
 -/
skyscraperPresheafFunctor : {X : TopCat} →
  (p₀ : ↑X) →
    [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst : CategoryTheory.Category.{w, v} C] →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Functor C (TopCat.Presheaf C X)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_op_iff_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor J C}, CategoryTheory.Limits.HasColimit F.op ↔ CategoryTheory.Limits.HasLimit F
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] (f : α → β) (a : α),
  IsLocalMax f a = IsMaxFilter f (nhds a) a
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instAddCommGroup : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → AddCommGroup ↥(MeasureTheory.Lp E p μ)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.sub_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f g : ContIntertwiningMap π₁ π₂) (v : V),
  (f - g) v = f v - g v
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux : ∀ {X Y U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X),
  fg = CategoryTheory.CategoryStruct.comp f g →
    ∀ [h : AlgebraicGeometry.IsOpenImmersion g] (V : U.Opens),
      (TopologicalSpace.Opens.map f.base).obj V =
        (TopologicalSpace.Opens.map fg.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V)
-- Mathlib.Topology.MetricSpace.Basic
/-- A metric space is second countable if one can reconstruct up to any `ε>0` any element of the
space from countably many data.  -/
Metric.secondCountable_of_countable_discretization : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε) → SecondCountableTopology α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the second vector passed to `oangle` from the first vector negates the sign of
the angle.  -/
Orientation.oangle_sign_sub_right_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle x (x - y)).sign = -(o.oangle x y).sign
-- Mathlib.Topology.UniformSpace.Cauchy
Ultrafilter.cauchy_of_totallyBounded' : ∀ {α : Type u} [uniformSpace : UniformSpace α] (f : Ultrafilter α), (↑f).TotallyBounded → Cauchy ↑f
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.factorThru_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P X E : C} [inst_1 : CategoryTheory.Projective P] (f : P ⟶ X)
  (e : E ⟶ X) [inst_2 : CategoryTheory.Epi e] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e)
      (CategoryTheory.CategoryStruct.comp e h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_h_e_nsmul : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → ⁅h, e⁆ = 2 • e
-- Batteries.Tactic.HelpCmd
_private.Batteries.Tactic.HelpCmd.0.Batteries.Tactic.elabHelpAttr : Option Lean.Ident → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.const_comp : ∀ {X Y Z : SSet} (y : Y.obj (Opposite.op { len := 0 })) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.const y) g =
    SSet.const ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) y)
-- Init.Meta.Defs
Lean.Syntax.setHeadInfo : Lean.Syntax → Lean.SourceInfo → Lean.Syntax
-- Mathlib.RingTheory.Flat.LocallyFree
/-- Let `M` be a finite flat `R`-module, `p` be a prime ideal of `R`. If `rankAtStalk M` is
constant, then there exists `a ∉ p` such that `M` is free after localization away from `a`.  -/
Module.Free.away_of_finite_of_flat_of_rankAtStalk_constant : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Module.Flat R M] (p : Ideal R) [inst_5 : p.IsPrime],
  (∀ (m : Ideal R) [inst_6 : m.IsMaximal],
      Module.rankAtStalk M { asIdeal := m, isPrime := ⋯ } = Module.rankAtStalk M { asIdeal := p, isPrime := ⋯ }) →
    ∃ a ∉ p, Module.Free (Localization.Away a) (LocalizedModule.Away a M)
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousInv.of_nhds_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1) →
    (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) →
      (∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) → ContinuousInv G
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.mk.sizeOf_spec : ∀ {α : Type u_1} {f : α → α} [inst : SizeOf α] (val : ℕ), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.Algebra.Lie.Extension
/-- A one-field structure giving a type synonym for a direct product. We use this to describe an
alternative Lie algebra structure on the product, where the bracket is shifted by a 2-cocycle.  -/
LieAlgebra.ofTwoCocycle : {R : Type u_5} →
  {L : Type u_6} →
    {M : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] → ↥(LieModule.Cohomology.twoCocycle R L M) → Type (max u_6 u_7)
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.decidableMemCenter.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (a : M) [inst_1 : Decidable (∀ (b : M), b * a = a * b)],
  Submonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) ⋯
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a
trivialization of `Z` containing `f x`.  -/
Bundle.Trivialization.continuousAt_of_comp_left : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {X : Type u_5} [inst_3 : TopologicalSpace X] {f : X → Z} {x : X}
  (e : Bundle.Trivialization F proj),
  ContinuousAt (proj ∘ f) x → proj (f x) ∈ e.baseSet → ContinuousAt (↑e ∘ f) x → ContinuousAt f x
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- Suppose we have a commutative square of functors

```
      Q
    A → B
  U ↓   ↓ V
    C → D
      L
```

where `U` has a right adjoint, `A` has reflexive equalizers and `V` is comonadic.
Then `Q` has a right adjoint if `L` has a right adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
 -/
CategoryTheory.isLeftAdjoint_square_lift_comonadic : ∀ {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] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D)
  (U : CategoryTheory.Functor A C) (L : CategoryTheory.Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint]
  [CategoryTheory.ComonadicLeftAdjoint V] [L.IsLeftAdjoint] [CategoryTheory.Limits.HasCoreflexiveEqualizers A],
  Q.IsLeftAdjoint
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc : ∀ {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) {Z : C} (h_1 : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx)
      (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).hom h_1) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      h_1
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEmbedding_ground_eq : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ↪ β), (M.mapEmbedding f).E = ⇑f '' M.E
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplex_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangleRotateShortComplex φ).g = (CochainComplex.mappingCone.triangle φ).rotate.mor₂
-- Mathlib.Data.Nat.Factorization.PrimePow
isPrimePow_iff_minFac_pow_factorization_eq : ∀ {n : ℕ}, n ≠ 1 → (IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.asIso'.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  [inst_1 : CategoryTheory.IsIso f], CategoryTheory.asIso' f = CategoryTheory.asIso' f_1
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `b` is topologically nilpotent, then `a * b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.mul_left : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsLinearTopology R R] (a : R) {b : R},
  IsTopologicallyNilpotent b → IsTopologicallyNilpotent (a * b)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.coe_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), ↑(H.addSubgroupOf K) = ⇑K.subtype ⁻¹' ↑H
-- Mathlib.Algebra.Notation.Pi.Defs
/-- **Alias** of `Function.prod_snd_fst`. -/
Pi.prod_snd_fst : ∀ {α : Type u_1} {β : Type u_2}, Function.prod Prod.snd Prod.fst = Prod.swap
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The equivalence `A ≌ B` whose functor is `F ⋙ eB.inverse` and
whose inverse functor is `G : B ⥤ A`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  {eB : B ≌ B'} →
                    {e' : A' ≌ B'} →
                      {F : CategoryTheory.Functor A B'} →
                        (eA.functor.comp e'.functor ≅ F) →
                          {G : CategoryTheory.Functor B A} → (eB.functor.comp e'.inverse ≅ G.comp eA.functor) → (A ≌ B)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_hom_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.unop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).inv
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.forgetToTopCatTopologicalRing : ∀ (R : TopCommRingCat), IsTopologicalRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Product of topological modules is commutative up to continuous linear isomorphism.  -/
ContinuousLinearEquiv.prodComm : (R₁ : Type u_1) →
  [inst : Semiring R₁] →
    (M₁ : Type u_4) →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          (M₂ : Type u_5) →
            [inst_3 : TopologicalSpace M₂] →
              [inst_4 : AddCommMonoid M₂] → [inst_5 : Module R₁ M₁] → [inst_6 : Module R₁ M₂] → (M₁ × M₂) ≃L[R₁] M₂ × M₁
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.maximal_normal_addSubgroupOf_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  Maximal (fun x => (H.addSubgroupOf x).Normal) (AddSubgroup.normalizer ↑H)
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_map_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M) (S' : Submodule R M₂),
  Submodule.map (f.coprod g) (S.prod S') = Submodule.map f S ⊔ Submodule.map g S'
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_inv_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor x).inv.hom = (CategoryTheory.Bicategory.leftUnitor x.hom).inv
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (M : Subsemigroup R),
  M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure ↑M
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : α → β), N.comapOn (f ⁻¹' N.E) f = N.comap f
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk'_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0)
  (n : ℕ),
  (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d (n + 2) (n + 1) =
    CategoryTheory.CategoryStruct.comp (ChainComplex.mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} => succ') n).hom
      (succ' ((ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d (n + 1) n)).snd.fst
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If a measure `μ` is
left-invariant and satisfies the right scaling condition, then it satisfies
`AddQuotientMeasureEqMeasurePreimage`.  -/
MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsAddLeftInvariant] [Countable ↥Γ] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsAddLeftInvariant]
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure μ]
  [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.addCovolume (↥Γ.op) G ν = μ Set.univ → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
-- Lean.Elab.Do.Legacy
/-- We use `MProd` instead of `Prod` to group values when expanding the
`do` notation. `MProd` is a universe monomorphic product.
The motivation is to generate simpler universe constraints in code
that was not written by the user.
Note that we are not restricting the macro power since the
`Bind.bind` combinator already forces values computed by monadic
actions to be in the same universe.
 -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.mkTuple : Array Lean.Syntax → Lean.MacroM Lean.Syntax
-- Lean.Parser.Extra
Lean.Parser.withForbidden.formatter : Lean.Parser.Token → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.Pos.revSkipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.GroupTheory.Congruence.Basic
/-- The product of an indexed collection of additive congruence relations.  -/
AddCon.pi : {ι : Type u_4} → {f : ι → Type u_5} → [inst : (i : ι) → Add (f i)] → ((i : ι) → AddCon (f i)) → AddCon ((i : ι) → f i)
-- Mathlib.Algebra.Ring.Equiv
/-- A ring isomorphism preserves multiplication.  -/
RingEquiv.map_mul : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (x y : R), e (x * y) = e x * e y
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of
the image `ι '' U` in the glued space is the limit of this diagram.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [CategoryTheory.Limits.HasLimits C] →
        {i : D.J} →
          TopologicalSpace.Opens ↑↑(D.U i) →
            CategoryTheory.Functor
              (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J))ᵒᵖ C
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.ΓIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv =
    AlgebraicGeometry.Scheme.Hom.appLE f (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U)
      ((TopologicalSpace.Opens.map f.base).obj U) ⋯
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.mul_toFun : ∀ {m1 m2 : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length m1 = List.length m2 → (m1.mul m2).toFun basis =ᶠ[Filter.atTop] m1.toFun basis * m2.toFun basis
-- Mathlib.Algebra.Group.AddChar
AddChar.eq_zero_iff : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {ψ : AddChar A M}, ψ = 0 ↔ ∀ (x : A), ψ x = 1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coe_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f g : AddMonoidAlgebra R M), ⇑(f + g).coeff = ⇑f.coeff + ⇑g.coeff
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {fallback : β k} {f : β k → β k}, (t.modify k f).getD k fallback = (Option.map f (t.get? k)).getD fallback
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.infinite_of_nonempty : ∀ (σ : Type u_2) (R : Type u_3) [Nonempty σ] [inst : CommSemiring R] [Nontrivial R], Infinite (MvPolynomial σ R)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves colimits and `G` reflects colimits, then `F` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
  [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.priorities : Lean.Meta.DefaultInstances → Lean.Meta.PrioritySet
-- Std.Internal.Do.Order.Basic
Lean.Order.top_le_prop : ∀ (x : Prop), x → Lean.Order.PartialOrder.rel Lean.Order.top x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_lid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 𝕜 E), ‖(TensorProduct.lid 𝕜 E) x‖₊ = ‖x‖₊
-- Init.Data.Rat.Lemmas
Rat.ofInt_den : ∀ {n : ℤ}, (Rat.ofInt n).den = 1
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.integral_comp_polarCoord_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℂ → E),
  ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p
-- Mathlib.GroupTheory.Nilpotent
/-- A sequence of subgroups of `G` is an ascending central series if `H 0` is trivial and
`⁅H (n + 1), G⁆ ⊆ H n` for all `n`. Note that we do not require that `H n = G` for some `n`.  -/
Subgroup.IsAscendingCentralSeries : {G : Type u_1} → [inst : Group G] → (ℕ → Subgroup G) → Prop