mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.waitForExpectedType.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3},
  GaloisConnection (MvPolynomial.zeroLocus K) (MvPolynomial.vanishingIdeal k)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCancelMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CancelMonoid Mᵐᵒᵖ], DomMulAct.instCancelMonoidOfMulOpposite = inst
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mk.inj : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {toTheory : (L.withConstants α).Theory}
  {subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory} {isMaximal' : toTheory.IsMaximal}
  {toTheory_1 : (L.withConstants α).Theory} {subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1}
  {isMaximal'_1 : toTheory_1.IsMaximal},
  { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } =
      { toTheory := toTheory_1, subset' := subset'_1, isMaximal' := isMaximal'_1 } →
    toTheory = toTheory_1
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] {x y : WithTop α},
  x ≤ y → x.pred ≤ y.pred
-- Mathlib.Algebra.Ring.Defs
Distrib.rightDistribClass : ∀ (R : Type u_1) [inst : Distrib R], RightDistribClass R
-- Mathlib.Order.KrullDimension
_private.Mathlib.Order.KrullDimension.0.Order.height_add_const : ∀ {α : Type u_1} [inst : Preorder α] (a : α) (n : ℕ∞),
  Order.height a + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n
-- Mathlib.Data.Nat.GCD.Basic
Nat.div_mul_div : ∀ {n m k : ℕ}, m ∣ k → n ∣ m → k / m * (m / n) = k / n
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprElimAltInfo.repr : Lean.Meta.ElimAltInfo → ℕ → Std.Format
-- Mathlib.NumberTheory.Dioph
Poly.ext_iff : ∀ {α : Type u_1} {f g : Poly α}, f = g ↔ ∀ (x : α → ℕ), f x = g x
-- Mathlib.RingTheory.Spectrum.Prime.TensorProduct
PrimeSpectrum.continuous_tensorProductTo : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T], Continuous (PrimeSpectrum.tensorProductTo R S T)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Notation for the space of bundled `n`-times continuously differentiable
functions with support in a compact set `K`.  -/
Distributions.«term𝓓^{_}_{_}(_,_)» : Lean.ParserDescr
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.false.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α], sizeOf Std.Sat.AIG.Decl.false = 1
-- Mathlib.Data.Rat.Floor
Rat.isNat_intFloor_ofIsNNRat : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ), Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌊r⌋ (n / d)
-- Mathlib.GroupTheory.GroupAction.Support
MulAction.Supports.smul : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group H] [inst_1 : SMul G α] [inst_2 : SMul G β]
  [inst_3 : MulAction H α] [inst_4 : SMul H β] [SMulCommClass G H β] [SMulCommClass G H α] {s : Set α} {b : β} (g : H),
  MulAction.Supports G s b → MulAction.Supports G (g • s) (g • b)
-- Mathlib.Tactic.CategoryTheory.Slice
/-- `slice` is implemented by `evalSlice`.  -/
Mathlib.Tactic.Slice.convSlice___ : Lean.ParserDescr
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setFailIfUnchanged : Lean.Meta.Simp.Context → Bool → Lean.Meta.Simp.Context
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_eq_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {z : ℤ} {a : R},
  ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
-- Mathlib.Algebra.Group.Semiconj.Units
Units.conj_pow : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M) (n : ℕ), (↑u * x * ↑u⁻¹) ^ n = ↑u * x ^ n * ↑u⁻¹
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- `Functor.map` of a monoidal functor as a `AddMonoidHom`.  -/
CategoryTheory.Functor.homAddMonoidHom : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{w, u_2} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {M X : C} →
              [inst_4 : CategoryTheory.AddMonObj M] →
                (F : CategoryTheory.Functor C D) → [inst_5 : F.Monoidal] → (X ⟶ M) →+ (F.obj X ⟶ F.obj M)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- Asymptotic bound for the `Γ` function integrand.  -/
Real.Gamma_integrand_isLittleO : ∀ (s : ℝ), (fun x => Real.exp (-x) * x ^ s) =o[Filter.atTop] fun x => Real.exp (-(1 / 2) * x)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Ordinal.lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a homomorphism `f` from the quotient of a ring by a ring congruence
relation, `f` equals the homomorphism on the quotient induced by `f` composed
with the natural map from the ring to the quotient.  -/
RingCon.lift_apply_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M}
  (f : c.Quotient →+* P), c.lift (f.comp c.mk') ⋯ = f
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
Units.zero_lt : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] (u : αˣ), 0 < ↑u
-- Init.Tactics
/-- `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....
This is a low-level tactic, it will expose how recursive definitions have been
compiled by Lean.
 -/
Lean.Parser.Tactic.delta : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.div : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : DivisionMonoid β] {f f' : α → β},
  HasCompactMulSupport f → HasCompactMulSupport f' → HasCompactMulSupport (f / f')
-- Init.Data.SInt.Lemmas
Int8.toISize_ofNat : ∀ {n : ℕ}, n ≤ 127 → (OfNat.ofNat n).toISize = OfNat.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Maps
Equiv.Set.univ.eq_1 : ∀ (α : Type u_3),
  Equiv.Set.univ α = { toFun := Subtype.val, invFun := fun a => ⟨a, trivial⟩, left_inv := ⋯, right_inv := ⋯ }
-- Aesop.Tree.ExtractProof
Aesop.Goal.extractProof : Aesop.Goal → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addRight_apply : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M), ⇑u.addRight = fun x => x + ↑u
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Fin (orderOf x)` and `Subgroup.zpowers x`, sending `i` to `x ^ i`.  -/
finEquivZPowers : {G : Type u_1} → [inst : Group G] → {x : G} → IsOfFinOrder x → Fin (orderOf x) ≃ ↥(Subgroup.zpowers x)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vlt_mul_iff_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → (x * y <ᵥ x * z ↔ y <ᵥ z)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_mul_apply : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r₁ r₂ : k) (p : P1),
  (AffineMap.homothety c (r₁ * r₂)) p = (AffineMap.homothety c r₁) ((AffineMap.homothety c r₂) p)
-- Std.Time.Format.Basic
Std.Time.Awareness.only.injEq : ∀ (a a_1 : Std.Time.TimeZone), (Std.Time.Awareness.only a = Std.Time.Awareness.only a_1) = (a = a_1)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.prod.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : Group H]
  [inst_3 : TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H),
  U.prod V = { toSubgroup := (↑U).prod ↑V, isOpen' := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.iUnion_eq_of_caratheodory : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (i : ℕ), MeasurableSet (s i)) → Pairwise (Function.onFun Disjoint s) → m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
-- Mathlib.LinearAlgebra.Projection
/-- The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`.  -/
Submodule.projection_eq_self_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x = x ↔ x ∈ p
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F)
  (s : Set E), AnalyticOn 𝕜 (⇑f) s
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.eq_zero_of_isSumSq_of_neg_isSumSq : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [IsFormallyReal R] {s : R}, IsSumSq s → IsSumSq (-s) → s = 0
-- Mathlib.Order.Basic
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version takes `[Max α]` and `[Min α]` as arguments, then uses
them for `max` and `min` fields. See `LinearOrder.lift'` for a version that autogenerates `min` and
`max` fields, and `LinearOrder.liftWithOrd` for one that does not auto-generate `compare`
fields.

See also `Function.Injective.linearOrder` when only the proof fields need to be transferred.

See note [reducible non-instances].  -/
LinearOrder.lift : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder β] →
      [inst_1 : Max α] →
        [inst_2 : Min α] →
          (f : α → β) →
            Function.Injective f →
              (∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) → (∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) → LinearOrder α
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.toNegMemClass : ∀ {S : Type u_1} {R : Type u} {inst : NonUnitalNonAssocRing R} {inst_1 : SetLike S R}
  [self : NonUnitalSubringClass S R], NegMemClass S R
-- Init.Data.List.Find
List.IsPrefix.lookup_eq_some : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {b : β} {l₁ l₂ : List (α × β)},
  l₁ <+: l₂ → List.lookup k l₁ = some b → List.lookup k l₂ = some b
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.tensorUnit_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.WideSubcategory P)).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Data.Multiset.Basic
/-- Analogue of `strongDownwardInduction` with order of arguments swapped.  -/
Multiset.strongDownwardInductionOn : {α : Type u_1} →
  {p : Multiset α → Sort u_3} →
    {n : ℕ} →
      (s : Multiset α) →
        ((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) → s.card ≤ n → p s
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_filter_snd_le_of_le : ∀ {n k : ℕ},
  k ≤ n →
    {a ∈ Finset.HasAntidiagonal.antidiagonal n | a.2 ≤ k} =
      Finset.map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ))
        (Finset.HasAntidiagonal.antidiagonal k)
-- Mathlib.Logic.Equiv.Defs
Equiv.subsingleton.symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton α], Subsingleton β
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωSupImpl_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α × β)),
  (Prod.ωSupImpl c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
/-- The infinite sum in the formula `Nat.Partition.hasProd_genFun` always converges.  -/
Nat.Partition.summable_genFun_term : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] (f : ℕ → ℕ → R) (i : ℕ),
  Summable fun j => f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcompose =
    CategoryTheory.Limits.Cone.ext
      (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cone.postcompose α).obj c)).pt) ⋯
-- Mathlib.Algebra.Group.Graph
/-- The graph of a monoid homomorphism as a submonoid.

See also `MonoidHom.graph` for the graph as a subgroup.  -/
MonoidHom.mgraph : {G : Type u_1} → {H : Type u_2} → [inst : Monoid G] → [inst_1 : Monoid H] → (G →* H) → Submonoid (G × H)
-- Lean.Data.OpenDecl
Lean.instBEqOpenDecl : BEq Lean.OpenDecl
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ) (x : E),
  ExistsContDiffBumpBase.y D (-x) = ExistsContDiffBumpBase.y D x
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Expect.noConfusionType : Sort v✝ → Std.Http.Header.Expect → Std.Http.Header.Expect → Sort v✝
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isErased : Lean.IR.IRType → Bool
-- Mathlib.Data.List.Infix
List.tails_reverse : ∀ {α : Type u_1} (l : List α), l.reverse.tails = (List.map List.reverse l.inits).reverse
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.leftOp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor D Cᵒᵖ} (a : F ⊣ G.leftOp),
  a.leftOp.counit = CategoryTheory.NatTrans.op a.unit
-- Init.Data.Char.Basic
Char.instInhabited : Inhabited Char
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_succ_eq_sum_choose : ∀ (n : ℕ), Nat.fib (n + 1) = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, p.1.choose p.2
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.unipotentLower_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₂ ⟶ X₁),
  (CategoryTheory.Biprod.unipotentLower r).hom =
    CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.id X₁) 0 r (CategoryTheory.CategoryStruct.id X₂)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_id : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.AffineSpace.reindex id S = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.AffineSpace n S)
-- Mathlib.Analysis.Matrix.Normed
/-- Normed group instance (using the Frobenius norm) for matrices over a normed group.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.frobeniusNormedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [NormedAddCommGroup α] → NormedAddCommGroup (Matrix m n α)
-- Mathlib.Analysis.Convex.Combination
/-- The center of mass of a finite subset of a convex set belongs to the set
provided that all weights are non-negative, and the total weight is positive.  -/
Convex.centerMass_mem : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {s : Set E} {t : Finset ι} {w : ι → R} {z : ι → E} [inst_3 : LinearOrder R] [IsStrictOrderedRing R],
  Convex R s → (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
-- Mathlib.Logic.Equiv.Set
/-- If a function `f` is injective on a set `s`, then `s` is equivalent to `f '' s`.  -/
Equiv.Set.imageOfInjOn : {α : Type u_3} → {β : Type u_4} → (f : α → β) → (s : Set α) → Set.InjOn f s → ↑s ≃ ↑(f '' s)
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.mk : Lean.Lsp.DocumentUri → Lean.Lsp.Range → Lean.Lsp.Location
-- Init.Data.Range.Polymorphic.Basic
Std.Roc.mem_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {r : Std.Roc α} {a : α}, a ∈ r ↔ r.lower < a ∧ a ≤ r.upper
-- Mathlib.Data.Finset.Basic
Finset.filter_disjUnion : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s t : Finset α) (h : Disjoint s t),
  Finset.filter p (s.disjUnion t h) = (Finset.filter p s).disjUnion (Finset.filter p t) ⋯
-- Mathlib.Order.GameAdd
Sym2.gameAdd_iff : ∀ {α : Type u_1} {rα : α → α → Prop} {x y : α × α},
  Sym2.GameAdd rα s(x.1, x.2) s(y.1, y.2) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.ext_iff' : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L₁' L₂' : LieRinehartSubalgebra A L), L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'
-- Mathlib.Data.List.Destutter
List.destutter_cons_cons : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
  List.destutter R (a :: b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddGrpCat.Hom.mk.sizeOf_spec : ∀ {A B : AddGrpCat} (hom' : ↑A →+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.revMatchesAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos →
    String.Slice.Pattern.Model.RevMatchesAt pat endPos
-- Mathlib.Topology.Algebra.Group.Basic
/-- Any first countable topological additive group has an antitone neighborhood basis
`u : ℕ → set G` for which `u (n + 1) + u (n + 1) ⊆ u n`.
The existence of such a neighborhood basis is a key tool
for `QuotientAddGroup.completeSpace_right`.  -/
IsTopologicalAddGroup.exists_antitone_basis_nhds_zero : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] [FirstCountableTopology G],
  ∃ u, (nhds 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.snd f₂)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When both `S.f` and `S.g` are zero, the middle object `S.X₂` gives a homology data on S  -/
CategoryTheory.ShortComplex.HomologyData.ofZeros : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.f = 0 → S.g = 0 → S.HomologyData
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.update_eq_sub_add_single : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type u_1} [inst_1 : (i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i)
  (i : ι) (b : β i), f.update i b = (f - fun₀ | i => f i) + fun₀ | i => b
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsIntegrallyClosedIn (↥(integralClosure R A)) A
-- Mathlib.Data.List.Sort
List.SortedGE.sortedGT_of_nodup : ∀ {α : Type u_1} [inst : PartialOrder α] {l : List α}, l.SortedGE → l.Nodup → l.SortedGT
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression of a 2-morphism into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval : (Type → Type) → Type
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mem_range_root_of_mem_range_reflection_of_mem_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {r : M ≃ₗ[R] M}
  {α : M}, r ∈ Set.range P.reflection → α ∈ Set.range ⇑P.root → r • α ∈ Set.range ⇑P.root
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- The `OrderHom` underlying a `PositiveLinearMap`.  -/
PositiveLinearMap.toOrderHom : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] → [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → (E₁ →ₚ[R] E₂) → E₁ →o E₂
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesLimit K F] [CategoryTheory.Limits.PreservesLimit (K.comp F) G],
  CategoryTheory.Limits.PreservesLimit K (F.comp G)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.mem_vars_iff_degreeOf_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {i : σ},
  i ∈ p.vars ↔ MvPolynomial.degreeOf i p ≠ 0
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hasForgetToBddDistLat : CategoryTheory.HasForget₂ FinBddDistLat BddDistLat
-- Batteries.Data.RunningStats
/-- Add a new data point to running statistics.  -/
Batteries.RunningStats.push : Float → Batteries.RunningStats → Batteries.RunningStats
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasStrictDerivAt.add` -/
HasStrictDerivAt.fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt g g' x → HasStrictDerivAt (fun i => f i + g i) (f' + g') x
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3) (a : α) (b : β a)
  (es : Std.DHashMap.Internal.AssocList α β) (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (a : α) →
      (b : β a) → (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match Std.DHashMap.Internal.AssocList.cons a b es with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons a b es => h_2 a b es) =
    h_2 a b es
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_pi : ∀ (n : ℕ), Real.cos (↑n * Real.pi) = (-1) ^ n
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.utf8GetAux.match_1.splitter : (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : List Char) →
    (x_1 x_2 : String.Pos.Raw) →
      ((x x_3 : String.Pos.Raw) → motive [] x x_3) →
        ((c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p) → motive x x_1 x_2
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Returns true if `e` is a "shallow" expression.
Local variables, constants, and other atomic expressions are always shallow.
In general, an expression is considered to be shallow if its depth is at most `threshold`.

Since the implementation uses `Lean.Expr.approxDepth`, the `threshold` is clamped to `[0, 254]`.
 -/
Lean.PrettyPrinter.Delaborator.isShallowExpression : ℕ → Lean.Expr → Bool