mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.right : CategoryTheory.Limits.WalkingPair
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorUnit_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Comon C)).X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ φ_1 : K ⟶ L) (e_φ : φ = φ_1) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone φ = CochainComplex.mappingCocone φ_1
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.filterMap_eq_filter : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  Std.DHashMap.Internal.Raw₀.filterMap (fun k => Option.guard fun v => f k v) m = Std.DHashMap.Internal.Raw₀.filter f m
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (as : α), sizeOf { as := as } = 1 + sizeOf as
-- Init.Data.Vector.MapIdx
Vector.mapIdx_empty : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β}, Vector.mapIdx f #v[] = #v[]
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr.eq_1 : ONote.zero.repr = 0
-- Std.Async.Process
Std.IO.Process.ResourceUsageStats.mk.inj : ∀ {cpuUserTime cpuSystemTime : Std.Time.Millisecond.Offset}
  {peakResidentSetSizeKb sharedMemorySizeKb unsharedDataSizeKb unsharedStackSizeKb minorPageFaults majorPageFaults
    swapOperations blockInputOps blockOutputOps messagesSent messagesReceived signalsReceived voluntaryContextSwitches
    involuntaryContextSwitches : UInt64}
  {cpuUserTime_1 cpuSystemTime_1 : Std.Time.Millisecond.Offset}
  {peakResidentSetSizeKb_1 sharedMemorySizeKb_1 unsharedDataSizeKb_1 unsharedStackSizeKb_1 minorPageFaults_1
    majorPageFaults_1 swapOperations_1 blockInputOps_1 blockOutputOps_1 messagesSent_1 messagesReceived_1
    signalsReceived_1 voluntaryContextSwitches_1 involuntaryContextSwitches_1 : UInt64},
  { cpuUserTime := cpuUserTime, cpuSystemTime := cpuSystemTime, peakResidentSetSizeKb := peakResidentSetSizeKb,
        sharedMemorySizeKb := sharedMemorySizeKb, unsharedDataSizeKb := unsharedDataSizeKb,
        unsharedStackSizeKb := unsharedStackSizeKb, minorPageFaults := minorPageFaults,
        majorPageFaults := majorPageFaults, swapOperations := swapOperations, blockInputOps := blockInputOps,
        blockOutputOps := blockOutputOps, messagesSent := messagesSent, messagesReceived := messagesReceived,
        signalsReceived := signalsReceived, voluntaryContextSwitches := voluntaryContextSwitches,
        involuntaryContextSwitches := involuntaryContextSwitches } =
      { cpuUserTime := cpuUserTime_1, cpuSystemTime := cpuSystemTime_1,
        peakResidentSetSizeKb := peakResidentSetSizeKb_1, sharedMemorySizeKb := sharedMemorySizeKb_1,
        unsharedDataSizeKb := unsharedDataSizeKb_1, unsharedStackSizeKb := unsharedStackSizeKb_1,
        minorPageFaults := minorPageFaults_1, majorPageFaults := majorPageFaults_1, swapOperations := swapOperations_1,
        blockInputOps := blockInputOps_1, blockOutputOps := blockOutputOps_1, messagesSent := messagesSent_1,
        messagesReceived := messagesReceived_1, signalsReceived := signalsReceived_1,
        voluntaryContextSwitches := voluntaryContextSwitches_1,
        involuntaryContextSwitches := involuntaryContextSwitches_1 } →
    cpuUserTime = cpuUserTime_1 ∧
      cpuSystemTime = cpuSystemTime_1 ∧
        peakResidentSetSizeKb = peakResidentSetSizeKb_1 ∧
          sharedMemorySizeKb = sharedMemorySizeKb_1 ∧
            unsharedDataSizeKb = unsharedDataSizeKb_1 ∧
              unsharedStackSizeKb = unsharedStackSizeKb_1 ∧
                minorPageFaults = minorPageFaults_1 ∧
                  majorPageFaults = majorPageFaults_1 ∧
                    swapOperations = swapOperations_1 ∧
                      blockInputOps = blockInputOps_1 ∧
                        blockOutputOps = blockOutputOps_1 ∧
                          messagesSent = messagesSent_1 ∧
                            messagesReceived = messagesReceived_1 ∧
                              signalsReceived = signalsReceived_1 ∧
                                voluntaryContextSwitches = voluntaryContextSwitches_1 ∧
                                  involuntaryContextSwitches = involuntaryContextSwitches_1
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {Y : ModuleCat S}
  (a : TensorProduct R S ↑Y),
  (ModuleCat.Hom.hom (ModuleCat.ExtendRestrictScalarsAdj.Counit.map f)) a =
    (TensorProduct.lift
        { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      a
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_bot : ∀ {R : Type u} [inst : NonAssocSemiring R] {x : R}, x ∈ ⊥ ↔ ∃ n, ↑n = x
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.apply_mk : ∀ {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (f : U ⟶ V) (x : ↑X) (hx : x ∈ U), f ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Std.Async.System
/-- Time the CPU was idle.
 -/
Std.Async.System.CPUTimes.idleTime : Std.Async.System.CPUTimes → Std.Time.Millisecond.Offset
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.tokenWithAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_rii : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_rii._auto_1) {t : Std.TreeSet.Raw α cmp},
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Batteries.Data.UInt
UInt32.toNat_min : ∀ (x y : UInt32), (x ⊓ y).toNat = min x.toNat y.toNat
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_sUnion_congr : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable → (μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonneg_iff : ∀ {b x : ℝ}, 1 < b → 0 < x → (0 ≤ Real.logb b x ↔ 1 ≤ x)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Turn an element of a type `F`
satisfying `OrderHomClass F α β` and `MonoidWithZeroHomClass F α β`
into an actual `OrderMonoidWithZeroHom`.
This is declared as the default coercion from `F` to `α →+*₀o β`.
TODO: Following [#mathlib4 > Mathlib's morphism hierarchy]
(https://leanprover.zulipchat.com/#narrow/channel/287929-
mathlib4/topic/Mathlib.27s.20morphism.20hierarchy/with/554383157),
rename this to `OrderMonoidWithZeroHom.ofClass` and remove `@[coe]` tag.  -/
OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulZeroOneClass α] →
            [inst_3 : MulZeroOneClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [MonoidWithZeroHomClass F α β] → F → α →*₀o β
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_units_iff_val_mem : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) (x : Gˣ), x ∈ H.units ↔ ↑x ∈ H
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- `ContinuousAlternatingMap.restrictScalars` as a `ContinuousLinearMap`.  -/
ContinuousAlternatingMap.restrictScalarsCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        [ContinuousSMul 𝕜 E] →
                          (𝕜' : Type u_5) →
                            [inst_9 : NontriviallyNormedField 𝕜'] →
                              [inst_10 : NormedAlgebra 𝕜' 𝕜] →
                                [inst_11 : Module 𝕜' E] →
                                  [IsScalarTower 𝕜' 𝕜 E] →
                                    [inst_13 : Module 𝕜' F] →
                                      [inst_14 : IsScalarTower 𝕜' 𝕜 F] →
                                        [inst_15 : ContinuousConstSMul 𝕜' F] → E [⋀^ι]→L[𝕜] F →L[𝕜'] E [⋀^ι]→L[𝕜'] F
-- Mathlib.Algebra.Module.ZLattice.Basic
IsZLattice.mk : ∀ {K : Type u_1} [inst : NormedField K] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L], Submodule.span K ↑L = ⊤ → IsZLattice K L
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it' : Std.IterM m α)
  (out : α) (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeffAddEquiv_symm_apply`. -/
SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (coeff : G →₀ k),
  SkewMonoidAlgebra.coeffAddEquiv.symm coeff = { coeff := coeff }
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaType_obj_obj_coe : ∀ (X : Type uᵒᵖ) (G : CommGrpCat), ↑((CommGrpCat.coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_closure_singleton_self : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), x ∈ AddSubgroup.closure {x}
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residueFieldMap.eq_1 : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x =
    CommRingCat.ofHom
      (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)))
-- Mathlib.Algebra.Polynomial.Reverse
/-- The reverse of a polynomial f is the polynomial obtained by "reading f backwards".
Even though this is not the actual definition, `reverse f = f (1/X) * X ^ f.natDegree`.  -/
Polynomial.reverse : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Polynomial R
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.notMem_of_subset : ∀ {x y : ZFSet.{u_1}}, x ⊆ y → y ∉ x
-- Mathlib.Algebra.Free
FreeAddMagma.brecOn.go : {α : Type u} →
  {motive : FreeAddMagma α → Sort u_1} →
    (t : FreeAddMagma α) → ((t : FreeAddMagma α) → FreeAddMagma.below t → motive t) → motive t ×' FreeAddMagma.below t