mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : C}
  (f : X ⟶ Y) (i : (data X).I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i) =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀
      (CategoryTheory.CategoryStruct.comp ((data X).f i) f)
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- The constant homotopy from `f` to `f`.  -/
CategoryTheory.SimplicialObject.Homotopy.refl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} → (f : X ⟶ Y) → CategoryTheory.SimplicialObject.Homotopy f f
-- Mathlib.Probability.IdentDistribIndep
/-- If `(X i)` and `(Y i)` are families of independent random variables indexed by a countable
type `ι`, such that for each `i`, `X i` and `Y i` are identically distributed, then the products
`X` and `Y` are identically distributed.  -/
ProbabilityTheory.IdentDistrib.pi : ∀ {Ω : Type u_1} {Ω' : Type u_2} {ι : Type u_3} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [Countable ι] {E : ι → Type u_6}
  {mE : (i : ι) → MeasurableSpace (E i)} {X : (i : ι) → Ω → E i} {Y : (i : ι) → Ω' → E i},
  (∀ (i : ι), ProbabilityTheory.IdentDistrib (X i) (Y i) μ ν) →
    ProbabilityTheory.iIndepFun X μ →
      ProbabilityTheory.iIndepFun Y ν → ProbabilityTheory.IdentDistrib (fun ω x => X x ω) (fun ω x => Y x ω) μ ν
-- Init.System.IOError
IO.Error.protocolError.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.protocolError osCode details = IO.Error.protocolError osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α} {v : β},
  Std.ExtTreeMap.ofList [(k, v)] cmp = ∅.insert k v
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
/-- A Kan complex `S` satisfies the following horn-filling condition:
for every nonzero `n : ℕ` and `0 ≤ i ≤ n`,
every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`.  -/
SSet.KanComplex.hornFilling : ∀ {S : SSet} [S.KanComplex] {n : ℕ} {i : Fin (n + 2)} (σ₀ : (SSet.horn (n + 1) i).toSSet ⟶ S),
  ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 1) i).ι σ
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_right_nhdsLT : ∀ {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.Iio a)) = nhdsWithin (a + c) (Set.Iio (a + c))
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.mul : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConcaveOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → AntivaryOn f g s → ConcaveOn 𝕜 s (f * g)
-- Std.Tactic.BVDecide.Reflect
_private.Std.Tactic.BVDecide.Reflect.0.Std.Tactic.BVDecide.Reflect.verifyCert.match_1.eq_1 : ∀ (motive : Except String (Array Std.Tactic.BVDecide.LRAT.IntAction) → Sort u_1)
  (lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction)
  (h_1 : (lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction) → motive (Except.ok lratProof))
  (h_2 : (a : String) → motive (Except.error a)),
  (match Except.ok lratProof with
    | Except.ok lratProof => h_1 lratProof
    | Except.error a => h_2 a) =
    h_1 lratProof
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallySurjective_whisker_iff : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA],
  CategoryTheory.CoverPreserving J K H →
    ∀ [H.IsCocontinuous J K] [H.IsCoverDense K],
      CategoryTheory.Presheaf.IsLocallySurjective J (H.op.whiskerLeft f) ↔
        CategoryTheory.Presheaf.IsLocallySurjective K f
-- Init.Data.Vector.Range
Vector.fst_eq_of_mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n} {k : ℕ} (h : x ∈ xs.zipIdx k), x.1 = xs[x.2 - k]
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.cast_heq : ∀ {n m : ℕ} (c : Composition m) (hmn : m = n), c.cast hmn ≍ c
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Suppose that `f` and `g` are linear maps that compose to zero, and that `eM`, `eN`, and `eL`
indicated in the diagram below are linear equivalences to modules that all belong to the same
universe. Then this is the short complex in `ModuleCat` given by the bottom row in the diagram.
M --f--> N --g--> L
|        |        |
eM       eN       eL
|        |        |
v        v        v
M'-----> N'-----> L'
This complex is exact when we have `Function.Exact f g`, see
`ModuleCat.shortComplexOfConj_exact`.
 -/
ModuleCat.shortComplexOfConj : {R : Type u} →
  [inst : Ring R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type v} →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                {L : Type v} →
                  [inst_5 : AddCommGroup L] →
                    [inst_6 : Module R L] →
                      {M' : Type u_1} →
                        {N' : Type u_2} →
                          {L' : Type u_3} →
                            [inst_7 : AddCommGroup M'] →
                              [inst_8 : AddCommGroup N'] →
                                [inst_9 : AddCommGroup L'] →
                                  [inst_10 : Module R M'] →
                                    [inst_11 : Module R N'] →
                                      [inst_12 : Module R L'] →
                                        (M ≃ₗ[R] M') →
                                          (N ≃ₗ[R] N') →
                                            (L ≃ₗ[R] L') →
                                              (f : M' →ₗ[R] N') →
                                                (g : N' →ₗ[R] L') →
                                                  g ∘ₗ f = 0 → CategoryTheory.ShortComplex (ModuleCat R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {fallback : β} {f : β → β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.modify t k f) k fallback =
    (Option.map f (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Init.Data.Order.Factories
/-- This lemma derives a `LawfulOrderLT α` instance from a property involving an `LE α` instance.
 -/
Std.LawfulOrderLT.of_le : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α], (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) → Std.LawfulOrderLT α
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNontrivial : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [Nonempty m] [Nonempty n] [Nontrivial A], Nontrivial (CStarMatrix m n A)
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuous.upperHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f → ∀ (s : Set α) (x : α), UpperHemicontinuousWithinAt f s x
-- Init.Internal.Order.Basic
/-- The class `MonoBind m` indicates that every `m α` has a `PartialOrder`, and that the bind operation
on `m` is monotone in both arguments with regard to that order.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.MonoBind : (m : Type u → Type v) → [Bind m] → [(α : Type u) → Lean.Order.PartialOrder (m α)] → Prop
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove.eq_1 : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i = if i.castSucc < p then i.castSucc else i.succ
-- Init.Meta.Defs
Lean.Syntax.instRepr.repr : Lean.Syntax → ℕ → Std.Format
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instField : (n : ℕ) → (K : Type u_1) → [inst : Field K] → Field (CyclotomicField n K)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.mk.inj : ∀ {instName : Lean.Name} {typeInfos : Array Lean.InductiveVal} {auxFunNames : Array Lean.Name} {usePartial : Bool}
  {instName_1 : Lean.Name} {typeInfos_1 : Array Lean.InductiveVal} {auxFunNames_1 : Array Lean.Name}
  {usePartial_1 : Bool},
  { instName := instName, typeInfos := typeInfos, auxFunNames := auxFunNames, usePartial := usePartial } =
      { instName := instName_1, typeInfos := typeInfos_1, auxFunNames := auxFunNames_1, usePartial := usePartial_1 } →
    instName = instName_1 ∧ typeInfos = typeInfos_1 ∧ auxFunNames = auxFunNames_1 ∧ usePartial = usePartial_1
-- Mathlib.Data.Finset.Empty
/-- **Alias** of the reverse direction of `Finset.empty_ssubset`. -/
Finset.Nonempty.empty_ssubset : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∅ ⊂ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.insertMany t l).getKeyD k' fallback = k
-- Mathlib.Data.List.Chain
/-- Given a chain from `a` to `b`, and a predicate true at `a`, if `r x y → p x → p y` then
the predicate is true everywhere in the chain.
That is, we can propagate the predicate down the chain.
 -/
List.IsChain.cons_induction : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} (p : α → Prop) (l : List α),
  List.IsChain r (a :: l) → (∀ ⦃x y : α⦄, r x y → p x → p y) → p a → ∀ i ∈ l, p i
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support.length = p.length + 1
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → MeromorphicOn g U → MeromorphicOn (f + g) U
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.flip_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M)
  (m : M) (n : N), (e.flip m) n = (e n) m
-- Lean.Meta.Tactic.Apply
/-- Try to close the goal using `proof_irrel_heq`. Returns whether or not it succeeds.

We need to be somewhat careful not to assign metavariables while doing this, otherwise we might
specialize `Sort _` to `Prop`.
 -/
Lean.MVarId.proofIrrelHeq : Lean.MVarId → Lean.MetaM Bool
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainTermGoal : Lean.FromJson Lean.Lsp.PlainTermGoal
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.trans : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂} {v₃ : ι → P₃}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃],
  Congruent v₁ v₂ → Congruent v₂ v₃ → Congruent v₁ v₃
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.id_toAlgHom : ∀ (R : Type u_1) {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜],
  ↑(GradedAlgHom.id R 𝒜) = AlgHom.id R A
-- Mathlib.Algebra.CharP.Frobenius
MonoidHom.map_iterate_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R) (n : ℕ),
  f ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (f x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.instMonObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.Grp.instMonObj =
    { one := CategoryTheory.Grp.homMk CategoryTheory.MonObj.one.hom,
      mul := CategoryTheory.Grp.homMk CategoryTheory.MonObj.mul.hom, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Lean.Meta.Basic
/-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions.  -/
Lean.Meta.lambdaMetaTelescope : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Topology.MetricSpace.Basic
/-- Instantiate the reals as a metric space.  -/
Real.metricSpace : MetricSpace ℝ
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.sortedLT : ∀ {m : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m L → L.SortedLT
-- Mathlib.Topology.Compactness.Compact
Set.sUnion_isCompact_eq_univ : ∀ {X : Type u} [inst : TopologicalSpace X], ⋃₀ {s | IsCompact s} = Set.univ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.name : String → Lean.Lsp.ParameterInformationLabel
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.IsStableUnderShift.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A],
  autoParam (∀ (a : A), P.IsStableUnderShiftBy a)
      CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy._autoParam →
    P.IsStableUnderShift A
-- Mathlib.Analysis.Calculus.LogDeriv
/-- If two functions agree on a codiscrete subset of `𝕜`, then so do their logarithmic derivatives.
 -/
logDeriv_congr_codiscrete : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'},
  f =ᶠ[Filter.codiscrete 𝕜] g → logDeriv f =ᶠ[Filter.codiscrete 𝕜] logDeriv g
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to
`Discrete.functor (F.obj)`.  -/
CategoryTheory.Discrete.natIsoFunctor : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} →
        F ≅ CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal.eq_1 : ∀ (μ : ℝ) (v : NNReal) (x : ℝ),
  ProbabilityTheory.gaussianPDFReal μ v x = (√(2 * Real.pi * ↑v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * ↑v))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_image`.

---

The Hausdorff edistance is invariant under isometries.  -/
EMetric.hausdorffEdist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s t : Set α} {Φ : α → β},
  Isometry Φ → Metric.hausdorffEDist (Φ '' s) (Φ '' t) = Metric.hausdorffEDist s t
-- Mathlib.CategoryTheory.Limits.Types.Filtered
/-- An alternative relation on `Σ j, F.obj j`,
which generates the same equivalence relation as we use to define the colimit in `Type` above,
but that is more convenient when working with filtered colimits.

Elements in `F.obj j` and `F.obj j'` are equivalent if there is some `k : J` to the right
where their images are equal.
 -/
CategoryTheory.Limits.Types.FilteredColimit.Rel : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) → (j : J) × F.obj j → (j : J) × F.obj j → Prop
-- Mathlib.Order.Interval.Multiset
Multiset.right_notMem_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∉ Multiset.Ico a b
-- Mathlib.Logic.Denumerable
/-- See also `nonempty_encodable`, `nonempty_fintype`.  -/
nonempty_denumerable : ∀ (α : Type u_3) [Countable α] [Infinite α], Nonempty (Denumerable α)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f f_1 : X ⟶ Y),
  f = f_1 → CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f_1
-- Mathlib.Data.Nat.Prime.Infinite
/-- A version of `Nat.exists_infinite_primes` using the `BddAbove` predicate.  -/
Nat.not_bddAbove_setOfPred_prime : ¬BddAbove {p | Nat.Prime p}
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_mul_right_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.MeasurePreserving (fun t => (g * t)⁻¹) μ μ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (FreeMonoid α)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Mathlib.CategoryTheory.Action.Basic
/-- The natural isomorphism from restriction along the identity homomorphism to
the identity functor on `Action V G`.
 -/
Action.resId : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_3} → [inst_1 : Monoid G] → Action.res V (MonoidHom.id G) ≅ CategoryTheory.Functor.id (Action V G)
-- Init.Data.Int.Gcd
Int.gcd_mul_right_dvd_mul_gcd : ∀ (k m n : ℤ), k.gcd (m * n) ∣ k.gcd m * k.gcd n
-- Mathlib.RingTheory.WittVector.StructurePolynomial
map_wittStructureInt : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) =
    wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_eq_zero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : R), WithVal.toVal v x = 0 ↔ x = 0
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_map_ofDual`. -/
List.SortedLT.of_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, l.SortedLT → (List.map (⇑OrderDual.ofDual) l).SortedGT
-- Lean.Language.Lean.Types
/-- State after the module header has been processed including imports.  -/
Lean.Language.Lean.HeaderProcessedSnapshot : Type
-- Init.Data.Vector.Lemmas
Vector.back?_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.pop.back? = if n ≤ 1 then none else xs[n - 2]?
-- Mathlib.Order.Comparable
incompRel_of_incompRel_of_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  IncompRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → IncompRel (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.SetTheory.Cardinal.Order
/-- Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`.  -/
Cardinal.instSuccOrder : SuccOrder Cardinal.{u_1}
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Finpartition.energy_le_one : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α)
  [inst_1 : DecidableRel G.Adj], P.energy G ≤ 1
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.isScalarTower : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  {R' : Type u_6} [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] [inst_6 : MonoidWithZero R'] [inst_7 : DistribMulAction R' V₂]
  [inst_8 : PseudoMetricSpace R'] [inst_9 : IsBoundedSMul R' V₂] [inst_10 : SMul R R'] [IsScalarTower R R' V₂],
  IsScalarTower R R' (NormedAddGroupHom V₁ V₂)
-- Init.Data.UInt.Basic
/-- Multiplies two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the
`*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
USize.mul : USize → USize → USize
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_isLink : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) (e : β) (a a_1 : α'),
  (Graph.map f G).IsLink e a a_1 = Relation.Map (G.IsLink e) f f a a_1
-- Mathlib.Topology.Compactness.CountablyCompact
/-- Variant of `isCountablyCompact_iff_countable_open_cover` with `Set ℕ` instead of `Finset ℕ`.  -/
isCountablyCompact_iff_countable_open_cover' : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A ↔ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
-- Lean.Elab.Binders
/-- Position information provider for the Info Tree.
We currently do not track binder "macro expansion" steps in the info tree.
For example, suppose we expand a `_` into a fresh identifier. The fresh identifier
has synthetic position since it was not written by the user, and we would not get
hover information for the `_` because we also don't have this macro expansion step
stored in the info tree. Thus, we store the original `Syntax` in `ref`, and use
it when storing the binder information in the info tree.

Potential better solution: add a binder syntax category, an extensible `elabBinder`
(like we have `elabTerm`), and perform all macro expansion steps at `elabBinder` and
record them in the info tree.
 -/
Lean.Elab.Term.BinderView.ref : Lean.Elab.Term.BinderView → Lean.Syntax
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
/-- The indexed product of uniform spaces with nonarchimedean uniformities has a
nonarchimedean uniformity.  -/
IsUltraUniformity.pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [U : (i : ι) → UniformSpace (X i)] [h : ∀ (i : ι), IsUltraUniformity (X i)],
  IsUltraUniformity ((i : ι) → X i)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.withReader_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [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}
  {epost : EPred} (f : ρ → ρ) (x : ReaderT ρ m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp x (fun a x => post a r) epost (f r) ⦄ MonadWithReaderOf.withReader f x ⦃ post; epost ⦄
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.point_finite : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X),
  {i | (f i) x ≠ 0}.Finite