mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- Bundle an `S`-morphism of `S`-scheme with `P` into a morphism in `P.Over ⊤ S`.  -/
AlgebraicGeometry.Scheme.Hom.asOverProp : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X Y : AlgebraicGeometry.Scheme} →
    (f : X.Hom Y) →
      (S : AlgebraicGeometry.Scheme) →
        [inst : X.Over S] →
          [inst_1 : Y.Over S] →
            [f.IsOver S] → {hX : P (X ↘ S)} → {hY : P (Y ↘ S)} → X.asOverProp S hX ⟶ Y.asOverProp S hY
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuous_cosh : Continuous Complex.cosh
-- Init.Data.Array.Lemmas
Array.toList_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, (Array.map f xs).toList = List.map f xs.toList
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_add_inv_eq_inv : ∀ {p q r : ℝ}, p.HolderTriple q r → p⁻¹ + q⁻¹ = r⁻¹
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_swap : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (s : Multiset α),
  Multiset.foldr f b s = Multiset.foldl (fun x y => f y x) b s
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.runCore : {α : Type} → Lean.CoreM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Analysis.Analytic.Constructions
/-- `AnalyticAt.comp` for functions on product spaces  -/
AnalyticAt.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  {h : F × G → H} {f : E → F} {g : E → G} {x : E},
  AnalyticAt 𝕜 h (f x, g x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (fun x => h (f x, g x)) x
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- The inclusions `(F s).obj (k s) ⟶ colimit (F s)` induce a cocone on `pointwiseProduct F` with
cone point `∏ᶜ (fun s : α) => colimit (F s)`.  -/
CategoryTheory.Limits.coconePointwiseProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type u_1} →
      {I : α → Type u_2} →
        [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] →
          [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C] →
            {F : (i : α) → CategoryTheory.Functor (I i) C} →
              ((i : α) → CategoryTheory.Limits.Cocone (F i)) →
                CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pointwiseProduct F)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_lt_iff_nontrivial : ∀ {α : Type u}, 1 < Cardinal.mk α ↔ Nontrivial α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesBiproduct.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  {f : J → C} {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  (∀ {b : CategoryTheory.Limits.Bicone f} (a : b.IsBilimit), Nonempty (F.mapBicone b).IsBilimit) →
    CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.Topology.ClusterPt
/-- **Alias** of the forward direction of `clusterPt_iff_forall_mem_closure`. -/
ClusterPt.mem_closure_of_mem : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F → ∀ s ∈ F, x ∈ closure s
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.zsmul_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → ∀ (n : ℤ), n • x ∈ s
-- Mathlib.Topology.Instances.AddCircle.DenseSubgroup
/-- The additive subgroup of real numbers generated by `a` and `b` is dense
iff `a / b` is an irrational number.

Here we rely on the fact that `a / 0 = 0` in Mathlib,
so we don't need to add `b ≠ 0` as an assumption.  -/
dense_addSubgroupClosure_pair_iff : ∀ {a b : ℝ}, Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.mk.inj : ∀ {R : Type v} {inst : NonUnitalNonAssocSemiring R} {inst_1 : Star R} {toNonUnitalSubsemiring : NonUnitalSubsemiring R}
  {star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier}
  {toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R}
  {star_mem'_1 : ∀ {a : R}, a ∈ toNonUnitalSubsemiring_1.carrier → star a ∈ toNonUnitalSubsemiring_1.carrier},
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := star_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := star_mem'_1 } →
    toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.instCompleteLattice : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → CompleteLattice M.Submodule
-- Std.Data.Iterators.Producers.Empty
/-- Returns an iterator that terminates immediately.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.Iter.empty : (β : Type w) → Std.Iter β
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormedSpaceComplexProd : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {E : Type u_2} →
        {F : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : Module ℂ E] →
              [inst_4 : SMul A E] →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : Module ℂ F] →
                    [inst_7 : SMul A F] →
                      [inst_8 : CStarModule A E] →
                        [inst_9 : CStarModule A F] →
                          [inst_10 : StarOrderedRing A] → NormedSpace ℂ (WithCStarModule A (E × F))
-- Mathlib.Order.Hom.Bounded
BotHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] {f g : BotHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Order.Ideal
Order.Ideal.isProper_principal_iff : ∀ {P : Type u_1} [inst : PartialOrder P] [inst_1 : OrderTop P] {a : P}, (Order.Ideal.principal a).IsProper ↔ a ≠ ⊤
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.ofQuotientStabilizer_smul : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X) (g : G)
  (g' : G ⧸ MulAction.stabilizer G x),
  MulAction.ofQuotientStabilizer G x (g • g') = g • MulAction.ofQuotientStabilizer G x g'
-- Mathlib.GroupTheory.Exponent
Submonoid.exponent_top : ∀ (G : Type u) [inst : Monoid G], Monoid.exponent ↥⊤ = Monoid.exponent G
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.forgetToScheme_faithful : AlgebraicGeometry.AffineScheme.forgetToScheme.Faithful
-- Mathlib.Analysis.Distribution.Sobolev
/-- The Bessel potential operator is the Fourier multiplier with the function
`(1 + ‖x‖ ^ 2) ^ (s / 2)`.

Note that due to the convention of the Fourier transform, this is the operator
`(1 - (2 * π) ^ (-2) • Δ) ^ (s / 2)` not `(1 - Δ) ^ (s / 2)`.  -/
TemperedDistribution.besselPotential : (E : Type u_1) →
  (F : Type u_2) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [FiniteDimensional ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] → [inst_6 : NormedSpace ℂ F] → ℝ → TemperedDistribution E F →L[ℂ] TemperedDistribution E F
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_one : ∀ {α : Type u} [inst : One α], ↑1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g))
      (CategoryTheory.CategoryStruct.comp g' h)
-- Lean.Widget.InteractiveGoal
/-- The hypothesis is a type.  -/
Lean.Widget.InteractiveHypothesisBundle.isType? : Lean.Widget.InteractiveHypothesisBundle → Option Bool
-- Mathlib.Order.RelSeries
RelSeries.last_singleton : ∀ {α : Type u_1} {r : SetRel α α} (x : α), (RelSeries.singleton r x).last = x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, (Std.DHashMap.Raw.Const.insertMany m l).isEmpty = true → m.isEmpty = true
-- Lean.Elab.Import
_private.Lean.Elab.Import.0.Lean.Elab.osForbiddenNames : Array String
-- Std.Time.Zoned.Database.TzIf
/-- The index into the abbreviation string table for this time type.
 -/
Std.Time.TimeZone.TZif.LocalTimeType.abbreviationIndex : Std.Time.TimeZone.TZif.LocalTimeType → UInt8
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- The specialization of `SimpleGraph.Walk.map` for mapping walks to supergraphs.  -/
SimpleGraph.Walk.mapLe : {V : Type u} → {G G' : SimpleGraph V} → G ≤ G' → {u v : V} → G.Walk u v → G'.Walk u v
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_1.splitter : {σ : Type u_1} →
  {α : Type u_2} →
    (motive : Option (α × σ) → Sort u_3) →
      (x : Option (α × σ)) → (Unit → motive none) → ((fst : α) → (s : σ) → motive (some (fst, s))) → motive x
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
AbsoluteValue.IsEuclidean.map_lt_map_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {abv : AbsoluteValue R S} {x y : R}, abv.IsEuclidean → (abv x < abv y ↔ EuclideanDomain.r x y)
-- Init.WF
Acc.brecOn : ∀ {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Prop} {a : α} (t : Acc r a),
  (∀ (a : α) (t : Acc r a), Acc.below t → motive a t) → motive a t