mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g k c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset),
  Commute k c ↔
    ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.addConjMap_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a),
  Function.Bijective ⇑(SubAddAction.ofStabilizer.conjMap hg)
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- An auxiliary definition to be used in the proof of the fact that
`J.diagramFunctor D X` preserves limits.  -/
CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            {X : C} →
              {K : Type s} →
                [inst_3 : CategoryTheory.SmallCategory K] →
                  {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} →
                    {W : J.Cover X} →
                      (i : W.Arrow) →
                        CategoryTheory.Limits.Cone
                            (F.comp
                              ((J.diagramFunctor D X).comp
                                ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W)))) →
                          CategoryTheory.Limits.Cone (F.comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op i.Y)))
-- Lean.MetavarContext
/-- Execute `x` with an empty cache, and then restore the original cache.  -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.withFreshCache : {α : Type} → Lean.MetavarContext.MkBinding.M α → Lean.MetavarContext.MkBinding.M α
-- Init.Data.Int.LemmasAux
Int.natCast_nonpos_iff : ∀ {n : ℕ}, ↑n ≤ 0 ↔ n = 0
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.normalizer_commutator_ge_left : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), H₁ ≤ Subgroup.normalizer ↑⁅H₁, H₂⁆
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a fallback : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).getKeyD a fallback =
        if compare k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.out_top : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M], ⊤.out = 1
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxKeyD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : α),
  x.maxKeyD x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => k
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => r.maxKeyD fallback
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.ExtDTreeMap.Const.minEntry : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α (fun x => β) cmp) → t ≠ ∅ → α × β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fap.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fn : Lean.Name} {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13} {fn_1 : Lean.Name}
  {args_1 : Array (Lean.Compiler.LCNF.Arg pu)}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13},
  Lean.Compiler.LCNF.LetValue.fap fn args h = Lean.Compiler.LCNF.LetValue.fap fn_1 args_1 h_1 →
    fn = fn_1 ∧ args = args_1
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_right_of_le' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atTop → (∀ᶠ (x : α) in l, C ≤ g x) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.RingTheory.WittVector.Teichmuller
_private.Mathlib.RingTheory.WittVector.Teichmuller.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A metavariable. This key matches with anything.  -/
Lean.Meta.RefinedDiscrTree.Key.star : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f f_1 : α → C),
  f = f_1 →
    ∀ (a a_1 : ℕ),
      a = a_1 →
        CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f a =
          CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f_1 a_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.getKey? a).isSome = true ↔ a ∈ t
-- Mathlib.Data.Rat.Defs
Rat.ofInt_eq_cast : ∀ (n : ℤ), Rat.ofInt n = ↑n
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.toEnd : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → String.Legacy.Iterator.ValidFor (r.reverse ++ l) [] it.toEnd
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : (F ⨿ G).obj a),
  (CategoryTheory.FunctorToTypes.binaryCoproductEquiv F G a) z =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a)) z
-- Init.Data.String.Bootstrap
/-- Returns a new string that contains only the character `c`.

Because strings are encoded in UTF-8, the resulting string may take multiple bytes.

Examples:
* `String.singleton 'L' = "L"`
* `String.singleton ' ' = " "`
* `String.singleton '"' = "\""`
* `String.singleton '𝒫' = "𝒫"`
 -/
String.singleton : Char → String
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.eraseLead 0 = 0
-- Lean.Meta.Sym.Pattern
/-- If a metavariable is in this collection, when we perform the assignment `?m := v`,
we must check whether their types are compatible.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mvarsToCheckType : Lean.Meta.Sym.DefEqM.Context✝ → Array Lean.MVarId
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of reflecting effective epimorphisms.
 -/
CategoryTheory.Functor.ReflectsEffectiveEpis : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Data.ENat.Basic
instNontrivialENat : Nontrivial ℕ∞
-- Mathlib.Topology.Algebra.Order.Group
ContinuousWithinAt.abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => |f x|) s x
-- Lean.Data.Name
Lean.Name.isSuffixOf : Lean.Name → Lean.Name → Bool
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- `MeasurableSpace` structure generated by `TopologicalSpace`.  -/
borel : (α : Type u) → [TopologicalSpace α] → MeasurableSpace α
-- Mathlib.Algebra.Order.Group.Synonym
toDual_eq_one : ∀ {α : Type u_1} [inst : One α] {a : α}, OrderDual.toDual a = 1 ↔ a = 1
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Set.IsPWO.addSubmonoid_closure : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] {s : Set α},
  (∀ x ∈ s, 0 ≤ x) → s.IsPWO → (↑(AddSubmonoid.closure s)).IsPWO
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_indicator_ne_zero : ∀ {α : Type u_1} {f : α → NNReal}, Summable f → ∀ {s : Set α}, (∃ a ∈ s, f a ≠ 0) → ∑' (x : α), s.indicator f x ≠ 0
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vle_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x x' y y' : R}, x ≤ᵥ y → x' ≤ᵥ y' → x * x' ≤ᵥ y * y'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filterMap f t) k = (Std.DTreeMap.Raw.Const.get? t k).bind (f k')
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A version of `Circuit.strong_multi_elimination` where the collection of circuits is
a `Set (Set α)` and the distinguished elements are a `Set α`, rather than both being indexed.  -/
Matroid.IsCircuit.strong_multi_elimination_set : ∀ {α : Type u_1} {M : Matroid α} {C₀ : Set α},
  M.IsCircuit C₀ →
    ∀ (X : Set α) (S : Set (Set α)) (z : α),
      (∀ C ∈ S, M.IsCircuit C) →
        X ⊆ C₀ →
          (∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}) → z ∈ C₀ → (∀ C ∈ S, z ∉ C) → ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
-- Init.Data.Range.Polymorphic.PRange
/-- A range of elements of `α` with a closed lower bound and an open upper bound.

`a...b` or `a...<b` is the range of all values greater than or equal to `a : α` and
less than `b : α`. This is notation for `Rco.mk a b`.
 -/
Std.Rco : Type u → Type u
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofSurjective.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (val val_1 : ι → S) (e_val : val = val_1) (h : Function.Surjective ⇑(MvPolynomial.aeval val)),
  Algebra.Generators.ofSurjective val h = Algebra.Generators.ofSurjective val_1 ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} [inst_3 : Inhabited (β k)],
  m.WF → (Std.DHashMap.Raw.filter f m).get! k = (Option.filter (f k) (m.get? k)).get!
-- Mathlib.Topology.Instances.Int
Int.instDist : Dist ℤ