mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Basic
OrderHom.const_coe_coe : ∀ (α : Type u_6) [inst : Preorder α] {β : Type u_7} [inst_1 : Preorder β] (b : β),
  ⇑((OrderHom.const α) b) = Function.const α b
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `RingHom` on the LHS.  -/
Matrix.mvPolynomialX_mapMatrix_eval : ∀ {m : Type u_1} {R : Type u_3} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  (A : Matrix m m R), (MvPolynomial.eval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_iff_toBitVec : ∀ {b : UInt8}, ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = false ↔ BitVec.extractLsb' 6 2 b.toBitVec = 2#2
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- Adic completion preserves surjectivity  -/
AdicCompletion.map_surjective : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑f → Function.Surjective ⇑(AdicCompletion.map I f)
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Millisecond.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subMilliseconds : Std.Time.WallTime → Std.Time.Millisecond.Offset → Std.Time.WallTime
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mono₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₂ = 0 → CategoryTheory.Mono T.mor₃
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A commuting square induces a morphism of cokernels.  -/
CategoryTheory.Limits.cokernel.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {X' Y' : C} →
              (f' : X' ⟶ Y') →
                [inst_3 : CategoryTheory.Limits.HasCokernel f'] →
                  (p : X ⟶ X') →
                    (q : Y ⟶ Y') →
                      CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
                        (CategoryTheory.Limits.cokernel f ⟶ CategoryTheory.Limits.cokernel f')
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `WallTime` to a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.ofWallTime : Std.Time.WallTime → Std.Time.PlainDateTime
-- Std.Http.Test.Helpers
/-- GET with `Connection: close`.
 -/
Std.Http.Internal.Test.mkGetClose : optParam String "/" → String
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.source_subset_preimage_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.domChart.source ⊆ f ⁻¹' h.codChart.source
-- Mathlib.Algebra.GradedMonoid
/-- A default implementation of power on a graded monoid, like `npowRec`.
`GMonoid.gnpow` should be used instead.  -/
GradedMonoid.GMonoid.gnpowRec : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] → [GradedMonoid.GMul A] → [GradedMonoid.GOne A] → (n : ℕ) → {i : ι} → A i → A (n • i)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.π f b) =
    CategoryTheory.CategoryStruct.id (f b)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- If `C` has coequalizers, then it has reflexive coequalizers.  -/
CategoryTheory.Limits.hasReflexiveCoequalizers_of_hasCoequalizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoequalizers C],
  CategoryTheory.Limits.HasReflexiveCoequalizers C
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.let.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl decl_1 : Lean.Compiler.LCNF.LetDecl pu),
  (Lean.Compiler.LCNF.CodeDecl.let decl = Lean.Compiler.LCNF.CodeDecl.let decl_1) = (decl = decl_1)
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Server.ModuleImport.collapseIdenticalImports?.collapseMetaKinds : Lean.Lsp.LeanImportMetaKind → Lean.Lsp.LeanImportMetaKind → Lean.Lsp.LeanImportMetaKind
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.mul p₂) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Lean.Message
/-- If `true`, filter this message from non-language server output.
In the language server, silent messages are served as silent diagnostics.
See also `DiagnosticWith.isSilent?`.
 -/
Lean.BaseMessage.isSilent : {α : Type u} → Lean.BaseMessage α → Bool
-- Lean.Elab.Syntax
/-- (Try to) add a term info for the category `catName` at `ref`.  -/
Lean.Elab.Term.addCategoryInfo : Lean.Syntax → Lean.Name → Lean.Elab.TermElabM Unit
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent.inj : ∀ {x : Lean.Grind.AC.Var} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {x_1 : Lean.Grind.AC.Var}
  {c₁_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x_1 c₁_1 →
    x = x_1 ∧ c₁ = c₁_1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instIsBoundedSMul_1 : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : SeminormedAddCommGroup β] [inst_3 : NormedSpace 𝕜 β],
  IsBoundedSMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)
-- Mathlib.FieldTheory.SeparableDegree
/-- **Alias** of `Irreducible.natSepDegree_eq_one_iff_of_monic`.

---

A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `X ^ (q ^ n) - C y`
for some `n : ℕ` and `y : F`.  -/
Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic → Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = Polynomial.X ^ q ^ n - Polynomial.C y)
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.getUnusedLevelParam : Lean.CollectLevelParams.State → optParam Lean.Name `v → Lean.Level
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- `ContinuousAlgEquiv R A B`, with notation `A ≃A[R] B`, is the type of bijections
between the topological `R`-algebras `A` and `B` which are both homeomorphisms
and `R`-algebra isomorphisms.
 -/
ContinuousAlgEquiv : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [TopologicalSpace A] →
            [inst_3 : Semiring B] → [TopologicalSpace B] → [Algebra R A] → [Algebra R B] → Type (max u_2 u_3)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_right_mono : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] (n : ℕ),
  Monotone fun a => n • a
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.not_nonempty_iff_eq_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), ¬P.Nonempty ↔ P = ⊥
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight.eq_2 : ∀ (x n : ℕ), (Int.negSucc n).shiftRight x = Int.negSucc (n >>> x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM f init t = List.foldrM (fun a b => f a.fst a.snd b) init t.toList
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearMap.ker_ne_bot_of_finrank_lt : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂},
  Module.finrank K V₂ < Module.finrank K V → f.ker ≠ ⊥
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_of_subsingleton : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)], p.inertiaDeg' P = 0
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.δ_algSpec_left : ∀ {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ),
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.algSpec R) X Y) =
    (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).inv
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.comap f ⊤ = ⊤
-- Mathlib.Order.SupIndep
Finset.supIndep_product_iff : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α]
  {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α},
  (s.product t).SupIndep f ↔
    (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.mapHomologicalComplexXIso'.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n m m_1 : ℤ)
  (e_m : m = m_1) (hnm : n + 1 = m),
  CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm =
    CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m_1 ⋯
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.abs_logHeight_sym2_sub_le : ∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 →
          |Height.logHeight ![a * c, a * d + b * c, b * d] - (Height.logHeight ![a, b] + Height.logHeight ![c, d])| ≤ C
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_pure : ∀ {m : Type w → Type w'} {α : Type u} [inst : Monad m] [LawfulMonad m] {x : α},
  (Std.Iterators.HetT.pure x).Property = fun x_1 => x = x_1
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_finsetSum : ∀ {R : Type u} {S : Type v} {ι : Type y} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (s : Finset ι)
  (g : ι → Polynomial R) (x : S), Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval₂ f x (g i)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} (ε ε_1 : F ⟶ G) (e_ε : ε = ε_1) (hε : CategoryTheory.CategoryStruct.comp ε μ = η),
  CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε =
    CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε_1 ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insertIfNew_le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t.isEmpty = false}, (cmp ((t.insertIfNew k v).minKey ⋯) (t.minKey he)).isLE = true
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.FinCategory.fintypeObj : {J : Type v} → {inst : CategoryTheory.SmallCategory J} → [self : CategoryTheory.FinCategory J] → Fintype J
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.map_eq : ∀ {n : ℕ} (P : MvPFunctor.{u} n) {α β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f : (P.B a).Arrow α),
  MvFunctor.map g ⟨a, f⟩ = ⟨a, TypeVec.comp g f⟩
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.insertMin.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hr : t.Balanced),
      Std.DTreeMap.Internal.Impl.insertMin k v t hr = Std.DTreeMap.Internal.Impl.insertMin k v_1 t hr
-- Mathlib.CategoryTheory.Linear.Yoneda
/-- The Yoneda embedding for `R`-linear categories `C`
sending an object `X : C` to the `ModuleCat R`-valued presheaf on `C`,
with value on `Y : Cᵒᵖ` given by `ModuleCat.of R (unop Y ⟶ X)`.  -/
CategoryTheory.linearYoneda : (R : Type w) →
  [inst : Ring R] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (ModuleCat R))
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_uIoo : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.uIoo i j = Set.uIoo (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective : ∀ {R : Type u} [inst : CommRing R],
  Function.Bijective ⇑(algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op ⊤)))
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  Submodule.Quotient.mk 0 = 0
-- Lean.CoreM
/-- Return true if `ex` was generated by `throwMaxHeartbeat`.
This function is a bit hackish. The heartbeat exception should probably be an internal exception.
We used a similar hack at `Exception.isMaxRecDepth`  -/
Lean.Exception.isMaxHeartbeat : Lean.Exception → Bool
-- Std.Time.Format
/-- Parses a string into a `TimeZone` object. The input string must be in the format `"VV ZZZZZ"`.
 -/
Std.Time.TimeZone.fromTimeZone : String → Except String Std.Time.TimeZone
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Build a `LinearEquiv` from an isomorphism in the category `ModuleCat R`.  -/
CategoryTheory.Iso.toLinearEquiv : {R : Type u} → [inst : Ring R] → {X Y : ModuleCat R} → (X ≅ Y) → ↑X ≃ₗ[R] ↑Y
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
ExteriorAlgebra.GradedAlgebra.liftι_eq : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ)
  (x : ↥(⋀[R]^i M)), (ExteriorAlgebra.GradedAlgebra.liftι R M) ↑x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceMul : Lean.Meta.Simp.DSimproc
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.type : Lean.Lsp.SemanticTokenType
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.exp : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.exp (f x)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.symmetryEquiv_apply_coe : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (j : I₁₂) (x : ↑(c₂.π c₁ c₁₂ ⁻¹' {j})),
  ↑((c₁.symmetryEquiv c₂ c₁₂ j) x) = (x.1.2, x.1.1)
-- Mathlib.Topology.Instances.Nat
Nat.instDist : Dist ℕ
-- Mathlib.Data.Set.Defs
Set.instLawfulFunctor : LawfulFunctor Set
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.map : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] {f : G →+ H},
  Function.Surjective ⇑f →
    ∀ (n : ℕ), AddSubgroup.map f (AddSubgroup.upperCentralSeries G n) ≤ AddSubgroup.upperCentralSeries H n
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.exists_generator_lt_one' : ∀ {Γ : Type u_1} {inst : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst_1 : Ring A} {v : Valuation A Γ}
  [self : v.IsRankOneDiscrete], ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_of_le_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {K L : Subgroup G},
  K ≤ L → ∀ [H.IsFiniteRelIndex L], H.IsFiniteRelIndex K
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_sub : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddGroup (f i)] (i : I) (x y : f i),
  Pi.single i (x - y) = Pi.single i x - Pi.single i y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.mk : {α : Type u} → [inst : Lean.Grind.Semiring α] → α × α → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Algebra.Ring.CharZero
Nat.castEmbedding_apply : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (a : ℕ), Nat.castEmbedding a = ↑a
-- Init.Grind.AC
Lean.Grind.AC.refl : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx s = Lean.Grind.AC.Seq.denote ctx s
-- Lean.Environment
Lean.ConstantKind : Type
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_re_symm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), RCLike.re (inner 𝕜 x y) = RCLike.re (inner 𝕜 y x)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsQuasicoherentObjIsQuasicoherent : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
  (M : (SheafOfModules.isQuasicoherent R).FullSubcategory), M.obj.IsQuasicoherent
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_obj_as : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c), ((HomotopyCategory.quotient V c).obj C).as = C
-- Mathlib.Order.Ideal
/-- The infimum of two ideals of a co-directed order is their intersection.  -/
Order.Ideal.instMin : {P : Type u_1} → [inst : SemilatticeSup P] → [IsCodirectedOrder P] → Min (Order.Ideal P)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.mk : {γ : Type} →
  Lean.Name →
    Lean.Name →
      String →
        Lean.Name →
          (Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) →
            (Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit) → Lean.KeyedDeclsAttribute.Def γ
-- Mathlib.Data.Fintype.Basic
Fin.univ_map_def : ∀ {α : Type u_1} {n : ℕ} (f : Fin n ↪ α), Finset.map f Finset.univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }
-- Init.Data.Array.MinMax
Array.max?_singleton_append' : ∀ {α : Type u_1} {x : α} [inst : Max α] {xs : Array α}, (#[x] ++ xs).max? = some (Array.foldl max x xs)
-- Mathlib.Data.PNat.Xgcd
/-- `gcdD a b = gcd a b`  -/
PNat.gcdD : ℕ+ → ℕ+ → ℕ+
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.Map : ShareCommon.StateFactoryImpl → Type
-- Mathlib.Data.Finset.Density
Finset.dens_sdiff_add_dens_inter : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s \ t).dens + (s ∩ t).dens = s.dens
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {r : R},
  (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : G →₀ k},
  { coeff := a + b } = { coeff := a } + { coeff := b }
-- Mathlib.Analysis.Seminorm
Seminorm.continuous_iff : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  0 < r → (Continuous ⇑p ↔ p.ball 0 r ∈ nhds 0)
-- Init.Meta.Defs
/-- If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
the `approxDefEq` combinator.
 -/
Lean.Meta.ApplyConfig.approx : Lean.Meta.ApplyConfig → Bool
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsWeaklyRegular.of_isLocalizedModule : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  [inst_7 : Module S N] [IsScalarTower R S N] (T : Submonoid R) [IsLocalization T S] (f : M →ₗ[R] N)
  [IsLocalizedModule T f] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs → RingTheory.Sequence.IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_flatMap_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)} {a : α},
  (∀ (i : ℕ) (h : i < l.length), Std.Internal.List.containsKey a (f l[i]) = false) →
    Std.Internal.List.containsKey a (List.flatMap f l) = false
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_add_lt_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightMono α] {a b c d : α}, a + b < c → d ≤ a → d + b < c
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sSup s = 0` when `s` is a set of reals that's unbounded above, it suffices to show that `s`
contains a nonnegative element to show that `0 ≤ sSup s`.  -/
Real.sSup_nonneg' : ∀ {s : Set ℝ}, (∃ x ∈ s, 0 ≤ x) → 0 ≤ sSup s
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.bmod.inj : ∀ {m : ℕ} {r : ℤ} {i : ℕ} {x : Lean.Omega.Coeffs}
  {j j_1 : Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.exact r) x},
  Lean.Elab.Tactic.Omega.Justification.bmod m r i j = Lean.Elab.Tactic.Omega.Justification.bmod m r i j_1 → j = j_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.ext_iff : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {x y : CategoryTheory.Arrow.RightHomotopy f g}, x = y ↔ x.hom = y.hom