mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.code.inj : ∀ {ctx : Lean.Elab.ContextInfo} {infos : Std.TreeMap ℕ Lean.Elab.Info compare} {ctx_1 : Lean.Elab.ContextInfo}
  {infos_1 : Std.TreeMap ℕ Lean.Elab.Info compare},
  Lean.Widget.EmbedFmt.code✝ ctx infos = Lean.Widget.EmbedFmt.code✝ ctx_1 infos_1 → ctx = ctx_1 ∧ infos = infos_1
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- **Alias** of the reverse direction of `lipschitzWith_iff_dist_le_mul`. -/
LipschitzWith.of_dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  (∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzWith K f
-- Batteries.Data.List.Perm
List.Subperm.idxInj_injective : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys), Function.Injective h.idxInj
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div.sizeOf_spec : ∀ (k : ℤ) (e : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div k e) = 1 + sizeOf k + sizeOf e
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList_eq_if_roo : ∀ {α : Type u} {r : Std.Rco α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α],
  r.toList = if r.lower < r.upper then r.lower :: (r.lower<...r.upper).toList else []
-- Mathlib.Algebra.Homology.Homotopy
/-- A homotopy equivalence between two chain complexes consists of a chain map each way,
and homotopies from the compositions to the identity chain maps.

Note that this contains data;
arguably it might be more useful for many applications if we truncated it to a Prop.
 -/
HomotopyEquiv : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → HomologicalComplex V c → HomologicalComplex V c → Type (max u_1 v)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_le_length_mul_add_right : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_subset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_tryCatch_OptionT_apply : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (x : OptionT m α) (h : PUnit.{u_2 + 1} → OptionT m α),
  Lean.Order.PartialOrder.rel
    (Std.Internal.Do.wp x post (EPost.Cons.mk✝ (Std.Internal.Do.wp (h PUnit.unit) post epost) epost.tail))
    (Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost)
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.addMonoidObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J AddMonCat) → (j : J) → AddMonoid ↑(F.obj j)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₁_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1),
  (X.sc₁ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.le_order_smul : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {a : R}, φ.order ≤ (a • φ).order
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.coeff_supDegree_add_supDegree`. -/
AddMonoidAlgebra.apply_supDegree_add_supDegree : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) =
        AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.mk : {σ : Type} → ℕ → IO σ → Lean.EnvExtension.AsyncMode → Option (Lean.ReplayFn σ) → Lean.EnvExtension σ
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mk.injEq : ∀ {H : Type u_2} [inst : TopologicalSpace H] (members : Set (OpenPartialHomeomorph H H))
  (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e.trans e' ∈ members)
  (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
  (locality' :
    ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
  (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members)
  (members_1 : Set (OpenPartialHomeomorph H H))
  (trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e.trans e' ∈ members_1)
  (symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1) (id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1)
  (locality'_1 :
    ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1)
  (mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1),
  ({ members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' } =
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
        mem_of_eqOnSource' := mem_of_eqOnSource'_1 }) =
    (members = members_1)
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.roots_scaleRoots : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) {r : R},
  IsUnit r → (p.scaleRoots r).roots = Multiset.map (fun x => r * x) p.roots
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix.  -/
SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_of_one : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : DecidableEq α] [inst_3 : AddMonoid α] [inst_4 : One α],
  1 + SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = Matrix.of 1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C)
  (a : (∐ X.toFun).I),
  X.coproductIsoSelf.hom.f a =
    X.cofanPtIsoSelf.hom.f ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.f a)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle is at most `π / 2`, version subtracting vectors.  -/
InnerProductGeometry.angle_sub_le_pi_div_two_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → InnerProductGeometry.angle x (x - y) ≤ Real.pi / 2
-- Mathlib.RingTheory.Algebraic.Defs
/-- An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial
with coefficients in R.  -/
IsAlgebraic : (R : Type u) → {A : Type v} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → Prop
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Methods.toMethodsRef.unsafe_1 : Lean.Meta.Grind.Methods → Lean.Meta.Grind.MethodsRef
-- Mathlib.Order.Booleanisation
/-- The order on `Booleanisation α` is as follows: For `a b : α`,
* `a ≤ b` iff `a ≤ b` in `α`
* `a ≤ bᶜ` iff `a` and `b` are disjoint in `α`
* `aᶜ ≤ bᶜ` iff `b ≤ a` in `α`
* `¬ aᶜ ≤ b`  -/
Booleanisation.instLE : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → LE (Booleanisation α)
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n+1)` iff it has a `C^n` derivative.  -/
contDiff_succ_iff_hasFDerivAt : ∀ {𝕜 : 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}
  {n : ℕ}, ContDiff 𝕜 (↑n + 1) f ↔ ∃ f', ContDiff 𝕜 (↑n) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
-- Mathlib.Algebra.Notation.Support
Subsingleton.mulSupport_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] [Subsingleton M] (f : ι → M), Function.mulSupport f = ∅
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  Disjoint (MeasureTheory.addFundamentalInterior G s) (MeasureTheory.addFundamentalFrontier G s)
-- Init.Data.Vector.Lemmas
Vector.exists_of_mem_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {n : ℕ} {xs : Vector α n} {b : α_1},
  b ∈ Vector.map f xs → ∃ a ∈ xs, f a = b
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.tail.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharRole.tail = 1
-- Mathlib.Logic.Equiv.Prod
Equiv.punitProd_symm_apply : ∀ (α : Type u_9) (a : α), (Equiv.punitProd α).symm a = (PUnit.unit, a)
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- If `G` is a `Kᵣ₊₂`-free graph with `n` vertices containing a `Wᵣ,ₖ` but no `Wᵣ,ₖ₊₁`
then `G.minDegree ≤ (2 * r + k) * n / (2 * r + k + 3)`
 -/
SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ : ∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α],
  G.IsFiveWheelLike r k v w₁ w₂ s t →
    G.CliqueFree (r + 2) →
      ∀ [inst_1 : DecidableRel G.Adj] [inst_2 : Fintype α],
        G.FiveWheelLikeFree r (k + 1) → G.minDegree ≤ (2 * r + k) * Fintype.card α / (2 * r + k + 3)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.add.sizeOf_spec : ∀ (a b : Lean.Grind.CommRing.Expr), sizeOf (a.add b) = 1 + sizeOf a + sizeOf b
-- Mathlib.Data.Finset.Basic
Finset.disjoint_erase_comm : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)
-- Lean.Parser.Basic
/-- `withPosition(p)` runs `p` while setting the "saved position" to the current position.
This has no effect on its own, but various other parsers access this position to achieve some
composite effect:

* `colGt`, `colGe`, `colEq` compare the column of the saved position to the current position,
  used to implement Python-style indentation sensitive blocks
* `lineEq` ensures that the current position is still on the same line as the saved position,
  used to implement composite tokens

The saved position is only available in the read-only state, which is why this is a scoping parser:
after the `withPosition(..)` block the saved position will be restored to its original value.

This parser has the same arity as `p` - it just forwards the results of `p`.  -/
Lean.Parser.withPosition : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.totalDegree_le_of_dvd_of_isDomain : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R},
  f ∣ g → g ≠ 0 → f.totalDegree ≤ g.totalDegree
-- Mathlib.Algebra.Order.Module.Defs
/-- A constructor for `PosSMulReflectLT` requiring you to prove `a • b₁ < a • b₂ → b₁ < b₂` only
when `0 < a`  -/
PosSMulReflectLT.of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : Preorder β], (∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂) → PosSMulReflectLT α β
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α},
  μ s ≠ ⊤ → ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsCircuit.isNonloop_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, M.IsCircuit C → C.Nontrivial → e ∈ C → M.IsNonloop e
-- Mathlib.Algebra.Algebra.Basic
FaithfulSMul.algebraMap_injective : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  Function.Injective ⇑(algebraMap R A)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.len_mk : ∀ (n : ℕ), { len := n }.len = n
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- Up to technical conditions, If `T/S/R` is a tower of algebras, `P` is a prime of `T` unramified
in `R`, then `P ∩ S` (as a prime of `S`) is also unramified in `R`.
 -/
Algebra.IsUnramifiedAt.of_liesOver : ∀ (R : Type u_1) {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (p : Ideal S) (P : Ideal T)
  [P.LiesOver p] [inst_8 : p.IsPrime] [inst_9 : P.IsPrime] [Algebra.IsUnramifiedAt R P] [Algebra.EssFiniteType R S]
  [Algebra.EssFiniteType R T] [IsDedekindDomain S] [IsDomain T] [Module.IsTorsionFree S T], Algebra.IsUnramifiedAt R p
-- Mathlib.Topology.Inseparable
Specializes.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y},
  x₁ ⤳ x₂ → y₁ ⤳ y₂ → (x₁, y₁) ⤳ (x₂, y₂)
-- Mathlib.ModelTheory.FinitelyGenerated
/-- An equivalent expression of `Structure.cg`.  -/
FirstOrder.Language.Structure.cg_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M],
  FirstOrder.Language.Structure.CG L M ↔ ∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_four : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R),
  complEDS₂ b c d 4 = c ^ 2 * preNormEDS (b ^ 4) c d 6 - preNormEDS (b ^ 4) c d 5 ^ 2
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.natAddEmb m) (Finset.Ico i j) = Finset.Ico (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.LinearAlgebra.Determinant
Matrix.det_map' : ∀ {K : Type u_5} {m : Type u_6} {F : Type u_7} [inst : Field K] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : FunLike F (Matrix m m K) (Matrix m m K)] [AlgHomClass F K (Matrix m m K) (Matrix m m K)] (f : F)
  (x : Matrix m m K), (f x).det = x.det
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH0_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G), (groupHomology.shortComplexH0 A).Exact
-- Mathlib.Data.Finset.Basic
Finset.sdiff_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s → s \ t.erase a = insert a (s \ t)
-- Mathlib.Topology.Continuous
Continuous.comp' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, Continuous g → Continuous f → Continuous fun x => g (f x)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_norm_right`. -/
Asymptotics.IsBigOWith.norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith c l f g' → Asymptotics.IsBigOWith c l f fun x => ‖g' x‖
-- Mathlib.Analysis.SpecialFunctions.Pow.Integral
/-- An application of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function `f` on a measure space, the Lebesgue integral of `f` can
be written (roughly speaking) as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) > t}`.

See `MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul` for a version with sets of the form
`{ω | f(ω) ≥ t}` instead.  -/
MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ},
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      ∀ {p : ℝ},
        0 < p →
          ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
            ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero : ∀ {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [inst : SeminormedAddCommGroup E'] [inst_1 : NormedDivisionRing 𝕜]
  [inst_2 : Module 𝕜 E'] [NormSMulClass 𝕜 E'] {f : α → E'} {g : α → 𝕜} {l : Filter α},
  f =o[l] g → Filter.Tendsto (fun x => (g x)⁻¹ • f x) l (nhds 0)
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.simpAllTrace : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_right_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousAdd H] {c a : H},
  Filter.map (fun x => x + c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a + c) (Set.Ioi (a + c))
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrictOfInjective_comp : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M₁ →ₗ[R] M₂) (i : M₃ →ₗ[R] M₂) (hi : Function.Injective ⇑i)
  (hf : ∀ (x : M₁), f x ∈ i.range), i ∘ₗ f.codRestrictOfInjective i hi hf = f
-- Init.Data.Vector.Attach
Vector.unattach_push : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {a : { x // p x }} {xs : Vector { x // p x } n},
  (xs.push a).unattach = xs.unattach.push ↑a
-- Init.Data.List.Basic
/-- The first list is a non-contiguous sub-list of the second list. Typically written with the `<+`
operator.

In other words, `l₁ <+ l₂` means that `l₁` can be transformed into `l₂` by repeatedly inserting new
elements.
 -/
List.«term_<+_» : Lean.TrailingParserDescr
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.solveSomeLocalFVarIdCnstr?.go : Lean.Meta.Match.Alt →
  List (Lean.Expr × Lean.Expr) → Lean.MetaM (Option (Lean.FVarId × Lean.Expr) × List (Lean.Expr × Lean.Expr))
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded : Type → Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, k ∈ m.insertIfNew k v
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.mk : List Lean.Name →
  Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl →
    List Lean.MVarId →
      List Lean.Elab.Term.MVarErrorInfo →
        List Lean.Elab.Term.LevelMVarErrorInfo →
          Lean.MVarIdMap Lean.Name → List Lean.Elab.Term.LetRecToLift → Lean.Elab.Term.State
-- Init.PropLemmas
not_or_intro : ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂],
  (HomologicalComplex₂.total.mapIso e c₁₂).hom = HomologicalComplex₂.total.map e.hom c₁₂
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} {α β : F ⟶ G}, α.hom.hom = β.hom.hom → α = β
-- Mathlib.RingTheory.Ideal.Maps
Ideal.ne_bot_of_map_ne_bot : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I : Ideal R} [RingHomClass F R S], Ideal.map f I ≠ ⊥ → I ≠ ⊥
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.id_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₗc[R] B), (CoalgHom.id R B).comp φ = φ
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instCompleteLatticeWithTop : {α : Type u_1} → [CompleteLattice α] → CompleteLattice (WithTop α)
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instFromJsonCancelParams.fromJson : Lean.Json → Except String Lean.Lsp.CancelParams
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType_1 : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) →
          Module ((AlgebraicGeometry.structureSheafInType R R).obj.obj U)
            ((AlgebraicGeometry.structureSheafInType R M).obj.obj U)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_exists : ∀ {V : Type u_1} (G : SimpleGraph V), ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
-- Lean.Meta.Instances
Lean.Meta.Instances.erased : Lean.Meta.Instances → Lean.PHashSet Lean.Name
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- A local predicate must be local --- provided that it is locally satisfied, it is also globally
satisfied  -/
TopCat.LocalPredicate.locality : ∀ {X : TopCat} {T : ↑X → Type u_1} (self : TopCat.LocalPredicate T) {U : TopologicalSpace.Opens ↑X}
  (f : (x : ↥U) → T ↑x), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, self.pred fun x => f (i x)) → self.pred f
-- Mathlib.Data.Num.ZNum
ZNum.cast_lt : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum}, ↑m < ↑n ↔ m < n
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommRing β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Asymptotics.SuperpolynomialDecay l k f → abs ∘ g ≤ᶠ[l] abs ∘ f → Asymptotics.SuperpolynomialDecay l k g
-- Mathlib.GroupTheory.CommutingProbability
/-- A list of Dihedral groups whose product will have commuting probability `1 / n`.  -/
DihedralGroup.reciprocalFactors : ℕ → List ℕ
-- Lean.Meta.Sym.AbstractS
_private.Lean.Meta.Sym.AbstractS.0.Lean.Meta.Sym.abstractFVarsRange.go : ℕ → (xs : Array Lean.Expr) → Lean.FVarId → ℕ → (i : ℕ) → i < xs.size → Option ℕ