mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_add_four : ∀ {a : ByteArray} {i : ℕ} (ha : i + 4 ≤ a.size), a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.inter_univ : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), s ∩ Finset.univ = s
-- Mathlib.Topology.MetricSpace.Bounded
/-- In a pseudometric space with a conditionally complete linear order such that the order and the
metric structure give the same topology, any order-bounded set is metric-bounded.  -/
Metric.isBounded_of_bddAbove_of_bddBelow : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] {s : Set α},
  BddAbove s → BddBelow s → Bornology.IsBounded s
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {I : Type v}
  {ℐ : CategoryTheory.SmallCategory I} {hI : CategoryTheory.IsFiltered I} {F : CategoryTheory.Functor I C}
  {ι : F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A}
  {isColimit : CategoryTheory.Limits.IsColimit { pt := A, ι := ι }} {I_1 : Type v}
  {ℐ_1 : CategoryTheory.SmallCategory I_1} {hI_1 : CategoryTheory.IsFiltered I_1} {F_1 : CategoryTheory.Functor I_1 C}
  {ι_1 : F_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj A}
  {isColimit_1 : CategoryTheory.Limits.IsColimit { pt := A, ι := ι_1 }},
  { I := I, ℐ := ℐ, hI := hI, F := F, ι := ι, isColimit := isColimit } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F := F_1, ι := ι_1, isColimit := isColimit_1 } →
    I = I_1 ∧ ℐ ≍ ℐ_1 ∧ F ≍ F_1 ∧ ι ≍ ι_1 ∧ isColimit ≍ isColimit_1
-- Lean.Expr
Lean.MVarIdSet.ofList : List Lean.MVarId → Lean.MVarIdSet
-- Mathlib.Order.Category.FinBoolAlg
fintypeToFinBoolAlgOp_map : ∀ {X Y : FintypeCat} (f : X ⟶ Y),
  fintypeToFinBoolAlgOp.map f =
    (CategoryTheory.InducedCategory.homMk
        (BoolAlg.ofHom
          (have __src :=
            { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
              map_inf' := ⋯ };
          { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
            map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))).op
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.filter_equiv_self_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF → ((Std.TreeMap.Raw.filter f t).Equiv t ↔ ∀ (a : α) (h : a ∈ t), f (t.getKey a h) t[a] = true)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ) (x : R),
  (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) =
    (2 * ↑k + 1) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) -
      (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
-- Std.Internal.UV.UDP
/-- Gets the local address of a bound UDP socket.
 -/
Std.Internal.UV.UDP.Socket.getSockName : Std.Internal.UV.UDP.Socket → IO Std.Net.SocketAddress
-- Mathlib.Order.Filter.Pointwise
Filter.neBot_inv_iff : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α}, f⁻¹.NeBot ↔ f.NeBot
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
/-- The map associating to finitely many probability measures their product is a continuous map.  -/
MeasureTheory.ProbabilityMeasure.continuous_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [inst_2 : (i : ι) → TopologicalSpace (α i)] [inst_3 : ∀ (i : ι), SecondCountableTopology (α i)]
  [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (α i)] [inst_5 : ∀ (i : ι), OpensMeasurableSpace (α i)],
  Continuous fun μ => MeasureTheory.ProbabilityMeasure.pi μ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.fun.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl decl_1 : Lean.Compiler.LCNF.FunDecl pu),
  decl = decl_1 →
    ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
      k = k_1 →
        ∀ (h : pu = Lean.Compiler.LCNF.Purity.pure),
          Lean.Compiler.LCNF.Code.fun decl k h = Lean.Compiler.LCNF.Code.fun decl_1 k_1 h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyD k fallback = t₂.getKeyD k fallback
-- Batteries.Data.String.Lemmas
/-- The constructor for `ValidFor`.  -/
Substring.Raw.ValidFor.mk : ∀ {l m r : List Char},
  Substring.Raw.ValidFor l m r
    { str := String.ofList (l ++ m ++ r), startPos := { byteIdx := String.utf8Len l },
      stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } }
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.match_1.congr_eq_3 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) (x : ByteArray.utf8DecodeChar?.FirstByte)
  (h_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore)
  (heq_1 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore),
  (match h : x with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) ≍
    h_3 heq_1
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapₗ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (f : C(X, Y)) (g : LocallyConstant Y Z)
  (a : X), ((LocallyConstant.comapₗ R f) g) a = g (f a)
-- Mathlib.Order.UpperLower.Closure
/-- The biggest upper subset of an upper set `s` disjoint from a set `t`.  -/
UpperSet.sdiff : {α : Type u_1} → [inst : Preorder α] → UpperSet α → Set α → UpperSet α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- **Conditional Jensen's inequality**: in a Banach space `E` with a measure `μ` that is σ-finite
on a sub-σ-algebra `m`, if `φ : E → ℝ` is convex and lower-semicontinuous, then for any `f : α → E`
such that `f` and `φ ∘ f` are integrable, we have `φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m]`.  -/
ConvexOn.map_condExp_le_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConvexOn ℝ Set.univ φ →
    LowerSemicontinuous φ →
      MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.map_pair : ∀ {α : Type u} {β : Type v} {f : α → β} {a : α} {s : Stream'.Seq α},
  Stream'.Seq1.map f (a, s) = (f a, Stream'.Seq.map f s)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.of_mul_unit : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x y : B} {r : R},
  (algebraMap R B) r * y = 1 → IsIntegral R (x * y) → IsIntegral R x
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'_d_eq_fromOpcycles : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : e.BoundaryGE i),
  (K.truncGE' e).d i j =
    CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e hi' hi).hom
      (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i' j') (K.truncGE'XIso e hj' ⋯).inv)
-- Mathlib.Combinatorics.Additive.SmallTripling
/-- If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|A^±1 * ... * A^±1|` is at most `|A|` times a constant exponential in the number of
terms in the product.

When `A` is symmetric (`A⁻¹ = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_pow_of_small_tripling`.  -/
Finset.small_alternating_pow_of_small_tripling : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m →
    ↑(A ^ 3).card ≤ K * ↑A.card →
      ∀ (ε : Fin m → ℤ),
        (∀ (i : Fin m), |ε i| = 1) →
          ↑(List.map (fun i => A ^ ε i) (List.finRange m)).prod.card ≤ K ^ (3 * (m - 2)) * ↑A.card
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (self : D₁.Hom D₂) (i₁ i₂ : ι),
  CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (self.hom i₁)) (D₂.hom i₁ i₂) =
    CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (self.hom i₂))
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The underlying presheaf of a sheaf.  -/
CategoryTheory.Sheaf.val : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] → CategoryTheory.Sheaf J A → CategoryTheory.Functor Cᵒᵖ A
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.union_insert_right_equiv_union_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {p : α × β}, m₁.WF → m₂.WF → (m₁ ∪ m₂.insert p.1 p.2).Equiv ((m₁ ∪ m₂).insert p.1 p.2)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_sdiff₀`. -/
MeasureTheory.setIntegral_diff₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    MeasureTheory.IntegrableOn f s μ →
      t ⊆ s → ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
-- Mathlib.Geometry.Convex.Hull
_private.Mathlib.Geometry.Convex.Hull.0.Convexity.convexHull.eq_1 : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X],
  Convexity.convexHull R = ClosureOperator.ofCompletePred (Convexity.IsConvexSet R) ⋯
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `limsup (c - xᵢ) = c - liminf xᵢ`.  -/
limsup_const_sub : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [inst_3 : AddCommSemigroup R] [inst_4 : Sub R] [ContinuousSub R] [OrderedSub R]
  [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f → Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instHasZeroMorphisms : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.AddMon D)
-- Mathlib.RingTheory.RingHom.Flat
/-- Bijective ring maps are flat.  -/
RingHom.Flat.of_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Function.Bijective ⇑f → f.Flat
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.ext' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e e' : Bundle.Pretrivialization F proj), e.toPartialEquiv = e'.toPartialEquiv → e.baseSet = e'.baseSet → e = e'
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.instCategoryHom : {C : Type u_1} →
  [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    {X Y : CategoryTheory.CatEnriched C} → CategoryTheory.Category.{u_3, u_2} (X ⟶ Y)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, - y + x)` sends `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_neg_add_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, -z.2 + z.1)) (μ.prod ν) (ν.prod μ)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.isAddHaarMeasure_volume_pi : ∀ (ι : Type u_1) [inst : Fintype ι], MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
AntitoneOn.integrableOn_isCompact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact s → AntitoneOn f s → MeasureTheory.IntegrableOn f s μ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The canonical morphism from the biproduct over a restricted index type to the biproduct of
the full index type.  -/
CategoryTheory.Limits.biproduct.fromSubtype : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            (p : J → Prop) →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] → ⨁ Subtype.restrict p f ⟶ ⨁ f
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} [Subsingleton ↥X] (f : CategoryTheory.Retract X Y),
  AlgebraicGeometry.IsClosedImmersion f.i
-- Mathlib.Algebra.Module.Equiv.Basic
/-- `g : R ≃+* S` is `R`-linear when the module structure on `S` is `Module.compHom S g` .  -/
Module.compHom.toLinearEquiv : {R : Type u_9} → {S : Type u_10} → [inst : Semiring R] → [inst_1 : Semiring S] → (g : R ≃+* S) → R ≃ₗ[R] S
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteMulSupport.inv` -/
Function.HasFiniteMulSupport.fun_inv : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport fun i => (f i)⁻¹
-- Mathlib.Topology.Order.OrderClosed
frontier_lt_subset_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β], Continuous f → Continuous g → frontier {b | f b < g b} ⊆ {b | f b = g b}
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Data.TwoPointing
TwoPointing.sum_fst : ∀ {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β), (p.sum q).toProd.1 = Sum.inl p.toProd.1
-- Mathlib.GroupTheory.OrderOfElement
/-- This is the same as `orderOf_pow'` and `orderOf_pow''` but with one assumption less which is
automatic in the case of a finite cancellative monoid.  -/
orderOf_pow : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [Finite G] {n : ℕ} (x : G), orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
-- Mathlib.Order.Basic
/-- **Alias** of `gt_trans`. -/
lt_trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b < a → c < b → c < a
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.monotone_face : ∀ {n : ℕ} (i : Fin (n + 1)), Monotone fun I => I.face i
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toOrderMonoidHom_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β}
  {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f f_1 : X ≃ Y) (e_f : f = f_1)
  (K₁ K₁_1 : NNReal) (e_K₁ : K₁ = K₁_1) (K₂ K₂_1 : NNReal) (e_K₂ : K₂ = K₂_1) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂)
  (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D D_1 : Delone.DeloneSet X),
  D = D_1 →
    Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D =
      Delone.DeloneSet.mapBilipschitz f_1 K₁_1 K₂_1 ⋯ ⋯ ⋯ ⋯ D_1
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R], Polynomial.content 0 = 0
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
/-- If `f : X ⟶ S` is geometrically irreducible and open,
then `f` induces an equivalence between the irreducible components of `X` and `S`.  -/
AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv : {X S : AlgebraicGeometry.Scheme} →
  (f : X ⟶ S) →
    [AlgebraicGeometry.GeometricallyIrreducible f] →
      IsOpenMap ⇑f → ↑(irreducibleComponents ↥X) ≃ ↑(irreducibleComponents ↥S)
-- Init.Data.SInt.Basic
/-- Constructs an `Int8` from an `Int`, clamping if the value is too small or too large.  -/
Int8.ofIntTruncate : ℤ → Int8
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- `modularCyclotomicCharacter_aux g n` is a non-canonical auxiliary integer `j`,
only well-defined modulo the number of `n`-th roots of unity in `L`, such that `g(ζ)=ζ^j`
for all `n`-th roots of unity `ζ` in `L`.  -/
modularCyclotomicCharacter.aux : {L : Type u} → [inst : CommRing L] → [IsDomain L] → L ≃+* L → (n : ℕ) → [NeZero n] → ℤ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RccSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Orbit-stabilizer theorem.  -/
AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (b : X) [inst_2 : Fintype G]
  [inst_3 : Fintype ↑(AddAction.orbit G b)] [inst_4 : Fintype ↥(AddAction.stabilizer G b)],
  Fintype.card ↑(AddAction.orbit G b) * Fintype.card ↥(AddAction.stabilizer G b) = Fintype.card G
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.of_isTriangulatedClosed₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [P.IsTriangulatedClosed₃] [P.IsStableUnderShift ℤ], P.IsTriangulatedClosed₂
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω), ProbabilityTheory.variance 0 μ = 0
-- Init.Data.SInt.Lemmas
ISize.toNat_toBitVec_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 32 → (ISize.ofNat n).toBitVec.toNat = n
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              CategoryTheory.Category.{max t v', max (max (max (max u u') v) v') t} (F.DescentData f)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.apply_sup_le_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : AddCommMonoid β] [inst_3 : Preorder β] [AddLeftMono β] {f : α → β},
  f ⊥ = 0 → (∀ {s t : α}, f (s ⊔ t) ≤ f s + f t) → ∀ {s : ι → α} (t : Finset ι), f (t.sup s) ≤ ∑ i ∈ t, f (s i)
-- Std.Sync.Notify
Std.Notify.mk.inj : ∀ {state state_1 : Std.Mutex Std.Notify.State}, { state := state } = { state := state_1 } → state = state_1
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Turn a non-unital subring containing `1` into a subring.  -/
NonUnitalSubring.toSubring : {R : Type u} → [inst : NonAssocRing R] → (S : NonUnitalSubring R) → 1 ∈ S → Subring R
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- Any cyclic `f : Perm α` is isomorphic to the nontrivial `Cycle α`
that corresponds to repeated application of `f`.
The forward direction is implemented by finding this `Cycle α` using `Fintype.choose`.
 -/
Equiv.Perm.isoCycle' : {α : Type u_1} → [Fintype α] → [DecidableEq α] → { f // f.IsCycle } ≃ { s // s.Nodup ∧ s.Nontrivial }
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- **Alias** of `SheafOfModules.map_ιFree_mapFreeIso_inv`. -/
SheafOfModules.map_ιFree_mapFree_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I),
  CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) (SheafOfModules.mapFreeIso F I η).inv =
    CategoryTheory.CategoryStruct.comp η.inv (SheafOfModules.ιFree i)
-- Mathlib.Analysis.RCLike.Basic
RCLike.map_from_real : ∀ {K : Type u_1} [inst : RCLike K], RCLike.map ℝ K = RCLike.ofRealCLM
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlong_apply : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁)
  (φ : (j : ι₂) → R₁ (f j) → R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j))
  (x : RestrictedProduct (fun i => R₁ i) (fun i => A₁ i) 𝓕₁) (j : ι₂),
  (RestrictedProduct.mapAlong R₁ R₂ f hf φ hφ x) j = φ j (x (f j))