mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise.eq_1 : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
  (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant (↑C₁) Z) (g : LocallyConstant (↑C₂) Z)
  (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩) [inst_1 : DecidablePred fun x => x ∈ C₁],
  LocallyConstant.piecewise h₁ h₂ h f g hfg =
    { toFun := fun i => if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩, isLocallyConstant := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.range_homOfLE_app_union_range_b_app : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι) (d : SimplexCategoryᵒᵖ),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.homOfLE ⋯).app d)) ⊔
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((f.b j).app d)) =
    Set.univ
-- Init.Data.Array.Sort.Basic
_private.Init.Data.Array.Sort.Basic.0.Array.MergeSort.Internal.merge : {α : Type u_1} → Array α → Array α → autoParam (α → α → Bool) Array.MergeSort.Internal.merge._auto_1✝ → Array α
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerived_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
  CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n =
    CategoryTheory.CategoryStruct.id (F.leftDerived n)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {X Z : C}
  {α : Type u_1} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [inst_2 : Finite α]
  [hi : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc i)] (a : α), CategoryTheory.Limits.HasPullback f (i a)
-- Aesop.RuleTac.Basic
Aesop.RuleTacOutput.mk.inj : ∀ {applications applications_1 : Array Aesop.RuleApplication},
  { applications := applications } = { applications := applications_1 } → applications = applications_1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, (s -ᵥ t).Nonempty → s.Nonempty
-- Mathlib.Data.List.Basic
List.mem_filter_of_mem : ∀ {α : Type u} {p : α → Bool} {a : α} {l : List α}, a ∈ l → p a = true → a ∈ List.filter p l
-- Init.Data.Array.Lemmas
Array.size_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, (Array.ofFn f).size = n
-- Mathlib.GroupTheory.Focal
AddSubgroup.focalAddSubgroupOf.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.focalAddSubgroupOf = H.focalAddSubgroup.addSubgroupOf H
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.star_mono : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A], Monotone star
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_eval_neg : ∀ (n : ℕ) (x : ℚ),
  Polynomial.eval (-x) (Polynomial.bernoulli n) =
    (-1) ^ n * (Polynomial.eval x (Polynomial.bernoulli n) + ↑n * x ^ (n - 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A category with strong epi mono factorisations admits functorial epi/mono factorizations.  -/
CategoryTheory.Limits.functorialEpiMonoFactorizationData : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
      (CategoryTheory.MorphismProperty.epimorphisms C).FunctorialFactorizationData
        (CategoryTheory.MorphismProperty.monomorphisms C)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  MeasurableSet s → (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
-- Mathlib.CategoryTheory.FintypeCat
/-- `uSwitch.{u, v}` is an equivalence of categories with quasi-inverse `uSwitch.{v, u}`.  -/
FintypeCat.uSwitchEquivalence : FintypeCat ≌ FintypeCat
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A column partitioned matrix multiplied by a block matrix results in a column partitioned
matrix.  -/
Matrix.fromCols_mul_fromBlocks : ∀ {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R]
  [inst_1 : Fintype m₁] [inst_2 : Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R)
  (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R),
  A₁.fromCols A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instSemigroupWithZero : SemigroupWithZero Complex.UnitDisc
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.to₁₂₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : VAdd M N] [inst_1 : VAdd M P]
  [inst_2 : VAdd M Q] [inst_3 : VAdd N P] [inst_4 : VAdd N Q] [inst_5 : AddMonoid P] [inst_6 : AddAction P Q]
  [VAddAssocClass M N P] [VAddAssocClass M P Q] [VAddAssocClass N P Q], VAddAssocClass M N Q
-- Mathlib.Data.Finsupp.Weight
Finsupp.le_weight_of_ne_zero : ∀ {σ : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {w : σ → M},
  (∀ (s : σ), 0 ≤ w s) → ∀ {s : σ} {f : σ →₀ ℕ}, f s ≠ 0 → w s ≤ (Finsupp.weight w) f
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.diag_map_star : ∀ {n : Type u_3} {α : Type v} [inst : Star α] (A : Matrix n n α), (A.map star).diag = star A.diag
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimMap_epi : ∀ {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.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (α : F ⟶ G) [∀ (j : J), CategoryTheory.Epi (α.app j)],
  CategoryTheory.Epi (CategoryTheory.Limits.colimMap α)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.whiskerRight : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (G : CategoryTheory.Functor D E) (A : Type u_5)
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A]
  [inst_6 : CategoryTheory.HasShift E A] [inst_7 : F₁.CommShift A] [inst_8 : F₂.CommShift A] [inst_9 : G.CommShift A]
  [CategoryTheory.NatTrans.CommShift τ A], CategoryTheory.NatTrans.CommShift (CategoryTheory.Functor.whiskerRight τ G) A
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_left : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → (c * a ≤ c * b ↔ b ≤ a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashablePoly : Hashable Lean.Grind.CommRing.Poly
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntryD.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a), Std.DTreeMap.Internal.Impl.leaf.minEntryD x = x
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C}
  (h : V₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd i₁ i₂) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k l₂ = false →
    Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = false
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.toLinearMap_starProjection_eq_isComplProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], ↑K.starProjection = K.projection Kᗮ ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_pos : ∀ {a : Cardinal.{u_1}} (b : Cardinal.{u_1}), 0 < a → 0 < a ^ b
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.le.sizeOf_spec : sizeOf Mathlib.Meta.Positivity.OrderRel.le✝ = 1
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_idem : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a : CauSeq α abs),
  a ⊔ a = a
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.rpow_abs_le_mul_exp_abs : ∀ (x : ℝ) {t p : ℝ}, 0 ≤ p → t ≠ 0 → |x| ^ p ≤ (p / |t|) ^ p * Real.exp (|t| * |x|)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
PartialOrder.mem_nerve_degenerate_of_eq : ∀ {X : Type u_1} [inst : PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n + 1 }))
  {i : Fin (n + 1)}, s.obj i.castSucc = s.obj i.succ → s ∈ (CategoryTheory.nerve X).degenerate (n + 1)
-- Mathlib.Data.Matrix.Mul
Matrix.nonUnitalNonAssocSemiring : {n : Type u_3} → {α : Type v} → [NonUnitalNonAssocSemiring α] → [Fintype n] → NonUnitalNonAssocSemiring (Matrix n n α)
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.monoCoprodType : CategoryTheory.Limits.MonoCoprod (Type u)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.length_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keys.length = t.size
-- Mathlib.Order.ScottContinuity
/-- A function between preorders is said to be Scott continuous on a set `D` of directed sets if it
preserves `IsLUB` on elements of `D`.

The dual notion

```lean
∀ ⦃d : Set α⦄, d ∈ D →  d.Nonempty → DirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)
```

does not appear to play a significant role in the literature, so is omitted here.
 -/
ScottContinuousOn : {α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → Set (Set α) → (α → β) → Prop
-- Mathlib.Order.IsNormal
Order.IsNormal.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} [inst : LinearOrder α] [inst_1 : LinearOrder β]
  [inst_2 : LinearOrder γ], Order.IsNormal g → Order.IsNormal f → Order.IsNormal (g ∘ f)
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.sigmaImp.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : (n : ℕ) × L.BoundedFormula α n → (n : ℕ) × L.BoundedFormula α n → Sort u_4) (m : ℕ)
  (φ : L.BoundedFormula α m) (n : ℕ) (ψ : L.BoundedFormula α n)
  (h_1 : (m : ℕ) → (φ : L.BoundedFormula α m) → (n : ℕ) → (ψ : L.BoundedFormula α n) → motive ⟨m, φ⟩ ⟨n, ψ⟩),
  (match ⟨m, φ⟩, ⟨n, ψ⟩ with
    | ⟨m, φ⟩, ⟨n, ψ⟩ => h_1 m φ n ψ) =
    h_1 m φ n ψ
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- A special case for when `b₁` has grade 0.  -/
GradedTensorProduct.tmul_zero_coe_mul_coe_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {i₂ : ι} (a₁ : A) (b₁ : ↥(ℬ 0)) (a₂ : ↥(𝒜 i₂)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_map_left_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.left = φ.τ₁
-- Init.Data.BitVec.Lemmas
BitVec.zero_umod : ∀ {w : ℕ} {x : BitVec w}, 0#w % x = 0#w
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_3.eq_3 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  [inst_1 : Std.Iterator α₂ m β₂] (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.right.Step → Sort u_3)
  (hp : it.internalState.right.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₂' : Std.IterM m β₂) →
      (out₂ : β₂) →
        (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂)) →
          motive ⟨Std.IterStep.yield it₂' out₂, hp⟩)
  (h_2 :
    (it₂' : Std.IterM m β₂) →
      (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', hp⟩)
  (h_3 : (hp : it.internalState.right.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.done, hp⟩ with
    | ⟨Std.IterStep.yield it₂' out₂, hp⟩ => h_1 it₂' out₂ hp
    | ⟨Std.IterStep.skip it₂', hp⟩ => h_2 it₂' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_3 hp
-- Mathlib.CategoryTheory.Action.Basic
Action.forget_obj : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G] (M : Action V G),
  (Action.forget V G).obj M = M.V
-- Mathlib.CategoryTheory.Action.Basic
/-- Construct an isomorphism of `G` actions/representations
from an isomorphism of the underlying objects,
where the forward direction commutes with the group action.  -/
Action.mkIso : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {M N : Action V G} →
          (f : M.V ≅ N.V) →
            autoParam
                (∀ (g : G),
                  CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g))
                Action.mkIso._auto_1 →
              (M ≅ N)
-- Mathlib.Algebra.Group.ULift
ULift.one : {α : Type u} → [One α] → One (ULift.{u_1, u} α)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- An upper bound on a sum of restrictions of a measure `μ`. This can be used to compare
`∫ x ∈ X, f x ∂μ` with `∑ i, ∫ x ∈ (s i), f x ∂μ`, where `s` is a cover of `X`.  -/
MeasureTheory.Measure.sum_restrict_le : ∀ {α : Type u_2} {ι : Type u_6} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {M : ℕ},
  (∀ (i : ι), MeasurableSet (s i)) →
    (∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M) →
      (MeasureTheory.Measure.sum fun i => μ.restrict (s i)) ≤ M • μ.restrict (⋃ i, s i)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Iic_sdiff_Ioc_self_of_le`. -/
Set.Iic_diff_Ioc_self_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic b \ Set.Ioc a b = Set.Iic a
-- Lean.CoreM
/-- Return `true` if the exception was generated by one of our resource limits.  -/
Lean.Exception.isRuntime : Lean.Exception → Bool
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).A = c.pt
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_eq_false_of_lt : ∀ {s : String.Slice} {p q : s.Pos}, p < q → s.isEmpty = false
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], a ∉ t → t.get! a = default
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.commRingEquiv.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N],
  AddMonoidAlgebra.commRingEquiv =
    AddMonoidAlgebra.curryRingEquiv.symm.trans
      ((AddMonoidAlgebra.mapDomainRingEquiv R AddEquiv.prodComm).trans AddMonoidAlgebra.curryRingEquiv)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE?_eq_getEntryGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getKeyGE? k t = Option.map (fun x => x.fst) (Std.DTreeMap.Internal.Impl.getEntryGE? k t)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instNeg.eq_1 : ∀ {α : Type u_1} [inst : Neg α], OrderDual.instNeg = inst
-- Init.Grind.Tactics
/-- `grind?` takes the same arguments as `grind`, but reports an equivalent call to `grind only`
that would be sufficient to close the goal. This is useful for reducing the size of the `grind`
theorems in a local invocation.
 -/
Lean.Parser.Tactic.grindTrace : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_symm : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a₁ a₂ : α},
  a₁ ∈ MulAction.orbit G a₂ ↔ a₂ ∈ MulAction.orbit G a₁
-- Batteries.Data.MLList.Basic
/-- Folds a binary function across a monadic lazy list, from an initial starting value.
This will run forever if the list is infinite.  -/
MLList.foldM : {m : Type u_1 → Type u_1} → {β α : Type u_1} → [Monad m] → (β → α → m β) → β → MLList m α → m β
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.IsAdjointPair.eq_1 : ∀ {R : Type u_1} {n : Type u_11} {n' : Type u_13} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : Fintype n']
  (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R),
  J.IsAdjointPair J' A A' = (A.transpose * J' = J * A')
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y_1).left.left =
    Y_1.left.left
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.equivAdjoin.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), minpoly.equivAdjoin hx = AlgEquiv.ofBijective (AdjoinRoot.Minpoly.toAdjoin R x) ⋯
-- Mathlib.CategoryTheory.Comma.Basic
/-- Construct an isomorphism in the comma category given isomorphisms of the objects whose forward
directions give a commutative square.
 -/
CategoryTheory.Comma.isoMk : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L₁ : CategoryTheory.Functor A T} →
              {R₁ : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma L₁ R₁} →
                  (l : X.left ≅ Y.left) →
                    (r : X.right ≅ Y.right) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom =
                            CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom))
                          CategoryTheory.Comma.isoMk._auto_1 →
                        (X ≅ Y)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- Abbreviation for degeneracy maps in the `n`-truncated simplex category.  -/
SimplexCategory.Truncated.σ : (m : ℕ) →
  {n : ℕ} →
    Fin (n + 1) →
      (hn : autoParam ({ len := n + 1 }.len ≤ m) SimplexCategory.Truncated.σ._auto_1) →
        (hn' : autoParam ({ len := n }.len ≤ m) SimplexCategory.Truncated.σ._auto_3) →
          { obj := { len := n + 1 }, property := hn } ⟶ { obj := { len := n }, property := hn' }
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.id_hom : ∀ (X : SFinKer), (CategoryTheory.CategoryStruct.id X).hom = ProbabilityTheory.Kernel.id
-- Std.Http.Data.Headers.Basic
Std.Http.Header.ContentLength.inst : Std.Http.Header Std.Http.Header.ContentLength
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toNeg : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → Neg α
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_comp : ∀ {Γ : Type u_5} {Γ' : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_7} [inst_2 : CommRing R]
  {U : Type u_8} {V : Type u_9} {W : Type u_10} [inst_3 : AddCommGroup U] [inst_4 : Module R U]
  [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W]
  (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (g : Lex (Γ' × Γ)),
  HVertexOperator.coeff (A.comp B) g = HVertexOperator.coeff A (ofLex g).2 ∘ₗ HVertexOperator.coeff B (ofLex g).1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ t.insertManyIfNewUnit l} (contains : k ∈ t), (t.insertManyIfNewUnit l).getKey k h' = t.getKey k contains
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The open sets of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around all of their points.  -/
WithSeminorms.isOpen_iff_mem_balls : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → ∀ (U : Set E), IsOpen U ↔ ∀ x ∈ U, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] (f : (i : ι) → κ i → α),
  LowerSet.Iic (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, LowerSet.Iic (f i j)