mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Limits
Action.zero_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : Action V G}, Action.Hom.hom 0 = 0
-- Mathlib.Topology.MetricSpace.Dilation
/-- The `ratio` is equal to the distance ratio for any two points with nonzero finite distance.
`dist` and `nndist` versions below  -/
Dilation.ratio_unique : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
  edist x y ≠ 0 → edist x y ≠ ⊤ → edist (f x) (f y) = ↑r * edist x y → r = Dilation.ratio f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.right =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.right)
-- Mathlib.Data.Fintype.Basic
PLift.fintypeProp : (p : Prop) → [Decidable p] → Fintype (PLift p)
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.div_comp : ∀ {M : Type u_2} {N : Type u_3} {G : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommGroup G]
  (f g : N →* G) (h : M →* N), (f / g).comp h = f.comp h / g.comp h
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly : BEq Lean.Grind.CommRing.Poly
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β},
  H.IsInducedSubgraph G → (¬H.IsClosedSubgraph G ↔ ∃ e x y, G.IsLink e x y ∧ x ∈ H.vertexSet ∧ y ∉ H.vertexSet)
-- Mathlib.Algebra.Order.UpperLower
UpperSet.Ici_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], UpperSet.Ici 0 = 0
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.primeSpectrumProd_symm_inr : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (x : PrimeSpectrum S),
  (PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x) = PrimeSpectrum.comap (RingHom.snd R S) x
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instInhabitedLoogleResult : Inhabited LeanSearchClient.LoogleResult
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.comp_const : ∀ {X Y Z : SSet} (f : X ⟶ Y) (z : Z.obj (Opposite.op { len := 0 })),
  CategoryTheory.CategoryStruct.comp f (SSet.const z) = SSet.const z
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_congr : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] (f g : α → M),
  (∀ (a : α), f a = g a) → ∏ a, f a = ∏ a, g a
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.map_id : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {F : Type u_7} [inst_3 : FunLike F M M] {f : F}, LinearMap.IsProj m f → ∀ x ∈ m, f x = x
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_nsmul : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] [inst_3 : ContinuousAdd V]
  (n : ℕ) (K : ConvexBody V), ↑(n • K) = n • ↑K
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D]
  (P : CategoryTheory.ObjectProperty C) [inst_4 : P.IsSerreClass] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms], P.isoModSerre.IsInvertedBy F → P ≤ F.kernel
-- Batteries.Data.Array.Basic
/-- Find the first maximal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.maxD : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskerRight_app_fst : ∀ {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] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  {F₁ F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerRight f F₂).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁'.obj j) (F₂.obj j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j))
      (f.app j)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.meas_iInter : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {s : ι → Set Ω} [inst : Fintype ι],
  ProbabilityTheory.iIndepSets π μ → (∀ (i : ι), s i ∈ π i) → μ (⋂ i, s i) = ∏ i, μ (s i)
-- Mathlib.Order.Concept
Concept.intent_subset_intent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.intent ⊆ d.intent ↔ d ≤ c
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An inequality of subobjects is witnessed by some morphism between the corresponding objects.  -/
CategoryTheory.Subobject.ofMkLEMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A₁ A₂ : C} →
      (f : A₁ ⟶ B) →
        (g : A₂ ⟶ B) →
          [inst_1 : CategoryTheory.Mono f] →
            [inst_2 : CategoryTheory.Mono g] → CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g → (A₁ ⟶ A₂)
-- Std.Data.DHashMap.Lemmas
/-- Variant of `get_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Const.get_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.DHashMap.map f m},
  Std.DHashMap.Const.get (Std.DHashMap.map f m) k h' = f (m.getKey k ⋯) (Std.DHashMap.Const.get m k ⋯)
-- Lean.Meta.Constructions.SparseCasesOnEq
_private.Lean.Meta.Constructions.SparseCasesOnEq.0.Lean.Meta.isName : Lean.Environment → Lean.Name → Bool
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- maps every element of the W type to a canonical representative  -/
MvQPF.wrepr : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → (MvQPF.P F).W α → (MvQPF.P F).W α
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseMonthNarrow : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Ordinal
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_one_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ Y) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp 1 h) = CategoryTheory.CategoryStruct.comp 1 h
-- Mathlib.Algebra.Group.Shrink
equivShrink_div : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Div α] (x y : α),
  (equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y
-- Mathlib.InformationTheory.Hamming
Hamming.instSMul : {α : Type u_1} → {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → SMul α (β i)] → SMul α (Hamming β)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instAddCommMonoid =
    { toAddSemigroup := LowerSet.addCommSemigroup.toAddSemigroup, toZero := LowerSet.instZero, zero_add := ⋯,
      add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.iInf_rat_gt_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν → ∀ (a : α), ∀ᵐ (b : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, f' =O[l] k' → g' =O[l] k' → (fun x => (f' x, g' x)) =O[l] k'
-- Mathlib.Topology.Instances.PNat
PNat.instMetricSpace : MetricSpace ℕ+
-- Mathlib.RingTheory.PrincipalIdealDomain
isCoprime_of_dvd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] (x y : R),
  ¬(x = 0 ∧ y = 0) → (∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) → IsCoprime x y
-- Mathlib.Data.Set.Card
Set.encard_preimage_val_le_encard_right : ∀ {α : Type u_1} (P Q : Set α), (Subtype.val ⁻¹' Q).encard ≤ Q.encard
-- Lean.Parser.Level
Lean.Parser.Level.addLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [inst : TopologicalSpace E]
  [TopologicalSpace.MetrizableSpace E] {f g : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.NullMeasurableSet {x | f x = g x} μ
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.instSubringClass : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H],
  SubringClass (VonNeumannAlgebra H) (H →L[ℂ] H)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.pullbacks.IsStableUnderBaseChange
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.coe_snd : ∀ {R : Type u_1} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  ⇑(NonUnitalRingHom.snd R S) = Prod.snd
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_natCast_of_lt : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {n : ℕ}, n < p → (↑n).zmodRepr = n
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.go.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) (i : ℕ),
  Array.compareLex.go✝ cmp a₁ a₂ i =
    if h₁ : a₁.size ≤ i then if a₂.size ≤ i then Ordering.eq else Ordering.lt
    else
      if h₂ : a₂.size ≤ i then Ordering.gt
      else
        match cmp a₁[i] a₂[i] with
        | Ordering.lt => Ordering.lt
        | Ordering.eq => Array.compareLex.go✝ cmp a₁ a₂ (i + 1)
        | Ordering.gt => Ordering.gt
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves uniform equicontinuity on a subset.  -/
UniformEquicontinuousOn.comp : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β]
  {F : ι → β → α} {S : Set β}, UniformEquicontinuousOn F S → ∀ (u : κ → ι), UniformEquicontinuousOn (F ∘ u) S
-- Mathlib.Algebra.Group.Hom.Basic
AddHom.comp_add : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Add M] [inst_1 : AddCommSemigroup N]
  [inst_2 : AddCommSemigroup P] (g : N →ₙ+ P) (f₁ f₂ : M →ₙ+ N), g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`.  -/
mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt : ∀ {𝕜 : 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] [IsManifold I 1 M] {x : M} {y : E},
  y ∈ (extChartAt I x).target →
    mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
      ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If `α` is non-empty, an action is pretransitive if and only if the quotient has exactly one
element.  -/
MulAction.pretransitive_iff_unique_quotient_of_nonempty : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α] [Nonempty α],
  MulAction.IsPretransitive G α ↔ Nonempty (Unique (MulAction.orbitRel.Quotient G α))
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_hom_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y),
  (z • f).hom = CategoryTheory.CategoryStruct.comp ((↑z).app X) f.hom
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNormClass.toAddGroupNormClass : ∀ {E : Type u_3} {F : Type u_4} [inst : FunLike F E ℝ] [inst_1 : AddGroup E] [NonarchAddGroupNormClass F E],
  AddGroupNormClass F E ℝ
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.standard : Lean.Name → String → Lean.ExternEntry
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_pi : ∀ {η : Type u_2} {G : η → Type u_3} [inst : (i : η) → Group (G i)],
  Subgroup.center ((i : η) → G i) = Subgroup.pi Set.univ fun i => Subgroup.center (G i)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform.0.Finpartition.aux : ∀ {i j : ℕ}, 0 < j → j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.insert_of_notMem : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i : ι}, i ∉ s → (∀ j ∈ s, Disjoint (f i) (f j)) → (insert i s).PairwiseDisjoint f
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapIdx.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_1 acc
-- Mathlib.Order.SupClosed
latticeClosure_empty : ∀ {α : Type u_3} [inst : Lattice α], latticeClosure ∅ = ∅
-- Mathlib.RingTheory.RingHom.FiniteType
/-- If `S` is a finite type `R`-algebra, then `S' = M⁻¹S` is a finite type `R' = M⁻¹R`-algebra.  -/
RingHom.finiteType_localizationPreserves : RingHom.LocalizationPreserves @RingHom.FiniteType
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsTransitive.iUnion : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] {f : α → ZFSet.{u}},
  (∀ (i : α), (f i).IsTransitive) → (ZFSet.iUnion fun i => f i).IsTransitive
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_sup_prod : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M) {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (q₁ q₁' : Submodule R M'),
  p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The length of the `i`th row in `ofRowLens w hw` is the `i`th entry of `w`  -/
YoungDiagram.rowLen_ofRowLens : ∀ {w : List ℕ} {hw : w.SortedGE} (i : Fin w.length), (YoungDiagram.ofRowLens w hw).rowLen ↑i = w[i]
-- Mathlib.RingTheory.Unramified.Basic
/-- An `R`-algebra `A` is unramified if it is formally unramified and of finite type.  -/
Algebra.Unramified : (R : Type u_1) → [inst : CommRing R] → (A : Type u_2) → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.isUnit_inv_iff : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] [inst_4 : SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M}, IsUnit x⁻¹ ↔ IsUnit x
-- Init.Prelude
/-- Sequences two computations, allowing the second to depend on the value computed by the first.

If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the result of executing `x` to get
a value of type `α` and then passing it to `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `>>=` in identifiers is `bind`. -/
Bind.bind : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} → m α → (α → m β) → m β
-- Mathlib.Topology.Defs.Induced
instTopologicalSpaceSubtype : {X : Type u_1} → {p : X → Prop} → [t : TopologicalSpace X] → TopologicalSpace (Subtype p)
-- Lean.Syntax
_private.Lean.Syntax.0.Lean.Syntax.chooseNiceTrailStop : Substring.Raw → String.Pos.Raw
-- Init.Prelude
Nat.le_succ : ∀ (n : ℕ), n ≤ n.succ
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This typeclass provides the function `succ? : α → Option α` that computes the successor of
elements of `α`, or none if no successor exists.
It also provides the function `succMany?`, which computes `n`-th successors.

`succ?` is expected to be acyclic: No element is its own transitive successor.
If `α` is ordered, then every element larger than `a : α` should be a transitive successor of `a`.
These properties and the compatibility of `succ?` with `succMany?` are encoded in the typeclasses
`LawfulUpwardEnumerable`, `LawfulUpwardEnumerableLE` and `LawfulUpwardEnumerableLT`.

 -/
Std.PRange.UpwardEnumerable : Type u → Type u
-- Init.Core
instInhabitedForInStep.default : {α : Type u} → [Inhabited α] → ForInStep α
-- Mathlib.Order.Minimal
Minimal.not_lt : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : Preorder α], Minimal P x → P y → ¬y < x
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Given a refl quiver `V`, this is the refl functor `V ⥤rq FreeRefl V` which
is the counit of the adjunction between reflexive quivers and categories.  -/
CategoryTheory.Cat.toFreeRefl : (V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → V ⥤rq CategoryTheory.Cat.FreeRefl V
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_4 : ∀ (x : Turing.PartrecToTM2.Cont') (f fs : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.codeSupp' (f.cons fs) x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.cons fs) x) ∪
      (Turing.PartrecToTM2.codeSupp' f (Turing.PartrecToTM2.Cont'.cons₁ fs x) ∪
        (Turing.PartrecToTM2.trStmts₁
            (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
              (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ))
                Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main
                (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
                  (Turing.PartrecToTM2.trNormal fs x.cons₂)))) ∪
          (Turing.PartrecToTM2.codeSupp' fs x.cons₂ ∪
            Turing.PartrecToTM2.trStmts₁
              (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret x)))))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight W)],
  CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂ =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_sub_pi : ∀ (θ : Real.Angle), (θ - ↑Real.pi).sign = -θ.sign
-- Lean.Level
Lean.instBEqLevelMVarId : BEq Lean.LevelMVarId
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The images of `f : Arrow C` by two isomorphic functors `F : C ⥤ D` are
isomorphic arrows in `D`.  -/
CategoryTheory.Arrow.isoOfNatIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ≅ G) → (f : CategoryTheory.Arrow C) → F.mapArrow.obj f ≅ G.mapArrow.obj f
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.instIsProperOfIsFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f], AlgebraicGeometry.IsProper f
-- Batteries.Control.LawfulMonadState
/-- Setting the monad state to its current value has no effect.  -/
LawfulMonadStateOf.get_bind_set_bind : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] {α : Type u_1} (mx : σ → PUnit.{u_1 + 1} → m α),
  (do
      let s ← get
      let u ← set s
      mx s u) =
    do
    let s ← get
    mx s PUnit.unit
-- Mathlib.Order.Heyting.Basic
hnot_ne_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α} [Nontrivial α], ￢a ≠ a
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotationCoeff.eq_def : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) (x : ℕ),
  WittVector.frobeniusRotationCoeff p ha₁ ha₂ x =
    match x with
    | 0 => WittVector.RecursionBase.solution p a₁ a₂
    | n.succ =>
      WittVector.RecursionMain.succNthVal p n a₁ a₂ (fun i => WittVector.frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂
-- Std.Data.DTreeMap.Basic
/-- Computes the intersection of the given tree maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map.
 -/
Std.DTreeMap.inter : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupComap_apply_coe : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H' : Subgroup G')
  (x : ↥(Submonoid.comap f H'.toSubmonoid)), ↑((f.subgroupComap H') x) = f ↑x
-- Batteries.Data.String.Legacy
/-- Removes the specified number of characters (Unicode code points) from the start of the string.

If `n` is greater than `s.length`, returns `""`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.drop`.

Examples:
 * `"red green blue".drop 4 = "green blue"`
 * `"red green blue".drop 10 = "blue"`
 * `"red green blue".drop 50 = ""`
 -/
String.Legacy.drop : String → ℕ → String
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `f = g`, then `map f` is naturally isomorphic to `map g`.  -/
CategoryTheory.Over.mapCongr : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} → (f g : X ⟶ Y) → f = g → (CategoryTheory.Over.map f ≅ CategoryTheory.Over.map g)
-- Init.Data.UInt.Bitwise
UInt16.ofFin_xor : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a ^^^ b) = UInt16.ofFin a ^^^ UInt16.ofFin b
-- Lean.Util.CollectAxioms
/-- Axioms accumulated for the current constant being processed.  -/
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.axioms : Lean.CollectAxioms.State✝ → Lean.NameSet
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Construct a heap from a list by inserting all the elements.  -/
Batteries.PairingHeap.ofArray : {α : Type u} → (le : α → α → Bool) → Array α → Batteries.PairingHeap α le
-- Mathlib.Data.Finsupp.Order
Finsupp.bot_eq_zero : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsBotZeroClass α], ⊥ = 0
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.compare.lex : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Ordering