mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Producers.Monadic.Empty
_private.Std.Data.Iterators.Producers.Monadic.Empty.0.Std.Iterators.Types.Empty.instFinitenessRelation : {m : Type w → Type w'} →
  {β : Type w} → [inst : Monad m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Empty m β) m
-- Mathlib.Topology.WithTopology
WithTopology.instPreorder : {X : Type u_1} → (t : TopologicalSpace X) → [Preorder X] → Preorder (WithTopology X t)
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The canonical fork on `f g : A ⟶ B` given by the equalizer.  -/
CommRingCat.Under.equalizerFork : {R : CommRingCat} → {A B : CategoryTheory.Under R} → (f g : A ⟶ B) → CategoryTheory.Limits.Fork f g
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.val_multiset_prod : ∀ {G : Type u_3} [inst : CommGroup G] (H : Subgroup G) (m : Multiset ↥H), ↑m.prod = (Multiset.map Subtype.val m).prod
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.uniformContinuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun x => x.1 ×ˢ x.2
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instInjectiveObjι : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.InjectiveObject C),
  CategoryTheory.Injective ((CategoryTheory.InjectiveObject.ι C).obj X)
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Millisecond.Offset
-- Init.Data.Order.Lemmas
Classical.Order.instBEq : {α : Type u} → [LE α] → BEq α
-- Mathlib.Analysis.Seminorm
/-- A seminorm on a module over a normed ring is a function to the reals that is positive
semidefinite, positive homogeneous, and subadditive.  -/
Seminorm : (𝕜 : Type u_12) → (E : Type u_13) → [SeminormedRing 𝕜] → [AddGroup E] → [SMul 𝕜 E] → Type u_13
-- Init.Data.List.Pairwise
List.Sublist.nodup : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_subset : ∀ {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α}, hs.toFinset ⊆ t ↔ s ⊆ ↑t
-- Mathlib.Data.Ordmap.Invariants
/-- O(n). Computes the actual number of elements in the set, ignoring the cached `size` field.  -/
Ordnode.realSize : {α : Type u_1} → Ordnode α → ℕ
-- Mathlib.Data.Matrix.Basic
Matrix.instFintypeOfDecidableEq : {n : Type u_14} →
  {m : Type u_15} →
    [Fintype m] →
      [DecidableEq m] → [Fintype n] → [DecidableEq n] → (α : Type u_16) → [Fintype α] → Fintype (Matrix m n α)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- For each stratum, specify a linear map to `R` as the Hahn series coefficient.  -/
HahnEmbedding.Seed.coeff : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              (self : HahnEmbedding.Seed K M R) →
                                (c : FiniteArchimedeanClass M) → ↥(self.stratum c) →ₗ[K] R
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.spineEquiv.eq_1 : ∀ {X : SSet} (sx : X.StrictSegal) (n : ℕ),
  sx.spineEquiv n = { toFun := X.spine n, invFun := sx.spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
-- Init.Grind.Lemmas
Lean.Grind.Bool.and_eq_of_eq_true_left : ∀ {a b : Bool}, a = true → (a && b) = b
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Constructor for objects of the category `Functor.LeftExtension L F`.  -/
CategoryTheory.Functor.LeftExtension.mk : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} → {F : CategoryTheory.Functor C H} → (F ⟶ L.comp F') → L.LeftExtension F
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.instCoeAlgebraNorm : {R : outParam (Type u_1)} →
  {S : outParam (Type u_2)} →
    [inst : SeminormedCommRing R] →
      [inst_1 : Ring S] → [inst_2 : Algebra R S] → Coe (MulAlgebraNorm R S) (AlgebraNorm R S)
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instZero : Zero NONote
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_neg' : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalRing A] [inst_8 : StarRing A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R),
  cfcₙ (-f) = -cfcₙ f
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_mul_transpose_submatrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : AddCommMonoid α]
  [inst_3 : Mul α] (e : m ≃ n) (M : Matrix m n α), M.submatrix id ⇑e * M.transpose.submatrix (⇑e) id = M * M.transpose
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.ExtTreeMap.maxKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_le_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km : α} (hc : Std.DTreeMap.Internal.Impl.contains k t = true),
  t.minKey?.get ⋯ = km → (compare km k).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
CategoryTheory.instMonoidalClosedFunctorType : {C : Type v₁} →
  [inst : CategoryTheory.SmallCategory C] → CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type v₁))
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K) {Z : C}
  (h : ((CategoryTheory.evaluation K C).obj k).obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.evaluation K C).obj k)) j) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F j).app k) h
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_comp_lsingle : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (m : M),
  (MonoidAlgebra.domCongr R A e).toLinearMap ∘ₗ MonoidAlgebra.lsingle m = MonoidAlgebra.lsingle (e m)
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_zero_max_size : ∀ {a : ByteArray} {i : ℕ}, a.extract 0 (max i a.size) = a
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- When `j` is a limit element, this is the extension to `d.Extension val₀ j`
of a family of elements in `d.Extension val₀ i` for all `i < j`.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension.limit : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} →
              [WellFoundedLT J] →
                (j : J) → Order.IsSuccLimit j → ((i : J) → i < j → d.Extension val₀ i) → d.Extension val₀ j
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffOn.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => Real.sin (f x)) s
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two parallel morphisms `f` and `g` have a coequalizer if the diagram `parallelPair f g` has a
colimit.  -/
CategoryTheory.Limits.HasCoequalizer : {C : Type u} → {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if they are uncorrelated.  -/
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_inner : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [CompleteSpace E] [BorelSpace E]
  [SecondCountableTopology E] [inst_5 : NormedAddCommGroup F] [inst_6 : MeasurableSpace F] [CompleteSpace F]
  [BorelSpace F] [SecondCountableTopology F] [inst_10 : InnerProductSpace ℝ E] [inst_11 : InnerProductSpace ℝ F]
  {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P →
    (∀ (x : E) (y : F), ProbabilityTheory.covariance (fun ω => inner ℝ x (X ω)) (fun ω => inner ℝ y (Y ω)) P = 0) →
      ProbabilityTheory.IndepFun X Y P
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
IsAssociatedPrime.annihilator_le : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsAssociatedPrime I M → ⊤.annihilator ≤ I
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_add : ∀ (a b : UInt64), (a + b).toUInt16 = a.toUInt16 + b.toUInt16
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimage_image_factorisation_assoc : ∀ {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.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
/-- A linear equivalence between `⨂[R] i, Dual R (M i)` and `Dual R (⨂[R] i, M i)` when all
`M i` are finite free modules. If `f : (i : ι) → Dual R (M i)`, then this equivalence sends
`⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the natural
isomorphism `⨂[R] i, R ≃ R` given by multiplication (`constantBaseRingEquiv`).  -/
PiTensorProduct.dualDistribEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : ι → Type u_4} →
      [inst : CommRing R] →
        [inst_1 : (i : ι) → AddCommGroup (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [∀ (i : ι), Module.Finite R (M i)] →
              [∀ (i : ι), Module.Free R (M i)] →
                [Finite ι] →
                  (PiTensorProduct R fun i => Module.Dual R (M i)) ≃ₗ[R] Module.Dual R (PiTensorProduct R fun i => M i)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- Pull an opposite subsemiring back to a subsemiring along `MulOpposite.op`  -/
Subsemiring.unop : {R : Type u_2} → [inst : NonAssocSemiring R] → Subsemiring Rᵐᵒᵖ → Subsemiring R
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Group` across an `Equiv`  -/
Equiv.group : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Group β] → Group α
-- Lean.Meta.Tactic.SplitIf
/-- Return the condition and decidable instance of an `if` expression to case split.  -/
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.findIfToSplit? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.distortion_eq_of_sub_eq_div : ∀ {ι : Type u_1} [inst : Fintype ι] {I J : BoxIntegral.Box ι} {r : ℝ},
  (∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r) → I.distortion = J.distortion
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Hilbert spaces, see `charFunDual_eq_pi_iff`
for the Banach space version.  -/
MeasureTheory.charFun_eq_pi_iff : ∀ {ι : Type u_6} [inst : Fintype ι] {E : ι → Type u_7} [inst_1 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_2 : (i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), CompleteSpace (E i)]
  [∀ (i : ι), SecondCountableTopology (E i)] [∀ (i : ι), BorelSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)}
  {ν : MeasureTheory.Measure ((i : ι) → E i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (t : WithLp 2 ((i : ι) → E i)),
      MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) ν) t =
        ∏ i, MeasureTheory.charFun (μ i) (t.ofLp i)) ↔
    ν = MeasureTheory.Measure.pi μ
-- Mathlib.Order.Lattice
SemilatticeInf.dual_dual : ∀ (α : Type u_1) [H : SemilatticeInf α], OrderDual.instSemilatticeInf αᵒᵈ = H
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_zero_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖ ≤ 0 ↔ a = 0
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_point_eq_point_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Affine.Simplex k P 1) (n : Fin 1), (s.faceOpposite 0).points n = s.points 1
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.RecArgInfo.mk : Lean.Name →
  Lean.Elab.FixedParamPerm → ℕ → Array ℕ → Lean.Elab.Structural.IndGroupInst → ℕ → Lean.Elab.Structural.RecArgInfo
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- a morphism `F.obj j ⟶ X`  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      {j : J} →
                        CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j → (F.obj j ⟶ X)
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRight_apply_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] [IsDomain S] {f : M₁ →ₗ[R] S} {x : M} [Module.IsTorsionFree S M],
  f.smulRight x = 0 ↔ f = 0 ∨ x = 0
-- Init.Data.SInt.Basic
/-- Converts word-sized signed integers to 64-bit signed integers that denote the same number. This
conversion is lossless, because `ISize` is either `Int32` or `Int64`.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.toInt64 : ISize → Int64
-- Lean.SubExpr
Lean.SubExpr.Pos.pushType : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Init.Grind.Lemmas
Lean.Grind.eq_eq_of_eq_true_left : ∀ {a b : Prop}, a = True → (a = b) = b
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.Functor.FullyFaithful.hasShift.map_add_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift D A]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C)
  (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C),
  F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X))
          ((i (a + b)).inv.app X)))
-- Mathlib.Topology.Sheaves.Skyscraper
/-- Taking stalks of a sheaf is the left adjoint functor to `skyscraperSheafFunctor`
 -/
stalkSkyscraperSheafAdjunction : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀) ⊣ skyscraperSheafFunctor p₀
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff_lt_of_lt_add`. -/
MeasureTheory.measureReal_diff_lt_of_lt_add : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    s ⊆ t →
      ∀ (ε : ℝ),
        μ.real t < μ.real s + ε →
          autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff_lt_of_lt_add._auto_1 → μ.real (t \ s) < ε
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : α → β) (g : (a : β) → Option.map f x = some a → γ),
  Std.Internal.List.Option.dmap✝ (Option.map f x) g = Std.Internal.List.Option.dmap✝ x fun a h => g (f a) ⋯
-- Init.Data.Iterators.Basic
/-- Match pattern for the `skip` case. See also `IterStep.skip`.
 -/
Std.PlausibleIterStep.skip : {α : Type u} →
  {β : Type w} →
    {IsPlausibleStep : Std.IterStep α β → Prop} →
      (it' : α) → IsPlausibleStep (Std.IterStep.skip it') → Std.PlausibleIterStep IsPlausibleStep
-- Mathlib.Topology.Defs.Induced
/-- The topology on the domain is equal to the induced topology.  -/
Topology.IsInducing.eq_induced : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → tX = TopologicalSpace.induced f tY
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_signExtend : ∀ {w : ℕ} (x : BitVec w) {v i : ℕ},
  (BitVec.signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.mk : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                (toFun : E → F) → ContDiff ℝ (↑n) toFun → Set.EqOn toFun 0 (↑K)ᶜ → ContDiffMapSupportedIn E F n K
-- Init.Data.Array.Erase
Array.getElem_eraseIdx_of_ge : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (w : i < xs.size) {j : ℕ} (h : j < (xs.eraseIdx i w).size),
  i ≤ j → (xs.eraseIdx i w)[j] = xs[j + 1]
-- Mathlib.Order.Hom.Basic
OrderHom.comp_prod_comp_same : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f₁ f₂ : β →o γ) (g : α →o β), (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Icc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : Preorder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α},
  Filter.Tendsto a l Filter.atBot →
    Filter.Tendsto b l Filter.atTop → MeasureTheory.AECover μ l fun i => Set.Icc (a i) (b i)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.of_hasCokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasCokernel f],
  { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.HasRightHomology
-- Mathlib.Order.JordanHolder
CompositionSeries.eq_snoc_eraseLast : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} (h : 0 < s.length),
  s = (RelSeries.eraseLast s).snoc (RelSeries.last s) ⋯
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). The `pushforwardFamily` defined is compatible.  -/
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} (x : ℱ.obj (Opposite.op X)),
  (CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x).Compatible
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.continuous_proj : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E), Continuous Bundle.TotalSpace.proj
-- Init.Data.SInt.Lemmas
Int32.toInt_one : Int32.toInt 1 = 1
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.toMulEquiv_trans : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Mul C] [inst_3 : Star A]
  [inst_4 : Star B] [inst_5 : Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C), (e₁.trans e₂).toMulEquiv = e₁.trans e₂.toMulEquiv
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] (j : J)
  {Z : CategoryTheory.Functor D C}
  (h : CategoryTheory.Limits.colimit (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit F G).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j) h
-- Mathlib.Analysis.Normed.Group.Basic
edist_eq_enorm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), edist a b = ‖-a + b‖ₑ
-- Init.Data.Ord.Basic
Ordering.not_isEq_eq_isNe : ∀ {o : Ordering}, (!o.isEq) = o.isNe
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) [J.HasPullbacks] {X : C}
  {R : CategoryTheory.Presieve X}, R ∈ J.coverings X → R.HasPairwisePullbacks
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanHalfSpace.convex : ∀ {n : ℕ} [inst : NeZero n], Convex ℝ {x | 0 ≤ x.ofLp 0}
-- Mathlib.Order.SetNotation
SupSet.mk : {α : Type u_1} → (Set α → α) → SupSet α