mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.cokernel_funext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {FC : C → C → Type u_2} {CC : C → Type u_3} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [inst_3 : CategoryTheory.ConcreteCategory C FC] {M N K : C} {f : M ⟶ N} [inst_4 : CategoryTheory.Limits.HasCokernel f]
  {g h : CategoryTheory.Limits.cokernel f ⟶ K},
  (∀ (n : CategoryTheory.ToType N),
      (CategoryTheory.ConcreteCategory.hom g)
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) n) =
        (CategoryTheory.ConcreteCategory.hom h)
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) n)) →
    g = h
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapComp_inv_app : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂}
  (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K),
  (CategoryTheory.Pi.comapComp C f g).inv.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
-- Mathlib.Topology.UniformSpace.Basic
closure_eq_inter_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {t : SetRel α α}, closure t = ⋂ d ∈ uniformity α, SetRel.comp d (t.comp d)
-- Mathlib.RingTheory.SimpleModule.Isotypic
le_isotypicComponent_iff : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M] {m : Submodule R M},
  m ≤ isotypicComponent R M S ↔ IsIsotypicOfType R (↥m) S
-- Mathlib.Algebra.Star.Conjneg
conjneg_sum : ∀ {ι : Type u_1} {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R]
  (s : Finset ι) (f : ι → G → R), conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i)
-- Lean.Structure
Lean.StructureInfo.mk : Lean.Name → Array Lean.Name → Array Lean.StructureFieldInfo → Array Lean.StructureParentInfo → Lean.StructureInfo
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.is_topological_valuation : ∀ {R : Type u} {inst : Ring R} {Γ₀ : outParam (Type v)} {inst_1 : LinearOrderedCommGroupWithZero Γ₀}
  [self : Valued R Γ₀] (s : Set R), s ∈ nhds 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
-- Mathlib.AlgebraicGeometry.Artinian
/-- The underlying type of an Artinian Scheme is finite  -/
AlgebraicGeometry.IsArtinianScheme.finite : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsArtinianScheme X], Finite ↥X
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_mono_right : ∀ (b : Ordinal.{u_1}) {x y : Ordinal.{u_1}}, x ≤ y → Ordinal.log b x ≤ Ordinal.log b y
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.Cauchy.commRing : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : CommRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → CommRing (CauSeq.Completion.Cauchy abv)
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`.  -/
MonotoneOn : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Set α → Prop
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsTorsionQuot.mono : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {I J K L : Ideal A},
  F.IsTorsionQuot I K → I ≤ J → L ≤ K → F.IsTorsionQuot J L
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂),
  Std.DTreeMap.Raw.Const.get (m₁ ∪ m₂) k ⋯ = Std.DTreeMap.Raw.Const.get m₂ k mem
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toExtensionHom_comp : ∀ {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' ι') {R'' : Type u_4} {S'' : Type u_5}
  {ι'' : Type u_6} [inst_6 : CommRing R''] [inst_7 : CommRing S''] [inst_8 : Algebra R'' S'']
  (P'' : Algebra.Generators R'' S'' ι'') [inst_9 : Algebra R R'] [inst_10 : Algebra R' R''] [inst_11 : Algebra R' S'']
  [inst_12 : Algebra S S'] [inst_13 : Algebra S' S''] [inst_14 : Algebra S S''] [inst_15 : Algebra R S']
  [inst_16 : IsScalarTower R S S'] [inst_17 : Algebra R R''] [inst_18 : Algebra R S'']
  [inst_19 : IsScalarTower R R'' S''] [inst_20 : IsScalarTower R S S''] [inst_21 : IsScalarTower R' R'' S'']
  [inst_22 : IsScalarTower R' S' S''] [inst_23 : IsScalarTower S S' S''] [inst_24 : IsScalarTower R R' R'']
  [inst_25 : IsScalarTower R R' S'] (f : P'.Hom P'') (g : P.Hom P'),
  (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : NormedField 𝕜] {f : α → E} {l : Filter α}
  {c : 𝕜} {g : α → 𝕜}, c ≠ 0 → ((f =Θ[l] fun x => c * g x) ↔ f =Θ[l] g)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_top_of_ne : ∀ {V : Type u_1} {u v : V}, u ≠ v → ⊤.dist u v = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two antitone functions is antitone.  -/
AntitoneOn.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftMono α] [MulRightMono α], AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x * g x) s
-- Mathlib.CategoryTheory.Limits.Filtered
/-- Class for having all filtered colimits of a given size.  -/
CategoryTheory.Limits.HasFilteredColimitsOfSize : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.map_vadd_zmultiples : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α],
  Function.Periodic f c → ∀ (a : ↥(AddSubgroup.zmultiples c)) (x : α), f (a +ᵥ x) = f x
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Iic : ∀ {n : ℕ} (a : Fin n), Finset.map Fin.valEmbedding (Finset.Iic a) = Finset.Iic ↑a
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.germ_stalkToLocalizationₗ_assoc : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hx : x ∈ U) {Z : ModuleCat R} (h : ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.structurePresheafInModuleCat R M).germ U x hx)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.openToLocalizationₗ✝ R M U x hx) h
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.one_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (x : ↥(Opposite.unop V)),
  ↑1 x = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
/-- A functor `F : J ⥤ C` is well-order-continuous if for any limit element `m : J`,
`F.obj m` identifies to the colimit of the `F.obj j` for `j < m`.  -/
CategoryTheory.Functor.IsWellOrderContinuous : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} → [inst_1 : PartialOrder J] → CategoryTheory.Functor J C → Prop
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S (Turing.TM1.Stmt.move a q) = Turing.TM1.SupportsStmt S q
-- Mathlib.CategoryTheory.Shift.Basic
/-- The monoidal functor from `A` to `C ⥤ C` given a `HasShift` instance.  -/
CategoryTheory.shiftMonoidalFunctor : (C : Type u) →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [CategoryTheory.HasShift C A] → CategoryTheory.Functor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)
-- Mathlib.Data.EReal.Basic
EReal.rec_bot : ∀ {motive : EReal → Sort u_1} (bot : motive ⊥) (coe : (a : ℝ) → motive ↑a) (top : motive ⊤),
  EReal.rec bot coe top ⊥ = bot
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminorm_smul_le : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (a : 𝕜) (x : PiTensorProduct 𝕜 fun i => E i),
  ‖a • x‖ ≤ ‖a‖ * ‖x‖
-- Mathlib.Tactic.Use
/-- When the goal `mvarId` is an inductive datatype with a single constructor,
this applies that constructor, then returns metavariables for the non-parameter explicit arguments
along with metavariables for the parameters and implicit arguments.

The first list of returned metavariables correspond to the arguments that `⟨x,y,...⟩` notation uses.
The second list corresponds to everything else: the parameters and implicit arguments.
The third list consists of those implicit arguments that are instance implicits, which one can
try to synthesize. The third list is a sublist of the second list.

Returns metavariables for all arguments whether or not the metavariables are assigned.
 -/
Mathlib.Tactic.applyTheConstructor : Lean.MVarId → Lean.MetaM (List Lean.MVarId × List Lean.MVarId × List Lean.MVarId)
-- Init.Prelude
/-- The second element of a pair.  -/
MProd.snd : {α β : Type u} → MProd α β → β
-- Init.Data.UInt.Lemmas
UInt8.ofNat_uInt32ToNat : ∀ (n : UInt32), UInt8.ofNat n.toNat = n.toUInt8
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local min on `s` at `a` and `y` belongs to the positive tangent cone
of `s` at `a`, then `0 ≤ f' y`.  -/
IsLocalMinOn.fderivWithin_nonneg : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E},
  IsLocalMinOn f s a → y ∈ posTangentConeAt s a → 0 ≤ (fderivWithin ℝ f s a) y
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.orderedInsert.eq_def : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (x : List α),
  List.orderedInsert r a x =
    match x with
    | [] => [a]
    | b :: l => if r a b then a :: b :: l else b :: List.orderedInsert r a l
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.algHom_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : MvPolynomial σ R →ₐ[R] A) (r : R), f (MvPolynomial.C r) = (algebraMap R A) r
-- Mathlib.Algebra.Quaternion
/-- Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$,
denoted as `ℍ[R,a,b]`.
Implemented as a structure with four fields: `re`, `imI`, `imJ`, and `imK`.  -/
Quaternion.«termℍ[_,_,_]» : Lean.ParserDescr
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.mk.sizeOf_spec : ∀ {α β : Type} [inst : SizeOf α] [inst_1 : SizeOf β] (socket : Option α) (expect : Option ℕ)
  (response : Option (Std.Channel (Except IO.Error (Std.Http.Response β)))) (responseBody : Option β)
  (requestBody : Option Std.Http.Body.Stream) (timeout : Std.Time.Millisecond.Offset)
  (keepAliveTimeout : Option Std.Time.Millisecond.Offset) (headerTimeout : Option Std.Time.Timestamp)
  (connectionContext : Std.CancellationContext),
  sizeOf
      { socket := socket, expect := expect, response := response, responseBody := responseBody,
        requestBody := requestBody, timeout := timeout, keepAliveTimeout := keepAliveTimeout,
        headerTimeout := headerTimeout, connectionContext := connectionContext } =
    1 + sizeOf socket + sizeOf expect + sizeOf response + sizeOf responseBody + sizeOf requestBody + sizeOf timeout +
          sizeOf keepAliveTimeout +
        sizeOf headerTimeout +
      sizeOf connectionContext
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.mk.inj : ∀ {alt : String} {name : Lean.StrLit} {alt_1 : String} {name_1 : Lean.StrLit},
  { alt := alt, name := name } = { alt := alt_1, name := name_1 } → alt = alt_1 ∧ name = name_1
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_mulVec_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n),
  (M.submatrix e₁ ⇑e₂).mulVec v = M.mulVec (v ∘ ⇑e₂.symm) ∘ e₁
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.mk.inj : ∀ {C : Type u_1} {ι : Type u_2} {inst : CategoryTheory.Category.{u_3, u_1} C}
  {inst_1 : CategoryTheory.Category.{u_4, u_2} ι} {inst_2 : CategoryTheory.Abelian C}
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} {hom : (n : ℤ) → X.H n ⟶ X'.H n}
  {comm :
    autoParam
      (∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
          CategoryTheory.CategoryStruct.comp ((hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
            (X'.δ f g n₀ n₁ hn₁))
      CategoryTheory.Abelian.SpectralObject.Hom.comm._autoParam}
  {hom_1 : (n : ℤ) → X.H n ⟶ X'.H n}
  {comm_1 :
    autoParam
      (∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁)
            ((hom_1 n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
          CategoryTheory.CategoryStruct.comp ((hom_1 n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
            (X'.δ f g n₀ n₁ hn₁))
      CategoryTheory.Abelian.SpectralObject.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.range_powSMulQuotInclusion : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) (N : Submodule R M),
  (Submodule.powSMulQuotInclusion I M h N).range = Submodule.map (I ^ c • N).mkQ (I ^ a • N)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the goal has local declarations that have not yet been processed by `grind`.

A local declaration is "pending" if its index is greater than or equal to `nextDeclIdx`.
This is used to determine whether `grind` needs to internalize new hypotheses.
 -/
Lean.Meta.Grind.Goal.hasPendingLocalDecls : Lean.Meta.Grind.Goal → Lean.MetaM Bool
-- Init.Data.SInt.Bitwise
Int64.and_neg_one : ∀ {a : Int64}, a &&& -1 = a
-- Mathlib.Algebra.Order.Group.Synonym
toDual_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.Data.NNReal.Defs
NNReal.half_le_self : ∀ (a : NNReal), a / 2 ≤ a
-- Mathlib.Analysis.RCLike.Basic
/-- A copy of an `RCLike` field in which the `NormedField` field is adjusted to be become defeq
to a propeq one.  -/
RCLike.copy_of_normedField : {𝕜 : Type u_3} → (h : RCLike 𝕜) → (hk : NormedField 𝕜) → hk = h.toNormedField → RCLike 𝕜
-- Mathlib.Analysis.Real.Spectrum
QuasispectrumRestricts.le_nnreal_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A},
  QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ quasispectrum NNReal a, x ≤ r) ↔ ∀ x ∈ quasispectrum ℝ a, x ≤ ↑r
-- Batteries.Data.Range.Lemmas
Std.Legacy.Range.size_stop_le_start : ∀ (r : Std.Legacy.Range), r.stop ≤ r.start → r.size = 0
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q]
  (X : Q.Over ⊤ S) (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.smallPretopology P Q).toGrothendieck X ↔
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
-- Mathlib.Order.Cover
Set.sdiff_singleton_covBy : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → s \ {a} ⋖ s
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.nat_card_ofStabilizer_add_one_eq : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] (a : α),
  Nat.card ↥(SubMulAction.ofStabilizer G a) + 1 = Nat.card α
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.fac' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsHomLift f φ],
  p.map φ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  Std.ExtDHashMap.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.ExtDHashMap.Const.get m a ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.Tactic.NormNum.LegendreSymbol
_private.Mathlib.Tactic.NormNum.LegendreSymbol.0.Mathlib.Meta.NormNum.jacobiSymNat.eq_1 : ∀ (a b : ℕ), Mathlib.Meta.NormNum.jacobiSymNat a b = jacobiSym (↑a) b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The number of infinite real places of the number field `K`.  -/
NumberField.InfinitePlace.nrRealPlaces : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℕ
-- Mathlib.Data.Nat.Count
Nat.count_succ : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p (n + 1) = Nat.count p n + if p n then 1 else 0
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.eq_of_glueDist_eq_zero : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y)
  (ε : ℝ), 0 < ε → ∀ (p q : X ⊕ Y), Metric.glueDist Φ Ψ ε p q = 0 → p = q
-- Mathlib.Analysis.Calculus.Deriv.Basic
fderiv_eq_deriv_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x y : 𝕜}, (fderiv 𝕜 f x) y = deriv f x * y
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The underlying object of `(Monad.comparison R).obj X` is just `R.obj X`.
 -/
CategoryTheory.Monad.comparisonForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → (CategoryTheory.Monad.comparison h).comp h.toMonad.forget ≅ R
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSimple.isAtom_top : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L], IsAtom ⊤
-- Mathlib.Data.Nat.Factorial.NatCast
IsUnit.natCast_of_isNilpotent_of_coprime : ∀ {A : Type u_1} [inst : CommRing A] {n p : ℕ}, IsNilpotent ↑p → p.Coprime n → IsUnit ↑n
-- Mathlib.Analysis.Asymptotics.TVS
/-- Eta-expanded form of `Asymptotics.IsBigOTVS.symm` -/
Asymptotics.IsBigOTVS.fun_symm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (fun i => f₁ i - f₂ i) =O[𝕜; l] g → (fun i => f₂ i - f₁ i) =O[𝕜; l] g
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineToSimplex_edge : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m) (j l : ℕ)
  (hjl : j + l ≤ m),
  (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.intervalEdge j l hjl) ⋯ h).op))
      (sx.spineToSimplex m h f) =
    sx.spineToDiagonal l ⋯ (f.interval j l hjl)
-- Mathlib.Algebra.Order.Module.Defs
le_of_smul_le_smul_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulReflectLE α β], a • b₁ ≤ a • b₂ → 0 < a → b₁ ≤ b₂
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.result : Lean.Meta.SynthInstance.Answer → Lean.Meta.AbstractMVarsResult
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_nat_mul_neg : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M},
  Multipliable f → ∏' (n : ℕ), f ↑n * f (-↑n) = (∏' (n : ℤ), f n) * f 0
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.im_zero : Complex.UnitDisc.im 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
`f` is a strictly monotone function on `D`.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly positive.  -/
strictMonoOn_of_deriv_pos : ∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, 0 < deriv f x) → StrictMonoOn f D
-- Init.Data.Array.Monadic
Array.idRun_mapM : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Id β}, (Array.mapM f xs).run = Array.map (fun x => (f x).run) xs
-- Mathlib.Order.WellFoundedSet
BddBelow.isWF : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α] [LocallyFiniteOrder α], BddBelow s → s.IsWF
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_empty_right_iff : ∀ {s : String.Slice} {p : s.Pos} {t : String}, p.Splits t "" ↔ p = s.endPos ∧ t = s.copy
-- Mathlib.NumberTheory.PrimeCounting
Nat.prime_of_mem_primesBelow : ∀ {p n : ℕ}, p ∈ n.primesBelow → Nat.Prime p
-- Lean.Language.Basic
/-- Pair of (optional) old snapshot task usable for incremental reuse and new snapshot promise for
incremental reporting. Inside the elaborator, we build snapshots by carrying such bundles and then
checking if we can reuse `old?` if set or else redoing the corresponding elaboration step. In either
case, we derive new bundles for nested snapshots, if any, and finally `resolve` `new` to the result.

Note that failing to `resolve` a created promise will block the language server indefinitely!
We use `withAlwaysResolvedPromise`/`withAlwaysResolvedPromises` to ensure this doesn't happen.

In the future, the 1-element history `old?` may be replaced with a global cache indexed by strong
hashes but the promise will still need to be passed through the elaborator.
 -/
Lean.Language.SnapshotBundle : Type → Type
-- Lean.Elab.DocString
/-- More information to show users  -/
Lean.Doc.CodeSuggestion.moreInfo : Lean.Doc.CodeSuggestion → Option String