mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- In a bialgebra, `1` is a group-like element.  -/
IsGroupLikeElem.one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  IsGroupLikeElem R 1
-- Mathlib.Data.PNat.Basic
PNat.div_add_mod : ∀ (m k : ℕ+), ↑k * m.div k + ↑(m.mod k) = ↑m
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α), μ (c +ᵥ s) = μ s
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Identify the stalk at a point of the sheaf-of-commutative-rings of functions from `M` to `R`
(for `R` a smooth ring) with the stalk at that point of the corresponding sheaf of types.  -/
smoothSheafCommRing.forgetStalk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [inst_12 : ContMDiffRing I (↑⊤) R] →
                                            (x : ↑(TopCat.of M)) →
                                              ↑((smoothSheafCommRing IM I M R).presheaf.stalk x) ≅
                                                (smoothSheaf IM I M R).presheaf.stalk x
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.apply_mem_spectrum : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : Algebra 𝕜 A] [Nontrivial 𝕜] (φ : ↑(WeakDual.characterSpace 𝕜 A)) (a : A), φ a ∈ spectrum 𝕜 a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_rcc_eq : ∀ {m n i : ℕ}, ((m...=n).toList[i]?.isSome = true) = (i < n + 1 - m)
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.size_eq_length_iter : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {s : Std.Slice γ}
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.size = (Std.Slice.Internal.iter s).length
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_mul : ∀ (x y : GaussianInt), GaussianInt.toComplex (x * y) = GaussianInt.toComplex x * GaussianInt.toComplex y
-- Mathlib.Order.Interval.Set.OrderIso
/-- Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element  -/
OrderIso.IciBot : {α : Type u_1} → [inst : Preorder α] → [inst_1 : OrderBot α] → ↑(Set.Ici ⊥) ≃o α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) s.fst = f
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂_isPartialInv : ∀ {α : Type u_1} [inst : Encodable α], Function.IsPartialInv Encodable.encode (Encodable.decode₂ α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α} {fallback : β}
  {h : a ∈ t}, t[a] = t.getD a fallback
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.of_counit : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : Coalgebra R X], CoalgebraStruct.counit = CoalgebraStruct.counit
-- Mathlib.Data.Finset.Sort
/-- Two parametrizations `orderEmbOfFin` of the same set take the same value on `i` and `j` if
and only if `i = j`. Since they can be defined on a priori not defeq types `Fin k` and `Fin l`
(although necessarily `k = l`), the conclusion is rather written `(i : ℕ) = (j : ℕ)`.  -/
Finset.orderEmbOfFin_eq_orderEmbOfFin_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {k l : ℕ} {s : Finset α} {i : Fin k} {j : Fin l} {h : s.card = k}
  {h' : s.card = l}, (s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.mem_toModuleCatObj : ∀ {R : Type u} {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module (Matrix ι ι R) M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R (Matrix ι ι R) M] (i : ι) {x : M},
  x ∈ MatrixModCat.toModuleCatObj R M i ↔ ∃ y, Matrix.single i i 1 • y = x
-- Mathlib.Data.Finset.Prod
Finset.offDiag_singleton : ∀ {α : Type u_1} (a : α), {a}.offDiag = ∅
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.rat_sub : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (r : ℚ), LiouvilleWith p (↑r - x)
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ` into a limit for `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.isLimitOfCoconeOfConeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F.unop} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c) → CategoryTheory.Limits.IsLimit c
-- Mathlib.Topology.Constructions
Topology.IsInducing.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {e : X → Y},
  Topology.IsInducing e → ∀ {s : Set Y} (hs : ∀ (x : X), e x ∈ s), Topology.IsInducing (Set.codRestrict e s hs)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
strictAnti_mul_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a : R}, a < 0 → StrictAnti fun x => x * a
-- Mathlib.Topology.Algebra.Algebra
Submodule.range_valA : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (p : Subalgebra R A), (↑p.valA).range = p
-- Mathlib.Logic.Equiv.Fin.Basic
Nat.divModEquiv_symm_apply : ∀ (n : ℕ) [inst : NeZero n] (p : ℕ × Fin n), n.divModEquiv.symm p = p.1 * n + ↑p.2
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Convert the heap to a list in arbitrary order.  -/
Batteries.BinomialHeap.Imp.Heap.toListUnordered : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → List α
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_of_bijective_algebraMap : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [StrongRankCondition R], Function.Bijective ⇑(algebraMap R S) → Module.finrank R S = 1
-- Init.Data.List.Lemmas
List.map_const_fun : ∀ {β : Type u_1} {α : Type u_2} {x : β}, List.map (Function.const α x) = fun x_1 => List.replicate x_1.length x
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.mk.inj : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {inst : (i : ι) → Group (G i)} {inst_1 : Group H}
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι}
  {toPair : Monoid.CoprodI.Word.Pair G i}
  {normalized : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair.tail.toList → g ∈ d.set i_1}
  {toPair_1 : Monoid.CoprodI.Word.Pair G i}
  {normalized_1 : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair_1.tail.toList → g ∈ d.set i_1},
  { toPair := toPair, normalized := normalized } = { toPair := toPair_1, normalized := normalized_1 } →
    toPair = toPair_1
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.LeftResolution X₂),
  (CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id L).f = CategoryTheory.CategoryStruct.id L.X₁
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U),
  CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) =
    CategoryTheory.SemiCartesianMonoidalCategory.toUnit X
-- Init.Data.Char.Basic
/-- Returns `true` if the character is an ASCII hexadecimal digit.

The ASCII hexadecimal digits are the following: `0123456789abcdefABCDEF`.
 -/
Char.isHexDigit : Char → Bool
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A scheme is Noetherian if and only if it is covered by finitely many affine opens whose
sections are Noetherian rings.  -/
AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top : ∀ {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} [Finite ι] {S : ι → ↑X.affineOpens},
  ⨆ i, ↑(S i) = ⊤ →
    (AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i))))
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `add_apply`. -/
MeasureTheory.VectorMeasure.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁), (Matrix.toLin v₁ v₁) 1 = LinearMap.id
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, yx)` sends the measure `μ × ν` to `ν × μ`.
This is the map `SR` in [Halmos, §59].
`S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`.  -/
MeasureTheory.measurePreserving_prod_mul_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)
-- Std.Do.PostCond
Std.Do.ExceptConds.and.eq_1 : ∀ (x_2 y_2 : Std.Do.ExceptConds Std.Do.PostShape.pure), (x_2 ∧ₑ y_2) = PUnit.unit
-- Mathlib.Data.Seq.Computation
Computation.results_thinkN_pure : ∀ {α : Type u} (a : α) (n : ℕ), ((Computation.pure a).thinkN n).Results a n
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- The range of a linear map is FG if and only if the kernel is CoFG.  -/
Submodule.range_fg_iff_ker_cofg : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N}, f.range.FG ↔ f.ker.CoFG
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F]
  (x_1 : carrier (Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx))
      ((CategoryTheory.ConcreteCategory.hom (α.c.app (Opposite.op U))) x_1)
-- Plausible.Functions
Plausible.TotalFunction.withDefault.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (a : List ((_ : α) × β)) (a_1 : β),
  sizeOf (Plausible.TotalFunction.withDefault a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Separation.Basic
instT1SpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)],
  T1Space ((i : ι) → X i)
-- Mathlib.Order.Category.BddLat
BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd : (CategoryTheory.forget₂ BddLat SemilatInfCat).comp (CategoryTheory.forget₂ SemilatInfCat PartOrd) =
  (CategoryTheory.forget₂ BddLat BddOrd).comp (CategoryTheory.forget₂ BddOrd PartOrd)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_coe_iff : ∀ {α : Type u_1} {n : ℕ} {s : ↑(Set.powersetCard α n)} {a : α}, a ∈ ↑s ↔ a ∈ s
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.coe_injective : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂], Function.Injective DFunLike.coe
-- Mathlib.RingTheory.AdjoinRoot
/-- `AdjoinRoot.map` as an `AlgEquiv`.  -/
AdjoinRoot.mapAlgEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                (f : S ≃ₐ[R] T) →
                  (p : Polynomial S) →
                    (q : Polynomial T) → Associated (Polynomial.map (↑f) p) q → AdjoinRoot p ≃ₐ[R] AdjoinRoot q
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- A category that has larger limits also has smaller limits.  -/
CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}]
  [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C], CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v, u} C
-- Mathlib.Data.Set.Prod
Set.eval_image_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι},
  i ∈ s → (s.pi t).Nonempty → Function.eval i '' s.pi t = t i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtTreeMap.unitOfList l cmp = ∅.insertManyIfNewUnit l
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.nilradical_eq_bot : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X], X.nilradical = ⊥
-- Init.Data.SInt.Lemmas
Int64.toInt32_add : ∀ (a b : Int64), (a + b).toInt32 = a.toInt32 + b.toInt32
-- Mathlib.Algebra.Star.SelfAdjoint
Commute.isStarNormal_sub : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : StarRing R] {a b : R},
  Commute a (star b) → ∀ [ha : IsStarNormal a] [hb : IsStarNormal b], IsStarNormal (a - b)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.addEquiv_symm_apply_toCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  (toCLM : E →SL[σ] F), (ContinuousLinearMapWOT.addEquiv.symm toCLM).toCLM = toCLM
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_succ : ∀ (n : ℕ), n.succ.superFactorial = (n + 1).factorial * n.superFactorial
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_or_dep : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, autoParam (X ⊆ M.E) Matroid.indep_or_dep._auto_1 → M.Indep X ∨ M.Dep X
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The dimension of the reified matrix  -/
Mathlib.Tactic.Determinant.Ctx.dimension : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → ℕ
-- Mathlib.Data.Finset.Sups
Finset.diffs_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s₁ s₂ t : Finset α},
  s₁ ⊆ s₂ → s₁.diffs t ⊆ s₂.diffs t
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a
neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
`z₀`.  -/
AnalyticAt.unique_eventuallyEq_pow_smul_nonzero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {m n : ℕ},
  (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ m • g z) →
    (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z) → m = n
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeDiff : {α : Type u} → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s \ t)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.sphere.instIsTopologicalGroup : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜], IsTopologicalGroup ↑(Metric.sphere 0 1)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- A continuous function with an explicit bound is a bounded continuous function.  -/
BoundedContinuousFunction.mkOfBound : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (f : C(α, β)) → (C : ℝ) → (∀ (x y : α), dist (f x) (f y) ≤ C) → BoundedContinuousFunction α β
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_const : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M] [Nonempty ι]
  (a : M), (Finset.univ.expect fun _i => a) = a
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modifyThe_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : PUnit.{u + 1} → σ → Pred} {epost : EPred} (f : σ → σ),
  Std.Internal.Do.wp (modifyThe σ f) post epost =
    Std.Internal.Do.wp (MonadStateOf.modifyGet fun s => (PUnit.unit, f s)) post epost
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- Elementary tensors are members of the minimal tensor product.  -/
PointedCone.tmul_mem_minTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H] {x : G}
  {y : H} {C₁ : PointedCone R G} {C₂ : PointedCone R H}, x ∈ C₁ → y ∈ C₂ → x ⊗ₜ[R] y ∈ C₁.minTensorProduct C₂
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.hom_ext : ∀ {α : Type u} {R : Type v} [inst : CommRing R] ⦃f g : FreeCommRing α →+* R⦄,
  (∀ (x : α), f (FreeCommRing.of x) = g (FreeCommRing.of x)) → f = g
-- Mathlib.Data.Set.Card
Set.le_ncard_sdiff : ∀ {α : Type u_1} (s t : Set α), autoParam s.Finite Set.le_ncard_sdiff._auto_1 → t.ncard - s.ncard ≤ (t \ s).ncard
-- Mathlib.Algebra.Polynomial.DenomsClearable
denomsClearable_of_natDegree_le : ∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ℕ)
  (a : R), bi * i b = 1 → ∀ (f : Polynomial R), f.natDegree ≤ N → DenomsClearable a b N f i
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_pi_lambda : ∀ {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (X a)]
  (f : α → (a : δ) → X a), (∀ (a : δ), Measurable fun c => f c a) → Measurable f
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.finGcdMap_div : ∀ {r : ℕ} [NeZero r] (v : Fin 2 → ℤ), EisensteinSeries.finGcdMap v = r → IsCoprime ((v / ↑r) 0) ((v / ↑r) 1)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.of_subsingleton : ∀ {𝕜 : 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} [T1Space E],
  s.Subsingleton → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The sum of a locally finite collection of sections is `C^k` iff each section is.
Version at a point within a set.  -/
ContMDiffWithinAt.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u x₀) →
      ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑' (i : ι), t i x⟩) u x₀
-- Mathlib.GroupTheory.Nilpotent
/-- If `N` is a normal subgroup of `G`, then the set `{x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ N}`
is a subgroup of `G` (because it is the preimage in `G` of the centre of the
quotient group `G/N`.)
 -/
Subgroup.upperCentralSeriesStep : {G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [N.Normal] → Subgroup G