mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- `ClassGroup.mkMMem` is a specialization of `ClassGroup.mk0` to (the finite set of)
ideals that contain `M := ∏ m ∈ finsetApprox L f abs, m`.
By showing this function is surjective, we prove that the class group is finite.  -/
ClassGroup.mkMMem : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} →
                [inst_4 : DecidableEq ι] →
                  [inst_5 : Fintype ι] →
                    (bS : Module.Basis ι R S) →
                      (adm : abv.IsAdmissible) →
                        [inst_6 : Infinite R] →
                          [inst_7 : DecidableEq R] →
                            [IsDedekindDomain S] →
                              { J // (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ J } → ClassGroup S
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulActionHomClass F M X Y` states that `F` is a type of
morphisms which are equivariant with respect to actions of `M`
This is an abbreviation of `MulActionSemiHomClass`.  -/
MulActionHomClass : (F : Type u_8) →
  (M : outParam (Type u_9)) →
    (X : outParam (Type u_10)) → (Y : outParam (Type u_11)) → [SMul M X] → [SMul M Y] → [FunLike F X Y] → Prop
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm.eq_1 : ∀ (x y : NNReal), x.agm y = ⨅ n, (x.agmSequences y n).2
-- Lean.Meta.Match.Match
/-- Logs an error indicating that the alternative at `ref` contains an unexpected number of patterns.
Remark: we allow `α` to be arbitrary because this error may be thrown before or after elaborating
pattern syntax.
 -/
Lean.Meta.Match.logIncorrectNumberOfPatternsAt : {α : Type} → [Lean.ToMessageData α] → Lean.Syntax → String → ℕ → ℕ → List α → Lean.MetaM Unit
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α} {fallback : β a}
  {c : ℕ}, (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getD a fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Comon (CategoryTheory.Functor C D)),
  CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.obj A =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A.X
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Convert between two algebras of different quadratic forms, sending vectors to vectors, scalars
to scalars, and adjusting products by a contraction term.

This is $\lambda_B$ from [bourbaki2007] §9 Lemma 2.  -/
CliffordAlgebra.changeForm : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q Q' : QuadraticForm R M} →
            {B : LinearMap.BilinForm R M} →
              LinearMap.BilinMap.toQuadraticMap B = Q' - Q → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q'
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Extend an ordered partition of `n` entries, by adding to the `i`-th part a new point to the
left.  -/
OrderedFinpartition.extendMiddle : {n : ℕ} → (c : OrderedFinpartition n) → Fin c.length → OrderedFinpartition (n + 1)
-- Init.Prelude
/-- `a ^^^ b` computes the bitwise XOR of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^^^` in identifiers is `xor`. -/
HXor.hXor : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HXor α β γ] → α → β → γ
-- Mathlib.Data.Option.Basic
Option.orElse_eq_none : ∀ {α : Type u_1} (o o' : Option α), (o <|> o') = none ↔ o = none ∧ o' = none
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in the left argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (f : A ⟶ A')
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f B)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B))
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B))
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingFilterBasis.submodulesBasisIsBasis : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (BR : RingFilterBasis R) {B : ι → Submodule R M}, BR.SubmodulesBasis B → SubmodulesBasis B
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instSetLike : {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] → SetLike (AffineSubspace k P) P
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of an element of `K`.  -/
Height.mulHeight₁ : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → K → ℝ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_commute_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  Commute (cfc f a) (cfc g a)
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt64.size ≤ n → (UInt64.ofNatClamp n).toFin = ⟨UInt64.size - 1, UInt64.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonIdIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.mapMonIdIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Mon.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapMon.obj X).X) ⋯ ⋯) ⋯
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Minute.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subMinutes : Std.Time.WallTime → Std.Time.Minute.Offset → Std.Time.WallTime
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b)
  {Z : C} (h : (E.sigmaOfIsColimit hc hd).X a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (d.inj i)
      (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₁ r) h) =
    CategoryTheory.CategoryStruct.comp (E.p₁ i.snd) (CategoryTheory.CategoryStruct.comp (c.inj i.fst.1) h)
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLTOrdinal : LT Std.Time.Minute.Ordinal
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        ∀ {ε : NNReal}, 0 < ε → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s