mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instNontrivial : ∀ (R : Type u_1) [inst : CommRing R] [Nontrivial R], Nontrivial (FractionRing R)
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_Id_eq : ∀ {type : Type u_1} {p : type → Prop} {x : Id type}, SatisfiesM p x ↔ p x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.CostructuredArrow.essentiallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [CategoryTheory.LocallySmall.{w, v₂, u₂} D],
  CategoryTheory.EssentiallySmall.{w, v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)
-- Mathlib.LinearAlgebra.Complex.Module
/-- There is an `AlgHom` from `ℂ` to any `ℝ`-algebra with an element that squares to `-1`.

See `Complex.lift` for this as an equiv.  -/
Complex.liftAux : {A : Type u_1} → [inst : Ring A] → [inst_1 : Algebra ℝ A] → (I' : A) → I' * I' = -1 → ℂ →ₐ[ℝ] A
-- Mathlib.RingTheory.Ideal.Nonunits
/-- The set of non-invertible elements of a monoid.  -/
nonunits : (α : Type u_4) → [Monoid α] → Set α
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure.  -/
AddSubmonoid.toAddMonoid : {M : Type u_5} → [inst : AddMonoid M] → (S : AddSubmonoid M) → AddMonoid ↥S
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsConnected C],
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)
-- Mathlib.Data.Set.Operations
Set.prod_image_right : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β),
  t ×ˢ (f '' s) = (fun x => (x.1, f x.2)) '' t ×ˢ s
-- Std.Time.Format.Modifier
/-- Hour, minute, and second without colon (e.g., "+013015")
 -/
Std.Time.OffsetX.hourMinuteSecond : Std.Time.OffsetX
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
/-- This lemma matches more generally than `Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk` when
using `rw ← `.  -/
Finset.Nat.prod_antidiagonal_eq_prod_range_succ : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 ij.2 = ∏ k ∈ Finset.range n.succ, f k (n - k)
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.SMulInvariantMeasure.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : SMul M α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s) → MeasureTheory.SMulInvariantMeasure M α μ
-- Mathlib.RepresentationTheory.Homological.Resolution
classifyingSpaceUniversalCover.compForgetAugmented.toModule.eq_1 : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  classifyingSpaceUniversalCover.compForgetAugmented.toModule k G =
    ((CategoryTheory.SimplicialObject.Augmented.whiskering (Type u) (ModuleCat k)).obj
          (ModuleCat.monoidAlgebraFree k)).obj
      (classifyingSpaceUniversalCover.compForgetAugmented G)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- When the derivative of a function is nonnegative, then it is automatically integrable,
Ioc version.  -/
intervalIntegral.integrableOn_deriv_of_nonneg : ∀ {g' g : ℝ → ℝ} {a b : ℝ},
  ContinuousOn g (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioo a b, 0 ≤ g' x) → MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.ext : ∀ {ι : Type u_1} {x y : AbstractSimplicialComplex ι}, x.faces = y.faces → x = y
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Construct an isomorphism of commutative monoid objects by giving an isomorphism between the
underlying objects and checking compatibility with unit and multiplication only in the forward
direction.  -/
CategoryTheory.CommMon.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M N : CategoryTheory.CommMon C} →
          (e : M.X ≅ N.X) →
            autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
                CategoryTheory.CommMon.mkIso._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                      CategoryTheory.MonObj.mul)
                  CategoryTheory.CommMon.mkIso._auto_3 →
                (M ≅ N)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.lt_of_shiftLeft_lt : ∀ {a b c : ℕ}, a <<< b < c → a < c
-- Mathlib.Logic.Basic
dite_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α}
  {s : β}, (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
-- Mathlib.MeasureTheory.Measure.Restrict
/-- **Alias** of the reverse direction of `MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ`.

---

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `sUnion`).  -/
MeasureTheory.Measure.ext_of_sUnion_eq_univ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable → ⋃₀ S = Set.univ → (∀ s ∈ S, μ.restrict s = ν.restrict s) → μ = ν
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.instNontrivial : Nontrivial UpperHalfPlane
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [inst_1 :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)],
  CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F =
    ((CategoryTheory.Limits.ReflexiveCofork.isColimitEquiv F (CategoryTheory.Limits.colimit.cocone F)).symm
          (CategoryTheory.Limits.colimit.isColimit F)).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit
        (CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a : G} {b : k}, SkewMonoidAlgebra.single a b = 0 ↔ b = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.descShortComplex_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)
      (CochainComplex.mappingCone.descShortComplex S₂) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₁) f.τ₃
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Given an object `W` equipped with morphisms `p₁ : W ⟶ E.X i₁`, `p₂ : W ⟶ E.X i₂`,
this is the sieve of `W` which consists of morphisms `g : Z ⟶ W` such that there exists `j`
and `h : Z ⟶ E.Y j` such that `g ≫ p₁ = h ≫ E.p₁ j` and `g ≫ p₂ = h ≫ E.p₂ j`.
See lemmas `sieve₁_eq_pullback_sieve₁'` and `sieve₁'_eq_sieve₁` for equational lemmas
regarding this sieve.  -/
CategoryTheory.PreOneHypercover.sieve₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        {i₁ i₂ : E.I₀} → {W : C} → (W ⟶ E.X i₁) → (W ⟶ E.X i₂) → CategoryTheory.Sieve W
-- Mathlib.Data.Set.Card
Set.encard_insert_le : ∀ {α : Type u_1} (s : Set α) (x : α), (insert x s).encard ≤ s.encard + 1
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceFrom_cast : ∀ {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos}, (t.sliceFrom (pos.cast hst)).copy = (s.sliceFrom pos).copy
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (b : CategoryTheory.LocallyDiscrete Cᵒᵖ)
  (X : CategoryTheory.ObjectProperty.FullSubcategory (CategoryTheory.Presheaf.IsSheaf (J.over (Opposite.unop b.as))))
  (X_1 : (CategoryTheory.Over (Opposite.unop b.as))ᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).hom.app X_1 = CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), ↑(⨆ i, f i) = ⋃ i, ↑(f i)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given an ordered finpartition of `n+1`, with a leftmost atom equal to `{0}`, remove this
atom to form an ordered finpartition of `n`.  -/
OrderedFinpartition.eraseLeft : {n : ℕ} → (c : OrderedFinpartition (n + 1)) → Set.range (c.emb 0) = {0} → OrderedFinpartition n
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_apply_obj : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : Quiver.SingleObj α), (Quiver.SingleObj.toPrefunctor f).obj a = id a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- the index type for the sections  -/
SheafOfModules.GeneratingSections.I : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] → {M : SheafOfModules R} → M.GeneratingSections → Type u
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
/-- The integral of `mulExpNegMulSq ε ∘ g` with respect to a finite measure `P` can be
approximated by the integral of the sequence approximating the exponential function.  -/
tendsto_integral_mul_one_add_inv_smul_sq_pow : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (g : BoundedContinuousFunction E ℝ),
  0 < ε →
    Filter.Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) Filter.atTop
      (nhds (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P))
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.instMonoDesc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono (CategoryTheory.Limits.coequalizer.desc f ⋯)
-- Init.Data.List.Basic
List.isPrefixOf_nil_left : ∀ {α : Type u} {l : List α} [inst : BEq α], [].isPrefixOf l = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.of.sizeOf_spec : ∀ (η : Mathlib.Tactic.BicategoryLike.HorizontalComp),
  sizeOf (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η) = 1 + sizeOf η
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Initial.left_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Algebra F} (h : CategoryTheory.Limits.IsInitial A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) A.str =
    CategoryTheory.CategoryStruct.id A.a
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Annotates the term with the current expression position and registers `TermInfo`
to associate the term to the current expression.
 -/
Lean.PrettyPrinter.Delaborator.annotateTermInfo : Lean.Term → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- Translation of preimage is contained in preimage of translation  -/
smul_preimage_set_subsetₛₗ : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : SMul M α]
  [inst_1 : SMul N β] [inst_2 : FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : M) (t : Set β),
  c • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (σ c • t)
-- Mathlib.Topology.Connected.PathConnected
pathComponent_subset_component : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), pathComponent x ⊆ connectedComponent x
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- Build an isomorphism in the category `CoalgCat R` from a
`CoalgEquiv`.  -/
CoalgEquiv.toCoalgIso : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommGroup Y] →
            [inst_4 : Module R Y] →
              [inst_5 : Coalgebra R X] → [inst_6 : Coalgebra R Y] → (X ≃ₗc[R] Y) → (CoalgCat.of R X ≅ CoalgCat.of R Y)
-- Mathlib.Probability.Notation
/-- `𝔼[X]` is the expectation of `X`, defined as its Lebesgue integral.  -/
ProbabilityTheory.«term𝔼[_]» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The image of an open set under a continuous map is analytic.  -/
IsOpen.analyticSet_image : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [PolishSpace β] {s : Set β},
  IsOpen s → ∀ {f : β → α}, Continuous f → MeasureTheory.AnalyticSet (f '' s)
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ),
  AlgebraicTopology.DoldKan.N₁Γ₀.app K =
    (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
      (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).mapIso (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.copy_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (s : Set A) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Order.Comparable
AntisymmRel.not_incompRel : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, AntisymmRel r a b → ¬IncompRel r a b
-- Mathlib.Geometry.Euclidean.Volume.Measure
Isometry.euclideanHausdorffMeasure_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : EMetricSpace Y] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℕ},
  Isometry f →
    ∀ (s : Set Y),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (f ⁻¹' s) =
        (MeasureTheory.Measure.euclideanHausdorffMeasure d) (s ∩ Set.range f)
-- Init.Omega.Constraint
/-- A linear combination of two constraints.  -/
Lean.Omega.Constraint.combo : ℤ → Lean.Omega.Constraint → ℤ → Lean.Omega.Constraint → Lean.Omega.Constraint
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_eq_binaryRec : ∀ (f : Bool → Bool → Bool),
  Nat.bitwise f = fun n =>
    Nat.binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => Nat.binaryRec (bif f true false then Nat.bit a m else 0) (fun b n x => Nat.bit (f a b) (Ia n)) n)
      n
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRiiIterIteratorOfUpwardEnumerableOfLeast? : {α : Type} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.ToStream (Std.Rii α) (Std.Iter α)
-- Mathlib.Data.Int.ModEq
Int.abs_modEq_two : ∀ {a : ℤ}, |a| ≡ a [ZMOD 2]
-- Init.System.IO
IO.TaskState.noConfusionType : Sort v✝ → IO.TaskState → IO.TaskState → Sort v✝
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₁_desc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₁ (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₁
-- Mathlib.Data.Ordmap.Invariants
Ordnode.All.imp : ∀ {α : Type u_1} {P Q : α → Prop}, (∀ (a : α), P a → Q a) → ∀ {t : Ordnode α}, Ordnode.All P t → Ordnode.All Q t
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- **Alias** of `AddMonoidHom.coe_finsetSum`. -/
AddMonoidHom.coe_finset_sum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : ι → M →+ N)
  (s : Finset ι), ⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)