mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.below.of_isAtomic : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop}
  {φ : L.BoundedFormula α n} (h : φ.IsAtomic), FirstOrder.Language.BoundedFormula.IsQF.below ⋯
-- Std.Time.Date.Unit.Week
/-- Convert `Millisecond.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Week.Offset
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.mk.inj : ∀ {toDerive : Lean.NameMap Lean.ExprSet} {toOmit : Array (Lean.Ident × Lean.Name)}
  {toDerive_1 : Lean.NameMap Lean.ExprSet} {toOmit_1 : Array (Lean.Ident × Lean.Name)},
  { toDerive := toDerive, toOmit := toOmit } = { toDerive := toDerive_1, toOmit := toOmit_1 } →
    toDerive = toDerive_1 ∧ toOmit = toOmit_1
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_le_log : ∀ {n : ℕ}, ArithmeticFunction.vonMangoldt n ≤ Real.log ↑n
-- Mathlib.RepresentationTheory.Equiv
Representation.freeLiftLEquiv_symm_apply : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (α : Type w') (f : α → V), (σ.freeLiftLEquiv α).symm f = σ.freeLift f
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The bottom marker is fixed throughout the calculation, so we use the `addBottom` function
to express the program state in terms of a tape with only the stacks themselves.  -/
Turing.TM2to1.addBottom : {K : Type u_1} →
  {Γ : K → Type u_2} → Turing.ListBlank ((k : K) → Option (Γ k)) → Turing.ListBlank (Turing.TM2to1.Γ' K Γ)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
_private.Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite.0.SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding.match_1.eq_1 : ∀ (motive : Fin 3 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()) =
    h_1 ()
-- Mathlib.Tactic.Says
/-- This option is only used in CI to negate `says.verify`.  -/
Mathlib.Tactic.Says.says.no_verify_in_CI : Lean.Option Bool
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `AddSubgroup` generated by a set includes the set.  -/
AddSubgroup.subset_closure : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G}, k ⊆ ↑(AddSubgroup.closure k)
-- Init.Data.Nat.MinMax
Nat.max_eq_left : ∀ {a b : ℕ}, b ≤ a → max a b = a
-- Lean.Meta.Sym.ProofInstInfo
/-- Analyzes the type signature of `declName` and returns information about which arguments
are proofs or instances. Returns `none` if no arguments are proofs or instances.
 -/
Lean.Meta.Sym.mkProofInstInfo? : Lean.Name → Lean.MetaM (Option Lean.Meta.Sym.ProofInstInfo)
-- Mathlib.GroupTheory.GroupAction.Pointwise
Set.MapsTo.smul_setₛₗ : ∀ {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} {s : Set α} {t : Set β},
  Set.MapsTo (⇑f) s t → ∀ (c : M), Set.MapsTo (⇑f) (c • s) (σ c • t)