mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ENat.Basic
instOrderedSubENat : OrderedSub ℕ∞
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.eval_charpoly : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), Polynomial.eval b (MulSemiringAction.charpoly G b) = 0
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerStarAlgEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : StarRing R]
  (x : TensorProduct R (Matrix m m R) (Matrix n n R)),
  (Matrix.kroneckerStarAlgEquiv m n R) x = (kroneckerLinearEquiv m m n n R) x
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrink.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F F_1 : CategoryTheory.Functor C (Type w')) (e_F : F = F_1)
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F],
  CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F = CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F_1
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mk.sizeOf_spec : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_3} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_4} [inst_4 : AddCommGroup F] [inst_5 : Module S F] [inst_6 : SizeOf R]
  [inst_7 : SizeOf S] [inst_8 : SizeOf E] [inst_9 : SizeOf F] (domain : Submodule R E) (toFun : ↥domain →ₛₗ[σ] F),
  sizeOf { domain := domain, toFun := toFun } = 1 + sizeOf domain + sizeOf toFun
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.Limits.pullback.snd S.hom T.hom)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymmPart_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.esymmPart σ R (Nat.Partition.indiscrete 0) = 1
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The functor `Spec : CommRingCatᵒᵖ ⥤ Scheme` is fully faithful.  -/
AlgebraicGeometry.Spec.fullyFaithful : AlgebraicGeometry.Scheme.Spec.FullyFaithful
-- Mathlib.Algebra.Category.Ring.Limits
/-- Construction of a limit cone in `SemiRingCat`.
(Internal use only; use the limits API.)
 -/
SemiRingCat.HasLimits.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_succ_of_not_isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α], ¬IsMax a → ¬Order.IsSuccPrelimit (Order.succ a)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Auxiliary definition for `fullsubcategory`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.mapId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) →
        [inst_1 : P.IsClosedUnderMapObj] →
          (X : B) → P.map (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (P.Obj X)
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.mk.inj : ∀ {newName? : Option Lean.Name} {text? since? : Option String} {newName?_1 : Option Lean.Name}
  {text?_1 since?_1 : Option String},
  { newName? := newName?, text? := text?, since? := since? } =
      { newName? := newName?_1, text? := text?_1, since? := since?_1 } →
    newName? = newName?_1 ∧ text? = text?_1 ∧ since? = since?_1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsLittleOIsLittleO : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      {G : Type u_5} →
        [inst : Norm E] →
          [inst_1 : Norm F] →
            [inst_2 : Norm G] →
              {l : Filter α} → Trans (fun x1 x2 => x1 =o[l] x2) (fun x1 x2 => x1 =o[l] x2) fun x1 x2 => x1 =o[l] x2
-- Mathlib.Topology.Perfect
instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T1Space α] [ConnectedSpace α] [Nontrivial α], PerfectSpace α
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- In a commutative Noetherian ring `R`, the height of a (finitely-generated) ideal is smaller
than or equal to the minimum number of generators for this ideal.  -/
Ideal.height_le_spanRank_toENat : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R),
  I ≠ ⊤ → I.height ≤ Cardinal.toENat (Submodule.spanRank I)
-- Mathlib.Algebra.Algebra.Basic
LinearMap.map_mul_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R),
  f (a * (algebraMap R A) r) = f a * (algebraMap R B) r
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cochainsMap_comp : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z),
  ContinuousCohomology.cochainsMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cochainsMap φ f) (ContinuousCohomology.cochainsMap ψ g)
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.exists_continuous_nnreal_forall_closedEBall_subset`.

---

Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ≥0)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
EMetric.exists_continuous_nnreal_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x ↑(δ x) ⊆ U i
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- If `C` holds for the `algebraMap` of `r : R` into `TensorAlgebra R M`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `TensorAlgebra R M`.
 -/
TensorAlgebra.induction : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {C : TensorAlgebra R M → Prop},
  (∀ (r : R), C ((algebraMap R (TensorAlgebra R M)) r)) →
    (∀ (x : M), C ((TensorAlgebra.ι R) x)) →
      (∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)) →
        (∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : TensorAlgebra R M), C a
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- If `f` assumes the value `1` on a compact set `K` then `rieszMeasure K ≤ Λ f`.  -/
RealRMK.rieszMeasure_le_of_eq_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X]
  {f : CompactlySupportedContinuousMap X ℝ},
  (∀ (x : X), 0 ≤ f x) →
    ∀ {K : Set X}, IsCompact K → (∀ x ∈ K, f x = 1) → (RealRMK.rieszMeasure Λ) K ≤ ENNReal.ofReal (Λ f)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_singleton_append : ∀ {m n : ℕ}, m ≤ n → (m...=n).toArray = #[m] ++ ((m + 1)...=n).toArray
-- Init.Data.SInt.Lemmas
UInt16.toInt16_ofNat' : ∀ {n : ℕ}, (UInt16.ofNat n).toInt16 = Int16.ofNat n
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_eq_zero : ∀ {n : ℕ∞}, ↑n = 0 ↔ n = 0
-- Lean.Widget.UserWidget
Lean.Widget.UserWidgetDefinition.mk.injEq : ∀ (name javascript name_1 javascript_1 : String),
  ({ name := name, javascript := javascript } = { name := name_1, javascript := javascript_1 }) =
    (name = name_1 ∧ javascript = javascript_1)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.all.eq_1 : ∀ (s : Substring.Raw) (p : Char → Bool), Substring.Raw.Legacy.all s p = !Substring.Raw.Legacy.any s fun c => !p c
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_sub : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Ring R] (v : AbsoluteValue R S)
  (x y : WithAbs v), (x - y).ofAbs = x.ofAbs - y.ofAbs
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_pi : ∀ {ι : Type u_4} [inst : Fintype ι] {α : ι → Type v} {β : ι → Type u_5} [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [inst_2 : (i : ι) → MeasurableSpace (β i)] (μ : (i : ι) → MeasureTheory.Measure (α i))
  (ν : (i : ι) → MeasureTheory.Measure (β i)) {f : (i : ι) → α i → β i}
  [hν : ∀ (i : ι), MeasureTheory.SigmaFinite (ν i)],
  (∀ (i : ι), MeasureTheory.MeasurePreserving (f i) (μ i) (ν i)) →
    MeasureTheory.MeasurePreserving (fun a i => f i (a i)) (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.pi ν)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.map Fin.castSuccEmb (Finset.Icc i j) = Finset.Icc i.castSucc j.castSucc
-- Mathlib.Condensed.Discrete.Characterization
CondensedMod.isDiscrete_iff_isDiscrete_forget : ∀ (R : Type (u + 1)) [inst : Ring R] (M : CondensedMod R),
  Condensed.IsDiscrete M ↔ Condensed.IsDiscrete ((Condensed.forget R).obj M)
-- Mathlib.Analysis.Asymptotics.Lemmas
summable_of_isBigO : ∀ {ι : Type u_1} {E : Type u_2} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ},
  Summable g → f =O[Filter.cofinite] g → Summable f
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- To construct a morphism between right extensions, we need a 2-morphism between the extensions,
and to check that it is compatible with the counits.  -/
CategoryTheory.Bicategory.RightExtension.homMk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {s t : CategoryTheory.Bicategory.RightExtension f g} →
            (η : s.extension ⟶ t.extension) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) t.counit = s.counit)
                  CategoryTheory.Bicategory.RightExtension.homMk._auto_1 →
                (s ⟶ t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.cosk_reflective : ∀ (n : ℕ), CategoryTheory.IsIso (SSet.coskAdj n).counit
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If we replace a row of a matrix by a linear combination of its rows, then the determinant is
multiplied by the coefficient of that row.  -/
Matrix.det_updateRow_sum : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (j : n) (c : n → R), (A.updateRow j (∑ k, c k • A k)).det = c j • A.det
-- Lean.Util.ParamMinimizer
/-- An expensive monotonic predicate for testing whether a given parameter
configuration works or not.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.test : {m : Type → Type} → Lean.Util.ParamMinimizer.Context✝ m → Array Bool → m Bool
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point of a site, the skyscraper sheaf functor is right adjoint
to the fiber functor on sheaves.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.Limits.HasProducts A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                Φ.sheafFiber ⊣ Φ.skyscraperSheafFunctor
-- Init.Data.List.Pairwise
List.Pairwise.pmap : ∀ {α : Type u_1} {R : α → α → Prop} {β : Type u_2} {l : List α},
  List.Pairwise R l →
    ∀ {p : α → Prop} {f : (a : α) → p a → β} (h : ∀ x ∈ l, p x) {S : β → β → Prop},
      (∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)) → List.Pairwise S (List.pmap f l h)
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousAt.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  LowerSemicontinuousAt f a → LowerSemicontinuousAt g a → LowerSemicontinuousAt (fun x => max (f x) (g x)) a
-- Init.Data.List.Monadic
List.mapM.loop.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) (x : List β),
  List.mapM.loop f [] x = pure x.reverse
-- Mathlib.Algebra.Group.Hom.Defs
MulHomClass.toMulHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F), ↑f = { toFun := ⇑f, map_mul' := ⋯ }
-- Mathlib.RingTheory.Norm.Transitivity
/-- `aux M k` is lower triangular.  -/
Algebra.Norm.Transitivity.auxMat_blockTriangular : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m),
  (Algebra.Norm.Transitivity.auxMat M k).BlockTriangular fun x => x ≠ k
-- Mathlib.Order.Basic
LE.le.ge : ∀ {α : Type u_2} [inst : LE α] {a b : α}, a ≤ b → b ≥ a
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.Etale f] {Ω : Type u} [inst : Field Ω] [IsSepClosed Ω]
  (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) (x : ↥X),
  f x = s default → ∃ l, CategoryTheory.CategoryStruct.comp l f = s ∧ l default = x
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal M` turns a homogeneously-indexed collection of matrices
`M : o → Matrix m n α'` into an `m × o`-by-`n × o` block matrix which has the entries of `M` along
the diagonal and zero elsewhere.

See also `Matrix.blockDiagonal'` if the matrices may not have the same size everywhere.
 -/
Matrix.blockDiagonal : {m : Type u_2} →
  {n : Type u_3} →
    {o : Type u_4} → {α : Type u_12} → [DecidableEq o] → [Zero α] → (o → Matrix m n α) → Matrix (m × o) (n × o) α
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.cod_le_cod : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N}, f ≤ g → f.cod ≤ g.cod
-- Mathlib.Topology.UniformSpace.Closeds
Filter.HasBasis.uniformity_compacts : ∀ {α : Type u_1} [inst : UniformSpace α] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s →
    (uniformity (TopologicalSpace.Compacts α)).HasBasis p fun i =>
      Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
-- Init.Data.OfScientific.Basic
OfScientific.mk : {α : Type u} → (ℕ → Bool → ℕ → α) → OfScientific α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_iff_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S}, f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (↑y₂ * x₁) = f (↑y₁ * x₂)
-- Mathlib.Data.Finsupp.Single
/-- `single a b` is the finitely supported function with value `b` at `a` and zero otherwise.  -/
Finsupp.single : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → α → M → α →₀ M
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.getKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.instHasProjectiveResolution : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughProjectives C] (Z : C), CategoryTheory.HasProjectiveResolution Z
-- Init.Data.Ord.Basic
Ordering.isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = !o == Ordering.eq
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₃ h₁₃.p₁ = h.p₁
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Server.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.TCP.Socket), sizeOf { native := native } = 1 + sizeOf native
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.compl : ∀ {α : Type u_1} {s : Set (Set α)} (t : Set α),
  MeasurableSpace.GenerateMeasurable s t → MeasurableSpace.GenerateMeasurable s tᶜ
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom_apply : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] (f : X →* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CommGrpCat.ofHom f)) x = f x
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params : Type
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Product of a list of elements in a subgroup is in the subgroup.  -/
Subgroup.list_prod_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {l : List G}, (∀ x ∈ l, x ∈ K) → l.prod ∈ K
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- The product of two functions of temperate growth is again of temperate growth.  -/
Function.HasTemperateGrowth.mul : ∀ {R : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing R]
  [inst_3 : NormedAlgebra ℝ R] {f g : E → R},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth (f * g)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α} {v : β}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Init.Data.SInt.Lemmas
Int64.toInt_le : ∀ (x : Int64), x.toInt ≤ Int64.maxValue.toInt
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.of_opens : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {x : M} [IsManifold I n M]
  (s : TopologicalSpace.Opens M) (hx : x ∈ s), Manifold.IsImmersionAt I I n Subtype.val ⟨x, hx⟩
-- Aesop.Forward.RuleInfo
Aesop.instInhabitedForwardRuleInfo : Inhabited Aesop.ForwardRuleInfo
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `HahnSeries.truncLT` as a linear map.  -/
HahnSeries.truncLTLinearMap : {Γ : Type u_1} →
  (R : Type u_3) →
    {V : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module R V] → [DecidableLT Γ] → Γ → HahnSeries Γ V →ₗ[R] HahnSeries Γ V
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.autMap.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f f_1 : A ⟶ B),
  f = f_1 →
    ∀ (σ σ_1 : CategoryTheory.Aut A),
      σ = σ_1 → CategoryTheory.PreGaloisCategory.autMap f σ = CategoryTheory.PreGaloisCategory.autMap f_1 σ_1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_X : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R], SkewPolynomial.X.coeff n = if 1 = n then 1 else 0
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- Auxiliary definition for `HomologicalComplex.restrictionToTruncGE'`.  -/
HomologicalComplex.restrictionToTruncGE'.f : {ι : 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.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] → (i : ι) → (K.restriction e).X i ⟶ (K.truncGE' e).X i
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- An equalizer of `f` and `g` is a kernel of `f - g`.  -/
CategoryTheory.Preadditive.isLimitKernelForkOfFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          {c : CategoryTheory.Limits.Fork f g} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.kernelForkOfFork c)
-- Mathlib.Data.TwoPointing
TwoPointing.ext : ∀ {α : Type u_3} {x y : TwoPointing α}, x.toProd.1 = y.toProd.1 → x.toProd.2 = y.toProd.2 → x = y
-- Mathlib.Topology.UniformSpace.Uniformizable
/-- Given a pair consisting of a closed set `c` contained in an open set `u`
satisfying the predicate `IsThickening`, it is always possible to refine it to two pairs
`c ⊆ v` and `closure v ⊆ u` satisfying `IsThickening`. We can then use the general `Urysohns.CU`
construction to obtain the desired real-valued function.  -/
_private.Mathlib.Topology.UniformSpace.Uniformizable.0.urysohns_main : ∀ {X : Type u_1} [inst : UniformSpace X] {c u : Set X},
  IsThickening✝ c u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ IsThickening✝ c v ∧ IsThickening✝ (closure v) u
-- Init.Core
iff_false_intro : ∀ {a : Prop}, ¬a → (a ↔ False)
-- Mathlib.Order.WellFoundedSet
Finset.isWF_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (s : Finset ι) {f : ι → Set α}, (s.sup f).IsWF ↔ ∀ i ∈ s, (f i).IsWF
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_descCochain_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n)
  (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      ((CochainComplex.mappingCocone.descCochain φ α β h).v q r hr) =
    β.v p r ⋯
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.vadd_stabilizer_of_no_doubling_aux : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A + A).card ≤ A.card →
    a ∈ A → a +ᵥ ↑(AddAction.stabilizer G A) = ↑A ∧ AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G A) = ↑A