mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.prec.injEq : ∀ (a a_1 a_2 a_3 : Nat.Partrec.Code), (a.prec a_1 = a_2.prec a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.List.Basic
List.filterTR.loop : {α : Type u} → (α → Bool) → List α → List α → List α
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsCompleteMultipartite.comap : ∀ {α : Type u} {G : SimpleGraph α} {β : Type u_1} {H : SimpleGraph β} (f : H ↪g G),
  G.IsCompleteMultipartite → H.IsCompleteMultipartite
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Relation between two elements in `S.arrow`, the data of which
involves a commutative square.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → S.Arrow → S.Arrow → Type (max u v)
-- Mathlib.FieldTheory.KummerExtension
rootsOfUnityEquivOfPrimitiveRoots.congr_simp : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_7} {F : Type u_8} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [inst_5 : MonoidHomClass F R S] {n : ℕ} [inst_6 : NeZero n] {f f_1 : F}
  (e_f : f = f_1) (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty),
  rootsOfUnityEquivOfPrimitiveRoots hf hζ = rootsOfUnityEquivOfPrimitiveRoots ⋯ hζ
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instNontrivialOfIsReduced : ∀ (K : Type u) [inst : CommRing K] [IsReduced K] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP K p]
  [Nontrivial K], Nontrivial (PerfectClosure K p)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.lhomWithConstants_injective : ∀ (L : FirstOrder.Language) (α : Type w'), (L.lhomWithConstants α).Injective
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.mk.inj : ∀ {L : FirstOrder.Language} {M : Type u_1} {inst : L.Structure M} {toSubstructure : L.Substructure M}
  {isElementary' : toSubstructure.IsElementary} {toSubstructure_1 : L.Substructure M}
  {isElementary'_1 : toSubstructure_1.IsElementary},
  { toSubstructure := toSubstructure, isElementary' := isElementary' } =
      { toSubstructure := toSubstructure_1, isElementary' := isElementary'_1 } →
    toSubstructure = toSubstructure_1
-- Mathlib.Algebra.Lie.TraceForm
/-- The orthogonal complement of an ideal with respect to the killing form is an ideal.  -/
LieIdeal.killingCompl : (R : Type u_1) →
  (L : Type u_3) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L → LieIdeal R L
-- Init.System.IO
IO.FS.FileType.symlink.sizeOf_spec : sizeOf IO.FS.FileType.symlink = 1
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.pullbackMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X₁ X₂ S : C}
  (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.pullback f₁ f₂)),
  ∃ x₁ x₂,
    ∃ (h : (CategoryTheory.ConcreteCategory.hom f₁) x₁ = (CategoryTheory.ConcreteCategory.hom f₂) x₂),
      x = CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_lt_cons : ∀ {α : Type u_1} {s t : Multiset α} (a : α), s < t → a ::ₘ s < a ::ₘ t
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- Every positive `x` is between two successive integer powers of
another `y` greater than one. This is the same as `exists_mem_Ico_zpow`,
but with ≤ and < the other way around.  -/
exists_mem_Ioc_zpow : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K}
  [ExistsAddOfLE K], 0 < x → 1 < y → ∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.getBinderIds : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const : ∀ {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] (r : R) (a : A),
  autoParam (p a) cfc_const._auto_1 → cfc (fun x => r) a = (algebraMap R A) r
-- Mathlib.Order.WithBot
WithTop.untop_le_untop_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α} (hy : y ≠ ⊤) (hx : x ≠ ⊤), y.untop hy ≤ x.untop hx ↔ y ≤ x
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.toArray_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α}, r.iter.toArray = r.toArray
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isTop_toDual_iff`. -/
IsBot.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsTop (OrderDual.toDual a)
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.localizedModuleFunctor.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  ModuleCat.localizedModuleFunctor S =
    { obj := fun M => M.localizedModule S, map := fun {X Y} => ModuleCat.localizedModuleMap S, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instPreorder : {α : Type u_1} → [Preorder α] → Preorder αᵐᵒᵖ
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.mem_toArray_iff_isPlausibleIndirectOutput : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.LawfulDeterministicIterator α Id]
  {it : Std.Iter β} {out : β}, out ∈ it.toArray ↔ it.IsPlausibleIndirectOutput out
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.measurable_gaussianPDF : ∀ (μ : ℝ) (v : NNReal), Measurable (ProbabilityTheory.gaussianPDF μ v)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with addition.  -/
Real.circleAverage_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f₁ c R →
    CircleIntegrable f₂ c R → Real.circleAverage (f₁ + f₂) c R = Real.circleAverage f₁ c R + Real.circleAverage f₂ c R
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertFormatPart : Std.Time.FormatPart → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.RingTheory.Ideal.Operations
Submodule.set_smul_top_eq_span : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R), s • ⊤ = Ideal.span s
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.erase a)