mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `inv_mul_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
 -/
inv_mul_le_of_le_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ b * c → b⁻¹ * a ≤ c
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ofMatroid : {α : Type u_2} → Matroid α → Matroid.Matroidᵣ α
-- Init.Prelude
/-- `sepBy1` is just like `sepBy`, except it takes 1 or more instead of
0 or more occurrences of `p`.  -/
Lean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.ZeroAtInfty
ZeroAtInftyContinuousMapClass.norm_le : ∀ {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : FunLike 𝓕 E F] [ZeroAtInftyContinuousMapClass 𝓕 E F] (f : 𝓕) (ε : ℝ),
  0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
-- Init.Data.BitVec.Basic
BitVec.umod_eq : ∀ {w : ℕ} (x y : BitVec w), x.umod y = x % y
-- Batteries.Tactic.PrintPrefix
/-- `takeNameSuffix n name` returns a pair `(pre, suf)` where `suf` contains the last `n` components
of the name and `pre` contains the rest.
 -/
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.takeNameSuffix : ℕ → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Lean.Name × Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abLeftHomologyData_H_coe : ∀ (S : CategoryTheory.ShortComplex Ab),
  ↑S.abLeftHomologyData.H = (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a right homology data is preserved by a functor `F`, this functor
preserves the cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F
-- Mathlib.NumberTheory.ModularForms.LFunction
CuspForm.hasSum_L : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : CuspFormClass F Γ k],
  ↑k / 2 + 1 < s.re →
    HasSum (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑n ^ s)
      (↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s)
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.decidableMemCenter : {M : Type u_1} →
  [inst : AddSemigroup M] → (a : M) → [Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubsemigroup.center M)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.toTerm : Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β], ⇑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.instHasIterationOfShapeArrow : ∀ (J : Type w) [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C], CategoryTheory.Limits.HasIterationOfShape J (CategoryTheory.Arrow C)
-- Mathlib.Dynamics.OmegaLimit
/-- The ω-limit of a set `s` under `ϕ` with respect to a filter `f` is `⋂ u ∈ f, cl (ϕ u s)`.  -/
omegaLimit.termω : Lean.ParserDescr
-- Mathlib.Algebra.CubicDiscriminant
/-- Map a cubic polynomial across a semiring homomorphism.  -/
Cubic.map : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → Cubic R → Cubic S
-- Mathlib.Data.Num.Lemmas
PosNum.cast_to_nat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : PosNum), ↑↑n = ↑n
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C}
  [inst_4 : HomotopicalAlgebra.IsCofibrant X] [inst_5 : HomotopicalAlgebra.IsCofibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.RootedConnected.nonempty_path : ∀ {V : Type u} {inst : Quiver V} {r : V} [self : Quiver.RootedConnected r] (b : V), Nonempty (Quiver.Path r b)
-- Init.Data.Int.Order
Int.ofNat_natAbs_of_nonpos : ∀ {a : ℤ}, a ≤ 0 → ↑a.natAbs = -a
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The embedding of an independent set of an induced subgraph of the subgraph `G` is an independent
set in `G` and vice versa.  -/
SimpleGraph.isIndepSet_induce : ∀ {α : Type u_1} (G : SimpleGraph α) {F : Set α} {s : Set ↑F},
  (⊤.induce F).coe.IsIndepSet s ↔ G.IsIndepSet (Subtype.val '' s)
-- Mathlib.Topology.UnitInterval
unitInterval.symm_involutive : Function.Involutive unitInterval.symm
-- Mathlib.Data.FunLike.Embedding
/-- The class `EmbeddingLike F α β` expresses that terms of type `F` have an
injective coercion to injective functions `α ↪ β`.
 -/
EmbeddingLike : (F : Sort u_1) → (α : outParam (Sort u_2)) → (β : outParam (Sort u_3)) → [FunLike F α β] → Prop
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_one_iff : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {r : ℝ}, a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.preservesColimit_span_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P X Y Z : C} {inl : X ⟶ P} {inr : Y ⟶ P} {f : Z ⟶ X} {g : Z ⟶ Y},
  CategoryTheory.IsPushout f g inl inr →
    (CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F ↔
      CategoryTheory.IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr))
-- Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Nat.factors_eq : ∀ (n : ℕ), UniqueFactorizationMonoid.normalizedFactors n = ↑n.primeFactorsList
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term_†» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₁_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (f : Fin 1 → ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.exteriorPower.iso₁ M).hom) (ModuleCat.exteriorPower.mk f) = f 0
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.incNumCalls : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The middle left map in the reverse hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with the real-valued measure of a set defined with a distance.

The `IsFiniteMeasure` hypothesis is necessary, otherwise `μ.real {...}` could be zero because
the measure of the set is infinite.  -/
MeasureTheory.tendstoInMeasure_iff_measureReal_dist : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoMetricSpace E] [MeasureTheory.IsFiniteMeasure μ] {f : ι → α → E} {l : Filter ι} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ.real {x | ε ≤ dist (f i x) (g x)}) l (nhds 0)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.isSeparated_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  J₁ ≤ J₂ → CategoryTheory.Presieve.IsSeparated J₂ P → CategoryTheory.Presieve.IsSeparated J₁ P
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.RootOrdered.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → α → Sort u_2) (x : α)
  (h_1 : (x : α) → motive RBTree.RBNode.Path.root x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (x : α) → (r : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.Path.left c parent x r) v)
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → (v : α) → motive (RBTree.RBNode.Path.right c l x parent) v),
  (match RBTree.RBNode.Path.root, x with
    | RBTree.RBNode.Path.root, x => h_1 x
    | RBTree.RBNode.Path.left c parent x r, v => h_2 c parent x r v
    | RBTree.RBNode.Path.right c l x parent, v => h_3 c l x parent v) =
    h_1 x
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.lift_comp : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [inst : HomotopicalAlgebra.Fibration p]
  (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y)
  (comm :
    ∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b),
  CategoryTheory.CategoryStruct.comp (hf.lift p b comm) p = b
-- Aesop.Rule
Aesop.LocalNormSimpRule.simpTheorem : Aesop.LocalNormSimpRule → Lean.Term
-- Mathlib.CategoryTheory.Quotient
/-- A `HomRel` is a congruence when it's an equivalence on every hom-set, and it can be composed
from left and right.  -/
CategoryTheory.Congruence : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → Prop
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_induced_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] {G : Type u_4} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 G] (g₁ g₂ : G) (f : G →ₗ[𝕜] E),
  inner 𝕜 g₁ g₂ = inner 𝕜 (f g₁) (f g₂)
-- Init.Data.UInt.BasicAux
instSubUInt32 : Sub UInt32
-- Lean.Parser.Term
Lean.Parser.Term.leading_parser : Lean.Parser.Parser
-- Mathlib.Analysis.Complex.Hadamard
/-- The interpolation of `sSupNormIm` on the two boundaries.
In other words, this is the right side of the target inequality:
`|f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|`.

Note that if `sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0` then the power is not continuous
since `0 ^ 0 = 1`. Hence the use of `ite`.  -/
Complex.HadamardThreeLines.interpStrip : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℂ → ℂ
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_ofEquivFun : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] [inst_4 : DecidableEq ι] (e : M ≃ₗ[R] ι → R),
  ⇑(Module.Basis.ofEquivFun e) = fun i => e.symm (Pi.single i 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_3 : Inhabited α] {l : List α} {k : α},
  l.contains k = false → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey! k = default
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instSDiff : {α : Type u_2} → [inst : TopologicalSpace α] → SDiff (TopologicalSpace.Clopens α)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.trans : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =O[l] g → g =O[l] k → f =O[l] k
-- Mathlib.Topology.Order.OrderClosed
ge_of_tendsto' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {f : β → α}
  {a b : α} {x : Filter β} [hx : x.NeBot], Filter.Tendsto f x (nhds a) → (∀ (c : β), b ≤ f c) → b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `(a,b)` is a kernel pair for `f₁ ≫ f₂` and `a ≫ f₁ = b ≫ f₁`, then `(a,b)` is a kernel pair for
just `f₁`.
That is, to show that `(a,b)` is a kernel pair for `f₁` it suffices to only show the square
commutes, rather than to additionally show it's a pullback.
 -/
CategoryTheory.IsKernelPair.cancel_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp a f₁ = CategoryTheory.CategoryStruct.comp b f₁ →
    CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b → CategoryTheory.IsKernelPair f₁ a b
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_succ : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {n : ℕ} {a : α},
  List.findIdxNth p (a :: xs) (n + 1) =
    if p a = true then List.findIdxNth p xs n + 1 else List.findIdxNth p xs (n + 1) + 1
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which the
descending central series reaches `⊥` in its `n`-th term.  -/
AddSubgroup.least_descending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G], Nat.find ⋯ = AddGroup.nilpotencyClass G
-- Init.Data.BitVec.Lemmas
BitVec.sle_eq_not_slt : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = !y.slt x
-- Init.Meta.Defs
/-- Split disjunctions in the context.

Note that with `splitDisjunctions := false` omega will not be able to solve `x = y` goals
as these are usually handled by introducing `¬ x = y` as a hypothesis, then replacing this with
`x < y ∨ x > y`.

On the other hand, `omega` does not currently detect disjunctions which, when split,
introduce no new useful information, so the presence of irrelevant disjunctions in the context
can significantly increase run time.
 -/
Lean.Meta.Omega.OmegaConfig.splitDisjunctions : Lean.Meta.Omega.OmegaConfig → Bool
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_rio : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_rio._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e.fst bound).isLT) t.toList
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.combine.go.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (k₁ k₂ : ℤ)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)),
  (match Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ with
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_1 k₁ k₂
-- Mathlib.Tactic.CrossRefAttribute
/-- Returns the declaration names of results carrying the cross-reference `tag`.  -/
_private.Mathlib.Tactic.CrossRefAttribute.0.Lean.Environment.getCrossRefDeclNames : Lean.Environment → String → Array Lean.Name
-- Mathlib.Analysis.Normed.Affine.Convex
/-- We can intercalate a convex polytope between a compact convex set and one of its neighborhoods.
 -/
Convex.exists_subset_interior_convexHull_finset_of_isCompact : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s t : Set E},
  Convex ℝ s → IsCompact s → t ∈ nhdsSet s → ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- **Alias** of `Ordinal.CNF.sortedGT`.

---

The exponents of the Cantor normal form are decreasing.  -/
Ordinal.CNF.sorted : ∀ (b o : Ordinal.{u_1}), (List.map Prod.fst (Ordinal.CNF b o)).SortedGT
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
      Std.Internal.List.maxKey? l = (Std.Internal.List.keys l).getLast?
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_lt_mk_iff : ∀ {α : Type u}, Cardinal.aleph0 < Cardinal.mk α ↔ Uncountable α
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₃ = φ.unop.hom₁.op
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.finrank_linearMap_self : ∀ (R : Type u) (S : Type u') (M : Type v) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S]
  [inst_8 : Module R S] [inst_9 : SMulCommClass R S S], Module.finrank S (M →ₗ[R] S) = Module.finrank R M
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalCommRingOfIsTopologicalRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : NonUnitalCommRing β] → [IsTopologicalRing β] → NonUnitalCommRing C(α, β)
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_inv`

---

The order of the inverse is the negative of the order.  -/
fun_meromorphicOrderAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, meromorphicOrderAt (fun i => (f i)⁻¹) x = -meromorphicOrderAt f x
-- Mathlib.Order.Preorder.Chain
IsChain.image : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} [inst : FunLike F α β]
  [RelHomClass F r r'], IsChain r s → ∀ (φ : F), IsChain r' (⇑φ '' s)
-- Mathlib.Algebra.Group.Basic
zpow_neg : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹
-- Mathlib.Geometry.Manifold.HasGroupoid
OpenPartialHomeomorph.singletonChartedSpace_mem_atlas_eq : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : OpenPartialHomeomorph α H)
  (h : e.source = Set.univ), ∀ e' ∈ ChartedSpace.atlas, e' = e
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Recover the monotone map from a morphism in the simplex category.  -/
SimplexCategory.Hom.toOrderHom : {a b : SimplexCategory} → a.Hom b → Fin (a.len + 1) →o Fin (b.len + 1)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.not_isSuccLimit_zero : ¬Order.IsSuccLimit 0
-- Init.GetElem
instGetElem?OfGetElemOfDecidable : {coll : Type u_1} →
  {idx : Type u_2} →
    {elem : Type u_3} →
      {valid : coll → idx → Prop} →
        [GetElem coll idx elem valid] →
          [(xs : coll) → (i : idx) → Decidable (valid xs i)] → GetElem? coll idx elem valid
-- Mathlib.Algebra.GroupWithZero.Defs
mul_left_injective₀ : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsRightCancelMulZero M₀] {b : M₀},
  b ≠ 0 → Function.Injective fun a => a * b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a space with second countable topology, strongly measurable and measurable are equivalent.  -/
stronglyMeasurable_iff_measurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [SecondCountableTopology β],
  MeasureTheory.StronglyMeasurable f ↔ Measurable f
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : DecidableEq ι] (i j : ι),
  (b.coord i) (b j) = if i = j then 1 else 0
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Factorized rational functions are meromorphic in normal form on `univ`.
 -/
Function.FactorizedRational.meromorphicNFOn_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ),
  MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) Set.univ
-- Mathlib.CategoryTheory.Equivalence
/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
functor.  -/
CategoryTheory.Equivalence.funInvIdAssoc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (e : C ≌ D) → (F : CategoryTheory.Functor C E) → e.functor.comp (e.inverse.comp F) ≅ F
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context.mk.injEq : ∀ (ringId : ℕ) (checkCoeffDvd : Bool) (ringId_1 : ℕ) (checkCoeffDvd_1 : Bool),
  ({ ringId := ringId, checkCoeffDvd := checkCoeffDvd } = { ringId := ringId_1, checkCoeffDvd := checkCoeffDvd_1 }) =
    (ringId = ringId_1 ∧ checkCoeffDvd = checkCoeffDvd_1)
-- Mathlib.Data.Int.ModEq
Int.sub_modulus_mul_modEq_iff : ∀ {n a b c : ℤ}, a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.StrongHomClass.mk : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  [inst : FunLike F M N] [inst_1 : L.Structure M] [inst_2 : L.Structure N],
  (∀ (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)) →
    (∀ (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x) →
      L.StrongHomClass F M N
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastLegendreSym.eq_1 : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), fastLegendreSym✝ p a = jacobiSym a p
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.iterate_lt_nfp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, StrictMono f → ∀ {a : Ordinal.{u}}, a < f a → ∀ (n : ℕ), f^[n] a < Ordinal.nfp f a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roo_eq_add : ∀ {m n i : ℕ}, i < n - (m + 1) → (m<...n).toArray[i]! = m + 1 + i