mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.mk : {R : Type u} →
  [inst : Ring R] →
    (carrier : Type v) → [isAddCommGroup : AddCommGroup carrier] → [isModule : Module R carrier] → ModuleCat R
-- Mathlib.Topology.MetricSpace.Bounded
/-- The diameter of a set in a metric space. To get controllable behavior even when the diameter
should be infinite, we express it in terms of the `ediam`  -/
Metric.diam : {α : Type u} → [PseudoMetricSpace α] → Set α → ℝ
-- Init.GrindInstances.Ring.Fin
Fin.intCast.eq_1 : ∀ {n : ℕ} [inst : NeZero n] (a : ℤ), Fin.intCast a = if 0 ≤ a then Fin.ofNat n a.natAbs else -Fin.ofNat n a.natAbs
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_left_K : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.K = h.left.K
-- Init.Data.Nat.Bitwise.Basic
/-- Shifts the binary representation of a value left by the specified number of bits. Usually accessed
via the `<<<` operator.

Examples:
 * `1 <<< 2 = 4`
 * `1 <<< 3 = 8`
 * `0 <<< 3 = 0`
 * `0xf1 <<< 4 = 0xf10`
 -/
Nat.shiftLeft : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a + b).re = a.re + b.re
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.instPreservesFiniteProductsUnderTensorProd : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S], CategoryTheory.Limits.PreservesFiniteProducts (R.tensorProd S)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
pos_of_left_mul_lt_le : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R]
  [AddRightReflectLE R], b * a < c * a → b ≤ c → 0 < a
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instSMulWithZeroSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} → [inst_3 : Zero X] → [SMulWithZero L X] → (F : IntermediateField K L) → SMulWithZero (↥F) X
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_mul_le : ∀ {M : Type u_2} [inst : Mul M] {s t : Set M}, Cardinal.mk ↑(s * t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
-- Init.Data.ByteArray.Bootstrap
List.toByteArray.loop.eq_def : ∀ (x : List UInt8) (x_1 : ByteArray),
  List.toByteArray.loop x x_1 =
    match x, x_1 with
    | [], r => r
    | b :: bs, r => List.toByteArray.loop bs (r.push b)
-- Lean.Parser.Term
/-- `+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
 -/
Lean.Parser.Term.posConfigItem : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.Images
/-- `f` factors through its coimage via the canonical morphism `p`.  -/
CategoryTheory.Abelian.coimage.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasKernel f]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.Abelian.factorThruCoimage f) =
    f
-- Mathlib.Data.List.DropRight
List.rdrop_eq_reverse_drop_reverse : ∀ {α : Type u_1} (l : List α) (n : ℕ), l.rdrop n = (List.drop n l.reverse).reverse
-- Mathlib.Data.Nat.Bitwise
Nat.testBit_eq_false_of_lt : ∀ {n i : ℕ}, n < 2 ^ i → n.testBit i = false
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.mk.injEq : ∀ (fvarId : Lean.FVarId) (idx : ℕ) (fvarId_1 : Lean.FVarId) (idx_1 : ℕ),
  ({ fvarId := fvarId, idx := idx } = { fvarId := fvarId_1, idx := idx_1 }) = (fvarId = fvarId_1 ∧ idx = idx_1)
-- Mathlib.CategoryTheory.PEmpty
/-- The (unique) functor from an empty category.  -/
CategoryTheory.functorOfIsEmpty : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u') → [inst_1 : CategoryTheory.Category.{v', u'} D] → [IsEmpty C] → CategoryTheory.Functor C D
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker_sound : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (proof : Array Std.Tactic.BVDecide.LRAT.IntAction),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker f proof = Std.Tactic.BVDecide.LRAT.Internal.Result.success →
        Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.nsmul_neg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M} {n : ℕ}, a < 0 → n ≠ 0 → n • a < 0
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.smallCategoryFinalModel : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    [inst_1 : CategoryTheory.FinallySmall J] → CategoryTheory.SmallCategory (CategoryTheory.FinalModel J)
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.unop_inj : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ}, Function.Injective Quiver.Hom.unop
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.eqToHom_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (h : X = Y),
  CategoryTheory.Arrow.Hom.left (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.InnerProductSpace.Completion
SeparationQuotient.inner_mk_mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 (SeparationQuotient.mk x) (SeparationQuotient.mk y) = inner 𝕜 x y
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_ofHom : ∀ {M N : Type u} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), AddMagmaCat.Hom.hom (AddMagmaCat.ofHom f) = f
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, k ∈ m.insertManyIfNewUnit l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_prod' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [L.LeAtTop] {s : Finset β}, Function.mulSupport f ⊆ ↑s → ∏'[L] (b : β), f b = ∏ b ∈ s, f b
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_single : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (p : ι → Prop)
  [inst_2 : DecidablePred p] (i : ι) (x : β i), (DFinsupp.filter p fun₀ | i => x) = if p i then fun₀ | i => x else 0
-- Init.Data.SInt.Basic
instShiftLeftInt8 : ShiftLeft Int8
-- Mathlib.CategoryTheory.Sites.Plus
/-- A natural transformation `P ⟶ Q` induces a natural transformation
between diagrams whose colimits define the values of `plus`.  -/
CategoryTheory.GrothendieckTopology.diagramNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → (X : C) → J.diagram P X ⟶ J.diagram Q X
-- Init.Data.Ord.Basic
instOrdNat : Ord ℕ
-- Mathlib.Order.Closure
/-- The underlying function  -/
LowerAdjoint.toFun : {α : Type u_1} → {β : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → {u : β → α} → LowerAdjoint u → α → β
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeComp_inv_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (β : H ⟶ G) (α : G ⟶ F) (X : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.Cocone.precomposeComp β α).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `locallyLipschitz_inv_iff`. -/
LocallyLipschitz.inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz f → LocallyLipschitz f⁻¹
-- Mathlib.Computability.Language
Language.le_iff : ∀ {α : Type u_1} (l m : Language α), l ≤ m ↔ l + m = m
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.eq_of_le_pure : ∀ {X : Type u_2} {α : Filter X}, α.NeBot → ∀ {x y : X}, α ≤ pure x → α ≤ pure y → x = y
-- Mathlib.Algebra.Opposites
MulOpposite.instMul : {α : Type u_1} → [Mul α] → Mul αᵐᵒᵖ
-- Mathlib.Algebra.Group.Hom.Defs
map_nsmul : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddMonoid G] [inst_2 : AddMonoid H]
  [AddMonoidHomClass F G H] (f : F) (n : ℕ) (a : G), f (n • a) = n • f a
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.eq_of_le_of_cast_pow_eq_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (R : Type u_1) [inst : CommRing R] [CharP R p], ∀ i ≤ n, ↑p ^ i = 0 → i = n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.ppBasis? : Lean.Meta.Grind.Arith.CommRing.M✝ (Option Lean.MessageData)
-- Mathlib.Order.Hom.Order
OrderHom.instSemilatticeSup : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : SemilatticeSup β] → SemilatticeSup (α →o β)
-- Mathlib.Order.Lattice
Lattice.mk : {α : Type u} →
  [toSemilatticeSup : SemilatticeSup α] →
    (inf : α → α → α) →
      (∀ (a b : α), inf a b ≤ a) → (∀ (a b : α), inf a b ≤ b) → (∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c) → Lattice α
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.mkForInBody : Lean.Syntax →
  Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF →
    m₂.WF → ∀ (f : (a : α) → β a → γ a), m₁.Equiv m₂ → (Std.DHashMap.Raw.map f m₁).Equiv (Std.DHashMap.Raw.map f m₂)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.isCentralScalar : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] [inst_6 : DistribMulAction Rᵐᵒᵖ V₂] [inst_7 : IsCentralScalar R V₂],
  IsCentralScalar R (NormedAddGroupHom V₁ V₂)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_indep_iff_of_subset : ∀ {α : Type u_1} {X I : Set α} {M : Matroid α}, I ⊆ X → ((M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) ↔ M.Indep I)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- (Implementation)
The canonical map `(s.X ×[X] Uᵢ) ×[s.X] (s.X ×[X] Uⱼ) ⟶ (Uᵢ ×[Z] Y) ×[X] Uⱼ`

This is used in `gluedLift`.  -/
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (s : CategoryTheory.Limits.PullbackCone f g) →
            (i j : 𝒰.I₀) →
              CategoryTheory.Limits.pullback ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
                  ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
                (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V (i, j)
-- Mathlib.Data.Sigma.Interval
Sigma.card_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i),
  (Finset.Icc a b).card = if h : a.fst = b.fst then (Finset.Icc (h ▸ a.snd) b.snd).card else 0
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- **Alias** of the reverse direction of `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`. -/
LipschitzOnWith.approximatesLinearOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, LipschitzOnWith c (f - ⇑f') s → ApproximatesLinearOn f f' s c
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_congr : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α},
  (a == b) = true → Std.Internal.List.getValue? a l = Std.Internal.List.getValue? b l
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_sub : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f g : PowerSeries R), PowerSeries.subst a (f - g) = PowerSeries.subst a f - PowerSeries.subst a g
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_le_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K},
  ArchimedeanClass.FiniteResidueField.mk x ≤ ArchimedeanClass.FiniteResidueField.mk y ↔
    x ≤ y ∨ ArchimedeanClass.FiniteResidueField.mk x = ArchimedeanClass.FiniteResidueField.mk y
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.commutator_coe_linear_map : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {D1 D2 : LieDerivation R L L}, ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
-- Lean.ErrorExplanation
Lean.ErrorExplanation.instToJsonMetadata : Lean.ToJson Lean.ErrorExplanation.Metadata
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The open immersion `Spec Γ(X, U) ⟶ X` for an affine `U`.  -/
AlgebraicGeometry.IsAffineOpen.fromSpec : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} → AlgebraicGeometry.IsAffineOpen U → (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) ⟶ X)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g.hom =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right sq)
-- Init.Data.SInt.Lemmas
Int16.le_maxValue : ∀ (a : Int16), a ≤ Int16.maxValue
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftHomotopy_lifts : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E))
  (H_0 : ∀ (a : A), H (0, a) = p (f a)), p ∘ ⇑(cov.liftHomotopy H f H_0) = ⇑H
-- Init.Data.SInt.Lemmas
ISize.mul_one : ∀ (a : ISize), a * 1 = a
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_right_comm`.  -/
Filter.map_map₂_distrib_right : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : Filter α}
  {g : Filter β} {n : γ → δ} {m' : α → β' → δ} {n' : β → β'},
  (∀ (a : α) (b : β), n (m a b) = m' a (n' b)) → Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' f (Filter.map n' g)
-- Init.Data.Fin.Lemmas
Fin.subsingleton_iff_le_one : ∀ {n : ℕ}, Subsingleton (Fin n) ↔ n ≤ 1
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- **Vitali's convergence theorem**: A sequence of functions `f` converges to `g` in Lp if and
only if it is uniformly integrable and converges to `g` in measure.  -/
MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : ℕ → α → β} {g : α → β} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        MeasureTheory.MemLp g p μ →
          (MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ↔
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0))
-- Mathlib.Algebra.Ring.Commute
/-- Representation of a difference of two squares of commuting elements as a product.  -/
Commute.mul_self_sub_mul_self_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotMapOfEquivQuotMapCMapMk.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f = Ideal.quotEquivOfEq ⋯
-- Mathlib.MeasureTheory.Group.Measure
MeasurableSet.add_closure_zero_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : AddGroup G]
  [IsTopologicalAddGroup G] {s : Set G}, MeasurableSet s → s + closure {0} = s
-- Mathlib.MeasureTheory.Measure.AddContent
/-- The function associating to an interval `Ioc u v` the difference `f v - f u`.
Use instead `AddContent.ofIoc` which upgrades this function to an additive content.  -/
MeasureTheory.AddContent.onIocAux : {α : Type u_1} → [LinearOrder α] → {G : Type u_3} → [AddCommGroup G] → (α → G) → Set α → G
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.dvd_mul_of_dvd_ne : ∀ {p1 p2 n : ℕ}, p1 ≠ p2 → Nat.Prime p1 → Nat.Prime p2 → p1 ∣ n → p2 ∣ n → p1 * p2 ∣ n
-- Init.Data.Option.Array
Option.toArray_eq_singleton_iff : ∀ {α : Type u_1} {a : α} {o : Option α}, o.toArray = #[a] ↔ o = some a
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Measurable.re : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m : MeasurableSpace α} {f : α → 𝕜},
  Measurable f → Measurable fun x => RCLike.re (f x)
-- Mathlib.Analysis.Seminorm
/-- Let `p i` be a family of seminorms on `E`. Let `s` be an absorbent set in `𝕜`.
If all seminorms are uniformly bounded at every point of `s`,
then they are bounded in the space of seminorms.  -/
Seminorm.bddAbove_of_absorbent : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} {s : Set E},
  Absorbent 𝕜 s → (∀ x ∈ s, BddAbove (Set.range fun x_1 => (p x_1) x)) → BddAbove (Set.range p)
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- The cover of any object `W : C` attached to a family of objects `Y` that satisfy
`J.CoversTop Y`  -/
CategoryTheory.GrothendieckTopology.CoversTop.cover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {I : Type u_1} → {Y : I → C} → J.CoversTop Y → (W : C) → J.Cover W
-- Init.Data.Rat.Lemmas
Rat.mkRat_eq_zero : ∀ {d : ℕ} {n : ℤ}, d ≠ 0 → (mkRat n d = 0 ↔ n = 0)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- Removing the leading `o` from a term of `MaxProducts C` yields a list which `isGood` with respect to
`C'`.
 -/
Profinite.NobelingProof.GoodProducts.maxTail_isGood : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C →
    Profinite.NobelingProof.contained C (Order.succ o) →
      ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)),
        ⊤ ≤
            Submodule.span ℤ
              (Set.range
                (Profinite.NobelingProof.GoodProducts.eval
                  (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))) →
          Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.C' C ho) (↑l).Tail
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiInf_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {f : β → α}, ⨅ i ∈ ∅, f i = sInf ∅
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_eq_of_omega0_le_left : ∀ {a b : Ordinal.{u_1}}, Ordinal.omega0 ≤ a → 0 < b → (a ^ b).card = max a.card b.card
-- Mathlib.CategoryTheory.Limits.Sifted
/-- The product of two sifted categories is sifted.  -/
CategoryTheory.IsSifted.prod_isSifted : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  [CategoryTheory.IsSifted C] [CategoryTheory.IsSifted D], CategoryTheory.IsSifted (C × D)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j) {Z : SSet}
  (h : (f.filtration (Order.succ j)).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (f.b j) h) =
    CategoryTheory.CategoryStruct.comp c.mapToSucc h
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (x : Std.Sat.AIG.Decl α) →
      (x = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
        ((idx : α) → x = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → x = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive x
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character is `1` or `-1` on nonzero arguments.  -/
quadraticChar_dichotomy : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  a ≠ 0 → (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1
-- Mathlib.Order.InitialSeg
PrincipalSeg.trans_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t), (f.trans g).top = g.toRelEmbedding f.top
-- Mathlib.Data.Finset.NatDivisors
Nat.divisorsHom_apply : ∀ (n : ℕ), Nat.divisorsHom n = n.divisors
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.ι_colimitIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G] (X : C) {Z : E}
  (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Final.colimitIso F G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X)) h
-- Mathlib.Data.Sum.Order
Sum.instAntisymmLiftRel_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Antisymm r] [Std.Antisymm s],
  Std.Antisymm (Sum.LiftRel r s)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instNonemptyQuotient : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) [Nonempty X], Nonempty (Quotient S.toSetoid)