mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.right_unitality_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) h))
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert_T : ∀ {R : Type u_3} [inst : CommSemiring R] (n : ℤ),
  LaurentPolynomial.invert (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
-- Mathlib.Topology.Inseparable
SpecializingMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_re : Continuous fun q => q.re
-- Mathlib.Tactic.NormNum.BigOperators
/-- This represents the result of trying to determine whether the given expression
`s : Q(Multiset $α)` is either empty or consists of an element inserted into a strict subset.  -/
Mathlib.Meta.Multiset.ProveZeroOrConsResult : {u : Lean.Level} → {α : Q(Type u)} → Q(Multiset «$α») → Type
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_eq_fderiv : ∀ {𝕜 : 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} {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F] [T2Space F],
  UniqueDiffWithinAt 𝕜 s x → DifferentiableAt 𝕜 f x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↑S.toSubalgebra = ↑S
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_inf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f →
    ∀ (S T : AddSubsemigroup N), AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T) = S ⊓ T
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) =
          (Std.DTreeMap.Internal.Impl.contains k m₁ || Std.DTreeMap.Internal.Impl.contains k m₂)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.toNNReal : ∀ {p q r : ℝ}, p.HolderTriple q r → p.toNNReal.HolderTriple q.toNNReal r.toNNReal
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toNat = n % 2 ^ 32
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x x' y : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F x x'),
  RingCat.Colimits.Relation.below x_1 → motive x x' x_1 → RingCat.Colimits.Relation.below ⋯
-- Lean.Message
Lean.MessageDataContext.mk.injEq : ∀ (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options)
  (env_1 : Lean.Environment) (mctx_1 : Lean.MetavarContext) (lctx_1 : Lean.LocalContext) (opts_1 : Lean.Options),
  ({ env := env, mctx := mctx, lctx := lctx, opts := opts } =
      { env := env_1, mctx := mctx_1, lctx := lctx_1, opts := opts_1 }) =
    (env = env_1 ∧ mctx = mctx_1 ∧ lctx = lctx_1 ∧ opts = opts_1)
-- Mathlib.Analysis.Normed.Module.Basic
/-- A subspace of a normed space is also a normed space, with the restriction of the norm.  -/
Submodule.normedSpace : {𝕜 : Type u_6} →
  {R : Type u_7} →
    [inst : SMul 𝕜 R] →
      [inst_1 : NormedField 𝕜] →
        [inst_2 : Ring R] →
          {E : Type u_8} →
            [inst_3 : SeminormedAddCommGroup E] →
              [inst_4 : NormedSpace 𝕜 E] →
                [inst_5 : Module R E] → [IsScalarTower 𝕜 R E] → (s : Submodule R E) → NormedSpace 𝕜 ↥s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.StronglyConnectedComponent.IsSStronglyConnected.pos_cycle : ∀ {V : Type u_2} [inst : Quiver V], Quiver.IsSStronglyConnected V → ∀ (v : V), ∃ p, 0 < p.length
-- Init.Data.BitVec.Bitblast
BitVec.getElem_sub : ∀ {w i : ℕ} {x y : BitVec w} (h : i < w),
  (x - y)[i] = (x[i] ^^ ((~~~y + 1#w)[i] ^^ BitVec.carry i x (~~~y + 1#w) false))
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant], μ.AbsolutelyContinuous μ.neg
-- Mathlib.NumberTheory.NumberField.ClassNumber
_private.Mathlib.NumberTheory.NumberField.ClassNumber.0.termM_ : Lean.ParserDescr
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-closed right-unbounded.

The type of the resulting slices is `γ`.
 -/
Std.Rci.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.none : Lean.Lsp.TextDocumentSyncKind
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.localNormSimpRule.inj : ∀ {r r_1 : Aesop.LocalNormSimpRule},
  Aesop.LocalRuleSetMember.localNormSimpRule r = Aesop.LocalRuleSetMember.localNormSimpRule r_1 → r = r_1
-- Init.Data.String.Basic
/-- Returns `true` if `p` is a valid UTF-8 position in the string `s`.

This means that `p ≤ s.rawEndPos` and `p` lies on a UTF-8 character boundary. At runtime, this
operation takes constant time.

Examples:
 * `String.Pos.isValid "abc" ⟨0⟩ = true`
 * `String.Pos.isValid "abc" ⟨1⟩ = true`
 * `String.Pos.isValid "abc" ⟨3⟩ = true`
 * `String.Pos.isValid "abc" ⟨4⟩ = false`
 * `String.Pos.isValid "𝒫(A)" ⟨0⟩ = true`
 * `String.Pos.isValid "𝒫(A)" ⟨1⟩ = false`
 * `String.Pos.isValid "𝒫(A)" ⟨2⟩ = false`
 * `String.Pos.isValid "𝒫(A)" ⟨3⟩ = false`
 * `String.Pos.isValid "𝒫(A)" ⟨4⟩ = true`
 -/
String.Pos.Raw.isValid : String → String.Pos.Raw → Bool
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNatClamp_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt64 = UInt64.ofNatLT (USize.size - 1) USize.toUInt64_ofNatClamp_of_le._proof_1
-- Init.Data.SInt.Lemmas
Int64.sub_nonneg_of_le : ∀ {a b : Int64}, 0 ≤ b → b ≤ a → 0 ≤ a - b
-- Mathlib.ModelTheory.LanguageMap
/-- Adds constants to a language map.  -/
FirstOrder.Language.LHom.addConstants : {L : FirstOrder.Language} →
  (α : Type w') → {L' : FirstOrder.Language} → (L →ᴸ L') → (L.withConstants α →ᴸ L'.withConstants α)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Adding an analytic function to a meromorphic one does not change the pole divisor.  -/
MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  MeromorphicOn f₁ U → AnalyticOnNhd 𝕜 f₂ U → (MeromorphicOn.divisor (f₁ + f₂) U)⁻ = (MeromorphicOn.divisor f₁ U)⁻
-- Mathlib.Tactic.CongrExclamation
CongrMetaM : Type → Type
-- Mathlib.Data.List.GetD
List.getElem?_getD_singleton_default_eq : ∀ {α : Type u} (d : α) (n : ℕ), [d][n]?.getD d = d
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.mem_interedges_iff : ∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β}
  {x : α × β}, x ∈ Rel.interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
-- Mathlib.Algebra.Order.Group.Units
/-- The units of an ordered commutative monoid form an ordered commutative group.  -/
Units.isOrderedMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], IsOrderedMonoid αˣ
-- Init.Data.String.Defs
String.Pos.Raw.IsValidForSlice.le_rawEndPos : ∀ {s : String.Slice} {p : String.Pos.Raw}, String.Pos.Raw.IsValidForSlice s p → p ≤ s.rawEndPos
-- Init.Control.EState
EStateM.instMonadAttach : {ε σ : Type u} → MonadAttach (EStateM ε σ)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A pseudometric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
reflexivity `dist x x = 0`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

Note that we do not require `dist x y = 0 → x = y`. See metric spaces (`MetricSpace`) for the
similar class with that stronger assumption.

Any pseudometric space is a topological space and a uniform space (see `TopologicalSpace`,
`UniformSpace`), where the topology and uniformity come from the metric.
Note that a T1 pseudometric space is just a metric space.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g.
ensures that we do not get a diamond when doing
`[PseudoMetricSpace α] [PseudoMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  -/
PseudoMetricSpace : Type u → Type u
-- Init.Data.Vector.Lemmas
Vector.map_reverse : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n},
  Vector.map f xs.reverse = (Vector.map f xs).reverse
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrRight_trans : ∀ {ι : Type u_7} {R : ι → Type u_8} {S : ι → Type u_9} {T : ι → Type u_10}
  [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)]
  [inst_2 : (i : ι) → NonUnitalNonAssocSemiring (T i)] (e : (i : ι) → R i ≃+* S i) (f : (i : ι) → S i ≃+* T i),
  (RingEquiv.piCongrRight e).trans (RingEquiv.piCongrRight f) = RingEquiv.piCongrRight fun i => (e i).trans (f i)
-- Mathlib.GroupTheory.Coxeter.Basic
/-- Reindex a Coxeter system through a bijection of the indexing sets.  -/
CoxeterSystem.reindex : {B : Type u_1} →
  {B' : Type u_2} →
    {W : Type u_3} →
      [inst : Group W] →
        {M : CoxeterMatrix B} → CoxeterSystem M W → (e : B ≃ B') → CoxeterSystem (CoxeterMatrix.reindex e M) W
-- Lean.Parser.Do
Lean.Parser.Term.termUnless.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk : {α : Sort u_1} → {β : Sort u_2} → (toFun : α → β) → Function.Injective toFun → α ↪ β
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
structure from the norm properties. Note that in most cases this instance creates bad definitional
equalities (e.g., it does not take into account a possibly existing `UniformSpace` instance on
`E`).  -/
GroupNorm.toNormedGroup : {E : Type u_5} → [inst : Group E] → GroupNorm E → NormedGroup E
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_X₂ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], (K.shortComplexTruncLE e).X₂ = K
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKeyD k' fallback =
    if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Std.Http.Data.URI.Parser
/-- Parses a URI (Uniform Resource Identifier).

URI = scheme ":" hier-part [ "?" query ] [ "#" fragment ]
hier-part = "//" authority path-abempty / path-absolute / path-rootless / path-empty
 -/
Std.Http.URI.Parser.parseURI : optParam Std.Http.URI.Config { } → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instCoeSubgroup.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G],
  ClosedSubgroup.instCoeSubgroup G = { coe := ClosedSubgroup.toSubgroup }
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `polishSource s` is similar to `polishPP s`, but expects the input to be actual source code.
For this reason, `polishSource s` performs more conservative changes:
it only replace all whitespace starting from a linebreak (`\n`) with a single whitespace.  -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.polishSource : String → String × Array ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  (m₁.union m₂ ⋯ ⋯).getKey k ⋯ = m₂.getKey k mem
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rio.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.toArray = (Std.Rio.Internal.iter r).toArray
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_lt_of_le' : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulMono α β] [SMulPosStrictMono α β],
  a₁ < a₂ → b₁ ≤ b₂ → 0 ≤ a₂ → 0 < b₁ → a₁ • b₁ < a₂ • b₂
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- The presheaf of modules associated to a submodule.  -/
PresheafOfModules.Submodule.toPresheafOfModules : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → M.Submodule → PresheafOfModules R
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
stronglyMeasurable_derivWithin_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F],
  MeasureTheory.StronglyMeasurable fun x => derivWithin f (Set.Ici x) x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Grp C)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (t : P.obj (Opposite.op X)),
  x.IsAmalgamation t = ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : R f), (CategoryTheory.ConcreteCategory.hom (P.map f.op)) t = x f h
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RioSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lcurry_apply : ∀ (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] [inst_9 : AddCommMonoid N]
  [inst_10 : Module R N] [inst_11 : AddCommMonoid P] [inst_12 : Module R P] [inst_13 : Module A P]
  [inst_14 : IsScalarTower R A P] [inst_15 : Module B P] [inst_16 : IsScalarTower R B P] [inst_17 : SMulCommClass A B P]
  (f : TensorProduct R M N →ₗ[A] P),
  (TensorProduct.AlgebraTensorModule.lcurry R A B M N P) f = TensorProduct.AlgebraTensorModule.curry f
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : MulZeroClass β]
  [inst_3 : ContinuousMul β] (f g : CompactlySupportedContinuousMap α β), ⇑(f * g) = ⇑f * ⇑g
-- Init.Data.Vector.Attach
Vector.attachWith_map_subtype_val : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector α n} (H : ∀ a ∈ xs, p a),
  Vector.map Subtype.val (xs.attachWith p H) = xs
-- Mathlib.GroupTheory.Descent
/-- If `G` is an additive group and `f : G →+ G` is an endomorphism sending
subgroups into themselves, and if there is a "height function" `h : G → ℝ` with respect
to `f` and a finite subset `s` of `G`, then `G` is finitely generated.  -/
AddGroup.fg_of_descent : ∀ {G : Type u_1} [inst : AddGroup G] {f : G →+ G},
  (∀ (U : AddSubgroup G), AddSubgroup.map f U ≤ U) →
    ∀ {s : Set G} {h : G → ℝ} {a b c : ℝ},
      0 ≤ a →
        a < b →
          s.Finite →
            s + ↑f.range = Set.univ →
              (∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g + x) + c) →
                (∀ (x : G), b * h x - c ≤ h (f x)) → ∀ [Northcott h], AddGroup.FG G
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → HasFPowerSeriesWithinAt f p s x
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_some : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)]
  [inst_2 : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : Irreducible p)
  (s : Multiset { a // Irreducible a }), p.count ↑s = Multiset.count ⟨p, hp⟩ s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s : Finset α), (-s).card = s.card
-- Mathlib.Algebra.Opposites
MulOpposite.instIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsRightCancelAdd α], IsRightCancelAdd αᵐᵒᵖ
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Any finite collection of objects in a filtered category has an object "to the right".
 -/
CategoryTheory.IsFiltered.sup_objs_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C),
  ∃ S, ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Give the morphism to a terminal object from any other.  -/
CategoryTheory.Limits.IsTerminal.from : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Limits.IsTerminal X → (Y : C) → Y ⟶ X
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to `TopCat` preserves pullbacks of inclusions if they exist.  -/
CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  [CompHausLike.HasExplicitPullbacksOfInclusions P],
  CategoryTheory.PreservesPullbacksOfInclusions (CompHausLike.compHausLikeToTop P)
-- Mathlib.Topology.Algebra.FilterBasis
groupFilterBasisOfComm.eq_1 : ∀ {G : Type u_1} [inst : CommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (one : ∀ U ∈ sets, 1 ∈ U)
  (mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U) (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x => x⁻¹) ⁻¹' U),
  groupFilterBasisOfComm sets nonempty inter_sets one mul inv =
    { sets := sets, nonempty := nonempty, inter_sets := ⋯, one' := ⋯, mul' := ⋯, inv' := ⋯, conj' := ⋯ }
-- Mathlib.Algebra.Group.Prod
subAddMonoidHom.eq_1 : ∀ {α : Type u_6} [inst : SubtractionCommMonoid α],
  subAddMonoidHom = { toFun := fun a => a.1 - a.2, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Declaration
Lean.instBEqReducibilityHints : BEq Lean.ReducibilityHints
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.range_mapBaseChange : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  (KaehlerDifferential.mapBaseChange R A B).range = (KaehlerDifferential.map R A B B).ker
-- Mathlib.Order.Disjoint
/-- If `x` and `y` are to be complementary in an order, they should be codisjoint.  -/
IsCompl.codisjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Codisjoint x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A pair of morphisms `h : Y ⟶ W` and `k : Z ⟶ W` satisfying `f ≫ h = g ≫ k` induces a morphism
`l : pushout f g ⟶ W` such that `pushout.inl _ _ ≫ l = h` and `pushout.inr _ _ ≫ l = k`.  -/
CategoryTheory.Limits.pushout.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            (h : Y ⟶ W) →
              (k : Z ⟶ W) →
                CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k →
                  { l //
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l = h ∧
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l = k }
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ioi : ∀ {a : ℝ}, 0 < a → Real.log '' Set.Ioi a = Set.Ioi (Real.log a)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_apply_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIcoDiv hp a a = 0
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.eq_bot_of_comap_eq_bot : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {I : Ideal S} [inst_2 : Algebra R S]
  [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S], Ideal.comap (algebraMap R S) I = ⊥ → I = ⊥
-- Init.Data.Vector.Lemmas
Vector.map_push : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {as : Vector α n} {x : α},
  Vector.map f (as.push x) = (Vector.map f as).push (f x)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A commutative simple group is a finite group.  -/
IsSimpleGroup.finite : ∀ {α : Type u_1} [inst : CommGroup α] [IsSimpleGroup α], Finite α
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.prev_eq_self' : ∀ {ι : Type u_1} (c : ComplexShape ι) (j : ι), (∀ (k : ι), ¬c.Rel k j) → c.prev j = j
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (n : ℕ),
  HasSmallInductiveDimensionLE X n → ¬HasSmallInductiveDimensionLT X n → smallInductiveDimension X = ↑n
-- Lean.Data.Json.Stream
Lean.IO.FS.Stream.readUTF8 : IO.FS.Stream → ℕ → IO String
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.tryPostponeIfDiscrTypeIsMVar : Lean.Syntax → Lean.Elab.TermElabM Unit
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsContained.not_cliqueFree : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, (SimpleGraph.completeGraph (Fin n)).IsContained G → ¬G.CliqueFree n