mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_comp_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜),
  (iteratedDeriv n fun z => f (z - s)) = fun t => iteratedDeriv n f (t - s)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_of_continuous : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] {f : X → R} {g : ContinuousMapZero X R} (hf : Continuous f) (hf₀ : f 0 = 0),
  ContinuousMapZero.mkD f g = { toFun := f, continuous_toFun := hf, map_zero' := hf₀ }
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.continuousAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → ContinuousAt f x
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.instIsMultiplicativeInnerFibrations : SSet.innerFibrations.IsMultiplicative
-- Init.Core
/-- Indicates that a task should be scheduled on a dedicated thread.

Any priority higher than `Task.Priority.max` will result in the task being scheduled
immediately on a dedicated thread. This is particularly useful for long-running and/or
I/O-bound tasks since Lean will, by default, allocate no more non-dedicated workers
than the number of cores to reduce context switches.
 -/
Task.Priority.dedicated : Task.Priority
-- Init.Data.Int.Linear
Int.lcm.eq_1 : ∀ (m n : ℤ), m.lcm n = m.natAbs.lcm n.natAbs
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.node.sizeOf_spec : ∀ (step : Aesop.Script.Step) (index : ℕ) (children : Array Aesop.Script.StepTree),
  sizeOf (Aesop.Script.StepTree.node step index children) = 1 + sizeOf step + sizeOf index + sizeOf children
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piFinTwo_apply : ∀ (R : Type u) [inst : Semiring R] (M : Fin 2 → Type v) [inst_1 : (i : Fin 2) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin 2) → Module R (M i)], ⇑(LinearEquiv.piFinTwo R M) = fun f => (f 0, f 1)
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- If `f` is a modular form and `f'` a cusp form, then `petersson k f f'` is bounded.  -/
CuspFormClass.petersson_bounded_right : ∀ (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F')
  [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] [ModularFormClass F Γ k]
  [CuspFormClass F' Γ k], ∃ C, ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.preimage_ofSnowflaking_closedEBall`. -/
Metric.Snowflaking.preimage_ofSnowflaking_emetricClosedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.closedEBall x r =
    Metric.closedEBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.Topology.Algebra.Monoid
/-- The continuous map `fun y => y * x`  -/
ContinuousMap.mulRight : {X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Mul X] → [SeparatelyContinuousMul X] → X → C(X, X)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ},
  Filter.Tendsto g y z → Filter.Tendsto f x y → Filter.Tendsto (g ∘ f) x z
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.mk.inj : ∀ {G : Type u} {inst : TopologicalSpace G} {H : Type v} {inst_1 : TopologicalSpace H} {inst_2 : Mul G} {inst_3 : Mul H}
  {toMulEquiv : G ≃* H}
  {continuous_toFun : autoParam (Continuous toMulEquiv.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toMulEquiv.invFun) Homeomorph.continuous_invFun._autoParam}
  {toMulEquiv_1 : G ≃* H}
  {continuous_toFun_1 : autoParam (Continuous toMulEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toMulEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam},
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 } →
    toMulEquiv = toMulEquiv_1
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The identity partial map.  -/
AlgebraicGeometry.Scheme.PartialMap.id : (X : AlgebraicGeometry.Scheme) → X.PartialMap X
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.unitsEquivUnitsType.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M),
  S.unitsEquivUnitsType =
    {
      toFun := fun x =>
        match x with
        | ⟨val, h⟩ =>
          { val := ⟨(Units.coeHom M) val, ⋯⟩, inv := ⟨(Units.coeHom M) val⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ },
      invFun := fun x => ⟨{ val := ↑↑x, inv := ↑↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.Basic
Pi.cstarRing' : ∀ {ι : Type u_4} {R₁ : Type u_5} [inst : NonUnitalNormedRing R₁] [inst_1 : StarRing R₁] [CStarRing R₁]
  [inst_3 : Fintype ι], CStarRing (ι → R₁)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Commutativity of addition in commutative subobjects.  -/
setLike_add_comm : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Add M] [inst_2 : AddMemClass S M] {s : S}
  [IsAddCommutative ↥s] ⦃a b : M⦄, a ∈ s → b ∈ s → a + b = b + a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.source_subset_preimage_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.source ⊆ ↑e ⁻¹' e.target
-- Mathlib.Data.Finsupp.Lex
/-- The partial order on `Finsupp`s obtained by the colexicographic ordering.
See `Finsupp.Colex.linearOrder` for a proof that this partial order is in fact linear.  -/
Finsupp.Colex.partialOrder : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LinearOrder α] → [PartialOrder N] → PartialOrder (Colex (α →₀ N))
-- Init.Data.Float.Model.Float
/-- Converts a `UInt8` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofUInt8 : UInt8 → Float.Model
-- Mathlib.Algebra.Group.Units.Defs
/-- The inverse of a unit in a `Monoid`.  -/
Units.instInv : {α : Type u} → [inst : Monoid α] → Inv αˣ
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.cons_congr : ∀ {α : Type u} {s t : Stream'.WSeq α} (a : α), s ~ʷ t → Stream'.WSeq.cons a s ~ʷ Stream'.WSeq.cons a t
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisorsRight M₀
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal.congr_simp : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv =
    NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv
-- Mathlib.Computability.DFA
DFA.accepts.eq_1 : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.accepts = M.acceptsFrom M.start
-- Mathlib.Topology.Bornology.BoundedOperation
add_bounded_of_bounded_of_bounded : ∀ {R : Type u_1} {X : Type u_2} [inst : PseudoMetricSpace R] [inst_1 : Add R] [BoundedAdd R] {f g : X → R},
  (∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C) →
    (∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C) → ∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_exists_ne : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → (∃ y ∈ s, y ≠ x) → s.Nontrivial
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
ContinuousLinearMap.fpowerSeries_apply_add_two : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) (n : ℕ),
  f.fpowerSeries x (n + 2) = 0
-- Lean.Data.Json.Basic
Lean.Json.arr.inj : ∀ {elems elems_1 : Array Lean.Json}, Lean.Json.arr elems = Lean.Json.arr elems_1 → elems = elems_1
-- Lean.Meta.Instances
_private.Lean.Meta.Instances.0.Lean.Meta.mkInstanceKey : Lean.Expr → Lean.MetaM (Array Lean.Meta.InstanceKey)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A semilinear surjection between modules with the module topology is an open quotient map.  -/
IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Ring R] [inst_1 : Ring S]
  {A : Type u_3} [inst_2 : AddCommGroup A] [inst_3 : Module R A] [inst_4 : TopologicalSpace A] [IsModuleTopology R A]
  {B' : Type u_5} [inst_6 : AddCommGroup B'] [inst_7 : Module S B'] [inst_8 : TopologicalSpace B']
  [IsModuleTopology S B'] {σ : R →+* S},
  IsOpenQuotientMap ⇑σ → ∀ (φ : A →ₛₗ[σ] B'), Function.Surjective ⇑φ → IsOpenQuotientMap ⇑φ
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.end_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (ij : ι × ι),
  b.end ij = (Matrix.toLin b b) ((Matrix.stdBasis R ι ι) ij)
-- Std.Http.Internal.Char
Std.Http.Internal.Char.quotedPairChar.eq_3 : ∀ (c : Char),
  (c = '\t' → False) →
    (c = ' ' → False) → Std.Http.Internal.Char.quotedPairChar c = (false || Std.Http.Internal.Char.vchar c)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The left diagonal datum `(H₁, Δ, H₁)`. Not an instance, since `H₂` cannot be inferred.  -/
IsHeckeTriple.diag_left : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂], IsHeckeTriple Δ H₁ H₁
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (Std.DTreeMap.Const.alter t k f).contains k = (f (Std.DTreeMap.Const.get? t k)).isSome
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_nat_mod : ∀ (l : List ℕ) (n : ℕ), l.sum % n = (List.map (fun x => x % n) l).sum % n
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary products.  -/
CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C} [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.holo : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : ModularFormClass F Γ k] (f : F), MDiff ⇑f
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given an additive congruence relation `c` on an `AddMonoid` and a homomorphism `f`
constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces
on the quotient.  -/
AddCon.lift_range : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (H : c ≤ AddCon.ker f), AddMonoidHom.mrange (c.lift f H) = AddMonoidHom.mrange f
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.fintypeQuotientRightRel.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} [inst_1 : Fintype (α ⧸ s)],
  QuotientGroup.fintypeQuotientRightRel =
    Fintype.ofEquiv (α ⧸ s) (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalRing : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [NonUnitalRing Y] → NonUnitalRing (LocallyConstant X Y)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f V).inv)
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (a : α),
  s.erase a = { carrier := ↑s \ ↑(UpperSet.Ici a), lower' := ⋯ }
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), ⇑↑h = ⇑h
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.Analysis.Normed.Group.Uniform
SeminormedCommGroup.to_lipschitzMul : ∀ {E : Type u_2} [inst : SeminormedCommGroup E], LipschitzMul E
-- Mathlib.InformationTheory.KullbackLeibler.Basic
/-- If `μ ≪ ν` and `μ univ = ν univ`, then `toReal` of the Kullback-Leibler divergence is equal to
an integral, without any integrability condition.  -/
InformationTheory.toReal_klDiv_of_measure_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    μ Set.univ = ν Set.univ → (InformationTheory.klDiv μ ν).toReal = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x / y, y)` preserves the measure `μ × ν`.  -/
MeasureTheory.measurePreserving_div_prod : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 / z.2, z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le_csInf' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s t : Set α}, t.Nonempty → t ⊆ s → sInf s ≤ sInf t
-- Mathlib.Topology.Continuous
continuous_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous id
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.isAddUnit_detp_smul_mul_adjp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A B : Matrix n n R} {d : n → R},
  A * B = Matrix.diagonal d →
    IsAddUnit (Matrix.detp 1 A • (B * Matrix.adjp (-1) B) + Matrix.detp (-1) A • (B * Matrix.adjp 1 B))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_right_zero : ∀ {α : Type u_2} [inst : AddGroup α] {b : α}, Finset.preimage 0 (fun x => x + b) ⋯ = {-b}
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_single : ∀ {α : Type u_1} (s : Finset α) (a : α) (n : ℕ) [inst : DecidableEq α], Nat.multinomial s (Pi.single a n) = 1
-- Mathlib.RingTheory.FinitePresentation
RingHom.finitePresentation_algebraMap : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  (algebraMap A B).FinitePresentation ↔ Algebra.FinitePresentation A B
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.coneOfIsRightKanExtension_π : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (c : CategoryTheory.Limits.Cone F),
  (F'.coneOfIsRightKanExtension α c).π = F'.liftOfIsRightKanExtension α ((CategoryTheory.Functor.const D).obj c.pt) c.π
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ENNReal.eventually_pow_one_div_le : ∀ {x : ENNReal}, x ≠ ⊤ → ∀ {y : ENNReal}, 1 < y → ∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- Whether a graph is `n`-partite, which is whether its vertex set
can be partitioned in at most `n` independent sets.  -/
SimpleGraph.Partitionable : {V : Type u} → SimpleGraph V → ℕ → Prop
-- Mathlib.SetTheory.ZFC.Class
Class.sUnion_empty : ∅.sUnion = ∅
-- Init.Data.SInt.Lemmas
Int16.toBitVec_toUInt16 : ∀ (x : Int16), x.toUInt16.toBitVec = x.toBitVec
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.joinTypes? : Lean.Expr → Lean.Expr → Option Lean.Expr
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonVersionedTextDocumentIdentifier.toJson : Lean.Lsp.VersionedTextDocumentIdentifier → Lean.Json
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center : ∀ (z w : UpperHalfPlane) (r : ℝ), cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toArray` always terminates after finitely many steps.
 -/
Std.Iter.toArray : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Array β
-- Init.Data.Array.Basic
/-- Returns the first non-`none` result of applying the monadic function `f` to each element of the
array in reverse order, from right to left. Once a non-`none` result is found, no further elements
are checked. Returns `none` if `f` returns `none` for all elements of the array.

Examples:
```lean example
#eval #[1, 2, 0, -4, 1].findSomeRevM? (m := Except String) fun x => do
  if x = 0 then throw "Zero!"
  else if x < 0 then return (some x)
  else return none
```
```output
Except.ok (some (-4))
```
```lean example
#eval #[1, 2, 0, 4, 1].findSomeRevM? (m := Except String) fun x => do
  if x = 0 then throw "Zero!"
  else if x < 0 then return (some x)
  else return none
```
```output
Except.error "Zero!"
```
 -/
Array.findSomeRevM? : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m (Option β)) → Array α → m (Option β)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_mul_mk : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] (x y : R),
  QuadraticAlgebra.omega * { re := x, im := y } = { re := a * y, im := x + b * y }
-- Mathlib.Topology.UniformSpace.Basic
/-- If `s ∈ 𝓤 α`, then for any natural `n`, for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ○ ... ○ t ⊆ s` (`n` compositions).  -/
eventually_uniformity_iterate_comp_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∀ (n : ℕ), ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, (fun x => t.comp x)^[n] t ⊆ s
-- Mathlib.Data.Finite.Defs
/-- **Alias** of the reverse direction of `not_infinite_iff_finite`. -/
Finite.not_infinite : ∀ {α : Sort u_1}, Finite α → ¬Infinite α
-- Mathlib.Algebra.Quaternion
Quaternion.im_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] (a : Quaternion R) [inst_1 : SMulZeroClass S R] (s : S),
  (s • a).im = s • a.im
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instBaseSMulZeroClass : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_5} →
      [inst : PartialOrder Γ] →
        [inst_1 : AddCommMonoid V] → [inst_2 : SMulZeroClass R V] → SMulZeroClass R (HahnModule Γ R V)
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- The universal property of free modules: giving a function `(ChooseBasisIndex R M) → N`, for `N`
an `R`-module, is the same as giving an `R`-linear map `M →ₗ[R] N`.

This definition is parameterized over an extra `Semiring S`,
such that `SMulCommClass R S M'` holds.
If `R` is commutative, you can set `S := R`; if `R` is not commutative,
you can recover an `AddEquiv` by setting `S := ℕ`.
See library note [bundled maps over different rings].  -/
Module.Free.constr : (R : Type u) →
  (M : Type v) →
    (N : Type z) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Module.Free R M] →
              [inst_4 : AddCommMonoid N] →
                [inst_5 : Module R N] →
                  {S : Type z} →
                    [inst_6 : Semiring S] →
                      [inst_7 : Module S N] →
                        [inst_8 : SMulCommClass R S N] → (Module.Free.ChooseBasisIndex R M → N) ≃ₗ[S] M →ₗ[R] N
-- Batteries.Data.BitVec.Basic
/-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering.  -/
BitVec.ofFnLE : {n : ℕ} → (Fin n → Bool) → BitVec n
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instIdempotentOpMeet : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.IdempotentOp fun x1 x2 => Lean.Order.meet x1 x2
-- Init.Core
NonScalar.mk.sizeOf_spec : ∀ (val : ℕ), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.HasWeakLimit.mk : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C}
  (d : CategoryTheory.Limits.WeakLimitCone F), CategoryTheory.Limits.HasWeakLimit F
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.sigmaImp.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (n : ℕ) × L.BoundedFormula α n → (n : ℕ) × L.BoundedFormula α n → Sort u_4) →
      (x x_1 : (n : ℕ) × L.BoundedFormula α n) →
        ((m : ℕ) → (φ : L.BoundedFormula α m) → (n : ℕ) → (ψ : L.BoundedFormula α n) → motive ⟨m, φ⟩ ⟨n, ψ⟩) →
          motive x x_1
-- Init.Grind.Offset
Lean.Grind.isLt : ℕ → ℕ → Bool
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_norm_iff : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.MemLp (fun x => ‖f x‖) p μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.Data.Num.Basic
/-- `bit b n` appends the bit `b` to the end of `n`, where `bit tt x = x1` and `bit ff x = x0`.  -/
Num.bit : Bool → Num → Num
-- Lean.DocString.Types
Lean.Doc.instReprListItem.repr : {α : Type u_1} → [Repr α] → Lean.Doc.ListItem α → ℕ → Std.Format
-- Mathlib.Analysis.Complex.CanonicalDecomposition
_private.Mathlib.Analysis.Complex.CanonicalDecomposition.0.Complex.sum_apply_smul_single_eq_self : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : DecidableEq X] {U : Set X}
  {F : Function.locallyFinsuppWithin U ℤ} (h : F.support.Finite),
  ∑ x ∈ h.toFinset, F x • Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single x 1) ⋯ = F
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (f g : X ⟶ Y), f.left = g.left → f.right = g.right → f = g
-- Init.System.IO
/-- Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is
encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from
the handle may block and/or return data.
 -/
IO.FS.Handle.readBinToEndInto : IO.FS.Handle → ByteArray → IO ByteArray