mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The sum of vectors from the centroid to each vertex is zero.  -/
Affine.Simplex.centroid_weighted_vsub_eq_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n), ∑ i, (s.points i -ᵥ s.centroid) = 0
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_hom_leftUnitor : ∀ {R : Type u} [inst : CommRing R] {M : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(Algebra.TensorProduct.lid R ↑M)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.CommRing.Poly)
  (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₂))
  (k₁ k₂ : ℤ),
  p₁ = Lean.Grind.CommRing.Poly.num k₁ →
    p₂ = Lean.Grind.CommRing.Poly.num k₂ →
      (match p₁, p₂ 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.Data.Nat.Prime.Defs
Nat.Primes.coe_nat_injective : Function.Injective Subtype.val
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_diseq_subst : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.diseq_eq_subst_cert x p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≠ 0
-- Init.Data.SInt.Basic
/-- Obtains the `Int16` that is 2's complement equivalent to the `UInt16`.  -/
UInt16.toInt16 : UInt16 → Int16
-- Init.Data.Ord.Basic
isLE_compareOfLessAndEq : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [DecidableLE α] [inst_4 : DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ {x y : α}, ¬x ≤ y ↔ y < x) →
      (∀ (x y : α), x ≤ y ∨ y ≤ x) → ∀ {x y : α}, (compareOfLessAndEq x y).isLE = true ↔ x ≤ y
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection_mul_transvection_same : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n],
  i ≠ j → ∀ (c d : R), Matrix.transvection i j c * Matrix.transvection i j d = Matrix.transvection i j (c + d)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.skipWhile_prop_eq_skipWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} (curr : s.Pos),
  curr.skipWhile p = curr.skipWhile fun x => decide (p x)
-- Mathlib.NumberTheory.Modular
/-- Every pair `![c, d]` of coprime integers is the "bottom row" of some element `g=[[*,*],[c,d]]`
of `SL(2,ℤ)`.  -/
ModularGroup.bottom_row_surj : ∀ {R : Type u_1} [inst : CommRing R], Set.SurjOn (fun g => ↑g 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}
-- Lean.Environment
/-- Returns the current extension state. See `AsyncMode` for details on how modifications from
different environment branches are reconciled.

Overriding the extension's default `AsyncMode` is usually not recommended and should be considered
only for important optimizations.
 -/
Lean.EnvExtension.getState : {σ : Type} →
  [Inhabited σ] →
    (ext : Lean.EnvExtension σ) →
      Lean.Environment → optParam Lean.EnvExtension.AsyncMode ext.asyncMode → optParam Lean.Name Lean.Name.anonymous → σ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X_1 Y : X} (f : X_1 ⟶ Y),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).snd.map f = (J.map f).snd
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.DistribNotState.mk.sizeOf_spec : ∀ (fvars : List Lean.Expr) (currentGoal : Lean.MVarId),
  sizeOf { fvars := fvars, currentGoal := currentGoal } = 1 + sizeOf fvars + sizeOf currentGoal
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The index type parametrising the data of two morphisms `g₁ g₂ : Y ⟶ step W Z`, and
a map `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.  -/
CategoryTheory.OrthogonalReflection.D₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [CategoryTheory.Limits.HasPushouts C] → Type (max u v)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.instCategory : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] → CategoryTheory.Category.{max u_1 u_2, u_1} (CategoryTheory.Cat.FreeRefl V)
-- Init.Data.Nat.Basic
Nat.mul_zero : ∀ (n : ℕ), n * 0 = 0
-- Lean.Elab.ConfigEval.DeriveEvalTerm
Lean.Elab.ConfigEval.EvalTerm.checkExpectedNumberOfArguments : Lean.Name → ℕ → Lean.TSyntaxArray `term → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.congr_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  (CategoryTheory.MonoOver.congr X e).unitIso =
    CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.unitIso.app Y.obj.left) ⋯) ⋯
-- Mathlib.Data.ENat.Basic
ENat.instWellFoundedRelation : WellFoundedRelation ℕ∞
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (lhs rhs cin : aig.Ref),
  Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry aig { lhs := lhs, rhs := rhs, cin := cin } =
    (((aig.mkXorCached { lhs := lhs, rhs := rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := lhs, rhs := rhs }).ref, rhs := cin.cast ⋯ }).aig.mkAndCached
            { lhs := (lhs.cast ⋯).cast ⋯, rhs := (rhs.cast ⋯).cast ⋯ }).aig.mkOrCached
      {
        lhs :=
          ((aig.mkXorCached { lhs := lhs, rhs := rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := lhs, rhs := rhs }).ref, rhs := cin.cast ⋯ }).ref.cast
            ⋯,
        rhs :=
          (((aig.mkXorCached { lhs := lhs, rhs := rhs }).aig.mkAndCached
                    { lhs := (aig.mkXorCached { lhs := lhs, rhs := rhs }).ref, rhs := cin.cast ⋯ }).aig.mkAndCached
              { lhs := (lhs.cast ⋯).cast ⋯, rhs := (rhs.cast ⋯).cast ⋯ }).ref }
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_of_eqOn_coFG : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂} {A : Submodule K V},
  A.CoFG → Set.EqOn ⇑u ⇑v ↑A → u ≈ v
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- Pushforward for ultrafilters.  -/
Ultrafilter.map : {α : Type u} → {β : Type v} → (α → β) → Ultrafilter α → Ultrafilter β
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioi_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Ioi a = Set.Iio (a / c)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_mk : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂)
  (h : Continuous f.toFun), ↑{ toLinearMap := f, cont := h } = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_preΨ' : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℕ),
  (W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)
-- Mathlib.Topology.Order.LeftRight
nhdsWithin_uIoo_left_le_nhdsNE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {a b : α},
  nhdsWithin a (Set.uIoo a b) ≤ nhdsWithin a {a}ᶜ
-- Std.Time.Format.DateFormat
/-- Short PM marker (used by `a`/`aa`/`aaa`).
 -/
Std.Time.DateFormatSymbols.pmShort : Std.Time.DateFormatSymbols → String
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams.changes : Lean.Lsp.DidChangeWatchedFilesParams → Array Lean.Lsp.FileEvent
-- Mathlib.CategoryTheory.Filtered.FinallySmall
/-- If `C` is a locally small cofiltered initially small category,
this is a small cofiltered category, equipped with an initial functor to `C`
(see `fromCofilteredInitialModel`).  -/
CategoryTheory.InitiallySmall.CofilteredInitialModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofiltered C] →
      [CategoryTheory.LocallySmall.{w, v, u} C] → [CategoryTheory.InitiallySmall C] → Type w
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansionRingHom.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} (h h_1 : ℝ) (e_h : h = h_1) [inst : Γ.HasDetPlusMinusOne] (hh : 0 < h)
  (hΓ : h ∈ Γ.strictPeriods), ModularForm.qExpansionRingHom h hh hΓ = ModularForm.qExpansionRingHom h_1 ⋯ ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_inf_le : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s₁ s₂ : AffineSubspace k P₁),
  AffineSubspace.map f (s₁ ⊓ s₂) ≤ AffineSubspace.map f s₁ ⊓ AffineSubspace.map f s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i))
        h)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_sub_sum_filter : ∀ {α : Type u_1} {M : Type u_5} {G : Type u_8} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : AddCommGroup G] (g : α → M → G),
  f.sum g - (Finsupp.filter p f).sum g = (Finsupp.filter (fun a => ¬p a) f).sum g
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The type of copies as a subtype of *injective* homomorphisms.  -/
SimpleGraph.Copy : {α : Type u_4} → {β : Type u_5} → SimpleGraph α → SimpleGraph β → Type (max u_4 u_5)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_flip_iff : ∀ (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu],
  Contravariant N N (flip mu) r ↔ Contravariant N N mu r
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `CommSemiring` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.CommSemiring.commSemiringInst : Lean.Meta.Grind.Arith.CommRing.CommSemiring → Lean.Expr
-- Init.Data.List.MinMaxOn
/-- Returns an element of `l` that maximizes `f`. If `x`, `y` are such that
`f x = f y`, it returns whichever comes first in the list. Returns `none` if the list is
empty.

The correctness of this function assumes `β` to be linearly pre-ordered.
The property that `List.maxOn?` is the first minimizer in the list is guaranteed by the lemma
`List.getElem_get_maxIdxOn?`.
 -/
List.maxOn? : {β : Type u_1} → {α : Type u_2} → [i : LE β] → [DecidableLE β] → (α → β) → List α → Option α
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin_symm_apply_one : ∀ {n : ℕ} (e : Equiv.Perm (Fin (n + 1))) (p : Fin (n + 2)),
  (Equiv.Perm.decomposeFin.symm (p, e)) 1 = (Equiv.swap 0 p) (e 0).succ
-- Init.Data.String.Substring
/-- Removes leading whitespace from a substring by moving its start position to the first non-whitespace
character, or to its end position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
 -/
Substring.Raw.trimLeft : Substring.Raw → Substring.Raw
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I)
  (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : Y.I),
  (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).inv.φ i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (h (e.symm i)).inv
-- Mathlib.Logic.Equiv.Sum
/-- Combine two `Equiv`s using `PSum` in the domain and `Sum` in the codomain.  -/
Equiv.psumSum : {α₁ : Sort u_2} → {β₁ : Sort u_5} → {α₂ : Type u_9} → {β₂ : Type u_10} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕' β₁ ≃ α₂ ⊕ β₂
-- Lean.Parser.Extension
Lean.Parser.parserOfStackFn : ℕ → Lean.Parser.ParserFn
-- Mathlib.Topology.VectorBundle.Basic
/-- Preferred local trivialization of a vector bundle constructed from core, at a given point, as
a bundle trivialization  -/
VectorBundleCore.localTrivAt : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → B → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.Analysis.ODE.Gronwall
/-- A Grönwall-like inequality: if `f : ℝ → E` is continuous on `[a, b]`, has right derivative
`f' x` at every point `x ∈ [a, b)`, and satisfies the inequalities `‖f a‖ ≤ δ`,
`∀ x ∈ [a, b), ‖f' x‖ ≤ K * ‖f x‖ + ε`, then `‖f x‖` is bounded by `gronwallBound δ K ε (x - a)`
on `[a, b]`.  -/
norm_le_gronwallBound_of_norm_deriv_right_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {δ K ε a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ‖f a‖ ≤ δ → (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε) → ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ gronwallBound δ K ε (x - a)
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into either a `Fraction`. It's used for `nano`.
 -/
Std.Time.Fraction.classify : ℕ → Option Std.Time.Fraction
-- Mathlib.Topology.MetricSpace.PiNat
/-- Metric space structure on `Π (n : ℕ), E n` when the spaces `E n` have the discrete topology,
where the distance is given by `dist x y = (1/2)^n`, where `n` is the smallest index where `x` and
`y` differ. Not registered as a global instance by default.
Warning: this definition makes sure that the topology is defeq to the original product topology,
but it does not take care of a possible uniformity. If the `E n` have a uniform structure, then
there will be two non-defeq uniform structures on `Π n, E n`, the product one and the one coming
from the metric structure. In this case, use `metricSpaceOfDiscreteUniformity` instead.  -/
PiNat.metricSpace : {E : ℕ → Type u_1} →
  [inst : (n : ℕ) → TopologicalSpace (E n)] → [∀ (n : ℕ), DiscreteTopology (E n)] → MetricSpace ((n : ℕ) → E n)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.tendsto_klFun_atTop : Filter.Tendsto InformationTheory.klFun Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism from a terminal object is mono.  -/
CategoryTheory.Limits.IsTerminal.mono_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X)
  (f : X ⟶ Y), CategoryTheory.Mono f
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.equivalenceOfEquiv_unitIso : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I),
  (CategoryTheory.Pi.equivalenceOfEquiv C e).unitIso =
    CategoryTheory.NatIso.pi' fun i' =>
      (CategoryTheory.Pi.eval (fun i => C (e i)) i').leftUnitor ≪≫
        (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) ⋯).symm ≪≫
          (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).isoWhiskerLeft
              (CategoryTheory.Pi.eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫
            (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp
                  (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫
              (CategoryTheory.Functor.pi'
                      (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).isoWhiskerLeft
                  (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval fun i => C (e i'))
                      (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫
                ((CategoryTheory.Functor.pi'
                        (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).associator
                    (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval fun i => C (e i')))
                    (CategoryTheory.Pi.eval (fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor)).symm
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x a : α), Mathlib.Tactic.Abel.term n x a = n • x + a
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_invOrderIso_symm_apply : ∀ {G : Type u_2} [inst : Group G] (a : Submonoid G), ↑((RelIso.symm Submonoid.invOrderIso) a) = (↑a)⁻¹
-- Mathlib.Probability.Martingale.Upcrossing
/-- `lowerCrossingTime a b f N n` is the first time before time `N`, `f` reaches
below `a` after `f` reached above `b` for the `n`-th time.  -/
MeasureTheory.lowerCrossingTime : {Ω : Type u_1} → {ι : Type u_2} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → ℝ → ℝ → (ι → Ω → ℝ) → ι → ℕ → Ω → ι
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H0Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.H0Iso A =
    (groupCohomology.inhomogeneousCochains A).isoHomologyπ₀.symm ≪≫ groupCohomology.cocyclesIso₀ A
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.SemiconjBy.zpow_right : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A X Y : Matrix n' n' R}, IsUnit X.det → IsUnit Y.det → SemiconjBy A X Y → ∀ (m : ℤ), SemiconjBy A (X ^ m) (Y ^ m)
-- Mathlib.Algebra.Free
/-- Recursor for `FreeAddMagma` using `x + y` instead of `FreeAddMagma.add x y`.  -/
FreeAddMagma.recOnAdd : {α : Type u} →
  {C : FreeAddMagma α → Sort l} →
    (x : FreeAddMagma α) → ((x : α) → C (FreeAddMagma.of x)) → ((x y : FreeAddMagma α) → C x → C y → C (x + y)) → C x
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Converts an inductive constructor `c` into a `Shape` that will be used later in
while proving the iff theorem, and a proposition representing the constructor.
 -/
Mathlib.Tactic.MkIff.constrToProp : List Lean.Level → List Lean.Expr → List Lean.Expr → Lean.Name → Lean.MetaM (Mathlib.Tactic.MkIff.Shape × Lean.Expr)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ),
  (fun b => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) =ᵐ[ν a] fun b => f (a, b) q
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.isUniformEmbedding : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), IsUniformEmbedding ⇑h
-- Std.Http.Data.URI.Encoding
/-- Appends a single encoded character to an encoded string.
Requires that the character is not '%' to maintain the percent-encoding invariant.
 -/
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.push : {r : UInt8 → Bool} →
  Std.Http.URI.EncodedString r → (c : UInt8) → Std.Http.URI.isEncodedChar r c = true → Std.Http.URI.EncodedString r
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_toAddSubmonoid : ∀ {M : Type u_1} [inst : AddZeroClass M] {b : SaturatedAddSubmonoid M}, b.saturation = b
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.isLocalMax : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalMaxOn f s a → s ∈ nhds a → IsLocalMax f a
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal S),
  Algebra.ZariskisMainProperty R p →
    ∃ S', (Subalgebra.toSubmodule S').FG ∧ ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
-- Mathlib.Data.Multiset.MapFold
/-- `map f s` is the lift of the list `map` operation. The multiplicity
of `b` in `map f s` is the number of `a ∈ s` (counting multiplicity)
such that `f a = b`.  -/
Multiset.map : {α : Type u_1} → {β : Type v} → (α → β) → Multiset α → Multiset β
-- Std.Time.Format.Basic
/-- Configuration options for formatting and parsing date/time strings.
 -/
Std.Time.FormatConfig : Type
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_atBot : ∀ (f : CircleDeg1Lift), Filter.Tendsto (⇑f) Filter.atBot Filter.atBot