mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.mk : ∀ {R : Type u_3} [inst : Zero R] [inst_1 : Pow R ℕ] (x : R) (n : ℕ), x ^ n = 0 → IsNilpotent x
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- `ContinuousLinearMap.prod` as a `ContinuousLinearEquiv`.  -/
ContinuousLinearMap.prodL : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        (S : Type u_5) →
          [inst : NormedField 𝕜] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : TopologicalSpace F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [ContinuousConstSMul 𝕜 F] →
                              [inst_10 : AddCommGroup G] →
                                [inst_11 : Module 𝕜 G] →
                                  [inst_12 : TopologicalSpace G] →
                                    [inst_13 : IsTopologicalAddGroup G] →
                                      [ContinuousConstSMul 𝕜 G] →
                                        [inst_15 : Module S G] →
                                          [inst_16 : SMulCommClass 𝕜 S G] →
                                            [inst_17 : ContinuousConstSMul S G] →
                                              [inst_18 : Module S F] →
                                                [inst_19 : SMulCommClass 𝕜 S F] →
                                                  [inst_20 : ContinuousConstSMul S F] →
                                                    ((E →L[𝕜] F) × (E →L[𝕜] G)) ≃L[S] E →L[𝕜] F × G
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom_strictMono : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], StrictMono ⇑(LocallyFiniteOrder.orderAddMonoidHom G)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Structure used for constructing the root nodes of the 4 discrimination trees.  -/
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees : Type
-- Mathlib.MeasureTheory.Order.UpperLower
IsUpperSet.null_frontier : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)}, IsUpperSet s → MeasureTheory.volume (frontier s) = 0
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.nat_rawCast_2 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ} [inst_1 : n.AtLeastTwo], n.rawCast = OfNat.ofNat n
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {D : Set (Set α)} {f : α → β} {g : β → γ} {D' : Set (Set β)},
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) →
    Set.MapsTo (fun x => f '' x) D D' → ScottContinuousOn D' g → ScottContinuousOn D f → ScottContinuousOn D (g ∘ f)
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- This is the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the integral of a
function `f` on `G` times the lift to `G` of a function `g` on the quotient `G ⧸ Γ` with respect
to a right-invariant measure `μ` on `G`, is equal to the integral over the quotient of the
automorphization of `f` times `g`.  -/
QuotientGroup.integral_mul_eq_integral_automorphize_mul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {K : Type u_2} [inst_8 : NormedField K]
      [inst_9 : NormedSpace ℝ K] [μ.IsMulRightInvariant] {f : G → K},
      MeasureTheory.Integrable f μ →
        ∀ {g : G ⧸ Γ → K},
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
            essSup (fun x => ‖g x‖ₑ) (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) ≠ ⊤ →
              MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f)
                  (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
                ∫ (x : G), g ↑x * f x ∂μ =
                  ∫ (x : G ⧸ Γ),
                    g x * QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
* there is `C : ℝ` such that for all `x y : G`, `|h (x * y) + h(x / y) - 2 * (h x + h y)| ≤ C`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

then the torsion subgroup of `G` is finite.
 -/
CommGroup.finite_torsion_of_descent' : ∀ {G : Type u_1} [inst : CommGroup G] {h : G → ℝ} {C : ℝ},
  (∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C) → ∀ [Northcott h], Finite ↥(CommGroup.torsion G)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.mul_left : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  (a : FreeNonUnitalNonAssocAlgebra R X) {b c : FreeNonUnitalNonAssocAlgebra R X} (a_1 : FreeLieAlgebra.Rel R X b c),
  FreeLieAlgebra.Rel.below a_1 → motive b c a_1 → FreeLieAlgebra.Rel.below ⋯
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_left_inj : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit a → (b * a = c * a ↔ b = c)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
CategoryTheory.rightDualFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.RightRigidCategory C] (X : C),
  (CategoryTheory.rightDualFunctor C).obj X = { unmop := Opposite.op Xᘁ }
-- Mathlib.Order.Partition.Finpartition
Finpartition.instSemilatticeInf : {α : Type u_1} →
  [inst : DistribLattice α] → [inst_1 : OrderBot α] → [DecidableEq α] → {a : α} → SemilatticeInf (Finpartition a)
-- Mathlib.Order.Disjoint
/-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`.  -/
IsCompl : {α : Type u_1} → [inst : PartialOrder α] → [BoundedOrder α] → α → α → Prop
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- An auxiliary isomorphism of cones used to prove that `S.asLimitConeAux` is a limit cone.  -/
LightProfinite.isoMapCone : (S : LightProfinite) → lightToProfinite.mapCone S.asLimitConeAux ≅ S.toLightDiagram.cone
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite product indexed by a list.  -/
RingCon.listProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : Monoid S] (t : RingCon S) (l : List ι) {f g : ι → S},
  (∀ i ∈ l, t (f i) (g i)) → t (List.map f l).prod (List.map g l).prod
-- Mathlib.Tactic.GRewrite.Core
/-- Version of `getRel` that also returns the expression of the relation.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.getRel' : Lean.Expr → Option (Lean.Name × Option Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.RingTheory.Finiteness.Basic
/-- A finitely-generated submodule is finite as a module.  -/
Module.Finite.of_fg : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.FG → Module.Finite R ↥N
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac_assoc : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
  {Z_1 : AlgebraicGeometry.LocallyRingedSpace} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H')
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` forms an additive
commutative monoid.  -/
AddSubmonoid.closureAddCommMonoidOfComm : (M : Type u_1) →
  [inst : AddMonoid M] → {s : Set M} → (∀ a ∈ s, ∀ b ∈ s, a + b = b + a) → AddCommMonoid ↥(AddSubmonoid.closure s)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.mk : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                (L : Type u_5) →
                  (instLieRing : LieRing L) →
                    (instLieAlgebra : LieAlgebra R L) →
                      (incl : N →ₗ⁅R⁆ L) →
                        (proj : L →ₗ⁅R⁆ M) → LieAlgebra.IsExtension incl proj → LieAlgebra.Extension R N M
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_re_lt : ∀ (a : ℝ), frontier {z | z.re < a} = {z | z.re = a}
-- Mathlib.Order.Basic
/-- **Alias** of `ne_of_lt`. -/
LT.lt.ne : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → a ≠ b
-- Mathlib.Order.Max
not_isBot : ∀ {α : Type u_1} [inst : LE α] [NoBotOrder α] (a : α), ¬IsBot a
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.snd_comp_prod : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α] [inst_1 : SMul N γ]
  [inst_2 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), (MulActionHom.snd N γ δ).comp (f.prod g) = g
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_inj : ∀ {ι : Type u_2} {β : ι → Type u_3} {x y : (i : ι) → β i}, Hamming.toHamming x = Hamming.toHamming y ↔ x = y
-- Lean.SubExpr
Lean.SubExpr.Pos.instInhabited : Inhabited Lean.SubExpr.Pos
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Scaling by `c` around `x` scales the measure by `‖c‖₊ ^ d`.  -/
MeasureTheory.hausdorffMeasure_homothety_image : ∀ {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [inst_6 : BorelSpace P] {d : ℝ},
  0 ≤ d →
    ∀ (x : P) {c : 𝕜},
      c ≠ 0 →
        ∀ (s : Set P),
          (MeasureTheory.Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) =
            ‖c‖₊ ^ d • (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.Algebra.Order.Ring.Defs
/-- A strict ordered semiring is a nontrivial semiring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone.  -/
IsStrictOrderedRing : (R : Type u_1) → [Semiring R] → [PartialOrder R] → Prop
-- Mathlib.Analysis.Analytic.Constructions
/-- Scalar multiplication of one analytic function by another.  -/
AnalyticOnNhd.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {A : Type u_7}
  [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsBoundedSMul A F] [IsScalarTower 𝕜 A F]
  {f : E → A} {g : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → AnalyticOnNhd 𝕜 (fun x => f x • g x) s
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toAddCommGroup : AddCommGroup E] →
      [toMetricSpace : MetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖-x + y‖) NormedAddCommGroup.dist_eq._autoParam → NormedAddCommGroup E
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f)
      ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)) =
    (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
-- Mathlib.Topology.Homeomorph.Quotient
/-- Quotient spaces for equal relations are homeomorphic.  -/
Homeomorph.Quot.congrRight : {X : Type u_1} →
  [inst : TopologicalSpace X] → {r r' : X → X → Prop} → (∀ (x₁ x₂ : X), r x₁ x₂ ↔ r' x₁ x₂) → Quot r ≃ₜ Quot r'
-- Mathlib.RingTheory.Nakayama
Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N : Submodule R M}, N.FG → N = I • N → I ≤ N.annihilator.jacobson → N = ⊥
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfCone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.coconeLeftOpOfCone c).pt = Opposite.unop c.pt
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology.iCocycles_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ} (f : (Fin n → G) → ↑A)
  (h : (CategoryTheory.ConcreteCategory.hom (inhomogeneousCochains.d A n)) f = 0),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A n)) (groupCohomology.cocyclesMk f h) = f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.isAlgebraic_adjoin_pair : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L},
  IsIntegral K x → IsIntegral K y → Algebra.IsAlgebraic K ↥K⟮x, y⟯
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (d : n → R) {μ : R} (b : Module.Basis n R M) [IsDomain R],
  Module.End.maxGenEigenspace ((Matrix.toLin b b) (Matrix.diagonal d)) μ =
    Module.End.eigenspace ((Matrix.toLin b b) (Matrix.diagonal d)) μ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_add : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedAddMonoid β] (f g : α →+o β), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Topology.Algebra.Field
Nonneg.val_unitsHomeomorphPos_symm_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] [inst_4 : TopologicalSpace R] [inst_5 : ContinuousInv₀ R] (r : { r // 0 < r }),
  ↑↑((Nonneg.unitsHomeomorphPos R).symm r) = ↑r
-- Init.GrindInstances.ToInt
Lean.Grind.instLTIntIi : Lean.Grind.ToInt.LT ℤ Lean.Grind.IntInterval.ii
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.fullApproxDefEqImp : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Std.Async.Signal
/-- Child status has changed.
 -/
Std.Async.Signal.sigchld : Std.Async.Signal
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.splitter : (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingPair) →
    (Unit → motive CategoryTheory.Limits.WalkingPair.left) →
      (Unit → motive CategoryTheory.Limits.WalkingPair.right) → motive x
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Use the above equivalence to prove we have a limit.  -/
CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  [CategoryTheory.Limits.HasLimit (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)],
  CategoryTheory.Limits.HasLimit F
-- Init.Data.Sum.Lemmas
Sum.isRight_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.isRight = x.isLeft
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- If `p = ⊥`, then `M / p ≃ₗ[R] M`.  -/
Submodule.quotEquivOfEqBot : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → p = ⊥ → (M ⧸ p) ≃ₗ[R] M
-- Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
/-- The adjoint of the semisimple part of a JC decomposition lies in the subalgebra generated by
the adjoint of the sum.  -/
LieAlgebra.ad_mem_adjoin_of_isSemisimple : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [PerfectField K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {n s : Module.End K V},
  Commute n s →
    IsNilpotent n →
      s.IsSemisimple → (LieAlgebra.ad K (Module.End K V)) s ∈ K[(LieAlgebra.ad K (Module.End K V)) (n + s)]
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- The natural isomorphism exhibiting the compatibility of
`IsDenseSubsite.sheafEquiv` with sheafification.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              (A : Type u_4) →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                        [inst_6 : CategoryTheory.HasWeakSheafify K A] →
                          ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp
                              (CategoryTheory.presheafToSheaf J A) ≅
                            (CategoryTheory.presheafToSheaf K A).comp
                              (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G A).inverse
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_preimage_eq_zero_iff_of_countable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : α → β},
  s.Countable → (μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Inverse theorems that have been already asserted.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.invSet : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.PHashSet Lean.Expr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a : α} {fallback : β}, Std.DTreeMap.Raw.Const.getD t a fallback = (Std.DTreeMap.Raw.Const.get? t a).getD fallback
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_eq_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : NNReal},
  0 < r → (nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂}
  {c₁₂ : ComplexShape I₁₂} [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} {f g : (K.total c₁₂).X i₁₂ ⟶ A},
  f = g ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
      CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) f =
        CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) g
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_right_of_ge : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atBot → (∀ (x : α), g x ≤ C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra : {S : Type u_1} →
  {A : Type u_2} →
    [inst : NonUnitalCommCStarAlgebra A] →
      [inst_1 : SetLike S A] →
        [NonUnitalSubringClass S A] →
          [SMulMemClass S ℂ A] → [StarMemClass S A] → (s : S) → [h_closed : IsClosed ↑s] → NonUnitalCommCStarAlgebra ↥s
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The map from real embeddings to real infinite places as an equiv  -/
NumberField.InfinitePlace.mkReal : {K : Type u_1} → [inst : Field K] → { φ // NumberField.ComplexEmbedding.IsReal φ } ≃ { w // w.IsReal }
-- Std.Time.DateTime.WallTime
Std.Time.instDecidableEqWallTime : DecidableEq Std.Time.WallTime
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Mathlib.RingTheory.Regular.RegularSequence
LinearEquiv.isWeaklyRegular_congr' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] M₂) (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ (List.map (⇑σ) rs)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.union_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteInterface.mk.inj : ∀ {symm : Bool} {tactic : String} {replacement : Lean.Expr} {replacementString : String}
  {extraGoals : Array Lean.Widget.CodeWithInfos} {prettyLemma : Lean.Widget.CodeWithInfos} {lemmaType : Lean.Expr}
  {makesNewMVars symm_1 : Bool} {tactic_1 : String} {replacement_1 : Lean.Expr} {replacementString_1 : String}
  {extraGoals_1 : Array Lean.Widget.CodeWithInfos} {prettyLemma_1 : Lean.Widget.CodeWithInfos} {lemmaType_1 : Lean.Expr}
  {makesNewMVars_1 : Bool},
  { symm := symm, tactic := tactic, replacement := replacement, replacementString := replacementString,
        extraGoals := extraGoals, prettyLemma := prettyLemma, lemmaType := lemmaType, makesNewMVars := makesNewMVars } =
      { symm := symm_1, tactic := tactic_1, replacement := replacement_1, replacementString := replacementString_1,
        extraGoals := extraGoals_1, prettyLemma := prettyLemma_1, lemmaType := lemmaType_1,
        makesNewMVars := makesNewMVars_1 } →
    symm = symm_1 ∧
      tactic = tactic_1 ∧
        replacement = replacement_1 ∧
          replacementString = replacementString_1 ∧
            extraGoals = extraGoals_1 ∧
              prettyLemma = prettyLemma_1 ∧ lemmaType = lemmaType_1 ∧ makesNewMVars = makesNewMVars_1
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.instSubsingletonHomOfUnique : ∀ (V : Type u_2) [inst : CategoryTheory.ReflQuiver V] [Unique V] [∀ (x y : V), Subsingleton (x ⟶ y)]
  (x y : CategoryTheory.Cat.FreeRefl V), Subsingleton (x ⟶ y)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Convenience shortcut for `ModuleCat.hom_bijective.injective`.  -/
ModuleCat.hom_injective : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}, Function.Injective ModuleCat.Hom.hom
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_quotient_center`.

---

Quotienting the `center G` reduces the nilpotency class by 1.  -/
nilpotencyClass_quotient_center : ∀ {G : Type u_1} [inst : Group G], Group.nilpotencyClass (G ⧸ Subgroup.center G) = Group.nilpotencyClass G - 1