mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_inf : ∀ {M : Type u_1} [inst : Monoid M] (S T : Subgroup Mˣ), (S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits
-- Lean.Parser.Command
Lean.Parser.Command.moduleDoc.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_iff_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] (F : CategoryTheory.Functor C C') [F.IsEquivalence],
  CategoryTheory.IsCardinalPresentable (F.obj X) κ ↔ CategoryTheory.IsCardinalPresentable X κ
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.visit : Array Lean.Expr → Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A pullback cone on `f` and `g` is determined by morphisms `fst : W ⟶ X` and `snd : W ⟶ Y`
such that `fst ≫ f = snd ≫ g`.  -/
CategoryTheory.Limits.PullbackCone.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {W : C} →
            (fst : W ⟶ X) →
              (snd : W ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
                    CategoryTheory.Limits.PullbackCone.mk._auto_1 →
                  CategoryTheory.Limits.PullbackCone f g
-- Aesop.Stats.Basic
Aesop.sortRuleStatsTotals : Array (Aesop.DisplayRuleName × Aesop.RuleStatsTotals) → Array (Aesop.DisplayRuleName × Aesop.RuleStatsTotals)
-- Std.Http.Data.Status
/-- 405 Method Not Allowed
 -/
Std.Http.Status.methodNotAllowed : Std.Http.Status
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_map_eq_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ (S : Submonoid M), Submonoid.comap f (Submonoid.map f S) = S
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_inf_map_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S T : L.Substructure M),
      FirstOrder.Language.Substructure.comap f
          (FirstOrder.Language.Substructure.map f S ⊓ FirstOrder.Language.Substructure.map f T) =
        S ⊓ T
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forIn_eq_forInUncurried : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap α fun x => β} [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.forIn f init m = Std.DHashMap.Const.forInUncurried (fun a b => f a.1 a.2 b) init m
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → {X₁ : C₁} → (w : X₂ ⟶ Φ.functor.obj X₁) → W₂ w → Φ.RightResolution X₂
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- SimplexCategory is the category presented by generators and relation by the simplicial
identities.  -/
SimplexCategoryGenRel : Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.static : Lean.Lsp.SemanticTokenModifier
-- Lean.Server.References
/-- Declarations provided by the worker.  -/
Lean.Server.TransientWorkerILean.decls : Lean.Server.TransientWorkerILean → Lean.Lsp.Decls
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H K : CategoryTheory.Functor D E} (α : G ≅ H) (β : H ≅ K),
  F.isoWhiskerLeft (α ≪≫ β) = F.isoWhiskerLeft α ≪≫ F.isoWhiskerLeft β
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.PrelocalPredicate.mk.inj : ∀ {X : TopCat} {T : ↑X → Type u_1} {pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop}
  {res : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred f → pred fun x => f (i x)}
  {pred_1 : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop}
  {res_1 : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred_1 f → pred_1 fun x => f (i x)},
  { pred := pred, res := res } = { pred := pred_1, res := res_1 } → pred = pred_1
-- Mathlib.Data.Set.Subsingleton
/-- The `coe_sort` of a set `s` in a subsingleton type is a subsingleton.
For the corresponding result for `Subtype`, see `subtype.subsingleton`.  -/
Set.subsingleton_coe_of_subsingleton : ∀ {α : Type u} [Subsingleton α] {s : Set α}, Subsingleton ↑s
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `coeff g` as a linear map  -/
HahnSeries.coeff.linearMap : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid V] → [inst_3 : Module R V] → Γ → HahnSeries Γ V →ₗ[R] V
-- Lean.Meta.Tactic.Simp.Types
/-- Retrieve auto-generated congruence lemma for `f`.

Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
 -/
Lean.Meta.Simp.mkCongrSimp? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.CongrTheorem)
-- Mathlib.Data.SetLike.Basic
/-- **Alias** of `mem_of_le_of_mem`.

---

**Alias** of the forward direction of `SetLike.le_def`. -/
SetLike.GCongr.mem_of_le_of_mem : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : LE A] [IsConcreteLE A B] {S T : A},
  S ≤ T → ∀ ⦃x : B⦄, x ∈ S → x ∈ T
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instFullLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism : ∀ {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  (A B : CategoryTheory.ObjectProperty C) [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.HasShift C ℤ] [inst_5 : CategoryTheory.Preadditive C]
  [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_7 : CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C] [inst_9 : A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  [A.IsVerdierRightLocalizing B] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂)
  [inst_13 : L₁.IsLocalization (B.inverseImage A.ι).trW] [inst_14 : L₂.IsLocalization B.trW],
  ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z') {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom h))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)}, Std.ExtDHashMap.ofList l = List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.map f it)).toList = (Std.IterM.filterMapM (fun b => g (f b)) it).toList
-- Mathlib.Data.List.MinMax
List.argmin_eq_none : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α},
  List.argmin f l = none ↔ l = []
-- Mathlib.Data.Set.Image
Set.Sum.elim_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ),
  Set.range (Sum.elim f g) = Set.range f ∪ Set.range g
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → ∀ (g : G), orderOf g ≠ 2
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.quotient : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {I : Ideal S},
  f.IsIntegral → (Ideal.quotientMap I f ⋯).IsIntegral