mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.smul_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} {R : Type u_6} [inst_4 : Semiring R]
  [inst_5 : DistribMulAction R N] [inst_6 : ContinuousConstSMul R N] (r : R),
  v.MutuallySingular w → v.MutuallySingular (r • w)
-- Mathlib.Algebra.DualNumber
/-- A version of `TrivSqZeroExt.snd_mul` with `*` instead of `•`.  -/
DualNumber.snd_mul : ∀ {R : Type u_1} [inst : Semiring R] (x y : DualNumber R),
  TrivSqZeroExt.snd (x * y) = TrivSqZeroExt.fst x * TrivSqZeroExt.snd y + TrivSqZeroExt.snd x * TrivSqZeroExt.fst y
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallyDisconnected_of_totallyDisconnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α] (s : Set α), IsTotallyDisconnected s
-- Mathlib.Combinatorics.KatonaCircle
/-- `IsPrefix f s` means that the elements of `s` precede the elements of `sᶜ`
in the numbering `f`.  -/
Numbering.IsPrefix : {X : Type u_1} → [inst : Fintype X] → Numbering X → Finset X → Prop
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.compLeftInverse_apply_of_bdd : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : DivisionRing 𝕜]
  [inst_1 : DivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : SeminormedAddCommGroup Eₗ] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : Module 𝕜 Eₗ]
  (f : E →ₛₗ[σ₁₂] F) (g : E →ₗ[𝕜] Eₗ),
  (∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖) → ∀ (x : E) (y : Eₗ) (hx : g x = y), (f.compLeftInverse g) ⟨y, ⋯⟩ = f x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_obj_addGrp_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.AddMonObj.zero)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyIncomingCall.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyIncomingCall
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A `DayConvolutionUnit` structure on a functor `C ⥤ V` is the data of a pointwise
left Kan extension of `fromPUnit (𝟙_ V)` along `fromPUnit (𝟙_ C)`. Again, this is
made a class to ease proofs when constructing `DayConvolutionMonoidalCategory` structures, but one
should avoid registering it globally.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory V] → CategoryTheory.Functor C V → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Order.Ideal
Order.Ideal.sup_mem_iff : ∀ {P : Type u_1} [inst : SemilatticeSup P] {x y : P} {I : Order.Ideal P}, x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNat_inv_zero : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α}, Mathlib.Meta.NormNum.IsNat a 0 → Mathlib.Meta.NormNum.IsNat a⁻¹ 0
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.prod_apply : ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') (x : α),
  ↑(l.prod l') x = Sum.elim (↑l x) (↑l' x)
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivAt.of_comp_of_leftInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G}
  {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E},
  ContinuousAt g a →
    HasFDerivAt f f' (g a) →
      HasFDerivAt h h' a → f ∘ g =ᶠ[nhds a] h → Function.LeftInverse ⇑f'symm ⇑f' → HasFDerivAt g (f'symm ∘SL h') a
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_divLeft : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul G] [MeasurableInv G] (g : G),
  MeasurableEmbedding fun x => g / x
-- Mathlib.Data.Nat.Cast.Basic
Nat.ofNat_nsmul_eq_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) [inst_1 : n.AtLeastTwo] (a : α),
  OfNat.ofNat n • a = OfNat.ofNat n * a
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat.eq_def : ∀ (s₁ s₂ : Lean.Grind.AC.Seq),
  s₁.concat s₂ =
    match s₁ with
    | Lean.Grind.AC.Seq.var x => Lean.Grind.AC.Seq.cons x s₂
    | Lean.Grind.AC.Seq.cons x s => Lean.Grind.AC.Seq.cons x (s.concat s₂)
-- Mathlib.Topology.Neighborhoods
tendsto_atTop_of_eventually_const : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Type u_2} [inst_1 : Preorder ι] {u : ι → X} {i₀ : ι},
  (∀ i ≥ i₀, u i = x) → Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.krullDimLE_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R], Ring.KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.min? = some km → t.getD km fallback = km
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `not_lt_zero`. -/
not_lt_zero' : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], ¬a < 0
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C}
  [self : CategoryTheory.HomRel.IsStableUnderPrecomp r] {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z},
  r g g' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g')
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.algebraMap_posRootForm_posForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (x y : ↥(Submodule.span S (Set.range ⇑P.root))),
  (algebraMap S R) (((P.posRootForm S).posForm x) y) = (P.RootForm ↑x) ↑y
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.op_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g) (X_1 : CategoryTheory.Limits.WalkingCospan),
  c.op.π.app X_1 =
    CategoryTheory.CategoryStruct.comp (c.ι.app X_1).op
      (match X_1 with
        | none => CategoryTheory.Iso.refl (Opposite.op X)
        | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y)
        | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).inv
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Init.Data.Int.Order
Int.natCast_nonneg : ∀ (n : ℕ), 0 ≤ ↑n
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing linear maps as a bilinear map from `(M →ₛₗ[σ₁₂] N) × (N →ₛₗ[σ₂₃] P)`
to `M →ₛₗ[σ₁₃] P`.  -/
LinearMap.llcomp : {R : Type u_2} →
  [inst : CommSemiring R] →
    {R₂ : Type u_14} →
      (R₃ : Type u_15) →
        (M : Type u_17) →
          (N : Type u_18) →
            (P : Type u_19) →
              [inst_1 : CommSemiring R₂] →
                [inst_2 : CommSemiring R₃] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid N] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R₂ N] →
                            [inst_8 : Module R₃ P] →
                              {σ₁₂ : R →+* R₂} →
                                {σ₁₃ : R →+* R₃} →
                                  {σ₂₃ : R₂ →+* R₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      (N →ₛₗ[σ₂₃] P) →ₗ[R₃] (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_single_single : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Zero α] [inst_1 : Zero β] [inst_2 : Zero γ] [inst_3 : DecidableEq l] [inst_4 : DecidableEq m]
  [inst_5 : DecidableEq n] [inst_6 : DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) →
    (∀ (a : α), f a 0 = 0) →
      ∀ (a : α) (b : β),
        Matrix.kroneckerMap f (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) = Matrix.single (i₁, i₂) (j₁, j₂) (f a b)
-- Init.Data.SInt.Lemmas
Int32.ne_iff_ofBitVec_ne : ∀ {a b : BitVec 32}, a ≠ b ↔ Int32.ofBitVec a ≠ Int32.ofBitVec b
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.homMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] {X Y : C} [inst_5 : HomotopicalAlgebra.IsCofibrant X]
  [inst_6 : HomotopicalAlgebra.IsCofibrant Y] [inst_7 : HomotopicalAlgebra.IsFibrant X]
  [inst_8 : HomotopicalAlgebra.IsFibrant Y]
  (f : HomotopicalAlgebra.BifibrantObject.mk X ⟶ HomotopicalAlgebra.BifibrantObject.mk Y),
  ∃ g, f = HomotopicalAlgebra.BifibrantObject.homMk g
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.star_dotProduct_gram_mulVec : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype n] (v : n → E) (x y : n → 𝕜),
  star x ⬝ᵥ (Matrix.gram 𝕜 v).mulVec y = inner 𝕜 (∑ i, x i • v i) (∑ i, y i • v i)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
instAddTensorProduct : (R : Type u_3) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      (N : Type u_2) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → Add (TensorProduct R M N)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (a : α) (x : ℝ), MeasureTheory.Integrable (fun b => ↑(f (a, b)) x) (ν a)
-- Mathlib.Topology.Compactness.Compact
noncompactSpace_of_neBot : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.cocompact X).NeBot → NoncompactSpace X
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.Flat f ∧ AlgebraicGeometry.Surjective f ↔
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FaithfullyFlat
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `posPart_eq_self`. -/
posPart_of_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, 0 ≤ a → a⁺ = a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.support_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).support = List.map (⇑f) p.support
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.List.Nat.Basic
List.getElem?_intersperse_two_mul : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ}, (List.intersperse sep l)[2 * i]? = l[i]?
-- Init.Core
/-- Helper theorem for proving injectivity theorems  -/
Lean.injEq_helper : ∀ {P Q R : Prop}, (P → Q → R) → P ∧ Q → R
-- Std.Internal.Do.WP.Frame
/-- When `x` frames `(op F ·)`, `(op F ·)` commutes into the postcondition of `wp x`.  -/
Std.Internal.Do.WP.Frames.conj_wp_le_wp_conj : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {R : Type t}
  {op : R → Pred → Pred} {x : Prog} {F : R},
  Std.Internal.Do.WP.Frames op x F →
    ∀ (Q : Value → Pred) (E : EPred),
      Lean.Order.PartialOrder.rel (op F (Std.Internal.Do.wp x Q E)) (Std.Internal.Do.wp x (fun a => op F (Q a)) E)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_zpow : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (χ : MulChar R R') (f : R' →+* R'') (n : ℤ), χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
-- Mathlib.Order.Filter.CountableSeparatingOn
exists_seq_separating : ∀ (α : Type u_1) {p : Set α → Prop} {s₀ : Set α},
  p s₀ →
    ∀ (t : Set α) [HasCountableSeparatingOn α p t],
      ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.denoteExpr : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (c : 𝕜) (x : E) {r : ℝ}, 0 ≤ r → c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If a function defined on a topological group has a support contained in a
compact set, then either the function is trivial or the group is locally compact.  -/
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] [inst_4 : Zero α] [T1Space α] {f : G → α} {k : Set G},
  IsCompact k → Function.support f ⊆ k → Continuous f → f = 0 ∨ LocallyCompactSpace G
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_sum_Icc : ∀ (x : ℝ), Chebyshev.theta x = ∑ p ∈ Finset.Icc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p
-- Mathlib.Order.CompleteLattice.Defs
/-- Transfer `SupSet` across an `Equiv`.  -/
Equiv.supSet : {α : Type u_1} → {β : Type u_2} → α ≃ β → [SupSet β] → SupSet α
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isOpenEmbedding_iff_isIso_comp' : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f],
  Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instEpimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.epimorphisms C).IsMultiplicative
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Uniform integrability is preserved by restriction of the measure to a set.  -/
MeasureTheory.UnifIntegrable.restrict : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ → ∀ (E : Set α), MeasureTheory.UnifIntegrable f p (μ.restrict E)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.toList : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n → Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.Data.Quot
Quot.map₂_mk : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : α → β → γ)
  (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → t (f a b₁) (f a b₂))
  (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → t (f a₁ b) (f a₂ b)) (a : α) (b : β),
  Quot.map₂ f hr hs (Quot.mk r a) (Quot.mk s b) = Quot.mk t (f a b)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSet.unique : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α]
  {p q : Associates.FactorSet α}, p.prod = q.prod → p = q
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_mul_lt_opow : ∀ {b u v x : Ordinal.{u_1}}, v < b → u < x → b ^ u * v < b ^ x
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey!_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.maxKey! (Std.Internal.List.Const.modifyKey k f l) == Std.Internal.List.maxKey! l) = true
-- Init.Data.List.Sublist
List.infix_nil : ∀ {α : Type u_1} {l : List α}, l <:+: [] ↔ l = []
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The natural isomorphism of bifunctors `F(- ⊗ -) ≅ F- ⊗ F-`, provided each
`prodComparison F A B` is an isomorphism.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] →
                (CategoryTheory.MonoidalCategory.curriedTensor C).comp
                    ((CategoryTheory.Functor.whiskeringRight C C D).obj F) ≅
                  F.comp
                    ((CategoryTheory.MonoidalCategory.curriedTensor D).comp
                      ((CategoryTheory.Functor.whiskeringLeft C D D).obj F))
-- Mathlib.Algebra.Order.Sub.Defs
le_tsub_of_add_le_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + b ≤ c → a ≤ c - b
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.trans_isBigOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =Θ[𝕜; l] g → g =O[𝕜; l] k → f =O[𝕜; l] k
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis'.closure_eq_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → M.closure I = M.closure X
-- Mathlib.RingTheory.Etale.StandardEtale
/-- `R[X][Y]/⟨f, Yg-1⟩ ≃ R[X, Y]/⟨f, Yg-1⟩`  -/
StandardEtalePair.equivMvPolynomialQuotient : {R : Type u_1} →
  [inst : CommRing R] →
    (P : StandardEtalePair R) →
      P.Ring ≃ₐ[R]
        MvPolynomial (Fin 2) R ⧸
          Ideal.span
            {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
              (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.const_smul` -/
AnalyticAt.fun_const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (fun i => c • f i) x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ ∩ m₂)[k]! = default
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.sup_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}, (M ⊔ N) * P = M * P ⊔ N * P
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulR.inj : ∀ {a : Int.Internal.Linear.Expr} {k : ℤ} {a_1 : Int.Internal.Linear.Expr} {k_1 : ℤ},
  a.mulR k = a_1.mulR k_1 → a = a_1 ∧ k = k_1
-- Mathlib.Analysis.Normed.Group.Basic
ne_zero_of_mem_unit_sphere : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : ↑(Metric.sphere 0 1)), ↑x ≠ 0
-- Std.Time.DateTime.Timestamp
_private.Std.Time.DateTime.Timestamp.0.Std.Time.Timestamp.mk.sizeOf_spec : ∀ (val : Std.Time.Duration), sizeOf { val := val } = 1 + sizeOf val
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a b : α) (xs : List α) (le : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match a :: b :: xs, le with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_3 a b xs le
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithInitial C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
                motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
                  motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x) →
              ((x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                  motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x) →
                motive X Y f
-- Mathlib.Analysis.Complex.Basic
realPart.norm_le : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] [inst_1 : StarAddMonoid A] [inst_2 : NormedSpace ℂ A]
  [inst_3 : StarModule ℂ A] [NormedStarGroup A] (x : A), ‖realPart x‖ ≤ ‖x‖
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (idx : ℕ) (mkInitial : IO σ) (asyncMode : Lean.EnvExtension.AsyncMode)
  (replay? : Option (Lean.ReplayFn σ)),
  sizeOf { idx := idx, mkInitial := mkInitial, asyncMode := asyncMode, replay? := replay? } =
    1 + sizeOf idx + sizeOf asyncMode + sizeOf replay?