mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.PackageFactories
/-- Use this factory to conveniently define a preorder on a type `α` and all the associated operations
and instances given an `LE α` instance.

Creates a `PreorderPackage α` instance. Such an instance entails `LE α`, `LT α` and
`BEq α` instances as well as an `IsPreorder α` instance and `LawfulOrder*` instances proving the
compatibility of the operations with the preorder.

In the presence of `LE α`, `DecidableLE α`, `Refl (· ≤ ·)` and `Trans (· ≤ ·) (· ≤ ·) (· ≤ ·)`
instances, no arguments are required and the factory can be used as in this example:

```lean
public instance : PreorderPackage X := .ofLE X
```

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly
provide some arguments:

```lean
public instance : PreorderPackage X := .ofLE X {
  le_refl := sorry
  le_trans := sorry }
```

It is also possible to do all of this by hand, without resorting to `PreorderPackage`. This can
be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with
`PreorderPackage`.

**How the arguments are filled**

Lean tries to fill all of the fields of the `args : Packages.PreorderOfLEArgs α` parameter
automatically. If it fails, it is necessary to provide some of the fields manually.

* For the data-carrying typeclasses `LE`, `LT` and `BEq`, existing instances are always preferred.
  If no existing instances can be synthesized, it is attempted to derive an instance from the `LE`
  instance.
* Some proof obligations can be filled automatically if the data-carrying typeclasses have been
  derived from the `LE` instance. For example: If the `beq` field is omitted and no `BEq α` instance
  can be synthesized, it is derived from the `LE α` instance. In this case, `beq_iff_le_and_ge` can
  be omitted because Lean can infer that `BEq α` and `LE α` are compatible.
* Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans`
  instances can be synthesized.
 -/
Std.PreorderPackage.ofLE : (α : Type u) → autoParam (Std.Packages.PreorderOfLEArgs α) Std.PreorderPackage.ofLE._auto_1 → Std.PreorderPackage α
-- Mathlib.RingTheory.Unramified.Basic
Algebra.formallyUnramified_iff : ∀ (R : Type v) (A : Type u) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyUnramified R A ↔ Subsingleton Ω[A⁄R]
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left : ∀ {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] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D)
  {X Y : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).left = f.fiber.left
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.map_le_iff_le_comap : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f : L →ₗ⁅R⁆ L₂} {K : LieSubalgebra R L} {K' : LieSubalgebra R L₂},
  LieSubalgebra.map f K ≤ K' ↔ K ≤ LieSubalgebra.comap f K'
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalMod : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an % bn = rn → Mathlib.Meta.NormNum.IsNat (a % b) rn
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf)
      (AlgebraicGeometry.Proj.toSpecZero 𝒜) =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_lcm_helper : ∀ (x y d m : ℕ), x.gcd y = d → d.beq 0 = false → x * y = d * m → x.lcm y = m
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_prod_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] [inst_4 : DecidableLE (α × β)] (x : α × β),
  Finset.Ici x = Finset.Ici x.1 ×ˢ Finset.Ici x.2
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.subsingleton : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Subsingleton (Subalgebra R A)], Subsingleton (A →ₐ[R] B)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.w_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j)
      (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j') h
-- Mathlib.Algebra.Regular.Prod
IsAddRightRegular.sumMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddRightRegular a → IsAddRightRegular b → IsAddRightRegular (a, b)
-- Mathlib.RingTheory.Extension.Generators
/-- Reinterpret a hom between generators as a hom between extensions.  -/
Algebra.Generators.Hom.toExtensionHom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} →
                            [inst_6 : Algebra R R'] →
                              [inst_7 : Algebra S S'] →
                                [inst_8 : Algebra R S'] →
                                  [IsScalarTower R R' S'] →
                                    [IsScalarTower R S S'] → P.Hom P' → P.toExtension.Hom P'.toExtension
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence which maps a submodule of one module onto another,
restricts to a continuous linear equivalence of the two submodules.
This is `LinearEquiv.ofSubmodules` as a continuous linear equivalence.  -/
ContinuousLinearEquiv.ofSubmodules : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_3} →
      {M₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M₂] →
                  [inst_5 : TopologicalSpace M₂] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R₂ M₂} →
                        {σ₁₂ : R →+* R₂} →
                          {σ₂₁ : R₂ →+* R} →
                            {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                              {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                (e : M ≃SL[σ₁₂] M₂) →
                                  (p : Submodule R M) →
                                    (q : Submodule R₂ M₂) → Submodule.map (↑↑e) p = q → ↥p ≃SL[σ₁₂] ↥q
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K],
  MonoidHom.mker (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)) =
    Submonoid.map (algebraMap A K) (IsUnit.submonoid A)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_add : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : AddZeroClass Y]
  [inst_2 : DistribSMul N Y] (f g : X →ₑ[σ] Y), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.map_map_assoc : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9}
  {T : Type u_10} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
  [inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R Q] [inst_10 : Module R S] [inst_11 : Module R T] [inst_12 : Module R P]
  (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R (TensorProduct R M N) P),
  (TensorProduct.map f (TensorProduct.map g h)) ((TensorProduct.assoc R M N P) x) =
    (TensorProduct.assoc R Q S T) ((TensorProduct.map (TensorProduct.map f g) h) x)
-- Mathlib.Algebra.Divisibility.Basic
dvd_rfl : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, a ∣ a
-- Mathlib.GroupTheory.Congruence.Defs
Con.instPowQuotientNat : {M : Type u_4} → [inst : Monoid M] → (c : Con M) → Pow c.Quotient ℕ
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A scalar `μ` is a generalized eigenvalue for a linear map `f` and an exponent `k ∈ ℕ` if there
are generalized eigenvectors for `f`, `k`, and `μ`.  -/
Module.End.HasGenEigenvalue : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ → Prop
-- Init.Grind.AC
Lean.Grind.AC.instReprExpr : Repr Lean.Grind.AC.Expr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.mk.injEq : ∀ (f : Lean.Expr) (numArgs : ℕ) (f_1 : Lean.Expr) (numArgs_1 : ℕ),
  ({ f := f, numArgs := numArgs } = { f := f_1, numArgs := numArgs_1 }) = (f = f_1 ∧ numArgs = numArgs_1)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_of_indep_of_le_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → m₃ ≤ m₂ → ProbabilityTheory.Kernel.Indep m₁ m₃ κ μ
-- Mathlib.RingTheory.Flat.Equalizer
_private.Mathlib.RingTheory.Flat.Equalizer.0.LinearMap.lTensor_ker_subtype_tensorKerInv : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [inst_11 : Module.Flat R M] (x : ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker),
  (LinearMap.lTensor M f.ker.subtype) ((LinearMap.tensorKerInv S M f) x) = ↑x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t[k]? = some v ↔ ∃ (h : k ∈ t), t[k] = v
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.isSeparable : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L], Algebra.IsSeparable K L
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- **Alias** of `Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMap`. -/
Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap : ∀ {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O)
  [inst_4 : IsDiscreteValuationRing O] {ϖ : O},
  Irreducible ϖ → ↑(IsLocalRing.maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_symm_apply_coveringRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet Y),
  ((Delone.DeloneSet.mapIsometry f).symm D).coveringRadius = D.coveringRadius
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_neg_of_lt_zero : ∀ {x : ℝ}, x < 0 → -1 < x → Real.log x < 0
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.neg : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → Function.Antiperiodic f (-c)
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.mk.inj : ∀ {userName : Lean.Name} {type value : Lean.Expr} {binderInfo : Lean.BinderInfo} {kind : Lean.LocalDeclKind}
  {userName_1 : Lean.Name} {type_1 value_1 : Lean.Expr} {binderInfo_1 : Lean.BinderInfo} {kind_1 : Lean.LocalDeclKind},
  { userName := userName, type := type, value := value, binderInfo := binderInfo, kind := kind } =
      { userName := userName_1, type := type_1, value := value_1, binderInfo := binderInfo_1, kind := kind_1 } →
    userName = userName_1 ∧ type = type_1 ∧ value = value_1 ∧ binderInfo = binderInfo_1 ∧ kind = kind_1
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.map_invUnitsSub : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (u : Rˣ),
  (PowerSeries.map f) (PowerSeries.invUnitsSub u) = PowerSeries.invUnitsSub ((Units.map ↑f) u)
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The composition of morphisms is a morphism.  -/
NonUnitalAlgHom.comp : {R : Type u} →
  {S : Type u₁} →
    {T : Type u_1} →
      [inst : Monoid R] →
        [inst_1 : Monoid S] →
          [inst_2 : Monoid T] →
            {φ : R →* S} →
              {A : Type v} →
                {B : Type w} →
                  {C : Type w₁} →
                    [inst_3 : NonUnitalNonAssocSemiring A] →
                      [inst_4 : DistribMulAction R A] →
                        [inst_5 : NonUnitalNonAssocSemiring B] →
                          [inst_6 : DistribMulAction S B] →
                            [inst_7 : NonUnitalNonAssocSemiring C] →
                              [inst_8 : DistribMulAction T C] →
                                {ψ : S →* T} →
                                  {χ : R →* T} → (B →ₛₙₐ[ψ] C) → (A →ₛₙₐ[φ] B) → [κ : φ.CompTriple ψ χ] → A →ₛₙₐ[χ] C
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- `CNF.eval f` evaluates a Finsupp `f : Ordinal →₀ Ordinal`, interpreted as a
base `b` expansion on ordinals.  -/
Ordinal.CNF.eval : Ordinal.{u_1} → (Ordinal.{u_1} →₀ Ordinal.{u_1}) → Ordinal.{u_1}
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_pos : ∀ {G : Type u} [inst : AddMonoid G], 0 < AddMonoid.exponent G ↔ AddMonoid.ExponentExists G
-- Mathlib.Topology.UniformSpace.Real
Real.instCompleteSpace : CompleteSpace ℝ
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.lift_comp_of : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (F : FreeLieAlgebra R X →ₗ⁅R⁆ L), (FreeLieAlgebra.lift R) (⇑F ∘ FreeLieAlgebra.of R) = F
-- Mathlib.Order.Filter.CountablyGenerated
Filter.comap.isCountablyGenerated : ∀ {α : Type u_1} {β : Type u_2} (l : Filter β) [l.IsCountablyGenerated] (f : α → β),
  (Filter.comap f l).IsCountablyGenerated
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Augment a cosimplicial object with an object.  -/
CategoryTheory.CosimplicialObject.augment : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.CosimplicialObject C) →
      (X₀ : C) →
        (f : X₀ ⟶ X.obj { len := 0 }) →
          (∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
              CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) →
            CategoryTheory.CosimplicialObject.Augmented C
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableLtOrdinal : {x y : Std.Time.Month.Ordinal} → Decidable (x < y)
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Find an entry in the tree with key equal to `k`.  -/
RBTree.RBMap.findEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → Option (α × β)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntryD.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a) (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntryD x = ⟨k, v⟩
-- Init.Data.Bool
/-- De Morgan's law for boolean and  -/
Bool.not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y)
-- Mathlib.Analysis.Seminorm
Seminorm.instInf : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → Min (Seminorm 𝕜 E)
-- Init.Data.List.Nat.Erase
List.getElem?_eraseIdx : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_of_hasDerivWithinAt_Ioi : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Ioi x) x → slope f x y < f'
-- Mathlib.Order.Filter.Basic
Filter.inter_eventuallyEq_right : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
-- Mathlib.Topology.Algebra.Ring.Ideal
QuotientRing.isQuotientMap_coe_coe : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] (N : Ideal R) [IsTopologicalRing R],
  Topology.IsQuotientMap fun p => ((Ideal.Quotient.mk N) p.1, (Ideal.Quotient.mk N) p.2)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasDerivAt_exp_smul_const : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸) (t : 𝕂), HasDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
Set.range_add_eq_image_Ici : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {β : Type u_2} {f : α → β} {k : α}, (Set.range fun x => f (x + k)) = f '' Set.Ici k
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.forall_inv_mem : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α} {p : α → Prop}, (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ x ∈ s, p x⁻¹
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComapOfBijective_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (hf : Function.Bijective ⇑f) (p : Submodule R M),
  (Submodule.orderIsoMapComapOfBijective f hf) p = Submodule.map f p
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instReprBehaviorIfUnchanged : Repr Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.maxDegree_eq : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [Nonempty V] [inst_2 : DecidableRel G.Adj] {d : ℕ},
  G.IsRegularOfDegree d → G.maxDegree = d
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A square is a pushout square if its flip is.  -/
CategoryTheory.Limits.PushoutCocone.isColimitOfFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t.flip → CategoryTheory.Limits.IsColimit t
-- Mathlib.RingTheory.Flat.Stability
Module.Flat.localizedModule : ∀ {R : Type u} {M : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Flat R M]
  (S : Submonoid R), Module.Flat (Localization S) (LocalizedModule S M)
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  {a b : α} (hf : BoundedVariationOn f Set.univ),
  a ≤ b → hf.vectorMeasure (Set.Icc a b) = Function.rightLim f b - Function.leftLim f a
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_neg`. -/
MonovaryOn.of_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn (-f) (-g) s → MonovaryOn f g s
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.cobounded_aux : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoMetricSpace (α i)]
  [inst_2 : Fintype ι], Bornology.cobounded (PiLp p α) = Bornology.cobounded (PiLp p α)
-- Mathlib.Algebra.Category.BoolRing
/-- The category of Boolean rings.  -/
BoolRing : Type (u + 1)
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalLE_false : ∀ {a b : Ordinal.{u}} {an bn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an → Mathlib.Meta.NormNum.IsNat b bn → decide (an ≤ bn) = false → ¬a ≤ b
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.mulLeftRight_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] (x y z : R),
  (((ContinuousLinearMap.mulLeftRight 𝕜 R) x) y) z = x * z * y
-- Mathlib.Data.Finset.Range
Finset.mem_range_succ_iff : ∀ {a b : ℕ}, a ∈ Finset.range b.succ ↔ a ≤ b
-- Init.Data.UInt.Bitwise
UInt16.ofFin_and : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a &&& b) = UInt16.ofFin a &&& UInt16.ofFin b
-- Mathlib.NumberTheory.Real.Irrational
irrational_add_intCast_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (x + ↑m) ↔ Irrational x
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsMonomorphisms.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f) → F.ReflectsMonomorphisms
-- Mathlib.Dynamics.Flow
/-- The forward orbit of a point under a flow.  -/
Flow.forwardOrbit : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid τ] → Flow τ α → [inst : Preorder τ] → [AddLeftMono τ] → α → Set α
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The `MulEquiv` between two monoids with a unique element.  -/
MulEquiv.ofUnique : {M : Type u_16} → {N : Type u_17} → [Unique M] → [Unique N] → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The ideal defined by `restrictSupport R s` when `s` is an upper set.  -/
MvPolynomial.restrictSupportIdeal : {σ : Type u} → (R : Type v) → [inst : CommSemiring R] → (s : Set (σ →₀ ℕ)) → IsUpperSet s → Ideal (MvPolynomial σ R)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_Z : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y), (I.precompRelation g).Z = (I.precomp g).Y
-- Init.Data.List.Basic
List.tail_cons : ∀ {α : Type u} {a : α} {as : List α}, (a :: as).tail = as