mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Free
FreeSemigroup.mk : {α : Type u} → α → List α → FreeSemigroup α
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The counit map of `nerveAdjunction` is an isomorphism since the nerve functor is fully
faithful.  -/
CategoryTheory.nerveFunctorCompHoFunctorIso : CategoryTheory.nerveFunctor.comp SSet.hoFunctor ≅ CategoryTheory.Functor.id CategoryTheory.Cat
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_smul : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α), ⇑(c • μ) = c • ⇑μ
-- Std.Http.Protocol.H1.Parser
/-- Repeatedly applies `parser` until it returns `none` or the `maxCount` limit is
exceeded. Returns the collected results as an array.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.manyItems : {α : Type} → Std.Internal.Parsec.ByteArray.Parser (Option α) → ℕ → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap (φ + φ') =
    CategoryTheory.ShortComplex.cyclesMap φ + CategoryTheory.ShortComplex.cyclesMap φ'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k a : α} {v : β k}, (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Mathlib.NumberTheory.Divisors
Int.image_snd_divisorsAntidiag : ∀ {z : ℤ}, Finset.image Prod.snd z.divisorsAntidiag = z.divisors
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.contained_C1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.contained
    (Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o) o
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt64
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.norm_def : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (x : TrivSqZeroExt R M),
  ‖x‖ = ‖x.fst‖ + ‖x.snd‖
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.mulSupport_fun_pow_count_subset : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : CommMonoid M] (s : Multiset α) (f : α → M),
  (Function.mulSupport fun a => f a ^ Multiset.count a s) ⊆ ↑s.toFinset
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.sSup_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : Set (CategoryTheory.SubmonoidFunctor M)) (x : C), (sSup S).obj x = ⨆ F ∈ S, F.obj x
-- Lean.Meta.Sym.SymM
/-- Converts nested `Expr.proj`s into projection applications if possible.
The structural simplifier and pattern matcher do not handle kernel projection
terms; this preprocessing step folds them into projection function applications.
 -/
Lean.Meta.Sym.foldProjs : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.counit = e.counitIso.hom
-- Mathlib.Control.Basic
/-- Returns `pure true` if the computation succeeds and `pure false` otherwise.  -/
succeeds : {F : Type → Type v} → [Alternative F] → {α : Type} → F α → F Bool
-- Mathlib.Data.NNRat.Defs
NNRat.natAbs_num_coe : ∀ {q : ℚ≥0}, (↑q).num.natAbs = q.num
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.of_isNormal : ∀ {f : Ordinal.{u} → Ordinal.{u}},
  Order.IsNormal f →
    ∀ {a o : Ordinal.{u}},
      Order.IsSuccLimit a →
        ∀ {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}},
          a.IsFundamentalSequence o g → (f a).IsFundamentalSequence o fun b hb => f (g b hb)
-- Init.Data.List.Perm
List.Perm.drop : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {i : ℕ}, (List.take i l₁).Perm (List.take i l₂) → (List.drop i l₁).Perm (List.drop i l₂)
-- Mathlib.Algebra.NeZero
one_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [NeZero 1], 1 ≠ 0
-- Init.Data.Vector.Count
Vector.countP_reverse : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : Vector α n}, Vector.countP p xs.reverse = Vector.countP p xs
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_nsmul : ∀ {R : Type u} [inst : AddMonoid R] (x : R) (n : ℕ), Tropical.trop (n • x) = Tropical.trop x ^ n
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhds' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    Filter.map (↑(extChartAt I x)) (nhds y) = nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- An inequality constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Linear.IneqCnstr : Type
-- Mathlib.Topology.MetricSpace.Polish
/-- Given a closed set `s` in a Polish space, one can construct a finer Polish topology for
which `s` is both open and closed.  -/
IsClosed.isClopenable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {s : Set α}, IsClosed s → PolishSpace.IsClopenable s
-- Init.Data.UInt.Lemmas
UInt64.toFin_val : ∀ (x : UInt64), ↑x.toFin = x.toNat
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrp_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X Y : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H]
  (α : CategoryTheory.yonedaGrpObj G ⟶ CategoryTheory.yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredAsSmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C],
  CategoryTheory.IsCofiltered (CategoryTheory.AsSmall C)
-- Mathlib.Data.UInt
UInt64.toBitVec_zsmul : ∀ (z : ℤ) (a : UInt64), (z • a).toBitVec = z • a.toBitVec
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_eq_fourier_neg : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E) (w : V), FourierTransformInv.fourierInv f w = FourierTransform.fourier f (-w)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationAdjunction_counit_app_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Sheaf J D),
  ((CategoryTheory.sheafificationAdjunction J D).counit.app P).hom =
    CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P.obj) ⋯
-- Lean.Parser.Basic
/-- Information about the state of the parse prior to the failing parser's execution  -/
Lean.Parser.RecoveryContext : Type
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.left_inv : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} {inst : DecidableEq ι} {inst_1 : AddCommMonoid M} {inst_2 : SetLike σ M}
  {inst_3 : AddSubmonoidClass σ M} {ℳ : ι → σ} [self : DirectSum.Decomposition ℳ],
  Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'
-- Std.Time.Date.PlainDate
/-- Determines the era of the given `PlainDate` based on its year.
 -/
Std.Time.PlainDate.era : Std.Time.PlainDate → Std.Time.Year.Era
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.pow` -/
Function.HasTemperateGrowth.fun_pow : ∀ {R : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing R]
  [inst_3 : NormedAlgebra ℝ R] {f : E → R},
  Function.HasTemperateGrowth f → ∀ (k : ℕ), Function.HasTemperateGrowth fun i => f i ^ k
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsClosedUnderSubobjects
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- Classical **local contractibility**: for every point and every neighborhood U,
there exists a neighborhood V ⊆ U such that the inclusion V ↪ U is null-homotopic.

This is weaker than `StronglyLocallyContractibleSpace`.  -/
LocallyContractibleSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Mathlib.Data.NNReal.Basic
NNReal.coe_multiset_sum : ∀ (s : Multiset NNReal), ↑s.sum = (Multiset.map NNReal.toReal s).sum
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_head_smul_equivPair_tail : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (w : Monoid.CoprodI.Word M),
  Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head • ((Monoid.CoprodI.Word.equivPair i) w).tail = w
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitRight.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M],
  TensorProduct.directLimitRight f M =
    ((TensorProduct.comm R M (Module.DirectLimit G f)).trans (TensorProduct.directLimitLeft f M)).trans
      (Module.DirectLimit.congr (fun x => TensorProduct.comm R (G x) M) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer built from `equalizer.ι f g` is limiting.  -/
CategoryTheory.Limits.equalizerIsEqualizer : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasEqualizer f g] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.equalizer.ι f g) ⋯)
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
/-- A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with `SecondCountableTopology E`
is inner regular for finite measure sets with respect to compact sets.
 -/
MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α),
  μ.InnerRegularCompactLTTop
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_mul_of_dvd_right : ∀ {a b c : ℤ}, a ∣ c → a ∣ b * c
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverXBind : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        [inst_2 : P.IsStableUnderComposition] →
          {X : AlgebraicGeometry.Scheme} →
            (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
              (𝒱 : (x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) (𝒰.X x)) →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [(x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover.Over S (𝒱 x)] →
                      (j : (CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀) →
                        ((CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).X j).Over S
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instIdentities : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.identities C).IsMultiplicative
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity ((k, v) :: tl)) =
    ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany (Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v) tl)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.tactic.injEq : ∀ (stx stx_1 : Lean.Syntax),
  (Lean.Elab.CompletionInfo.tactic stx = Lean.Elab.CompletionInfo.tactic stx_1) = (stx = stx_1)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_sdiff_one : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure (s \ {1}) = Subgroup.closure s
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₄ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp self.m₃ v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mk.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v v_1 : ι → M} (e_v : v = v_1) (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)),
  Module.Basis.mk hli hsp = Module.Basis.mk ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.subsingleton_connectedComponent : ∀ {V : Type u} {G : SimpleGraph V}, G.Preconnected → Subsingleton G.ConnectedComponent
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_radius_top_of_neg_nat₃ : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] (a b : 𝕂)
  {k : ℕ}, (ordinaryHypergeometricSeries 𝔸 a b (-↑k)).radius = ⊤
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.inj_injective_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) (i : C),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (c.inj i))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose.sizeOf_spec : ∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂ : ℤ)
  (m₂ : Lean.Grind.CommRing.Mon) (c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose k₁ m₁ c₁ k₂ m₂ c₂) =
    1 + sizeOf k₁ + sizeOf m₁ + sizeOf c₁ + sizeOf k₂ + sizeOf m₂ + sizeOf c₂
-- Mathlib.Algebra.Field.Defs
Semifield.toDiv : {K : Type u_2} → [self : Semifield K] → Div K
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instEpiModuleCatH1π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupCohomology.H1π A)
-- Batteries.Data.UInt
UInt8.toUInt16_toNat : ∀ (x : UInt8), x.toUInt16.toNat = x.toNat
-- Mathlib.CategoryTheory.Presentable.Directed
/-- the objects in the diagram  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ → CategoryTheory.ObjectProperty J
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.t p₂ = CategoryTheory.CategoryStruct.comp self.c.snd p₂
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ιMapBifunctorMapObj.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂)
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (i : I) (j : J) (k : K)
  (h : p (i, j) = k),
  CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k h =
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k h
-- Mathlib.Topology.Irreducible
IsPreirreducible.interior : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t : Set X}, IsPreirreducible t → IsPreirreducible (interior t)
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_left_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
  normalize a = a → (lcm a b = a ↔ b ∣ a)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictFDerivAt_exp_smul_const : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝕊] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝕊] [inst_4 : NormedAlgebra 𝕂 𝔸] [inst_5 : Algebra 𝕊 𝔸] [inst_6 : ContinuousSMul 𝕊 𝔸]
  [inst_7 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  HasStrictFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_pos : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (x : α), x ≠ 0 → (0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.vectorSpan_image_eq_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ {s₁ s₂ : Set ι}, vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) ↔ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The functor forgetting the differential in a complex, obtaining a graded object.  -/
HomologicalComplex.forget : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (c : ComplexShape ι) → CategoryTheory.Functor (HomologicalComplex V c) (CategoryTheory.GradedObject ι V)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_range_inl : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace α], MeasurableSet (Set.range Sum.inl)
-- Mathlib.Algebra.Category.Grp.Limits
/-- We show that the forgetful functor `AddCommGrpCat ⥤ AddGrpCat` creates limits.

All we need to do is notice that the limit point has an `AddCommGroup` instance available,
and then reuse the existing limit.  -/
AddCommGrpCat.Forget₂.createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Topology.Instances.Rat
NNRat.instContinuousSMulNNReal : ContinuousSMul ℚ≥0 NNReal
-- Init.SizeOfLemmas
UInt16.sizeOf : ∀ (a : UInt16), sizeOf a = a.toNat + 3
-- Mathlib.Data.Set.Sigma
Set.Nonempty.sigma_snd : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)},
  (s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.mk : {w : ℕ} → ℕ → ℕ → BitVec w → BitVec w → BitVec.DivModState w
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.associated_map_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {x y : Polynomial R},
  Associated x y → Associated (Polynomial.map f x) (Polynomial.map f y)
-- Mathlib.Topology.IsClosedRestrict
Topology.reorderRestrictProd_mem_preimage_image_restrict : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι}
  (p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)),
  Topology.reorderRestrictProd S s p ∈ Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiable_add_const_iff`. -/
Differentiable.add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (c : F), Differentiable 𝕜 f → Differentiable 𝕜 fun y => f y + c
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
MonoidAlgebra.instIsCancelMulZeroOfIsCancelAddOfUniqueProds : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsCancelMulZero R] [inst_3 : Mul A]
  [UniqueProds A], IsCancelMulZero (MonoidAlgebra R A)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.exists_leftDescent_of_ne_one : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W},
  w ≠ 1 → ∃ i, cs.IsLeftDescent w i
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The coequalizer of an idempotent morphism and the identity is split epi.  -/
CategoryTheory.Limits.splitEpiOfIdempotentCoequalizer : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {f : X ⟶ X} →
        CategoryTheory.CategoryStruct.comp f f = f →
          [inst_1 : CategoryTheory.Limits.HasCoequalizer (CategoryTheory.CategoryStruct.id X) f] →
            CategoryTheory.SplitEpi (CategoryTheory.Limits.coequalizer.π (CategoryTheory.CategoryStruct.id X) f)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.trans_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant A] (P P' : HomotopicalAlgebra.Cylinder A) [inst_3 : P'.IsGood],
  (P.trans P').I = CategoryTheory.Limits.pushout P.i₁ P'.i₀
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasSum_subtype_iff_of_support_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α} {s : Set β},
  Function.support f ⊆ s → (HasSum (f ∘ Subtype.val) a ↔ HasSum f a)