mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.bsup_lt_ord_lift : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.lift.{v, u} o.card < c.cof → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.bsup f < c
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.mk.congr_simp : ∀ (toList toList_1 : List DyckStep) (e_toList : toList = toList_1)
  (count_U_eq_count_D : List.count DyckStep.U toList = List.count DyckStep.D toList)
  (count_D_le_count_U :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList) ≤ List.count DyckStep.U (List.take i toList)),
  { toList := toList, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } =
    { toList := toList_1, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }
-- Mathlib.Topology.Order.LocalExtr
isLocalMax_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {a : α} {b : β}, IsLocalMax (fun x => b) a
-- Mathlib.Combinatorics.Enumerative.Composition
List.splitWrtCompositionAux.eq_2 : ∀ {α : Type u_1} (x : List α) (n : ℕ) (ns : List ℕ),
  x.splitWrtCompositionAux (n :: ns) =
    match List.splitAt n x with
    | (l₁, l₂) => l₁ :: l₂.splitWrtCompositionAux ns
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.of.inj : ∀ {R : Type u_1} {X : Type u_2} {a a_1 : X}, FreeAlgebra.Pre.of a = FreeAlgebra.Pre.of a_1 → a = a_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_le_size : ∀ {w : ℕ} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (curr : ℕ) (s : aig.RefVec curr) (a : ℕ) (hcurr : curr ≤ w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls.size
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instUniqueSubtypeMemBot : {G : Type u_1} → [inst : AddGroup G] → Unique ↥⊥
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁ : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (x x_1 : D.J), D.oneHypercover.I₁ x x_1 = PUnit.{u + 1}
-- Init.Data.Nat.Div.Basic
Nat.mod_add_div : ∀ (m k : ℕ), m % k + k * (m / k) = m
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ico_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : LocallyFiniteOrder R]
  [Archimedean R] [Nontrivial R], Filter.Tendsto (fun n => Finset.Ico (-↑n) ↑n) Filter.atTop Filter.atTop
-- Mathlib.Data.ENat.Basic
ENat.add_lt_add_iff_left : ∀ {m n k : ℕ∞}, k ≠ ⊤ → (k + n < k + m ↔ n < m)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.mk.sizeOf_spec : ∀ {E : Type u_1} {c : E} [inst : SizeOf E] (rIn rOut : ℝ) (rIn_pos : 0 < rIn) (rIn_lt_rOut : rIn < rOut),
  sizeOf { rIn := rIn, rOut := rOut, rIn_pos := rIn_pos, rIn_lt_rOut := rIn_lt_rOut } =
    1 + sizeOf rIn + sizeOf rOut + sizeOf rIn_pos + sizeOf rIn_lt_rOut
-- Mathlib.Analysis.Complex.Isometry
/-- Takes an element of `ℂ ≃ₗᵢ[ℝ] ℂ` and checks if it is a rotation, returns an element of the
unit circle.  -/
rotationOf : (ℂ ≃ₗᵢ[ℝ] ℂ) → Circle
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_sum_univ : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3}
  [inst_9 : Fintype ι] (f : ι → R → R) (a : A),
  autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) cfc_sum_univ._auto_1 → cfc (∑ i, f i) a = ∑ i, cfc (f i) a
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3}
  [inst : MeasurableSpace γ] {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β}
  {g : β → MeasureTheory.Measure γ},
  AEMeasurable f m → AEMeasurable g (m.bind f) → (m.bind f).bind g = m.bind fun a => (f a).bind g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
IsSelfAdjoint.cfcₙ : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A IsSelfAdjoint] {f : R → R}
  {a : A}, IsSelfAdjoint (cfcₙ f a)
-- Mathlib.Algebra.Order.IsBotOne
ne_one_of_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], a < b → b ≠ 1
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.Under.closedUnderColimitsOfShape_discrete_empty : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T}
  [P.ContainsIdentities] [P.RespectsIso], P.underObj.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
-- Init.Data.Array.Lemmas
Array.replace_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α}, a ∉ xs → xs.replace a b = xs
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.symmetry_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.SymmetricCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (β_ Y X).hom h) = h
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig.mk.inj : ∀ {toConfig toConfig_1 : Lean.Meta.Simp.Config},
  { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1}
  {ρ α : Type u} {epost : EPred} [inst_4 : MonadExceptOf ε m] (x : ReaderT ρ m α) (h : ε → ReaderT ρ m α)
  (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp (MonadExceptOf.tryCatch (x.run r) fun e => (h e).run r) (fun a => post a r) epost ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Functoriality of limits.

Usually this morphism should be accessed through `lim.map`,
but may be needed separately when you have specified limits for the source and target functors,
but not necessarily for all functors of shape `J`.
 -/
CategoryTheory.Limits.limMap : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F G : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            [inst_3 : CategoryTheory.Limits.HasLimit G] →
              (F ⟶ G) → (CategoryTheory.Limits.limit F ⟶ CategoryTheory.Limits.limit G)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_one_of_one_lt_of_neg : ∀ {x : ENNReal} {z : ℝ}, 1 < x → z < 0 → x ^ z < 1
-- Lean.Expr
/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
makes a new function application with the results.  -/
Lean.Expr.traverseApp : {M : Type → Type u_1} → [Monad M] → (Lean.Expr → M Lean.Expr) → Lean.Expr → M Lean.Expr
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.isEq_compare_eq_beq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [Std.LawfulBEqCmp cmp] {a b : α}, (cmp a b).isEq = (a == b)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_op_smul_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] {a : A} {x y : E}, inner A (a • x) y = inner A x y * star a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Grind.Arith.Linear.Struct.u : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Level
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valuation.inversion_estimate : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x y : K} {γ : Γ₀ˣ}, y ≠ 0 → v (x - y) < min (↑γ * (v y * v y)) (v y) → v (x⁻¹ - y⁻¹) < ↑γ
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIrreducible_zeroLocus_iff : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.radical.IsPrime
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.Homotopic.equiv : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X}, Equivalence GenLoop.Homotopic
-- Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Meta.NormNum.isNat_ascFactorial : ∀ {n x l y : ℕ},
  Mathlib.Meta.NormNum.IsNat n x →
    Mathlib.Meta.NormNum.IsNat l y → ∀ (a : ℕ), x.ascFactorial y = a → Mathlib.Meta.NormNum.IsNat (n.ascFactorial l) a
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.qsmul_mk : ∀ {M : Type u_2} [inst : AddCommGroup M] (a : ℚ) (m : M) (s : ℕ+),
  a • DivisibleHull.mk m s = DivisibleHull.mk (a.num • m) (⟨a.den, ⋯⟩ * s)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- If the sequence of ordinal-indexed approximations takes a value twice,
then it actually stabilised at that value.  -/
OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b c : Ordinal.{u}},
  x ≤ f x →
    a < b →
      a ≤ c →
        OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b →
          OrdinalApprox.lfpApprox f x c ∈ Function.fixedPoints ⇑f
-- Lean.Elab.Tactic.RCases
/-- Get the name from a pattern, if provided  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.name? : Lean.Elab.Tactic.RCases.RCasesPatt → Option Lean.Name
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_const : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (a : α),
  (s.inf' H fun x => a) = a
-- Mathlib.Geometry.Diffeology.Basic
/-- The diffeology generated by a set `g` of plots.  -/
DiffeologicalSpace.generateFrom : {X : Type u_1} → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X)) → DiffeologicalSpace X
-- Mathlib.GroupTheory.GroupAction.Quotient
Subgroup.quotientCenterEmbedding_apply : ∀ {G : Type u_1} [inst : Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) (g : G) (s : ↑S),
  (Subgroup.quotientCenterEmbedding hS) (↑g) s = ⟨⁅g, ↑s⁆, ⋯⟩
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.tendsto_pow_atTop_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ},
  Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the left and `𝟙 X` on the right is a pullback square.  -/
CategoryTheory.IsPullback.zero_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPullback 0 0 (CategoryTheory.CategoryStruct.id X) 0
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.crlfToLf.go : String → String → String.Pos.Raw → String.Pos.Raw → String
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the base of a trivialization from a set to the whole space.  -/
Bundle.Trivialization.codExtend' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] →
            {s : Set B} →
              IsOpen s →
                {proj : Z → ↑s} →
                  Bundle.Trivialization F proj → [Nonempty (B → F → Z)] → Bundle.Trivialization F (Subtype.val ∘ proj)
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves limits if it creates limits and `D` has limits.  -/
CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.fromRel_eq_fromRel_iff_eq`. -/
Sym2.fromRel_eq_fromRell_iff_eq : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Std.Symm r₁) (sym₂ : Std.Symm r₂),
  Sym2.fromRel sym₁ = Sym2.fromRel sym₂ ↔ r₁ = r₂
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The Haar measure equals the Lebesgue measure on `ℝ`.  -/
MeasureTheory.addHaarMeasure_eq_volume : MeasureTheory.Measure.addHaarMeasure TopologicalSpace.PositiveCompacts.Icc01 = MeasureTheory.volume
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
        (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f)))
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of a Dirichlet character is differentiable, except at `s = 1` if the character is
trivial.
 -/
DirichletCharacter.differentiableAt_LFunction : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  s ≠ 1 ∨ χ ≠ 1 → DifferentiableAt ℂ (DirichletCharacter.LFunction χ) s
-- Mathlib.Tactic.Linter.DocString
/-- The "DocString" linter validates style conventions regarding doc-string formatting.
 -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.Style.docStringLinter : Lean.Linter
-- Mathlib.Algebra.GradedMonoid
/-- A tactic to for use as an optional value for `GMonoid.gnpow_zero'`.  -/
GradedMonoid.tacticApply_gmonoid_gnpowRec_zero_tac : Lean.ParserDescr
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] →
                  [inst_5 : Semiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [inst_7 : GradedAlgebra 𝒜] → Algebra S ↥(Submodule.baseChange S (𝒜 0))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.modify m k f) k = Option.map f (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfinitePos.pos : ∀ {x : ℝ*}, x.InfinitePos → 0 < x
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
/-- The closure of a property of objects of a category under limits of
shape `J` for a category `J`.  -/
CategoryTheory.ObjectProperty.limitClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Construct a cocone for the empty diagram given an object.  -/
CategoryTheory.Limits.asEmptyCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → C → CategoryTheory.Limits.Cocone (CategoryTheory.Functor.empty C)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.natAddLEFunctor_app' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n k l i : ℕ} (h : k + l ≤ n)
  {R₁ R₂ : CategoryTheory.ComposableArrows C n} (φ : R₁ ⟶ R₂)
  (x : autoParam (i ≤ l) CategoryTheory.ComposableArrows.natAddLEFunctor_app'._auto_1),
  CategoryTheory.ComposableArrows.app' ((CategoryTheory.ComposableArrows.natAddLEFunctor h).map φ) i x =
    CategoryTheory.ComposableArrows.app' φ (k + i) ⋯
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.T_S_rel : ModularGroup.S • ModularGroup.S • ModularGroup.S • ModularGroup.T • ModularGroup.S • ModularGroup.T • ModularGroup.S =
  ModularGroup.T⁻¹
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [hν : ProbabilityTheory.IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β},
      MeasurableSet s →
        ∀ {u : Set γ},
          u ∈ MeasurableSpace.countablePartition γ n →
            ∫ (x : γ) in u, κ.densityProcess ν n a x s ∂ν a = (κ a).real (u ×ˢ s)
-- Batteries.Data.PairingHeap
/-- `O(n)`. Convert the heap to a list in arbitrary order.  -/
Batteries.PairingHeap.toListUnordered : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → List α
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.of_neBot_imp : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {la : Filter α} {lb : Filter β},
  (la.NeBot → Filter.Tendsto f la lb) → Filter.Tendsto f la lb
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  (∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e) →
    HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLE_eq_span_X_pow : ∀ {R : Type u} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ},
  Polynomial.degreeLE R ↑n = Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) (Finset.range (n + 1)))
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.coe_fieldRange : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L),
  ↑f.fieldRange = Set.range ⇑f
-- Mathlib.FieldTheory.IntermediateField.Basic
AlgHom.coe_fieldRange : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L'), ↑f.fieldRange = Set.range ⇑f
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioc_sub_one_left_eq_Icc_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a : α}, ¬IsMin a → ∀ (b : α), Finset.Ioc (a - 1) b = Finset.Icc a b
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.zpow : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {α : Type u_1} {l : Filter α}
  {f : α → G} {x : G}, Filter.Tendsto f l (nhds x) → ∀ (z : ℤ), Filter.Tendsto (fun x => f x ^ z) l (nhds (x ^ z))
-- Mathlib.Analysis.Normed.Group.Uniform
Isometry.nnnorm_map_of_map_zero : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F},
  Isometry f → f 0 = 0 → ∀ (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_exp_eq_iff_re_eq : ∀ {x y : ℂ}, ‖Complex.exp x‖ = ‖Complex.exp y‖ ↔ x.re = y.re
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The canonical diffeomorphism `M ⊕ M' → M' ⊕ M`: this is `Sum.swap` as a diffeomorphism  -/
Diffeomorph.sumComm : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_5} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_9) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (n : WithTop ℕ∞) →
                        (M' : Type u_13) →
                          [inst_6 : TopologicalSpace M'] →
                            [inst_7 : ChartedSpace H M'] → Diffeomorph I I (M ⊕ M') (M' ⊕ M) n
-- Mathlib.Combinatorics.SimpleGraph.Star
/-- The star graph on `V` centered at `r`: every non-center vertex is adjacent to `r`.  -/
SimpleGraph.starGraph : {V : Type u_1} → V → SimpleGraph V
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.pathStar_bijective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V),
  (∀ (u : U), Function.Bijective (φ.star u)) → ∀ (u : U), Function.Bijective (φ.pathStar u)
-- Lean.Parser.Command
/-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`  -/
Lean.Parser.Command.optDeclSig : Lean.Parser.Parser
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_mul_apply : ∀ {f : ArithmeticFunction ℕ} {x : ℕ}, (ArithmeticFunction.zeta * f) x = ∑ i ∈ x.divisors, f i
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.iUnion_range_comap_comp_evalRingHom : ∀ {ι : Type u_3} {R : ι → Type u_4} [inst : (i : ι) → CommRing (R i)] [Finite ι] {S : Type u_5} [inst_2 : CommRing S]
  (f : S →+* (i : ι) → R i),
  ⋃ i, Set.range (PrimeSpectrum.comap ((Pi.evalRingHom R i).comp f)) = Set.range (PrimeSpectrum.comap f)
-- Init.System.IOError
IO.Error.mkAlreadyExistsFile : String → UInt32 → String → IO.Error
-- Mathlib.Data.List.Basic
List.mem_take_iff_idxOf_lt : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {n : ℕ} {l : List α},
  a ∈ l → (a ∈ List.take n l ↔ List.idxOf a l < n)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`.  -/
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C)
          (CategoryTheory.CommMon C)
-- Mathlib.Topology.ClusterPt
/-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty.  -/
interior_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot], interior {x} = ∅
-- Std.Time.Format.Modifier
Std.Time.Year.extended.inj : ∀ {num num_1 : ℕ}, Std.Time.Year.extended num = Std.Time.Year.extended num_1 → num = num_1
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMul.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.unitsSMul φ u w =
    if h : HNNExtension.NormalWord.Cancels u w then HNNExtension.NormalWord.unitsSMulWithCancel φ u w h
    else
      let g' := HNNExtension.NormalWord.unitsSMulGroup φ d u w.head;
      HNNExtension.NormalWord.cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯