mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.IR.Basic
Lean.IR.modifyJPs : Array Lean.IR.FnBody → (Lean.IR.FnBody → Lean.IR.FnBody) → Array Lean.IR.FnBody
-- Init.Data.SInt.Basic
/-- Non-strict inequality of 16-bit signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `≤` operator.
 -/
Int16.le : Int16 → Int16 → Prop
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], MonoidAlgebra.ofCoeff 0 = 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mem_orbit_subAdd_iff : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {p : SubAddAction R M} {x m : ↥p},
  x ∈ AddAction.orbit R m ↔ ↑x ∈ AddAction.orbit R ↑m
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.extendIso`.

---

A cocone extended by an isomorphism is isomorphic to the original cone.  -/
CategoryTheory.Limits.Cocones.extendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) → {X : C} → (f : s.pt ≅ X) → s ≅ s.extend f.hom
-- Init.Omega.Int
Lean.Omega.Nat.le_of_ge : ∀ {x y : ℕ}, x ≥ y → y ≤ x
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The isomorphism `(A.prod B).toSSet ≅ A.toSSet ⊗ B.toSSet`.  -/
SSet.Subcomplex.prodIso : {X Y : SSet} →
  (A : X.Subcomplex) →
    (B : Y.Subcomplex) → (A.prod B).toSSet ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj A.toSSet B.toSSet
-- Mathlib.Analysis.Convex.StdSimplex
/-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative
coordinates with total sum `1`. This is the free object in the category of convex spaces.  -/
stdSimplex : (𝕜 : Type u_2) → (ι : Type u_1) → [Semiring 𝕜] → [PartialOrder 𝕜] → [Fintype ι] → Set (ι → 𝕜)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a group structure.  -/
SubgroupClass.toGroup : {G : Type u_1} → [inst : Group G] → {S : Type u_4} → (H : S) → [inst_1 : SetLike S G] → [SubgroupClass S G] → Group ↥H
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.eq_symm_apply : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (f : Equidecomp X G) {x y : X},
  x ∈ f.target → y ∈ f.source → (y = ↑f.symm.toPartialEquiv x ↔ ↑f.toPartialEquiv y = x)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A set of points in an affine subspace is cospherical if and only if its image in the ambient
space is cospherical.  -/
EuclideanGeometry.Cospherical.subtype_val_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {S : AffineSubspace ℝ P} [Nonempty ↥S] [S.direction.HasOrthogonalProjection]
  {ps : Set ↥S}, EuclideanGeometry.Cospherical (Subtype.val '' ps) ↔ EuclideanGeometry.Cospherical ps
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divRight_nhds : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {c a : G},
  Filter.map (fun x => x / c) (nhds a) = nhds (a / c)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}, CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget PartOrdEmb)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredULift : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C],
  CategoryTheory.IsFiltered (ULift.{u₂, u} C)
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries a unital additive magma structure that distributes over a unital binary
operation, then the additive magma structure is a commutative additive monoid.  -/
EckmannHilton.addCommMonoid : {X : Type u} →
  {m₁ : X → X → X} →
    {e₁ : X} →
      EckmannHilton.IsUnital m₁ e₁ →
        [h : AddZeroClass X] → (∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) → AddCommMonoid X
-- Init.Data.Int.Gcd
Int.lcm_zero_right : ∀ (a : ℤ), a.lcm 0 = 0
-- Init.Data.UInt.Lemmas
UInt8.ofNat_mul : ∀ (a b : ℕ), UInt8.ofNat (a * b) = UInt8.ofNat a * UInt8.ofNat b
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Given `R`-algebras `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-bialgebra homomorphism `A →ₐc[R] B` is an `R`-algebra map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
«term_→ₐc[_]_» : Lean.TrailingParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getKey? a l = Std.Internal.List.getKey? a l'
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.braided : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {F : CategoryTheory.Functor C D} [self : F.LaxBraided] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) =
    CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanAddGroup.toIsTopologicalAddGroup : ∀ {G : Type u_1} {inst : AddGroup G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanAddGroup G],
  IsTopologicalAddGroup G
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (distance distance_1 : ℕ),
      distance = distance_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input_1 distance_1 curr hcurr s_1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.pow.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ => h_3 k) =
    h_1 ()
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeLeftOp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ},
  CategoryTheory.NatTrans.removeLeftOp (CategoryTheory.CategoryStruct.id F.leftOp) = CategoryTheory.CategoryStruct.id F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.diag_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X X] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) f = CategoryTheory.Limits.coprod.desc f f
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The cokernel cocone induced by the projection onto the quotient.  -/
ModuleCat.cokernelCocone : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Limits.CokernelCofork f
-- Mathlib.Data.Multiset.ZeroCons
Multiset.le_zero : ∀ {α : Type u_1} {s : Multiset α}, s ≤ 0 ↔ s = 0
-- Init.Data.Slice.Notation
Std.Roc.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Roc β → γ) → Std.Roc.Sliceable α β γ
-- Aesop.Tree.Data
Aesop.NodeState.unprovable.sizeOf_spec : sizeOf Aesop.NodeState.unprovable = 1
-- Init.Data.Array.Bootstrap
Array.append_eq_append : ∀ {α : Type u_1} {xs ys : Array α}, xs.append ys = xs ++ ys
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.minValueSealed : Int8
-- Mathlib.Data.Sum.Order
Sum.instTotalLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Total r] [Std.Total s],
  Std.Total (Sum.Lex r s)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- `C` has reflexive coequalizers if it has coequalizers for every reflexive pair.  -/
CategoryTheory.Limits.HasReflexiveCoequalizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.Sober
/-- A generic point of the closure of an irreducible space.  -/
IsIrreducible.genericPoint : {α : Type u_1} → [inst : TopologicalSpace α] → [QuasiSober α] → {S : Set α} → IsIrreducible S → α
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.nil : ∀ {α : Type u} [inst : DecidableEq α], FreeAddGroup.reduceCyclically [] = []
-- Mathlib.Algebra.Order.Group.Basic
zpow_lt_zpow_iff_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α},
  1 < a → (a ^ m < a ^ n ↔ m < n)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.antilipschitz : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), AntilipschitzWith (Dilation.ratio f)⁻¹ ⇑f
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.homeomorph.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  (hf : Topology.IsQuotientMap ⇑f), hf.homeomorph = hf.homeomorph
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instLTKey : LT Lean.Meta.DiscrTree.Key
-- Std.Time.Format.Modifier
Std.Time.Modifier.d.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.d presentation) = 1 + sizeOf presentation
-- Lean.LocalContext
/-- Return local hypotheses which are not "implementation detail", as `Expr`s.  -/
Lean.getLocalHyps : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → m (Array Lean.Expr)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.triangleMorphismId_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₁ = CategoryTheory.CategoryStruct.id T.obj₁
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : One R],
  (HahnSeries.single 0) 1 = 1
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.hasBasis_nhds_one : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (nhds 1).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 1) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.LinearAlgebra.Prod
Submodule.fstEquiv_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : ↥(Submodule.fst R M M₂)), (Submodule.fstEquiv R M M₂) x = (↑x).1
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- A term of `I` regarded as an ordinal.  -/
Profinite.NobelingProof.ord : (I : Type u) → [inst : LinearOrder I] → [WellFoundedLT I] → I → Ordinal.{u}
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Isδ₀.congr_simp : ∀ {Δ Δ' : SimplexCategory} (i i_1 : Δ' ⟶ Δ) (e_i : i = i_1) [inst : CategoryTheory.Mono i],
  AlgebraicTopology.DoldKan.Isδ₀ i = AlgebraicTopology.DoldKan.Isδ₀ i_1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.pullbackMap`. -/
CategoryTheory.MorphismProperty.pullback_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S}
  [inst_3 : CategoryTheory.Limits.HasPullbacksAlong f] {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'}
  [inst_4 : CategoryTheory.Limits.HasPullbacksAlong g'] {i₂ : Y ⟶ Y'},
  P i₁ →
    P i₂ →
      ∀ (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g'),
        P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Init.Data.Rat.Lemmas
Rat.mkRat_eq_iff : ∀ {d₁ d₂ : ℕ} {n₁ n₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → (mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁)
-- Mathlib.Order.Filter.Pointwise
Filter.instVAdd.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β],
  Filter.instVAdd =
    {
      vadd := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 +ᵥ x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ +ᵥ t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forwardMatches : Array Aesop.ForwardRuleMatch → Aesop.RuleTacDescr
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context.mk.sizeOf_spec : ∀ (config : Lean.Try.Config), sizeOf { config := config } = 1 + sizeOf config