mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.OpClass
/-- A symmetric operation satisfies `op a b = op b a`.  -/
IsSymmOp.symm_op : ∀ {α : Sort u} {β : Sort v} {op : α → α → β} [self : IsSymmOp op] (a b : α), op a b = op b a
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The simplex witnessing that `hom` and `inv` compose to the identity  -/
SSet.Edge.InvStruct.homInvId : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    {hom : SSet.Edge x₀ x₁} → (self : hom.InvStruct) → hom.CompStruct self.inv (SSet.Edge.id x₀)
-- Mathlib.CategoryTheory.Sums.Products
/-- The equivalence `Sum.functorEquiv` sends associativity of sums to associativity of products  -/
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (T : Type u_3) →
              [inst_3 : CategoryTheory.Category.{v_3, u_3} T] →
                ((CategoryTheory.sum.associativity A A' T).congrLeft.trans
                      ((CategoryTheory.Sum.functorEquiv A (A' ⊕ T) B).trans
                        (CategoryTheory.Equivalence.refl.prod (CategoryTheory.Sum.functorEquiv A' T B)))).functor ≅
                  (((CategoryTheory.Sum.functorEquiv (A ⊕ A') T B).trans
                          ((CategoryTheory.Sum.functorEquiv A A' B).prod CategoryTheory.Equivalence.refl)).trans
                      (CategoryTheory.prod.associativity (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)
                        (CategoryTheory.Functor T B))).functor
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn_2.go : {α : Type u} →
  {motive_1 : Lean.PersistentArrayNode α → Sort u_1} →
    {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} →
      {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1} →
        (t : List (Lean.PersistentArrayNode α)) →
          ((t : Lean.PersistentArrayNode α) → t.below → motive_1 t) →
            ((t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t) →
              ((t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t) →
                motive_3 t ×' Lean.PersistentArrayNode.below_2 t
-- Mathlib.Order.Hom.Basic
/-- A surjective order embedding is an order isomorphism.  -/
OrderIso.ofSurjective : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → (f : α ↪o β) → Function.Surjective ⇑f → α ≃o β
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.index_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D)
  (I : S.shape.R), (S.index P).snd I = P.map I.r.g₂.op
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.isLink_of_mem_mem : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β},
  H.IsInducedSubgraph G → ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- The coequalizer morphism `coequalizerπ` gives a split coequalizer on `f,g`.  -/
CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.HasSplitCoequalizer f g] →
          CategoryTheory.IsSplitCoequalizer f g (CategoryTheory.HasSplitCoequalizer.coequalizerπ f g)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.continuous_mul : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [inst_5 : NormedRing R]
  [SecondCountableTopologyEither X R] {f g : X → R},
  Continuous g → MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable (fun x => g x * f x) μ
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
_private.Mathlib.CategoryTheory.Functor.KanExtension.Pointwise.0.CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso_left : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} (F : CategoryTheory.Functor C H) {L' : CategoryTheory.Functor C D} (e : L ≅ L')
  (Y : D), L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The zero module has the module topology.  -/
IsModuleTopology.instSubsingleton : ∀ {R : Type u_1} [inst : TopologicalSpace R] {A : Type u_2} [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A] [Subsingleton A], IsModuleTopology R A
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- For a functor `F : J ⥤ C`, if `J` has an initial object then the image of it is isomorphic
to the limit of `F`.  -/
CategoryTheory.Limits.limitOfInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasInitial J] → CategoryTheory.Limits.limit F ≅ F.obj (⊥_ J)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalCommRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonUnitalCommRing α] → NonUnitalCommRing (WithConv (Matrix m n α))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.length_toList : ∀ {α : Type u_1} {t : Ordnode α}, t.Sized → t.toList.length = t.size
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_zero_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ m₂ _mΩ : MeasurableSpace Ω},
  ProbabilityTheory.Kernel.Indep m₁ m₂ 0 μ
-- Mathlib.SetTheory.ZFC.PSet
PSet.Mem.ext : ∀ {x y : PSet.{u}}, (∀ (w : PSet.{u}), w ∈ x ↔ w ∈ y) → x.Equiv y
-- Init.Data.SInt.Basic
ISize.toBitVec.inj : ∀ {x y : ISize}, x.toBitVec = y.toBitVec → x = y
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.lintegral_toKernel_univ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α),
  ∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univ ∂ν a = (κ a) Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instCompleteLattice : {V : Type u} → {G : SimpleGraph V} → CompleteLattice G.Subgraph
-- Init.Data.List.Find
List.IsInfix.find?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <:+: l₂ → List.find? p l₂ = none → List.find? p l₁ = none
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM1.init.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Λ] [inst_1 : Inhabited Γ] [inst_2 : Inhabited σ]
  (l : List Γ), Turing.TM1.init l = { l := some default, var := default, Tape := Turing.Tape.mk₁ l }
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonneg_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → x ≤ 1 → 0 ≤ Real.logb b x
-- Mathlib.Analysis.Distribution.Support
Distribution.isClosed_dsupport : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V}, IsClosed (Distribution.dsupport f)
-- Mathlib.Topology.Order.Hom.Esakia
OrderHom.copy.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f f_1 : α →o β) (e_f : f = f_1)
  (f' f'_1 : α → β) (e_f' : f' = f'_1) (h : f' = ⇑f), f.copy f' h = f_1.copy f'_1 ⋯
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instContinuousMapClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousMapClass (A →ₜ* B) A B
-- Mathlib.Order.Category.BoolAlg
BoolAlg.inv_hom_apply : ∀ {X Y : BoolAlg} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.Data.SInt.Lemmas
ISize.zero_sub : ∀ (a : ISize), 0 - a = -a
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function is strongly measurable with respect to the σ-algebra generated by the
first coordinates, then it only depends on those first coordinates.  -/
MeasureTheory.StronglyMeasurable.dependsOn_of_piLE : ∀ {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z}
  [inst_1 : Preorder ι] {i : ι} [inst_2 : TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z],
  MeasureTheory.StronglyMeasurable f → DependsOn f (Set.Iic i)
-- Init.Data.List.Nat.InsertIdx
List.getElem?_insertIdx_of_lt : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ}, j < i → (l.insertIdx i x)[j]? = l[j]?
-- Mathlib.Data.Set.Finite.Lattice
Set.Infinite.iUnion : ∀ {α : Type u} {ι : Sort u_1} {s : ι → Set α} (i : ι), (s i).Infinite → (⋃ i, s i).Infinite
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
conformalFactorAt_inner_eq_mul_inner : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F},
  HasFDerivAt f f' x → ∀ (H : ConformalAt f x) (u v : E), inner ℝ (f' u) (f' v) = conformalFactorAt H * inner ℝ u v
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_sub : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Sub M] (f g : α → M), ↑(f - g) = ↑f - ↑g
-- Mathlib.Data.Finset.Card
/-- A finset has cardinality at most 1 iff its underlying set is subsingleton.  -/
Finset.card_le_one_iff_subsingleton : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ (↑s).Subsingleton
-- Mathlib.Algebra.WithConv
WithConv.ofConv_surjective : ∀ {A : Type u_2}, Function.Surjective WithConv.ofConv
-- Std.Sync.Channel
Std.instNonemptyChannel : ∀ {α : Type}, Nonempty (Std.Channel α)
-- Mathlib.Combinatorics.Tiling.Tile
/-- A `Protoset G X ιₚ` is an indexed family of `Prototile G X`. This is a separate definition
rather than just using plain functions to facilitate defining associated API that can be used with
dot notation.  -/
DiscreteTiling.Protoset : (G : Type u_1) → (X : Type u_2) → Type u_3 → [inst : Group G] → [MulAction G X] → Type (max (max u_1 u_2) u_3)
-- Mathlib.Topology.IsClosedRestrict
/-- Given a set in a product space `s : Set (Π j, α j)` and a set of coordinates `S : Set ι`,
`Sᶜ.domRestrict '' s × (Π i : S, α i)` is the set of functions that coincide with an element of `s`
on `Sᶜ` and are arbitrary on `S`.
`reorderRestrictProd` sends a term of that type to `Π j, α j` by looking for the value at `j`
in one part of the product or the other depending on whether `j` is in `S` or not.  -/
Topology.reorderRestrictProd : {ι : Type u_1} →
  {α : ι → Type u_2} →
    (S : Set ι) → (s : Set ((j : ι) → α j)) → ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i) → (j : ι) → α j
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a finite-product-preserving presheaf on `Stonean`.  -/
Condensed.ofSheafStonean : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] →
      (F : CategoryTheory.Functor Stoneanᵒᵖ A) → [CategoryTheory.Limits.PreservesFiniteProducts F] → Condensed A
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- For any candidate `f`, `HD(f)` is larger than or equal to the Hausdorff distance in the
optimal coupling. This follows from the fact that `HD` of the optimal candidate is exactly
the Hausdorff distance in the optimal coupling, although we only prove here the inequality
we need.  -/
GromovHausdorff.hausdorffDist_optimal_le_HD : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {f : GromovHausdorff.Cb✝ X Y},
  f ∈ GromovHausdorff.candidatesB✝ X Y →
    Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y))
        (Set.range (GromovHausdorff.optimalGHInjr X Y)) ≤
      GromovHausdorff.HD f
-- Mathlib.Order.CompleteLattice.Basic
sSup_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] {s : Set β} {f : β → α}, sSup (f '' s) = ⨆ a, f ↑a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The right unitor isomorphism for Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                (F : CategoryTheory.Functor C V) →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] →
                      CategoryTheory.MonoidalCategory.DayConvolution.convolution F U ≅ F
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)} {p : α × β},
  ContinuousWithinAt Prod.snd s p
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_div_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  s / interior t ⊆ interior (s / t)
-- Mathlib.Data.Set.Image
Set.imageFactorization_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Surjective (Set.imageFactorization f s)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is uniformly equicontinuous on a set `S`, its closure for the product
topology is also uniformly equicontinuous. This would also be true for the coarser topology of
pointwise convergence on `S`, see `UniformEquicontinuousOn.closure'`.  -/
Set.UniformEquicontinuousOn.closure : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {A : Set (β → α)} {S : Set β},
  A.UniformEquicontinuousOn S → (closure A).UniformEquicontinuousOn S
-- Mathlib.Analysis.RCLike.ContinuousMap
/-- Lifting `C(X, ℝ)` to `C(X, 𝕜)` using `RCLike.ofReal`.  -/
ContinuousMap.realToRCLike : {X : Type u_1} → (𝕜 : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : RCLike 𝕜] → C(X, ℝ) → C(X, 𝕜)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_hom_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom fst' = fst
-- Mathlib.Topology.Sheaves.Skyscraper
/-- Taking skyscraper sheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
`p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
 -/
skyscraperSheafFunctor : {X : TopCat} →
  (p₀ : ↑X) →
    [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst : CategoryTheory.Category.{u, v} C] →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Functor C (TopCat.Sheaf C X)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_comap_le : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {S : L.Substructure N} {f : L.Hom M N},
  FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) ≤ S
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadIso.toNatIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Monad C} (h : M ≅ N),
  (CategoryTheory.MonadIso.toNatIso h).hom = (CategoryTheory.monadToFunctor C).map h.hom
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- If `m : M → N` is a subadditive function (`m (a + b) ≤ m a + m b`) and `s` is a nonempty set,
then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`.  -/
Finset.le_expect_nonempty_of_subadditive : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {f : ι → M} {s : Finset ι} (m : M → N),
  (∀ (a b : M), m (a + b) ≤ m a + m b) →
    (∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) →
      s.Nonempty → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)
-- Init.Data.Order.Ord
List.instTransOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.TransOrd α], Std.TransOrd (List α)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIcoDiv` is continuous on the right at every point.

In fact, a stronger statement is true:
it's eventually constant on the right, see `eventuallyEq_toIcoDiv_nhdsGE`.  -/
continuousWithinAt_toIcoDiv_Ici : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIcoDiv hp a) (Set.Ici x) x
-- Init.Data.Nat.Lemmas
Nat.mul_add_mul_div_of_dvd : ∀ {b d a c : ℕ}, b ≠ 0 → d ≠ 0 → b ∣ a → d ∣ c → (a * d + b * c) / (b * d) = a / b + c / d
-- Mathlib.Order.Filter.Defs
Filter.instPartialOrder : {α : Type u_1} → PartialOrder (Filter α)
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.ne_empty : ∀ {α : Type u} {s : Set α}, s.Nontrivial → s ≠ ∅
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
spectrum.hasDerivAt_resolvent_const_left : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {k : 𝕜}, k ∈ resolventSet 𝕜 a → HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
-- Mathlib.Algebra.GroupWithZero.Action.Units
eq_inv_smul_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ {x y : β}, x = a⁻¹ • y ↔ a • x = y
-- Init.Data.FloatArray.Basic
FloatArray.mk.sizeOf_spec : ∀ (data : Array Float), sizeOf { data := data } = 1 + sizeOf data
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  F.ReflectsMonomorphisms
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ),
  0 ≤ r → (r • j).posPart = r.toNNReal • j.posPart
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_memPartition_le_range : ∀ {α : Type u_1} (t : ℕ → Set α) (n : ℕ),
  MeasurableSpace.generateFrom (memPartition t n) ≤ MeasurableSpace.generateFrom (Set.range t)
-- Init.Data.SInt.Lemmas
instCommutativeISizeHAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.algebraMap_coroot'In_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S M] [inst_8 : IsScalarTower S R M]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] (i : ι) (x : ↥(P.rootSpan S)),
  (algebraMap S R) ((P.coroot'In S i) x) = (P.coroot' i) ↑x
-- Mathlib.Data.Nat.Factorization.PrimePow
IsPrimePow.minFac_pow_factorization_eq : ∀ {n : ℕ}, IsPrimePow n → n.minFac ^ n.factorization n.minFac = n
-- Mathlib.RingTheory.Congruence.Basic
RingCon.subsingleton_quotient : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c : RingCon R}, Subsingleton c.Quotient ↔ c = ⊤
-- Init.System.IO
/-- The file can be written to.  -/
IO.AccessRight.write : IO.AccessRight → Bool
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights_singleton_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)}, i ≠ j → s.touchpointWeights {i} j i < 0
-- Mathlib.Data.Set.Equitable
Set.EquitableOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LE β] [inst_1 : Add β] [inst_2 : One β] (s : Set α) (f : α → β),
  s.EquitableOn f = ∀ ⦃a₁ a₂ : α⦄, a₁ ∈ s → a₂ ∈ s → f a₁ ≤ f a₂ + 1
-- Mathlib.Order.Circular
/-- For any triple of points, the second is between the other two one way or another.  -/
CircularOrder.btw_total : ∀ {α : Type u_1} [self : CircularOrder α] (a b c : α), btw a b c ∨ btw c b a
-- Init.Data.Option.Basic
Option.get_some : ∀ {α : Type u_1} (x : α) (h : (some x).isSome = true), (some x).get h = x
-- Lean.Parser.Term
Lean.Parser.Tactic.quotSeq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.fintypeBot : {G : Type u_1} → [inst : AddGroup G] → Fintype ↥⊥
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_smul_eq_mulAut_conj : ∀ {G : Type u_3} [inst : Group G] (g h : G), ConjAct.toConjAct g • h = (MulAut.conj g) h
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalars₁₂_injective : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {N : Type u_7} {Pₗ : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ] [inst_5 : Module R M]
  [inst_6 : Module S N] [inst_7 : Module R Pₗ] [inst_8 : Module S Pₗ] [inst_9 : SMulCommClass S R Pₗ] (R' : Type u_14)
  (S' : Type u_15) [inst_10 : Semiring R'] [inst_11 : Semiring S'] [inst_12 : Module R' M] [inst_13 : Module S' N]
  [inst_14 : Module R' Pₗ] [inst_15 : Module S' Pₗ] [inst_16 : SMulCommClass S' R' Pₗ] [inst_17 : SMul S' S]
  [inst_18 : IsScalarTower S' S N] [inst_19 : IsScalarTower S' S Pₗ] [inst_20 : SMul R' R]
  [inst_21 : IsScalarTower R' R M] [inst_22 : IsScalarTower R' R Pₗ],
  Function.Injective (LinearMap.restrictScalars₁₂ R' S')
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The braiding natural isomorphism.  -/
CategoryTheory.termβ_ : Lean.ParserDescr
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_simple_ne : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.length (w * cs.simple i) ≠ cs.length w