mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Basic
List.replicate_right_inj : ∀ {α : Type u} {a b : α} {n : ℕ}, n ≠ 0 → (List.replicate n a = List.replicate n b ↔ a = b)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
/-- If `X` is a nonsingular simplicial set, this is the functor
`X.N ⥤ SemiSimplexCategory` which sends a nondegenerate
simplex `s : X.N` to `⦋s.dim⦌ₛ`.  -/
SSet.N.toSemiSimplexCategory : (X : SSet) → [X.Nonsingular] → CategoryTheory.Functor X.N SemiSimplexCategory
-- Init.Data.Order.Ord
Int.instTransOrd : Std.TransOrd ℤ
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instNonAssocSemiring : {R : Type u_1} → {a b : R} → [NonAssocSemiring R] → NonAssocSemiring (QuadraticAlgebra R a b)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.mk : {α : ℕ → ℕ → Type} →
  ({n m : ℕ} → α n m → ℕ → ℕ → ℚ) →
    ({n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m) →
      ({n m : ℕ} → α n m → List (ℕ × ℕ × ℚ)) →
        ({n m : ℕ} → List (ℕ × ℕ × ℚ) → α n m) →
          ({n m : ℕ} → α n m → ℕ → ℕ → α n m) →
            ({n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m) →
              ({n m : ℕ} → α n m → ℕ → ℚ → α n m) → Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α
-- Mathlib.Order.Filter.Basic
Filter.neBot_sup_of_left : ∀ {α : Type u} {f g : Filter α} [f.NeBot], (f ⊔ g).NeBot
-- Mathlib.Topology.FiberBundle.Basic
/-- An arbitrary homeomorphism between any fiber and the model fiber.
This is useful to transfer topological properties of the model fiber.  -/
FiberBundle.homeomorphAt : {B : Type u_2} →
  (F : Type u_3) →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        (E : B → Type u_5) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] → [FiberBundle F E] → (b : B) → E b ≃ₜ F
-- Mathlib.Computability.TuringMachine.Tape
/-- The tape of a Turing machine is composed of a head element (which we imagine to be the
current position of the head), together with two `ListBlank`s denoting the portions of the tape
going off to the left and right. When the Turing machine moves right, an element is pulled from the
right side and becomes the new head, while the head element is `cons`ed onto the left side.  -/
Turing.Tape : (Γ : Type u_1) → [Inhabited Γ] → Type u_1
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A (preadditive) category `C` is called abelian if it has all finite products,
all kernels and cokernels, and if every monomorphism is the kernel of some morphism
and every epimorphism is the cokernel of some morphism.

(This definition implies the existence of zero objects:
finite products give a terminal object, and in a preadditive category
any terminal object is a zero object.)
 -/
CategoryTheory.Abelian : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- A constructor for isomorphisms in CatCommSqOver  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} →
                      (eₗ : S.fst ≅ S'.fst) →
                        (eᵣ : S.snd ≅ S'.snd) →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F)
                                  S'.iso.hom =
                                CategoryTheory.CategoryStruct.comp S.iso.hom
                                  (CategoryTheory.Functor.whiskerRight eᵣ.hom G))
                              CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso._auto_1 →
                            (S ≅ S')
-- Mathlib.Computability.Ackermann
add_add_one_le_ack : ∀ (m n : ℕ), m + n + 1 ≤ ack m n
-- Mathlib.Data.Set.Insert
/-- The powerset of a singleton contains only `∅` and the singleton itself.  -/
Set.powerset_singleton : ∀ {α : Type u_1} (x : α), 𝒫 {x} = {∅, {x}}
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x x' : M} {y : M'}
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (ContMDiffAt I I' n f x' ↔
        ContinuousAt f x' ∧
          ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x'))
-- Mathlib.Combinatorics.Quiver.Covering
/-- Constructor for `Quiver.Star`. Defined to be `Sigma.mk`.  -/
Quiver.Star.mk : {U : Type u_1} → [inst : Quiver U] → {u v : U} → (u ⟶ v) → Quiver.Star u
-- Mathlib.Tactic.NormNum.Basic
/-- `norm_num` extension for `Int.negOfNat`.

It's useful for calling `derive` with the numerator of an `.isNegNNRat` branch.  -/
Mathlib.Meta.NormNum.evalNegOfNat : Mathlib.Meta.NormNum.NormNumExt
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.getLambdaBody : Lean.Expr → Lean.Expr
-- Mathlib.Data.Multiset.ZeroCons
Multiset.recOn_cons : ∀ {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)}
  {C_cons_heq :
    ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)}
  (a : α) (m : Multiset α), (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)
-- Mathlib.Analysis.Complex.CoveringMap
Homeomorph.inv₀.eq_1 : ∀ (G₀ : Type u_3) [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [inst_2 : ContinuousInv₀ G₀],
  Homeomorph.inv₀ G₀ =
    { toFun := fun g => ⟨(↑g)⁻¹, ⋯⟩, invFun := fun g => ⟨(↑g)⁻¹, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.neg_add_eq_neg_add_iff : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a b c d : α},
  IsAddUnit b → IsAddUnit d → (-b + a = -d + c ↔ a + d = c + b)
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_inj : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n] {v w : n → α},
  Matrix.circulant v = Matrix.circulant w ↔ v = w
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZif.repr : Std.Time.TimeZone.TZif.TZif → ℕ → Std.Format
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- The series expansion of the iterated derivative of `π cot (π z)`.  -/
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow : ∀ {k : ℕ},
  1 ≤ k →
    ∀ {z : ℂ},
      z ∈ UpperHalfPlane.upperHalfPlaneSet →
        iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z =
          (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), 1 / (z + ↑n) ^ (k + 1)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instSub : {ι : Type u_1} →
  {I₀ : WithTop (BoxIntegral.Box ι)} →
    {M : Type u_4} → [inst : AddCommGroup M] → Sub (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Init.System.IO
IO.FS.Mode.write.sizeOf_spec : sizeOf IO.FS.Mode.write = 1
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.congr_symm : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} [inst_3 : Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T),
  (WithAbs.congr v w f).symm = WithAbs.congr w v f.symm
-- Mathlib.Data.ZMod.Basic
ZMod.val_neg' : ∀ {n : ZMod 0}, (-n).val = n.val
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_smul_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  {c : NNReal} (hc : c ≠ 0), (c • μ').addHaarScalarFactor (c • μ) = μ'.addHaarScalarFactor μ
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G}
  (Γ : (CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ)) (a : B),
  (CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax Γ).app a = Γ.app a
-- Mathlib.Algebra.Polynomial.Basic
IsSMulRegular.polynomial : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] {a : S},
  IsSMulRegular R a → IsSMulRegular (Polynomial R) a
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A finite group of prime order is simple.  -/
isSimpleGroup_of_prime_card : ∀ {α : Type u_1} [inst : Group α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α = p → IsSimpleGroup α
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- Any invertible matrix rescales Lebesgue measure through the absolute value of its
determinant.  -/
Real.map_matrix_volume_pi_eq_smul_volume_pi : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : Matrix ι ι ℝ},
  M.det ≠ 0 →
    MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume =
      ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume
-- Std.Sync.Broadcast
/-- `ch.forAsync f` calls `f` for every message received on `ch`.

Note that if this function is called twice, each message will only arrive at exactly one invocation.
 -/
Std.Broadcast.Receiver.forAsync : {α : Type} →
  (α → BaseIO Unit) → Std.Broadcast.Receiver α → optParam Task.Priority Task.Priority.default → BaseIO (Task Unit)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_piUnique : ∀ {ι : Type u_1} [inst : Fintype ι] (X : ι → Type u_4) [inst_1 : Unique ι]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (X i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique X)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j) =
    CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjCyclesSelfIso c j B).inv
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_inj : ∀ {p q : NNReal}, ↑p = ↑q ↔ p = q
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) [inst_2 : CategoryTheory.IsFiltered J] (j j' : J) (α : j ⟶ j') (β : i₀ ⟶ j'),
  h.coconeιApp j = CategoryTheory.CategoryStruct.comp (F.map α) (h.isoMap β ⋯).inv
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKeyD : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → α → α
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.sieve₀_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  (CategoryTheory.PreOneHypercover.cylinder f g).sieve₀ =
    CategoryTheory.Sieve.generate
      (CategoryTheory.Presieve.bindOfArrows E.X E.f fun i =>
        (CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯)
            (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
-- Mathlib.Order.Hom.Basic
OrderIso.symm_trans : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (e₁ : α ≃o β)
  (e₂ : β ≃o γ), (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.applyComposition_single : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : 0 < n) (v : Fin n → E),
  p.applyComposition (Composition.single n hn) v = fun _j => (p n) v
-- Lean.Meta.Basic
Lean.Meta.mkFreshLevelMVars : ℕ → Lean.MetaM (List Lean.Level)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, (t.getThenInsertIfNew? k v).1 = t.get? k
-- Mathlib.Condensed.Light.Epi
LightCondMod.factorsThru_lightProfinite_epi_of_epi : ∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) [CategoryTheory.Epi f] {S : LightProfinite}
  (p : (LightCondensed.free R).obj S.toCondensed ⟶ Y),
  ∃ T π g,
    CategoryTheory.Epi π ∧
      CategoryTheory.CategoryStruct.comp ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π) p =
        CategoryTheory.CategoryStruct.comp g f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapAddMon_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapAddMon.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddMonIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddMonNatTrans a.unit)
        CategoryTheory.Functor.mapAddMonCompIso.hom)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {E : Type u₂} [inst_4 : CategoryTheory.Category.{v₂, u₂} E]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E) {A B : C},
  CategoryTheory.CartesianMonoidalCategory.prodComparison (F.comp G) A B =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CartesianMonoidalCategory.prodComparison G (F.obj A) (F.obj B))
-- Init.System.IO
/-- Configuration for a child process to be spawned.

Use `IO.Process.spawn` to start the child process. `IO.Process.output` and `IO.Process.run` can be
used when the child process should be run to completion, with its output and/or error code captured.
 -/
IO.Process.SpawnArgs : Type
-- Mathlib.NumberTheory.WellApproximable
UnitAddCircle.mem_addWellApproximable_iff : ∀ (δ : ℕ → ℝ) (x : UnitAddCircle),
  x ∈ addWellApproximable UnitAddCircle δ ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsup` of a function `u` along a filter `f` is a cluster point of `u` along `f`.  -/
MapClusterPt.limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot],
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) MapClusterPt.limsup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) MapClusterPt.limsup._auto_3 →
      MapClusterPt (Filter.limsup u f) f u
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `inf_eq_left`. -/
inf_of_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≤ b → a ⊓ b = a
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_eq_zero : ∀ {α : Type u} [inst : AddMonoid α] {a : AddUnits α}, ↑a = 0 ↔ a = 0
-- Mathlib.Algebra.Ring.Int.Parity
Odd.neg_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y Y' : C} → (X ⟶ Y') → (X ⟶ Y') → (s : Y ⟶ Y') → W s → W.LeftFraction₂ X Y
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A set `A` in a compactly coherent space is open iff for every compact set `K`, the intersection
`K ∩ A` is open in `K`.  -/
CompactlyCoherentSpace.isOpen_iff : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyCoherentSpace X] {A : Set X},
  IsOpen A ↔ ∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' A)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper : (α : Type u) → (α → Type v) → Type (max u v)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) [NoZeroDivisors R],
  (x * y).orderTop = x.orderTop + y.orderTop
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf'_product_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset β} {t : Finset γ}
  (h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).inf' h f = s.inf' ⋯ fun i => t.inf' ⋯ fun i' => f (i, i')
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_4.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_5 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- The induced subgraph of a connected component.  -/
SimpleGraph.ConnectedComponent.toSubgraph : {V : Type u} → {G : SimpleGraph V} → G.ConnectedComponent → G.Subgraph
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackIso_inv_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f]
  (a : (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀),
  (CategoryTheory.PreZeroHypercover.pullbackIso f E).inv.s₀ a = id a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget₂Mon_obj_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.BirationalOver.refl : ∀ {S X : AlgebraicGeometry.Scheme} (sX : X ⟶ S), AlgebraicGeometry.Scheme.BirationalOver sX sX
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.eq_mk : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)),
  ms = Tactic.ComputeAsymptotics.MultiseriesExpansion.mk ms.seq ms.toFun
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects finite limits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteLimits F],
  CategoryTheory.Limits.ReflectsFiniteColimits F.leftOp