mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.OrderClosed
closure_lt_subset_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → closure {b | f b < g b} ⊆ {b | f b ≤ g b}
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.commute_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) {a : R} {n : σ →₀ ℕ},
  Commute φ ((MvPowerSeries.monomial n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((MvPowerSeries.coeff m) φ) a
-- Lean.Parser.Term
Lean.Parser.Term.trailing_parser.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Implementation of `betaThroughLet`  -/
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux : Lean.Expr → List Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfMinpoly_symm : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h : minpoly A pb.gen = minpoly A pb'.gen), (pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.neg_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂), (-f).hom₁ = -f.hom₁
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation_1 : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [h : MeasureTheory.IsFiniteMeasure ν.variation], μ.HasProd ν B
-- Aesop.Index.RulePattern
_private.Aesop.Index.RulePattern.0.Aesop.RulePatternIndex.getCore.getSubexpr : Aesop.RulePatternIndex →
  Lean.Expr → StateRefT' IO.RealWorld (Array (Aesop.RuleName × Aesop.Substitution)) Aesop.BaseM Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeNF.of_j_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R} [W.IsCharThreeJNeZeroNF], W.IsCharThreeNF
-- Batteries.Lean.Meta.Basic
/-- `saturate1 goal tac` runs `tac` on `goal`, then on the resulting goals, etc.,
until `tac` does not apply to any goal any more (i.e. it returns `none`). The
order of applications is depth-first, so if `tac` generates goals `[g₁, g₂, ⋯]`,
we apply `tac` to `g₁` and recursively to all its subgoals before visiting `g₂`.
If `tac` does not apply to `goal`, `saturate1` returns `none`. Otherwise it
returns the generated subgoals to which `tac` did not apply. `saturate1`
respects the `MonadRecDepth` recursion limit.
 -/
Lean.Meta.saturate1 : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadRecDepth m] →
        [MonadLiftT (ST IO.RealWorld) m] →
          Lean.MVarId → (Lean.MVarId → m (Option (Array Lean.MVarId))) → m (Option (Array Lean.MVarId))
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.Localization.isoOfHom.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f),
  CategoryTheory.Localization.isoOfHom L W f hf = CategoryTheory.asIso (L.map f)
-- Mathlib.Tactic.TFAE
/-- Construct a name for a hypothesis introduced by `tfae_have`.  -/
Mathlib.Tactic.TFAE.mkTFAEId : Lean.TSyntax `Mathlib.Tactic.TFAE.Parser.tfaeType → Lean.MacroM Lean.Name
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.coneΓ_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (F : CategoryTheory.Sheaf J A) (U : Cᵒᵖ),
  F.coneΓ.π.app U = F.ΓRes U
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getLetDeclVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toSpanSingletonCLE_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousSMul 𝕜 E] (f : 𝕜 →L[𝕜] E),
  ContinuousLinearMap.toSpanSingletonCLE.symm f = f 1
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.BifibrantObject.homRel C f g →
    HomotopicalAlgebra.BifibrantObject.toHoCat.map f = HomotopicalAlgebra.BifibrantObject.toHoCat.map g
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.level_mem_conductorSet : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), n ∈ χ.conductorSet
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.coe_recolorOfEmbedding : ∀ {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} (f : α ↪ β),
  ⇑(G.recolorOfEmbedding f) = (SimpleGraph.Embedding.completeGraph f).toHom.comp
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, ∅.size = 0
-- Mathlib.GroupTheory.GroupAction.Hom
instAddActionSemiHomClassAddActionHom : ∀ {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [inst : VAdd M X] (Y : Type u_6) [inst_1 : VAdd N Y],
  AddActionSemiHomClass (X →ₑ[φ] Y) φ X Y
-- Lean.Parser.Command
Lean.Parser.Command.section.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Command
Lean.Parser.Command.initialize.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Util.FormatTable
instBEqAlignment.beq : Alignment → Alignment → Bool
-- Mathlib.Computability.Language
Language.instInhabited : {α : Type u_1} → Inhabited (Language α)
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.instInvolutiveNeg : {α : Type u} → [InvolutiveNeg α] → InvolutiveNeg (WithZero α)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `f` has a formal power series at x bounded by `1`, then `f` is constant equal
to `f x` in a neighborhood of `x`.  -/
HasFiniteFPowerSeriesAt.eventually_const_of_bound_one : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFiniteFPowerSeriesAt f pf x 1 → f =ᶠ[nhds x] fun x_1 => f x
-- Mathlib.Order.Interval.Set.OrdConnectedLinear
Set.ordConnected_iff_disjoint_Ioo_empty : ∀ {α : Type u_1} {I : Set α} [inst : LinearOrder α] [LocallyFiniteOrder α],
  I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Set.Ioo x y) I → Set.Ioo x y = ∅
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- The 1-dimensional derivative on Schwartz space as a continuous `𝕜`-linear map.  -/
SchwartzMap.derivCLM : (𝕜 : Type u_2) →
  (F : Type u_8) →
    [inst : NormedAddCommGroup F] →
      [inst_1 : NormedSpace ℝ F] →
        [inst_2 : RCLike 𝕜] → [inst_3 : NormedSpace 𝕜 F] → SchwartzMap ℝ F →L[𝕜] SchwartzMap ℝ F
-- Mathlib.Algebra.Group.Embedding
addLeftEmbedding_apply : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (g h : G), (addLeftEmbedding g) h = g + h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl =
    (compare k a == Ordering.eq || Std.DTreeMap.Internal.Impl.contains a t)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} [inst_2 : SizeOf J] [inst_3 : SizeOf C]
  (hom : A.pt ⟶ B.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j)
      CategoryTheory.Limits.ConeMorphism.w._autoParam),
  sizeOf { hom := hom, w := w } = 1 + sizeOf hom
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, m.getD a fallback = m[a]?.getD fallback
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRicSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRicSlice._auto_1) →
      Std.Ric.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RicSlice α β)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective.  -/
CategoryTheory.Functor.Full : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Lean.Meta.Tactic.Grind.AC.DenoteExpr
Lean.Grind.AC.Expr.denoteExpr : {M : Type → Type} → [Monad M] → [Lean.Meta.Grind.AC.MonadGetStruct M] → Lean.Grind.AC.Expr → M Lean.Expr
-- Mathlib.Data.Finsupp.SMul
Finsupp.distribMulActionHom_ext : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [inst : Monoid R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {f g : (α →₀ M) →+[R] N},
  (∀ (a : α) (m : M), (f fun₀ | a => m) = g fun₀ | a => m) → f = g
-- Mathlib.Data.List.Cycle
Cycle.Nontrivial.eq_1 : ∀ {α : Type u_1} (s : Cycle α), s.Nontrivial = ∃ x y, x ≠ y ∧ x ∈ s ∧ y ∈ s
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.l_csSup_of_directedOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α},
  GaloisConnection l u →
    ∀ {s : Set α}, DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → l (sSup s) = sSup (l '' s)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddRightCancelMonoid : {α : Type u_1} → [AddLeftCancelMonoid α] → AddRightCancelMonoid αᵃᵒᵖ
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addCommGroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddCommGroup β],
  e.addCommGroup = Function.Injective.addCommGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addEquivOfAddOrderOfEq_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g')
  (h : addOrderOf g = addOrderOf g'), (addEquivOfAddOrderOfEq hg hg' h) g = g'
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_map_toProd_iff_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((k, v) ∈ List.map (fun x => (x.fst, x.snd)) l ↔ Std.Internal.List.getValue? k l = some v)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom
        (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit) φ)
      (CategoryTheory.GradedObject.Monoidal.leftUnitor X').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X).hom φ
-- Mathlib.Algebra.Ring.Defs
Ring.mk : {R : Type u} →
  [toSemiring : Semiring R] →
    [toNeg : Neg R] →
      [toSub : Sub R] →
        [toZSMul : ZSMul R] →
          autoParam (∀ (a b : R), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam →
            autoParam (∀ (a : R), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a) SubNegMonoid.zsmul_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)) SubNegMonoid.zsmul_neg'._autoParam →
                  (∀ (a : R), -a + a = 0) →
                    [toIntCast : IntCast R] →
                      autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) AddGroupWithOne.intCast_ofNat._autoParam →
                        autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                            AddGroupWithOne.intCast_negSucc._autoParam →
                          Ring R
-- Init.Internal.Order.Basic
Lean.Order.csup_conj : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] (c P : α → Prop) (hchain : Lean.Order.chain c),
  (∀ (x : α), c x → ∃ y, c y ∧ Lean.Order.PartialOrder.rel x y ∧ P y) →
    Lean.Order.CCPO.csup hchain = Lean.Order.CCPO.csup ⋯
-- Mathlib.Algebra.GroupWithZero.Action.Units
inv_smul_eq_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ {x y : β}, a⁻¹ • x = y ↔ x = a • y
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_pow_eq_top' : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ}, I ⊔ J = ⊤ → I ⊔ J ^ n = ⊤
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.instMeasurableSub₂ : MeasurableSub₂ ENNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.instNonsingularToSSet : ∀ {X : SSet} (A : X.Subcomplex) [X.Nonsingular], A.toSSet.Nonsingular
-- Mathlib.Algebra.Order.Ring.Abs
abs_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α], |1| = 1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNNRatCast : {Γ : Type u_1} →
  {R : Type u_3} → [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [NNRatCast R] → NNRatCast (HahnSeries Γ R)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- A version of `relNorm_algebraMap` involving a tower of algebras `S/R/R'`.  -/
Ideal.relNorm_algebraMap' : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] (S : Type u_3) [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {R' : Type u_4}
  [inst_11 : CommRing R'] (I : Ideal R') [inst_12 : Algebra R' R] [inst_13 : Algebra R' S] [IsScalarTower R' R S],
  (Ideal.relNorm R) (Ideal.map (algebraMap R' S) I) = Ideal.map (algebraMap R' R) I ^ Module.finrank R S
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} {Y X : CategoryTheory.Limits.Cone F.leftOp} (f : Y ⟶ X),
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_nnratCast : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (q : ℚ≥0), ↑↑q = ↑q
-- Std.Http.Data.Body.Empty
Std.Http.Body.instCoeEmptyAny : Coe Std.Http.Body.Empty Std.Http.Body.Any
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.rpcProvider? : Lean.Lsp.LeanServerCapabilities → Option Lean.Lsp.RpcOptions
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.ext : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, (∀ (x : P), x ∈ I ↔ x ∈ J) → I = J
-- Mathlib.Algebra.Order.Module.Defs
OrderIso.smulRight_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β),
  (OrderIso.smulRight ha) b = a • b
-- Mathlib.NumberTheory.FrobeniusNumber
/-- A natural number `n` is the **Frobenius number** of a set of natural numbers `s` if it is an
upper bound on the complement of the additive submonoid generated by `s`.
In other words, it is the largest number that cannot be expressed as a sum of numbers in `s`.  -/
FrobeniusNumber : ℕ → Set ℕ → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pos_of_pos_of_lt_pi_div_two : ∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → 0 < Real.tan x
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.nilpotencyLength_eq_succ_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] (k : ℕ),
  LieModule.nilpotencyLength L M = k + 1 ↔
    LieModule.lowerCentralSeries R L M (k + 1) = ⊥ ∧ LieModule.lowerCentralSeries R L M k ≠ ⊥
-- Batteries.Data.UInt
UInt64.toUInt16_toNat : ∀ (x : UInt64), x.toUInt16.toNat = x.toNat % 2 ^ 16
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.instToStringExprDiff : ToString Lean.Widget.ExprDiff✝
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A coercion from morphisms to functions on pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.homToFun : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {P Q : C} →
        CoeFun (P ⟶ Q) fun x => CategoryTheory.Abelian.Pseudoelement P → CategoryTheory.Abelian.Pseudoelement Q
-- Init.Data.Option.Lemmas
Option.none_beq_none : ∀ {α : Type u_1} [inst : BEq α], (none == none) = true
-- Mathlib.Order.SupClosed
InfClosed.sInf_mem_of_nonempty : ∀ {α : Type u_3} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  InfClosed s → t.Finite → t.Nonempty → t ⊆ s → sInf t ∈ s
-- Init.Data.Nat.Div.Lemmas
Nat.lt_div_mul_self : ∀ {k x : ℕ}, 0 < k → k ≤ x → x - k < x / k * k
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyBefore.injEq : ∀ {s : String.Slice} (pos pos_1 : s.Pos),
  (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos =
      String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos_1) =
    (pos = pos_1)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- `CategoryStruct` on `B ⥤ᵖ C` where the (1-)morphisms are given by strong
transformations.  -/
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₂) v₁) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.Pseudofunctor B C)
-- Std.Internal.Do.Triple.Basic
/-- Hoare triple notation with a binder for the return value and an exception postcondition.  -/
Std.Internal.Do.tripleBinderEPost : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ((↑m).isEmpty = true ↔ ∀ (a : α), m.contains a = false)
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F} {x : E},
  AnalyticAt 𝕜 (fun x => v) x
-- Lean.LocalContext
Lean.LocalDecl.cdecl.injEq : ∀ (index : ℕ) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo)
  (kind : Lean.LocalDeclKind) (index_1 : ℕ) (fvarId_1 : Lean.FVarId) (userName_1 : Lean.Name) (type_1 : Lean.Expr)
  (bi_1 : Lean.BinderInfo) (kind_1 : Lean.LocalDeclKind),
  (Lean.LocalDecl.cdecl index fvarId userName type bi kind =
      Lean.LocalDecl.cdecl index_1 fvarId_1 userName_1 type_1 bi_1 kind_1) =
    (index = index_1 ∧ fvarId = fvarId_1 ∧ userName = userName_1 ∧ type = type_1 ∧ bi = bi_1 ∧ kind = kind_1)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, ¬x ≤ᵥ y ↔ y <ᵥ x
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- The real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`.  -/
Real.log : ℝ → ℝ
-- Std.Net.Addr
Std.Net.SocketAddress.v4.sizeOf_spec : ∀ (addr : Std.Net.SocketAddressV4), sizeOf (Std.Net.SocketAddress.v4 addr) = 1 + sizeOf addr
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f f_1 : M →ₛₗ[τ₁₂] M₂) (e_f : f = f_1) (h : p ≤ Submodule.comap f q),
  p.mapQ q f h = p.mapQ q f_1 ⋯
-- Mathlib.Topology.Sion
/-- The minimax theorem, in the saddle point form  -/
Sion.exists_isSaddlePointOn : ∀ {E : Type u_1} {F : Type u_2} {X : Set E} {Y : Set F} {f : E → F → ℝ} [inst : TopologicalSpace E]
  [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  X.Nonempty →
    Convex ℝ X →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
            ∀ [inst : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : Module ℝ F] [IsTopologicalAddGroup F]
              [ContinuousSMul ℝ F],
              Convex ℝ Y →
                Y.Nonempty →
                  IsCompact Y →
                    (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                      (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) → ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
-- Mathlib.Algebra.Lie.Basic
LieRing.toBracket : {L : Type v} → [self : LieRing L] → Bracket L L
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax right unity.  -/
CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X)) h)