mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_lt_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightStrictMono α] (a : α) {b : α}, 1 < b → a < b * a
-- Mathlib.Computability.Language
instDecidableEqSymbol.decEq : {T : Type u_4} → {N : Type u_5} → [DecidableEq T] → [DecidableEq N] → (x x_1 : Symbol T N) → Decidable (x = x_1)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
AddSubgroup.instCountableSubtypeMemZMultiples : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), Countable ↥(AddSubgroup.zmultiples a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : Inhabited β] {a : α} {c : ℕ},
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.emptyWithCapacity c) a = default
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relationsSolutionEquiv_apply_apply : ∀ {R : Type u} [inst : CommRing R] {N : Type u_2} [inst_1 : AddCommGroup N] [inst_2 : Module R N] {ι : Type u_4}
  [inst_3 : DecidableEq ι] {M : Type u_5} [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  (s : (exteriorPower.presentation.relations R ι M).Solution N) (m : ι → M),
  (exteriorPower.presentation.relationsSolutionEquiv s) m = s.var m
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks₂₂_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (v : l ⊕ m → α), (Matrix.diagonal v).toBlocks₂₂ = Matrix.diagonal fun i => v (Sum.inr i)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.tensorHom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄)
  (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).app X =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X) (g.app X)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_mul : ∀ {d : ℤ} (n m : ℤ√d), (n * m).norm = n.norm * m.norm
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsVertexCover.mono : ∀ {V : Type u_1} {G G' : SimpleGraph V} {c : Set V}, G ≤ G' → G'.IsVertexCover c → G.IsVertexCover c
-- Batteries.Tactic.HelpCmd
/-- The command `#help option` shows all options that have been defined in the current environment.
Each option has a format like:
```
option pp.all : Bool := false
  (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names,
  universe, and disable beta reduction and notations during pretty printing
```
This says that `pp.all` is an option which can be set to a `Bool` value, and the default value is
`false`. If an option has been modified from the default using e.g. `set_option pp.all true`,
it will appear as a `(currently: true)` note next to the option.

The form `#help option id` will show only options that begin with `id`.
 -/
Batteries.Tactic.«command#help_Option___» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.nonempty_iff_map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), Nonempty F.FullyFaithful ↔ ∀ (X Y : C), Function.Bijective F.map
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv`. -/
NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R]
  (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)),
  ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) =
    (NumberField.HeightOneSpectrum.adicAbv K v) ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The number of permutations of a given multiset.  -/
Multiset.countPerms : {α : Type u_1} → [DecidableEq α] → Multiset α → ℕ
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm' : ∀ {E : Type u_4} [inst : SeminormedGroup E] {x : E}, Filter.Tendsto (fun a => ‖a‖) (nhds x) (nhds ‖x‖)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.nonsingularLift_negMap : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : WeierstrassCurve.Projective.PointClass F},
  W.NonsingularLift P → W.NonsingularLift (W.negMap P)
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `a = False` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushEqFalse : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {K : Type u} [inst : Field K]
  (g : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X),
  AlgebraicGeometry.Scheme.descResidueField
      (AlgebraicGeometry.Scheme.stalkClosedPointTo (CategoryTheory.CategoryStruct.comp g f)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (g (IsLocalRing.closedPoint K)))
      (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo g))
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.throwWrongArgCount.checkNamedArgs : Lean.Elab.Term.CollectPatternVars.Context → Lean.Elab.Term.CollectPatternVars.M Unit
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- `Finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`.  -/
sigmaFinsuppLequivDFinsupp : {ι : Type u_1} →
  (R : Type u_2) →
    {η : ι → Type u_4} →
      {N : Type u_5} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid N] → [inst_2 : Module R N] → ((i : ι) × η i →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.left_apply_subtype : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  (a : { a // p a }), (ep.subtypeCongr en) ↑a = ↑(ep a)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
/-- `log` as a homeomorphism.  -/
ENNReal.logHomeomorph : ENNReal ≃ₜ EReal
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_hom : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N), ModuleCat.ofHom (ModuleCat.Hom.hom f) = f
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq_concat : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (i : B),
  cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
-- Mathlib.Topology.Order.IsNormal
/-- A normal function between well-orders is equivalent to a strictly monotone,
continuous function.  -/
Order.isNormal_iff_strictMono_and_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : TopologicalSpace α] [OrderTopology α]
  [inst_4 : LinearOrder β] [WellFoundedLT β] [inst_6 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Order.IsNormal f ↔ StrictMono f ∧ Continuous f
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsFinite
-- Init.Data.Vector.Range
Vector.mem_range : ∀ {m n : ℕ}, m ∈ Vector.range n ↔ m < n
-- Mathlib.Tactic.NormNum.Result
/-- Constructs a `Result` out of a raw int cast.
Assumes `e` is a raw int cast expression denoting `n`.  -/
Mathlib.Meta.NormNum.Result.ofRawInt : {u : Lean.Level} → {α : Q(Type u)} → ℤ → (e : Q(«$α»)) → Mathlib.Meta.NormNum.Result e
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqDecl : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.Decl pu)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.nodup_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp], t.keys.Nodup
-- Mathlib.Data.ENat.Basic
ENat.top_mul : ∀ {m : ℕ∞}, m ≠ 0 → ⊤ * m = ⊤
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_eq_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s : σ →₀ ℕ} {b : R}, (MvPolynomial.monomial s) b = 0 ↔ b = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) [inst_3 : NatCast F] (n : ℕ), derivWithin (↑n) s = 0
-- Aesop.Tree.Data
Aesop.instInhabitedGoalState : Inhabited Aesop.GoalState
-- Init.Data.SInt.Lemmas
Int64.toInt32_mul : ∀ (a b : Int64), (a * b).toInt32 = a.toInt32 * b.toInt32
-- Init.Data.Rat.Basic
Rat.den_pos : ∀ (self : ℚ), 0 < self.den
-- Mathlib.Algebra.Module.LinearMap.Defs
AddMonoidHom.toNatLinearMap_injective : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂],
  Function.Injective AddMonoidHom.toNatLinearMap
-- Init.Grind.Config
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test.  -/
Lean.Grind.Config.canonHeartbeats : Lean.Grind.Config → ℕ
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.preAleph_symm_eq_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.preAleph.symm c = c.ord
-- Mathlib.Tactic.Simps.Basic
/-- the list of projection numbers this expression corresponds to  -/
Simps.ParsedProjectionData.projNrs : Simps.ParsedProjectionData → Array ℕ
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instSMulCommClassTensorProduct_1 : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B], SMulCommClass B A (TensorProduct R A B)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord_source : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarSpaceCoord K).source = Set.univ ×ˢ Set.univ.pi fun i => Complex.polarCoord.source
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
lt_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a b : α}, a < |b|ₘ ↔ a < b ∨ a < b⁻¹
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.two_le_deg : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E] [Algebra.IsSeparable F E]
  (i : (Module.rank F E).ord.ToType),
  2 ≤
    Cardinal.mk
      (Field.Emb
        ↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
        ↥(↥(IntermediateField.adjoin F
                (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                  Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯)
-- Std.Http.Data.Status
/-- Checks if the type of the status code is informational, meaning that the request was received
and the process is continuing.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isInformational : Std.Http.Status → Bool
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If a groupoid `G` is `ClosedUnderRestriction`, then an open subset of a space which is
`HasGroupoid G` is naturally `HasGroupoid G`.  -/
TopologicalSpace.Opens.instHasGroupoid : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [HasGroupoid M G] (s : TopologicalSpace.Opens M) [ClosedUnderRestriction G],
  HasGroupoid (↥s) G
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, any sphere is preconnected.  -/
isPreconnected_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  1 < Module.rank ℝ E → ∀ (x : E) (r : ℝ), IsPreconnected (Metric.sphere x r)
-- Lean.Meta.Closure
Lean.Meta.Closure.State.exprMVarArgs : Lean.Meta.Closure.State → Array Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  {f : (a : α) → β a → Bool},
  m.WF → (Std.DHashMap.Raw.filter f m).toList.Perm (List.filter (fun p => f p.fst p.snd) m.toList)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {s : Set α},
  MeasurableSet s → MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.equiv_eq_restrict : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), ↑pkg.equiv = u.restrict ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.natCast_ne_bot : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑n ≠ ⊥
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.norm_def' : ∀ {n : Type u_2} {A : Type u_5} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A]
  [inst_3 : Fintype n] {M : CStarMatrix n n A}, ‖M‖ = ‖CStarMatrix.toCLMNonUnitalAlgHom M‖
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsSFiniteKernel.comapRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (hf : MeasurableEmbedding f), ProbabilityTheory.IsSFiniteKernel (κ.comapRight hf)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk.injEq : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (toMultilinearMap : MultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap.toFun v = 0)
  (toMultilinearMap_1 : MultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq'_1 : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap_1.toFun v = 0),
  ({ toMultilinearMap := toMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
      { toMultilinearMap := toMultilinearMap_1, map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 }) =
    (toMultilinearMap = toMultilinearMap_1)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `α` is a preorder with top, then `⊤` is a terminal object.  -/
CategoryTheory.Limits.isTerminalTop : {α : Type u_1} → [inst : Preorder α] → [inst_1 : OrderTop α] → CategoryTheory.Limits.IsTerminal ⊤
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see `charFunDual_pi`
for the Banach space version.  -/
MeasureTheory.charFun_pi : ∀ {ι : Type u_6} [inst : Fintype ι] {E : ι → Type u_7} [inst_1 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_2 : (i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)}
  {μ : (i : ι) → MeasureTheory.Measure (E i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (t : PiLp 2 E),
  MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi μ)) t =
    ∏ i, MeasureTheory.charFun (μ i) (t.ofLp i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → Std.DTreeMap.Internal.Impl.contains t.minKey! t = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f)
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).inv h)
-- Init.Data.SInt.Basic
/-- Decides whether one 16-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE Int16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int16) ≤ 7 then "yes" else "no") = "yes"`
 * `(if (15 : Int16) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"`
 * `show (7 : Int16) ≤ 7 by decide`
 -/
Int16.decLe : (a b : Int16) → Decidable (a ≤ b)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableSMul₂ M X] {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f • g) μ
-- Init.Data.Ord.Basic
instOrdBool : Ord Bool
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.contains.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    (a_1 == a || Std.DHashMap.Internal.AssocList.contains a es)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns all equivalence classes in the current goal.  -/
Lean.Meta.Grind.getEqcs : Lean.Meta.Grind.GoalM (List (List Lean.Expr))
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_dual_eq : ∀ {α : Type u_1} {E : Set α}, (Matroid.freeOn E)✶ = Matroid.loopyOn E
-- Mathlib.FieldTheory.Finite.GaloisField
GaloisField.splits_zmod_X_pow_sub_X : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)], (Polynomial.X ^ p - Polynomial.X).Splits
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.uncurry_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N),
  ((TensorProduct.uncurry σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n
-- Mathlib.Data.Num.Bitwise
/-- Right-shift the binary representation of a `Num`.  -/
Num.shiftr : Num → ℕ → Num
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.rel.prod : ∀ {I : Type u} [inst : DecidableEq I] {R : Type v} [inst_1 : CommSemiring R] {A : I → Type w}
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {i : I} {a₁ a₂ : A i},
  LinearAlgebra.FreeProduct.rel R A
    ((TensorAlgebra.tprod R (DirectSum I fun i => A i) 2) fun x =>
      match x with
      | 0 => (DirectSum.lof R I A i) a₁
      | 1 => (DirectSum.lof R I A i) a₂)
    ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) (a₁ * a₂)))
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β} {b : β},
  l.mapFinIdx f = List.replicate l.length b ↔ ∀ (i : ℕ) (h : i < l.length), f i l[i] h = b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, AddOpposite.op '' (-s) = -AddOpposite.op '' s
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The left extension along the identity.  -/
CategoryTheory.Bicategory.LeftExtension.alongId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → (g : a ⟶ c) → CategoryTheory.Bicategory.LeftExtension (CategoryTheory.CategoryStruct.id a) g
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_sup : ∀ {M : Type u_2} [inst : Mul M] (S₁ S₂ : Subsemigroup M), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Mathlib.Data.Set.Basic
Set.subset_union_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → ∀ (u : Set α), s ⊆ t ∪ u
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
/-- Construct a model that satisfies all constraints in the linarith model for the structure with id `structId`.
It also assigns values to (integer) terms that have not been internalized by the linarith model.
 -/
Lean.Meta.Grind.Arith.Linear.mkModel : Lean.Meta.Grind.Goal → ℕ → Lean.MetaM (Array (Lean.Expr × ℚ))
-- Mathlib.Topology.Algebra.ConstMulAction
Filter.Tendsto.const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  {f : β → α} {l : Filter β} {a : α},
  Filter.Tendsto f l (nhds a) → ∀ (c : M), Filter.Tendsto (fun x => c +ᵥ f x) l (nhds (c +ᵥ a))
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (v : n → R), (Matrix.toLinAlgEquiv' M) v = M.mulVec v
-- Mathlib.Algebra.Order.Hom.Submonoid
Submonoid.topOrderMonoidIso_apply : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Monoid α] (x : ↥⊤), Submonoid.topOrderMonoidIso x = ↑x
-- Mathlib.LinearAlgebra.Dual.Defs
Module.mapEvalEquiv_symm_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M] (W'' : Submodule R (Module.Dual R (Module.Dual R M))),
  (Module.mapEvalEquiv R M).symm W'' = Submodule.comap (Module.Dual.eval R M) W''