mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
/-- The composition product of a measure and a constant kernel is the product between the two
measures.  -/
MeasureTheory.Measure.compProd_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν],
  μ.compProd (ProbabilityTheory.Kernel.const α ν) = μ.prod ν
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instZero.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddConjClasses.instZero = { zero := ⟦0⟧ }
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_eq_bot : ∀ {M : Type u_1} [inst : Mul M] {c : Con M}, c.toSetoid = ⊥ ↔ c = ⊥
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : Subsingleton ι] (i : ι) (f : M [⋀^ι]→L[R] N) (x : M),
  ((ContinuousAlternatingMap.ofSubsingleton R M N i).symm f) x = f fun x_1 => x
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.toComposableArrows_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (a : Fin (1 + 1 + 1)),
  S.toComposableArrows.obj a =
    CategoryTheory.ComposableArrows.Precomp.obj (CategoryTheory.ComposableArrows.mk₁ S.g) S.X₁ a
-- Std.Http.Data.Chunk
/-- The byte data contained in this chunk.
 -/
Std.Http.Chunk.data : Std.Http.Chunk → ByteArray
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.TreeMap.getKeyLT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α → α
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn : ∀ (p : ℝ),
  (deriv fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun z =>
    p * z ^ (p - 1) * (1 - AkraBazziRecurrence.smoothingFn z) + z ^ (p - 1) / Real.log z ^ 2
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
/-- Let `X` and `Y` be locally of finite type `K`-schemes with `K` algebraically closed and `Y`
separated over `K`. Suppose `X` is reduced, then two `K`-morphisms `f g : X ⟶ Y` are equal if
they are equal on the closed points of a dense locally closed subset of `X`.  -/
AlgebraicGeometry.ext_of_apply_eq : ∀ {X Y : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [IsAlgClosed K] {f g : X ⟶ Y}
  (i : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsSeparated i]
  [AlgebraicGeometry.LocallyOfFiniteType i] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f i)] (S : Set ↥X),
  IsLocallyClosed S →
    Dense S →
      (∀ x ∈ S, IsClosed {x} → f x = g x) →
        CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i → f = g
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pos.skipWhile_string_eq_skipWhile_toSlice : ∀ {pat : String} {s : String.Slice} (curr : s.Pos), curr.skipWhile pat = curr.skipWhile pat.toSlice
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfc_nnreal_eq_image_cfc_real : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [IsTopologicalRing A] [T2Space A] [inst_6 : PartialOrder A] [inst_7 : NonnegSpectrumClass ℝ A]
  [inst_8 : StarOrderedRing A] [inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfc_nnreal_eq_image_cfc_real._auto_1 →
    (Set.range fun x => cfc x a) = (fun x => cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Raw.Const.getD (m₁ ∩ m₂) k fallback =
          if k ∈ m₂ then Std.DHashMap.Raw.Const.getD m₁ k fallback else fallback
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.case.sizeOf_spec : ∀ (tid : Lean.Name) (x : Lean.IR.VarId) (xType : Lean.IR.IRType) (cs : Array Lean.IR.Alt),
  sizeOf (Lean.IR.FnBody.case tid x xType cs) = 1 + sizeOf tid + sizeOf x + sizeOf xType + sizeOf cs
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_iff_filter : ∀ {α : Type u} [uniformSpace : UniformSpace α] {g : Filter α},
  g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_const' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (c : ℝ),
  (μ.tilted fun x => c) = (μ Set.univ)⁻¹ • μ
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_ciInf_mul_ciInf : ∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [inst : ConditionallyCompleteLattice α]
  [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α},
  (∀ (i : ι) (j : ι'), a ≤ g i * h j) → a ≤ iInf g * iInf h
-- Init.Data.Ord.Basic
Ordering.swap_gt : Ordering.gt.swap = Ordering.lt
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_2 : ∀ (k : Turing.PartrecToTM2.K') (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ')
  (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.push k s q) =
    insert (Turing.PartrecToTM2.Λ'.push k s q) (Turing.PartrecToTM2.trStmts₁ q)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  MeasureTheory.volume (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) *
      MeasureTheory.volume (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K))
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.nat_eq_lift_iff : ∀ {n : ℕ} {a : Cardinal.{u}}, ↑n = Cardinal.lift.{v, u} a ↔ ↑n = a
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.weightedHomogeneousSubmodule_one : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.weightedHomogeneousSubmodule R 1 n = MvPolynomial.homogeneousSubmodule σ R n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.self_lt_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulRightStrictMono α] {a : α}, a < 1 → a < a⁻¹
-- Mathlib.Data.QPF.Univariate.Basic
QPF.toFunctor : {F : Type u → Type v} → [self : QPF F] → Functor F
-- Mathlib.Probability.UniformOn
ProbabilityTheory.instIsZeroOrProbabilityMeasureUniformOn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (s : Set Ω),
  MeasureTheory.IsZeroOrProbabilityMeasure (ProbabilityTheory.uniformOn s)
-- Init.Data.Iterators.Basic
Std.Iterators.ProductivenessRelation.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (Rel : Std.IterM m β → Std.IterM m β → Prop) (wf : WellFounded Rel)
  (subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it)
  (Rel_1 : Std.IterM m β → Std.IterM m β → Prop) (wf_1 : WellFounded Rel_1)
  (subrelation_1 : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel_1 it' it),
  ({ Rel := Rel, wf := wf, subrelation := subrelation } = { Rel := Rel_1, wf := wf_1, subrelation := subrelation_1 }) =
    (Rel = Rel_1)
-- Mathlib.Data.Part
Part.mem_mk_iff : ∀ {α : Type u_1} {p : Prop} {o : p → α} {a : α}, a ∈ { Dom := p, get := o } ↔ ∃ (h : p), o h = a
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ¬Irreducible ↑p → ∃ a b, a ^ 2 + b ^ 2 = p
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.Limits.limit.π (F.obj j) k)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k)
      (CategoryTheory.Limits.limit.π (F.flip.obj k) j)
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.tensorProd_obj_right : ∀ (R S : CommRingCat) [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  ((R.tensorProd S).obj A).right = CommRingCat.of (TensorProduct ↑R ↑S ↑A.right)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ), Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.peek k a q) = Turing.TM2.SupportsStmt S q
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.one_add_α_sq : ∀ {q : ℕ}, (1 + LucasLehmer.X.α) ^ 2 = 2 * LucasLehmer.X.ω
-- Mathlib.Order.Interval.Finset.Defs
Prod.instLocallyFiniteOrderBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [LocallyFiniteOrderBot α] → [LocallyFiniteOrderBot β] → [DecidableLE (α × β)] → LocallyFiniteOrderBot (α × β)
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The sum over the values of `mulShift ψ b` for `ψ` primitive is zero when `b ≠ 0`
and `#R` otherwise.  -/
AddChar.sum_mulShift : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : DecidableEq R] {R' : Type u_2}
  [inst_3 : CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R),
  ψ.IsPrimitive → ∑ x, ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.forall_associated : ∀ {M : Type u_1} [inst : Monoid M] {p : Associates M → Prop},
  (∀ (a : Associates M), p a) ↔ ∀ (a : M), p (Associates.mk a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.eq_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p₁ : Lean.Grind.CommRing.Poly)
  (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.incl_map_φ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  (x : { I := PUnit.{w + 1}, obj := fun x => X }.I), ((CategoryTheory.Limits.FormalCoproduct.incl C).map f).φ x = f
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- The functor `Triangle C ⥤ Triangle D` that is induced by a functor `F : C ⥤ D`
which commutes with shift by `ℤ`.  -/
CategoryTheory.Functor.mapTriangle : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [F.CommShift ℤ] →
                CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C)
                  (CategoryTheory.Pretriangulated.Triangle D)
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_cons' : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (a : α) (comm : {x | x ∈ a ::ₘ s}.Pairwise Commute),
  (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.comp_id : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'), f.comp SimpleGraph.Hom.id = f
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities : Type
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Construct a prelax functor from a map on objects, and functors between the corresponding
hom types.  -/
CategoryTheory.PrelaxFunctor.mkOfHomFunctors : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : B → C) → ((a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)) → CategoryTheory.PrelaxFunctor B C
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_mk : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (A : V ≃ₗ[R] V)
  (h : LinearEquiv.det A = 1), ↑⟨A, h⟩ = A
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_sup_of_disjoint : ∀ {V : Type u_1} (v : V) {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑((G₁ ⊔ G₂).neighborSet v)]
  [inst_1 : Fintype ↑(G₁.neighborSet v)] [inst_2 : Fintype ↑(G₂.neighborSet v)] (h : Disjoint G₁ G₂),
  (G₁ ⊔ G₂).neighborFinset v = (G₁.neighborFinset v).disjUnion (G₂.neighborFinset v) ⋯
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAlt.self_eq_zero : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsAlt → ∀ (x : M₁), (B x) x = 0
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.map_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂)
  (t : F₁.Elements),
  ((CategoryTheory.CategoryOfElements.map α).obj t).snd = (CategoryTheory.ConcreteCategory.hom (α.app t.fst)) t.snd
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- **Alias** of `Multipliable.eventually_bounded_finsetProd`. -/
Multipliable.eventually_bounded_finset_prod : ∀ {ι : Type u_1} {v : ι → ℝ}, Multipliable v → ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
-- Init.Control.Basic
ForInStep.value_done : ∀ {β : Type u_1} (b : β), (ForInStep.done b).value = b
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} (f g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f + g) h =
    CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_lt_mul_of_neg_right : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a < b → c < 0 → b * c < a * c
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_left_id : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_sub : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a b : E i), lp.single p i (a - b) = lp.single p i a - lp.single p i b
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected.  -/
IsSelfAdjoint.isConnected_spectrum_compl : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → IsConnected (spectrum ℂ a)ᶜ
-- Mathlib.Data.UInt
USize.toBitVec_injective : Function.Injective USize.toBitVec
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `VectorMeasure.restrict` as an additive monoid homomorphism.  -/
MeasureTheory.VectorMeasure.restrictₗ : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {R : Type u_4} →
            [inst_2 : Semiring R] →
              [inst_3 : Module R M] →
                [inst_4 : ContinuousConstSMul R M] →
                  [inst_5 : ContinuousAdd M] →
                    Set α → MeasureTheory.VectorMeasure α M →ₗ[R] MeasureTheory.VectorMeasure α M
-- Mathlib.Analysis.Convex.Between
/-- A point lies in the interior of a 1-simplex if and only if it lies strictly between its
vertices.  -/
Affine.Simplex.mem_interior_iff_sbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {s : Affine.Simplex R P 1} {p : P}, p ∈ s.interior ↔ Sbtw R (s.points 0) p (s.points 1)
-- Init.Data.UInt.Lemmas
UInt16.ofFin_lt_iff_lt : ∀ {a b : Fin UInt16.size}, UInt16.ofFin a < UInt16.ofFin b ↔ a < b
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.homologyOp_hom_naturality : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (K.homologyOp i).hom =
    CategoryTheory.CategoryStruct.comp (L.homologyOp i).hom (HomologicalComplex.homologyMap φ i).op
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_addSubgroupOf_eq_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → AddSubgroup.map K.subtype (H.addSubgroupOf K) = H
-- Init.Data.Array.Lemmas
Array.toList_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {x : α}, (xs.setIfInBounds i x).toList = xs.toList.set i x
-- Mathlib.Order.RelIso.Basic
/-- The map `coe_fn : (r →r s) → (α → β)` is injective.  -/
RelHom.coe_fn_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions.mk : Option String → Lean.Lsp.StaticRegistrationOptions
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_one : ∀ (a : ℤ), a / 1 = a
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_snd : ∀ {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]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f k))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f k))
-- Mathlib.Data.Num.Lemmas
PosNum.le_to_nat : ∀ {m n : PosNum}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.inv_smul_integral_comp_sub_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c⁻¹ • ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
-- Mathlib.Algebra.Group.Even
/-- An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`,
for some root `r : α`.  -/
IsSquare : {α : Type u_2} → [Mul α] → α → Prop
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.cast_heq : ∀ {X : Type u} [inst : TopologicalSpace X] {x y x' y' : X} (hx : x' = x) (hy : y' = y)
  {γ : Path.Homotopic.Quotient x y}, γ.cast hx hy ≍ γ
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.single : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, b ∈ f a → StateTransition.Reaches₀ f a b
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
* for all `x : G`, `h (x ^ n) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

where `1 < b` and `c₀` are real numbers, then the torsion subgroup of `G` is finite.
 -/
CommGroup.finite_torsion_of_descent : ∀ {G : Type u_1} [inst : CommGroup G] {n : ℕ} {h : G → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : G), b * h x - c₀ ≤ h (x ^ n)) → ∀ [Northcott h], Finite ↥(CommGroup.torsion G)
-- Lean.Data.Lsp.Internal
/-- Used in the `$/lean/importClosure` watchdog -> worker notification.
Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
 -/
Lean.Lsp.LeanStaleDependencyParams : Type
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.continuous_of_ringHom : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace A] [IsModuleTopology R A]
  [inst_7 : TopologicalSpace B] [IsTopologicalSemiring B] (φ : A →+* B),
  Continuous ⇑(φ.comp (algebraMap R A)) → Continuous ⇑φ
-- Mathlib.Data.EReal.Operations
EReal.bot_sub : ∀ (x : EReal), ⊥ - x = ⊥
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.vars_sub_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R}
  [inst_1 : DecidableEq σ], (p - q).vars ⊆ p.vars ∪ q.vars
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j k : n) (r : R),
  (LieAlgebra.SpecialLinear.singleSubSingle i k) r - (LieAlgebra.SpecialLinear.singleSubSingle i j) r =
    (LieAlgebra.SpecialLinear.singleSubSingle j k) r
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Extract an isomorphism `(leftKanExtension L F) ⋙ G ≅ leftKanExtension L (F ⋙ G)` when `G`
preserves left Kan extensions.  -/
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (F : CategoryTheory.Functor A B) →
                    (L : CategoryTheory.Functor A C) →
                      [inst_4 : G.PreservesLeftKanExtension F L] →
                        [inst_5 : L.HasLeftKanExtension F] →
                          (L.leftKanExtension F).comp G ≅ L.leftKanExtension (F.comp G)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k), (s.orderEmbOfFin h) i ∈ s