mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
/-- Like `find?`, but instead of just returning the element, it returns the entire subtree
at the element and a path back to the root for reconstructing the tree.
 -/
RBTree.RBNode.zoom : {α : Type u_1} →
  (α → Ordering) →
    RBTree.RBNode α → optParam (RBTree.RBNode.Path α) RBTree.RBNode.Path.root → RBTree.RBNode α × RBTree.RBNode.Path α
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_pUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  (CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) = CategoryTheory.Presieve.singleton f
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If functions on AddCircle agree on the image of the interval `(a, a + p]` then they are equal  -/
AddCircle.Ioc_ext : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜), (∀ x ∈ Set.Ioc a (a + p), f ↑x = g ↑x) → f = g
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofSubmodule'_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥(Submodule.comap (↑f) U)), ↑((f.ofSubmodule' U) x) = f ↑x
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instInhabited : Inhabited AddMagmaCat
-- Mathlib.Data.Set.Prod
Set.image_prodMk_subset_prod_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β}, b ∈ t → (fun a => (a, b)) '' s ⊆ s ×ˢ t
-- Init.Data.String.TakeDrop
String.Slice.trim : String.Slice → String.Slice
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.natDegree_coe_units : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (u : (Polynomial R)ˣ), (↑u).natDegree = 0
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), (e.restr s).source = e.source ∩ interior s
-- Mathlib.Algebra.Lie.Derivation.BaseChange
Lie.Derivation.ofLieDerivation_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (d : LieDerivation R L L) (x : TensorProduct R A L),
  ((Lie.Derivation.ofLieDerivation A) d) x = (LinearMap.lTensor A ↑d) x
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt16 = OfNat.ofNat n
-- Mathlib.RingTheory.Etale.Pi
Algebra.FormallyEtale.instEtaleForallOfFinite : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), Algebra.Etale R (A i)], Algebra.Etale R ((i : I) → A i)
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
EuclideanGeometry.Sphere.secondInter.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P) (v : V),
  s.secondInter p v = (-2 * inner ℝ v (p -ᵥ s.center) / inner ℝ v v) • v +ᵥ p
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.epi_left_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasPushouts C]
  {f g : CategoryTheory.Over X} (h : f ⟶ g) [CategoryTheory.Epi h], CategoryTheory.Epi (CategoryTheory.Over.Hom.left h)
-- Mathlib.ModelTheory.Order
/-- The relational language consisting of a single relation representing `≤`.  -/
FirstOrder.Language.order : FirstOrder.Language
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec : ∀ (x x_1 : Lean.Grind.IntInterval),
  (x == x_1) =
    match x, x_1 with
    | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => a == b && a_1 == b_1
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => a == b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => a == b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => true
    | x, x_2 => false
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₂ =
    CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.right φ)
-- Init.Data.Iterators.Combinators.Attach
/-- “Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning an
iterator with values in the corresponding subtype `{ x // P x }`.

**Termination properties:**

* `Finite` instance: only if the base iterator is finite
* `Productive` instance: only if the base iterator is productive
 -/
Std.Iter.attachWith : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (P : β → Prop) → (∀ (out : β), it.IsPlausibleIndirectOutput out → P out) → Std.Iter { out // P out }
-- Lean.Parser.Command
Lean.Parser.Command.structFields : Lean.Parser.Parser
-- Mathlib.ModelTheory.Syntax
/-- The negation of a bounded formula is also a bounded formula.  -/
FirstOrder.«term∼_» : Lean.ParserDescr
-- Mathlib.Order.Filter.Basic
Filter.generate_singleton : ∀ {α : Type u} (s : Set α), Filter.generate {s} = Filter.principal s
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coneOfConeUncurry_π_app : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F}
  (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j))
  (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)) (j : J),
  (CategoryTheory.Limits.coneOfConeUncurry Q c).π.app j =
    (Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } }
-- Init.SimpLemmas
iff_self : ∀ (p : Prop), (p ↔ p) = True
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.mk : {G : Type u_1} →
  [inst : AddGroup G] →
    (toAddSubgroup : AddSubgroup G) →
      autoParam toAddSubgroup.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam →
        autoParam toAddSubgroup.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam →
          FiniteIndexNormalAddSubgroup G
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP_apply : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : FreeMonoid α),
  (FreeMonoid.countP p) l = Multiplicative.ofAdd (List.countP (fun b => decide (p b)) (FreeMonoid.toList l))
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_t' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i j k : D.J),
  (D.mapGlueData F).t' i j k =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso F (D.f i j) (D.f i k)).inv
      (CategoryTheory.CategoryStruct.comp (F.map (D.t' i j k))
        (CategoryTheory.Limits.PreservesPullback.iso F (D.f j k) (D.f j i)).hom)
-- Lean.Compiler.IR.Basic
/-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object.  -/
Lean.IR.FnBody.inc : Lean.IR.VarId → ℕ → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_eq_zero_iff : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], Metric.ediam s = 0 ↔ s.Subsingleton
-- Mathlib.Computability.EpsilonNFA
εNFA.eval_nil : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.eval [] = M.εClosure M.start
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sub : ∀ (x y : ℂ), Complex.cos (x - y) = Complex.cos x * Complex.cos y + Complex.sin x * Complex.sin y
-- Mathlib.Data.Rel
SetRel.isTrans_singleton : ∀ {α : Type u_1} (x : α × α), {x}.IsTrans
-- Mathlib.Topology.Separation.Regular
IsCompact.exists_isOpen_closure_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {K U : Set X},
  IsCompact K → U ∈ nhdsSet K → ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with the real-valued measure of a set defined with a norm.

The `IsFiniteMeasure` hypothesis is necessary, otherwise `μ.real {...}` could be zero because
the measure of the set is infinite.  -/
MeasureTheory.tendstoInMeasure_iff_measureReal_norm : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {l : Filter ι} {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ.real {x | ε ≤ ‖f i x - g x‖}) l (nhds 0)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  self.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map h))
        (self.mapComp g h).inv)
-- Mathlib.Data.List.Sort
List.sortedLE_range' : ∀ (a b s : ℕ), (List.range' a b s).SortedLE
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.monoOfLE_comp : ∀ {X : SSet} [inst : X.Nonsingular] {x y z : X.N} (h : x ≤ y) (h' : y ≤ z),
  CategoryTheory.CategoryStruct.comp (SSet.N.monoOfLE h) (SSet.N.monoOfLE h') = SSet.N.monoOfLE ⋯
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.updateBuiltinTokens : Lean.Parser.ParserInfo → Lean.Name → IO Unit
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The p-adic integers are a binomial ring, i.e. a ring where binomial coefficients make sense.  -/
PadicInt.instBinomialRing : {p : ℕ} → [hp : Fact (Nat.Prime p)] → BinomialRing ℤ_[p]
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.comp.inj : ∀ {e : Lean.Expr} {a a_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr}
  {a_2 a_3 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1 = Mathlib.Tactic.BicategoryLike.Mor₁.comp e_1 a_2 a_3 →
    e = e_1 ∧ a = a_2 ∧ a_1 = a_3
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : DecidableEq γ] (g : β → γ)
  (f : MeasureTheory.SimpleFunc α β), (MeasureTheory.SimpleFunc.map g f).range = Finset.image g f.range
-- Mathlib.RingTheory.Length
Module.length_ne_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M], Module.length R M ≠ ⊤
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.prevD_succ_cochainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (i : ℕ),
  (prevD (i + 1)) f = CategoryTheory.CategoryStruct.comp (f (i + 1) i) (Q.d i (i + 1))
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A}
  (α : M ⟶ F.obj (Opposite.op X)) (f : F ⟶ G) {Z : CategoryTheory.Functor Cᵒᵖ A} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.freeYonedaHomEquiv.symm α)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Presheaf.freeYonedaHomEquiv.symm (CategoryTheory.CategoryStruct.comp α (f.app (Opposite.op X)))) h
-- Mathlib.Algebra.Order.Field.Basic
one_le_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → (1 ≤ a / b ↔ a ≤ b)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
functionals `fun v => v x` are continuous.  -/
WeakDual : (𝕜 : Type u_6) →
  (E : Type u_7) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [ContinuousAdd 𝕜] →
          [ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] → [Module 𝕜 E] → [TopologicalSpace E] → Type (max u_6 u_7)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.setLIntegral_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α} (f : α → ENNReal) (s : Set α) [MeasurableSingletonClass α]
  [inst_2 : Decidable (a ∈ s)], ∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
-- Mathlib.Data.Finset.Card
/-- If a Finset in a Pi type is nontrivial (has at least two elements), then
its projection to some factor is nontrivial, and the fibers of the projection
are proper subsets.  -/
Finset.exists_of_one_lt_card_pi : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → DecidableEq (α i)] {s : Finset ((i : ι) → α i)},
  1 < s.card → ∃ i, 1 < (Finset.image (fun x => x i) s).card ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
-- Mathlib.CategoryTheory.Sites.Types
/-- The sheaf condition for `yoneda'`.  -/
CategoryTheory.Presheaf.isSheaf_yoneda' : ∀ {α : Type u}, CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda.obj α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ0_Δ : ∀ (R : Type u_1) [inst : CommRing R], (WeierstrassCurve.ofJ0 R).Δ = -27
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β}, (f • g).NeBot → f.NeBot
-- Lean.ToExpr
Lean.instToExprInt32.mkNat : ℕ → Lean.Expr
-- Lean.Meta.WrapInstance
/-- Wrap an instance value so its type matches the expected type exactly.
See the module docstring for the full algorithm specification.
 -/
Lean.Meta.wrapInstance : Lean.Expr → Lean.Expr → optParam Bool true → optParam Bool true → optParam Bool false → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.HalesJewett
/-- A line is monochromatic if all its points are the same color.  -/
Combinatorics.Line.IsMono : {α : Type u_5} → {ι : Type u_6} → {κ : Sort u_7} → ((ι → α) → κ) → Combinatorics.Line α ι → Prop
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.toLinearEquiv : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → B₁.IsometryEquiv B₂ → M₁ ≃ₗ[R] M₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p p_1 : G.Walk u v),
  p = p_1 → ∀ (h : G.Adj v w), p.concat h = p_1.concat h
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Raw.Const.get! (t.erase k) a =
        if cmp k a = Ordering.eq then default else Std.DTreeMap.Raw.Const.get! t a
-- Mathlib.Topology.Algebra.Group.Pointwise
group_inseparable_iff : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {x y : G},
  Inseparable x y ↔ x / y ∈ closure 1
-- Mathlib.Probability.Moments.SubGaussian
/-- Chernoff bound on the right tail of a sub-Gaussian random variable.  -/
ProbabilityTheory.HasSubgaussianMGF.measure_ge_le : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ {ε : ℝ}, 0 ≤ ε → μ.real {ω | ε ≤ X ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑c))
-- Mathlib.Analysis.LConvolution
/-- The definition of additive convolution of functions.  -/
MeasureTheory.lconvolution_def : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Add G] [inst_1 : Neg G] {f g : G → ENNReal}
  {μ : MeasureTheory.Measure G} {x : G}, MeasureTheory.lconvolution f g μ x = ∫⁻ (y : G), f y * g (-y + x) ∂μ
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is
the entire space.  -/
AddCircle.coe_image_Ico_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  (a : 𝕜) [Archimedean 𝕜], QuotientAddGroup.mk '' Set.Ico a (a + p) = Set.univ
-- Std.Net.Addr
Std.Net.IPAddr.v6.sizeOf_spec : ∀ (addr : Std.Net.IPv6Addr), sizeOf (Std.Net.IPAddr.v6 addr) = 1 + sizeOf addr
-- Mathlib.Dynamics.BirkhoffSum.Basic
/-- Birkhoff sum is "almost invariant" under `f`:
the difference between `birkhoffSum f g n (f x)` and `birkhoffSum f g n x`
is equal to `g (f^[n] x) - g x`.  -/
birkhoffSum_apply_sub_birkhoffSum : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) (x : α),
  birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftToTerminal_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z)
  (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.liftToTerminal F hZ).obj X =
    match X with
    | CategoryTheory.WithTerminal.of x => F.obj x
    | CategoryTheory.WithTerminal.star => Z
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.mk_injective : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι],
  (∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f i j hij)) → ∀ (i : ι), Function.Injective fun x => ⟦⟨i, x⟩⟧
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.falling_zero_subset : ∀ {α : Type u_2} [inst : DecidableEq α] (𝒜 : Finset (Finset α)), Finset.falling 0 𝒜 ⊆ {∅}
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.op_rightTriple : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.op.rightTriple = q.leftTriple.op
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey!_modify_eq_minKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).minKey! = t.minKey!
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungFun_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R), x.verschiebungFun.coeff 0 = 0
-- Init.Prelude
/-- Constructs a new empty array with initial capacity `c`.

This will be deprecated in favor of `Array.emptyWithCapacity` in the future.
 -/
Array.mkEmpty : {α : Type u} → ℕ → Array α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  (m.erase k).get? k = none
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_mk'_linearMap : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCancelCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] (D : A →ₗ[R] M)
  (h : ∀ (a b : A), D (a * b) = a • D b + b • D a), ↑(Derivation.mk' D h) = D
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z W) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CartesianMonoidalCategory.lift f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z W).hom h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CartesianMonoidalCategory.lift g h)) h_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofCompIso_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'}
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)), F.ofCompIso.I = F.I
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] [CategoryTheory.IsCardinalPresentable X κ]
  (F : CategoryTheory.Functor C C') [F.IsEquivalence], CategoryTheory.IsCardinalPresentable (F.obj X) κ
-- Init.MetaTypes
/-- If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded.
 -/
Lean.Meta.Simp.Config.unfoldPartialApp : Lean.Meta.Simp.Config → Bool
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_map : ∀ (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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D).obj x).map f =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labelling_obj : ∀ (V : Type u_1) {M : Type u_2} [inst : SMul M V] {S : Type u_3} (ι : S → M) (x : Quiver.SchreierGraph V ι),
  (Quiver.SchreierGraph.labelling V ι).obj x = Quiver.SingleObj.star S
-- Lean.Util.Heartbeats
/-- Returns the percentage of the max heartbeats allowed
that have been consumed so far in this computation.
 -/
Lean.heartbeatsPercent : Lean.CoreM ℕ