mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
/-- If a series of functions has summable `L^p` norms for some `1 ≤ p`, then the norms are ae
pointwise summable.  -/
MeasureTheory.summable_norm_of_tsum_eLpNorm_ne_top : ∀ {X : Type u_1} {E : Type u_2} {x : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : NormedAddCommGroup E]
  {ι : Type u_3} [Countable ι] {p : ENNReal},
  1 ≤ p →
    ∀ {f : ι → X → E},
      (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
        ∑' (n : ι), MeasureTheory.eLpNorm (f n) p μ ≠ ⊤ → ∀ᵐ (a : X) ∂μ, Summable fun n => ‖f n a‖
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_finset_logSizeBallSeq_le : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c i).finset.card ≤ J.card - i
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The `ι`-indexed symmetric tensor power of a semimodule `M` over a commutative semiring `R`
is the quotient of the `ι`-indexed tensor power of `M` by the relation that two tensors are equal
if they are related by a permutation of `ι`.  -/
SymmetricPower : (R : Type u) →
  Type u → [inst : CommSemiring R] → (M : Type v) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u v)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mul_toFun : ∀ (E : Type u_6) [inst : CommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : ContinuousMul E] (a : E × E),
  (ContinuousMonoidHom.mul E) a = a.1 * a.2
-- Aesop.Rule.Name
Aesop.RuleName.mk : Lean.Name → Aesop.BuilderName → Aesop.PhaseName → Aesop.ScopeName → UInt64 → Aesop.RuleName
-- Lean.Meta.Tactic.Grind.Internalize
/-- Internalizer for parametric `OfNat.ofNat` literals (see `isOfNatFinBitVecLiteral`).
For this kind of literal, we do **not** internalize its nested raw literal, but
we do internalize the type and instance to address issue #11545.
For example, we can have patterns of the form ``[P #0 (@OfNat.ofNat (Fin _) `[0] _)]``.

**Note**: `BitVec.ofNat` were previously internalized using `internalizeNonParametricLiteral`,
but it created problems when indexing theorems because `BitVec.ofNat` was not activated.
We now internalize this kind of application as a regular one.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeOfNatFinBitVecLiteral : Lean.Expr → ℕ → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_38 : HAdd Std.Time.Week.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β}, k ∉ t₂ → Std.ExtDTreeMap.Const.getD (t₁ ∩ t₂) k fallback = fallback
-- Init.Data.Array.Lex.Lemmas
Array.lt_irrefl : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] (xs : Array α), ¬xs < xs
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.mk.inj : ∀ {fvarId : Lean.FVarId} {val : Lean.InductiveVal} {fvarId_1 : Lean.FVarId} {val_1 : Lean.InductiveVal},
  { fvarId := fvarId, val := val } = { fvarId := fvarId_1, val := val_1 } → fvarId = fvarId_1 ∧ val = val_1
-- Mathlib.Algebra.Group.End
Equiv.Perm.mul_symm : ∀ {α : Type u_4} (e : Equiv.Perm α), e * Equiv.symm e = 1
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_trans : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g h : CauSeq α abs},
  f < g → g < h → f < h
-- Mathlib.Topology.Order.Hom.Basic
/-- `ContinuousOrderHomClass F α β` states that `F` is a type of continuous monotone maps.

You should extend this class when you extend `ContinuousOrderHom`.  -/
ContinuousOrderHomClass : (F : Type u_6) →
  (α : outParam (Type u_7)) →
    (β : outParam (Type u_8)) →
      [Preorder α] → [Preorder β] → [TopologicalSpace α] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.default.inj : ∀ {b b_1 : Lean.IR.FnBody}, Lean.IR.Alt.default b = Lean.IR.Alt.default b_1 → b = b_1
-- Aesop.Rule.Name
Aesop.instOrdDisplayRuleName : Ord Aesop.DisplayRuleName
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.lift_ι : ∀ {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : SSet.Subcomplex.range f ≤ B),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.lift f hf) B.ι = f
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumber_spec : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  ∃ G x, (G.cliqueFinset 3).card = ruzsaSzemerediNumber α ∧ G.LocallyLinear
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.map_of_epi_of_preservesCokernel : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.PreservesZeroMorphisms] [(S.map F).HasHomology],
      CategoryTheory.Epi S.g →
        CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F → (S.map F).Exact
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instMonoidQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Monoid R] → (c : RingCon R) → Monoid c.Quotient
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
/-- Cyclotomic polynomials are always positive on inputs larger than one.
Similar to `cyclotomic_pos` but with the condition on the input rather than index of the
cyclotomic polynomial.  -/
Polynomial.cyclotomic_pos' : ∀ (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  1 < x → 0 < Polynomial.eval x (Polynomial.cyclotomic n R)
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.mk.inj : ∀ {rules rules_1 : Array Aesop.Frontend.RuleExpr}, { rules := rules } = { rules := rules_1 } → rules = rules_1
-- Lean.Expr
/-- Annotate the pattern `p` with `stx`. This is an auxiliary annotation
for producing better hover information.
 -/
Lean.mkPatternWithRef : Lean.Expr → Lean.Syntax → Lean.Expr
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.hom_app_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C), CategoryTheory.IsIso (α.hom.app X)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.ae_inf_principal_eq_mk : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {s : Set α} (h : AEMeasurable f (μ.restrict s)),
  f =ᶠ[MeasureTheory.ae μ ⊓ Filter.principal s] AEMeasurable.mk f h
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.exists_equivalence : ∀ (Ω : Type w) (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω) →
    (∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)) →
      ∃ h, Nonempty (CategoryTheory.SmallCategoryOfSet.categoryFamily Ω h ≌ C)
-- Mathlib.Data.FinEnum
_private.Mathlib.Data.FinEnum.0.FinEnum.Finset.enum.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
/-- Lebesgue measure scaled by √(1 - x ^ 2)⁻¹.  -/
Polynomial.Chebyshev.measureT : MeasureTheory.Measure ℝ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mul_inf : ∀ {X : AlgebraicGeometry.Scheme} (I J K : X.IdealSheafData), I * (J ⊔ K) = I * J ⊔ I * K
-- Mathlib.Order.LiminfLimsup
Filter.le_limsup_of_frequently_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : ConditionallyCompleteLattice α] {f : Filter ι} {u : ι → α} {a : α},
  (∃ᶠ (i : ι) in f, a ≤ u i) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_of_frequently_le._auto_1 →
      a ≤ Filter.limsup u f
-- Mathlib.Topology.MetricSpace.Thickening
/-- If `s` is compact, `t` is open and `s ⊆ t`, some `cthickening` of `s` is contained in `t`.  -/
IsCompact.exists_cthickening_subset_open : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsCompact s → IsOpen t → s ⊆ t → ∃ δ, 0 < δ ∧ Metric.cthickening δ s ⊆ t
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_diseq : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] [Lean.Grind.AddRightCancel α] {a b : α}
  {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → a ≠ b → a' ≠ b'
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.colimitPointwiseProductToProductColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasColimit (F i)]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.pi F).comp (CategoryTheory.Limits.Pi.functor α))],
  CategoryTheory.Limits.colimitPointwiseProductToProductColimit F =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.pointwiseProduct F)
      (CategoryTheory.Limits.coconePointwiseProduct fun s => CategoryTheory.Limits.colimit.cocone (F s))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.IsInfinitePlace.eq_1 : ∀ {K : Type u_1} [inst : Field K] (w : AbsoluteValue K ℝ), NumberField.IsInfinitePlace w = ∃ φ, NumberField.place φ = w
-- Mathlib.FieldTheory.Normal.Basic
/-- The group homomorphism given by restricting an algebra isomorphism to a normal subfield
is surjective.  -/
AlgEquiv.restrictNormalHom_surjective : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K₁ E] [inst_6 : IsScalarTower F K₁ E]
  [inst_7 : Normal F K₁] [Normal F E], Function.Surjective ⇑(AlgEquiv.restrictNormalHom K₁)
-- Mathlib.Data.ENNReal.Inv
ENNReal.iSup_mul_le : ∀ {ι : Type u_3} {u v : ι → ENNReal}, ⨆ i, u i * v i ≤ (⨆ i, u i) * ⨆ i, v i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.nnnorm_le_iff_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A) (r : NNReal),
  autoParam (0 ≤ a) CStarAlgebra.nnnorm_le_iff_of_nonneg._auto_1 → (‖a‖₊ ≤ r ↔ a ≤ (algebraMap NNReal A) r)
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.pos_eq_zero : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → (it.i = 0 ↔ l = [])
-- Mathlib.Topology.UniformSpace.UniformEmbedding
closure_image_mem_nhds_of_isUniformInducing : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set (α × α)} {e : α → β} (b : β),
  IsUniformInducing e → IsDenseInducing e → s ∈ uniformity α → ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ nhds b
-- Mathlib.Order.Filter.Cofinite
/-- **Alias** of `Set.Finite.cofinite_inf_principal_sdiff`. -/
Set.Finite.cofinite_inf_principal_diff : ∀ {α : Type u_2} {s t : Set α},
  t.Finite → Filter.cofinite ⊓ Filter.principal (s \ t) = Filter.cofinite ⊓ Filter.principal s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) {m : ℕ}
  (β : CategoryTheory.Abelian.Ext Y Z m) {p : ℕ} (h : n + m = p), α.comp (-β) h = -α.comp β h
-- Mathlib.Computability.Partrec
Computable.nat_bodd : Computable Nat.bodd
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.z.eq_1 : ∀ (u : PNat.XgcdType), u.z = u.zp.succPNat
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Z) h
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_counitIso_hom : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N),
  e.toSingleObjEquiv.counitIso.hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` is a process independent from `Y` and for all `i`, `X' i` is almost everywhere equal
to `X i`, then `X'` is also independent from `Y`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.IndepFun.process_congr_left : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  ProbabilityTheory.IndepFun (fun ω i => X i ω) Y P →
    (∀ (i : S), X i =ᵐ[P] X' i) → ProbabilityTheory.IndepFun (fun ω i => X' i ω) Y P
-- Lean.Data.Lsp.Internal
/-- Module queries for extracting .ilean information in the watchdog.  -/
Lean.Lsp.LeanQueryModuleParams.queries : Lean.Lsp.LeanQueryModuleParams → Array Lean.Lsp.LeanModuleQuery
-- Init.Data.Rat.Lemmas
Rat.nonneg_antisymm : ∀ {q : ℚ}, 0 ≤ q → 0 ≤ -q → q = 0
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalEquiv_symm_apply : ∀ (R : Type u) (A : Type z) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : Polynomial R →ₐ[R] A), (Polynomial.aevalEquiv R A).symm f = f Polynomial.X
-- Mathlib.Topology.Maps.Strict.Module
/-- The isomorphism of topological modules `M ⧸ f.ker ≃ f.range` given by a strict linear
map `f : M → N`. This is an avatar of the first isomorphism theorem.  -/
ContinuousLinearEquiv.quotKerEquivRange : {R : Type u_1} →
  {M : Type u_3} →
    {Nₗ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup Nₗ] →
            [inst_3 : Module R M] →
              [inst_4 : Module R Nₗ] →
                {fₗ : M →ₗ[R] Nₗ} →
                  [inst_5 : TopologicalSpace M] →
                    [inst_6 : TopologicalSpace Nₗ] → Topology.IsStrictMap ⇑fₗ → (M ⧸ fₗ.ker) ≃L[R] ↥fₗ.range
-- Mathlib.Algebra.Module.ZLattice.Covolume
_private.Mathlib.Algebra.Module.ZLattice.Covolume.0.ZLattice.covolume.tendsto_card_le_div''_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  {X : Set E},
  (∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) →
    ∀ {F : E → ℝ},
      (∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) →
        ∀ {c : ℝ}, 0 < c → c • {x | x ∈ X ∧ F x ≤ 1} = {x | x ∈ X ∧ F x ≤ c ^ Fintype.card ι}
-- Mathlib.Algebra.Module.Lattice
/-- `Module.finrank` version of `IsLattice.rank`.  -/
Submodule.IsLattice.finrank_of_pi : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsDomain R]
  [IsPrincipalIdealRing R] {ι : Type u_4} [inst_5 : Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K))
  [Submodule.IsLattice K M], Module.finrank R ↥M = Fintype.card ι
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
LieDerivation.ad_apply_lieDerivation : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L)
  (D : LieDerivation R L L), (LieDerivation.ad R L) (D x) = -⁅x, D⁆
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : Option β → Option β}, (t.alter k f).getKey! k = if (f t[k]?).isSome = true then k else default
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- The *Laplacian matrix* `lapMatrix G R` of a graph `G`
is the matrix `L = D - A` where `D` is the degree and `A` the adjacency matrix of `G`.  -/
SimpleGraph.lapMatrix : {V : Type u_1} →
  (R : Type u_2) →
    [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableEq V] → [AddGroupWithOne R] → Matrix V V R
-- Std.Data.HashSet.Lemmas
_private.Std.Data.HashSet.Lemmas.0.Std.HashSet.ext : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m m' : Std.HashSet α}, m.inner = m'.inner → m = m'
-- Mathlib.Topology.EMetricSpace.Diam
/-- If the distance between any two points in a set is bounded by some constant, this constant
bounds the diameter.  -/
Metric.ediam_le : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  (∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) → Metric.ediam s ≤ d
-- Init.Tactics
/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`.  -/
Lean.Parser.Attr.normCastLabel : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Around any point `x`, the Riemannian distance between two points is controlled by the distance
in the extended chart. In other words, the extended chart is locally Lipschitz.  -/
eventually_riemannianEDist_le_edist_extChartAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0, ∀ᶠ (y : M) in nhds x, Manifold.riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.kernelIsoKer_inv_kernel_ι_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↥(ModuleCat.Hom.hom f).ker),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f))
      ((CategoryTheory.ConcreteCategory.hom (ModuleCat.kernelIsoKer f).inv) x) =
    ↑x
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_multiset_of_infinite : ∀ (α : Type u) [Infinite α], Cardinal.mk (Multiset α) = Cardinal.mk α
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_himp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α),
  ↑(s ⇨ t) = ↑s ⇨ ↑t
-- Lean.Elab.ConfigEval.Types
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (reflect : α → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.configItem)),
  sizeOf { reflect := reflect } = 1
-- Mathlib.Algebra.MvPolynomial.Funext
/-- Two multivariate polynomials over an infinite integral domain are equal
if they are equal upon evaluating them on an arbitrary assignment of the variables.  -/
MvPolynomial.funext : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p q : MvPolynomial σ R},
  (∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q) → p = q
-- Mathlib.SetTheory.ZFC.PSet
/-- Embedding of one universe in another  -/
PSet.embed : PSet.{max (u + 1) v}
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.X.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  P.X =
    (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) (Polynomial.C Polynomial.X)
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult : Type
-- Mathlib.Data.EReal.Inv
EReal.mul_le_mul_of_nonpos_right : ∀ {a b c : EReal}, b ≤ a → c ≤ 0 → a * c ≤ b * c
-- Mathlib.Data.List.Forall2
List.Forall₂.flip : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : List α} {b : List β},
  List.Forall₂ (flip R) b a → List.Forall₂ R a b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.normEq0_eq : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (c : ℕ), ↑↑c = 0 → Lean.Grind.CommRing.Poly.denote ctx (p.normEq0 c) = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_1728_of_two_eq_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F], 2 = 0 → WeierstrassCurve.ofJ 1728 = WeierstrassCurve.ofJ0 F
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F],
  (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom =
    CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- An auxiliary construction to move between the graded tensor product of internally-graded objects
and the tensor product of direct sums.  -/
GradedTensorProduct.auxEquiv : (R : Type u_1) →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              GradedTensorProduct R 𝒜 ℬ ≃ₗ[R]
                                TensorProduct R (DirectSum ι fun i => ↥(𝒜 i)) (DirectSum ι fun i => ↥(ℬ i))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKey!ₘ_eq_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getKey!ₘ a = Std.Internal.List.getKey! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get.eq_1 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : δ)
  (l r : Std.DTreeMap.Internal.Impl α fun x => δ)
  (hlk_2 : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true),
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.inner size k' v' l r) k hlk_2 =
    match h : compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get l k ⋯
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get r k ⋯
    | Ordering.eq => v'
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.exists_seq_forall_of_frequently : ∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
  (∃ᶠ (n : ι) in l, p n) → ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.apply_eq_iff_eq_symm_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N), e m = n ↔ m = e.symm n