mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.MahlerMeasure
/-- The Mahler measure of a cyclotomic polynomial is 1.  -/
Polynomial.cyclotomic_mahlerMeasure_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℂ] (n : ℕ),
  (Polynomial.map (algebraMap R ℂ) (Polynomial.cyclotomic n R)).mahlerMeasure = 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_radical : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I ≤ I.radical
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`
provided that `g` is injective.  -/
finsum_mem_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → α},
  Function.Injective g → ∑ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∑ᶠ (j : β), f (g j)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The nonsingular inverse is the same as `invOf` when `A` is invertible.  -/
Matrix.invOf_eq_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A], ⅟A = A⁻¹
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMapClass.instCoeTCCompactlySupportedContinuousMap : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : Zero β] →
          [inst_2 : TopologicalSpace β] →
            [inst_3 : FunLike F α β] →
              [CompactlySupportedContinuousMapClass F α β] → CoeTC F (CompactlySupportedContinuousMap α β)
-- Mathlib.Logic.Basic
dite_prop_iff_or : ∀ {P : Prop} [inst : Decidable P] {Q : P → Prop} {R : ¬P → Prop}, dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
-- Mathlib.Algebra.Ring.GeomSum
dvd_pow_pow_sub_self_of_dvd : ∀ {R : Type u_1} [inst : Ring R] {r : R} {p a b : ℕ}, a ∣ b → r ^ p ^ a - r ∣ r ^ p ^ b - r
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_zero_iff_subsingleton : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M], Module.rankAtStalk M = 0 ↔ Subsingleton M
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points of a set `t` to `s`, then the value of `g` at the average value of `f` over `t` is
less than or equal to the average value of `g ∘ f` over `t` provided that both `f` and `g ∘ f` are
integrable.  -/
ConvexOn.set_average_mem_epigraph : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
  ConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        μ t ≠ 0 →
          μ t ≠ ⊤ →
            (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
              MeasureTheory.IntegrableOn f t μ →
                MeasureTheory.IntegrableOn (g ∘ f) t μ →
                  (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
-- Mathlib.Computability.ContextFreeGrammar
/-- Rule `r` rewrites string `u` is to string `v` iff they share both a prefix `p` and postfix `q`
such that the remaining middle part of `u` is the input of `r` and the remaining middle part
of `u` is the output of `r`.  -/
ContextFreeRule.rewrites_iff : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v ↔ ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The continuous linear equivalence induced by a linear equivalence on a finite-dimensional
space.  -/
LinearEquiv.toContinuousLinearEquiv : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F : Type w} →
                  [inst_5 : AddCommGroup F] →
                    [inst_6 : Module 𝕜 F] →
                      [inst_7 : TopologicalSpace F] →
                        [IsTopologicalAddGroup F] →
                          [ContinuousSMul 𝕜 F] →
                            [CompleteSpace 𝕜] →
                              [T2Space E] → [T2Space F] → [FiniteDimensional 𝕜 E] → (E ≃ₗ[𝕜] F) → E ≃L[𝕜] F
-- Mathlib.Order.Defs.Unbundled
LowerSet.mk : {α : Type u_1} → [inst : LE α] → (carrier : Set α) → IsLowerSet carrier → LowerSet α
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instAndThenSimproc : AndThen Lean.Meta.Simp.Simproc
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- This result only holds for `DivisionSemiring`s instead of `GroupWithZero`s because zeta takes
values in ℕ, and hence the coercion requires an `AddMonoidWithOne`. TODO: Generalise zeta  -/
ArithmeticFunction.pdiv_zeta : ∀ {R : Type u_1} [inst : DivisionSemiring R] (f : ArithmeticFunction R), f.pdiv ↑ArithmeticFunction.zeta = f
-- Mathlib.Algebra.Order.SuccPred
antitone_of_le_sub_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f a ≤ f (a - 1)) → Antitone f
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.compl_mem_ae_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, sᶜ ∈ MeasureTheory.ae μ ↔ μ s = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A pseudometric space is second countable if, for every `ε > 0`, there is a countable set which
is `ε`-dense.  -/
Metric.secondCountable_of_almost_dense_set : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε) → SecondCountableTopology α
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.instCommMonoidWithZeroSubtypeMemSubmonoidMrange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : MulZeroOneClass G] →
      [inst_1 : CommMonoidWithZero H] → (f : G →*₀ H) → CommMonoidWithZero ↥(MonoidHom.mrange f)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.ker_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), (↑p.subtypeL).ker = ⊥
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_empty_iff : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → Set α}, ⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsIntegralNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.IsIntegral X],
  AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Scheme.Hom.normalization f)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans X Y)
  (θ : CategoryTheory.Oplax.OplaxTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Init.Data.String.Lemmas.Order
String.Pos.get_eq_get_ofSliceTo : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} {h : pos ≠ (s.sliceTo p₀).endPos},
  pos.get h = (String.Pos.ofSliceTo pos).get ⋯
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_sdiff_add_mk : ∀ {α : Type u} {S T : Set α}, T ⊆ S → Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T = Cardinal.mk ↑S
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.instInnerFibrationAppPreOfMonoOfQuasicategory : ∀ {A B : SSet} (i : A ⟶ B) [CategoryTheory.Mono i] (X : SSet) [X.Quasicategory],
  SSet.InnerFibration ((CategoryTheory.MonoidalClosed.pre i).app X)
-- Batteries.Data.List.Lemmas
List.insertP.loop.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (a : α) (a_1 : List α) (b : α) (l : List α),
  List.insertP.loop p a (b :: l) a_1 =
    bif p b then (a :: a_1).reverseAux (b :: l) else List.insertP.loop p a l (b :: a_1)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
Order.Coframe.sdiff_le_iff : ∀ {α : Type u_1} [self : Order.Coframe α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.coe_indicatorConst : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E),
  ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c) = MeasureTheory.indicatorConstLp p hs hμs c
-- Init.Data.Stream
Std.instStreamRangeNat : Std.Stream Std.Legacy.Range ℕ
-- Mathlib.RingTheory.PicardGroup
/-- A flat `R`-module as a `R`-submodule of a faithful `R`-algebra.  -/
Module.Flat.submoduleAlgebra : {R : Type u} →
  {M : Type v} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → (TensorProduct R A M ≃ₗ[A] A) → Submodule R A
-- Lean.Server.Snapshots
/-- What Lean knows about the world after the header and each command.  -/
Lean.Server.Snapshots.Snapshot : Type
-- Lean.Data.Options
Lean.OptionDecl.name : Lean.OptionDecl → Lean.Name
-- Init.Data.Vector.Lemmas
Vector.ne_of_not_mem_push : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, a ∉ xs.push b → a ≠ b
-- Mathlib.Analysis.ODE.PicardLindelof
/-- A time-dependent bound on the distance between the `n`-th iterates of `next` on two curves  -/
ODE.FunSpace.dist_iterate_next_apply_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α β : ODE.FunSpace t₀ x₀ r L) (n : ℕ) (t : ↑(Set.Icc tmin tmax)),
  dist (((ODE.FunSpace.next hf hx)^[n] α).toFun t) (((ODE.FunSpace.next hf hx)^[n] β).toFun t) ≤
    (↑K * |↑t - ↑t₀|) ^ n / ↑n.factorial * dist α β
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.PanelWidgetProps.mk.sizeOf_spec : ∀ (pos : Lean.Lsp.Position) (goals : Array Lean.Widget.InteractiveGoal)
  (termGoal? : Option Lean.Widget.InteractiveTermGoal) (selectedLocations : Array Lean.SubExpr.GoalsLocation),
  sizeOf { pos := pos, goals := goals, termGoal? := termGoal?, selectedLocations := selectedLocations } =
    1 + sizeOf pos + sizeOf goals + sizeOf termGoal? + sizeOf selectedLocations
-- Batteries.Tactic.GeneralizeProofs
/-- Configuration for the `generalize_proofs` tactic.
 -/
Batteries.Tactic.GeneralizeProofs.Config : Type
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.sUnion : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsRelUpperSet s P) → IsRelUpperSet (⋃₀ S) P
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (f : E [⋀^ι]→L[𝕜] F) (s : Set (ι → E)) (x : ι → E),
  HasFDerivWithinAt (⇑f) (f.linearDeriv x) s x
-- Mathlib.Analysis.LConvolution
/-- Convolution of the zero function with a function returns the zero function.  -/
MeasureTheory.zero_lconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Add G] [inst_1 : Neg G] (f : G → ENNReal)
  (μ : MeasureTheory.Measure G), MeasureTheory.lconvolution 0 f μ = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} {fallback : α},
  t.Ordered → t.getKeyD k fallback = Std.Internal.List.getKeyD k t.toListModel fallback
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f f_1 : R →+* P) (e_f : f = f_1) (hIJ : I = Ideal.comap f J),
  Localization.localRingHom I J f hIJ = Localization.localRingHom I J f_1 ⋯
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.ccosh : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.cosh (f x)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_functor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapIso i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp i.inv X.hom
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
AddSubgroup.instIsAddCyclicOfDiscreteTopology : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] [DiscreteTopology G], IsAddCyclic G
-- Mathlib.Data.Fin.Rev
Fin.add_rev_cast : ∀ {n : ℕ} (j : Fin (n + 1)), ↑j + ↑j.rev = n
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.restore : Lean.Elab.Tactic.Grind.SavedState → optParam Bool false → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Data.Set.Image
Set.preimage_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_ofObjects_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {I : Type u_1} (X : I → C) (Y : C),
  CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.ofObjects X Y) ≤
    CategoryTheory.Sieve.ofObjects (F.obj ∘ X) (F.obj Y)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft.toMonadHorizontalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft m] → Mathlib.Tactic.BicategoryLike.MonadHorizontalComp m
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.mk.inj : ∀ {ctxInfo : Lean.Elab.ContextInfo} {tacticInfo : Lean.Elab.TacticInfo} {useAfter indented : Bool} {priority : ℕ}
  {ctxInfo_1 : Lean.Elab.ContextInfo} {tacticInfo_1 : Lean.Elab.TacticInfo} {useAfter_1 indented_1 : Bool}
  {priority_1 : ℕ},
  { ctxInfo := ctxInfo, tacticInfo := tacticInfo, useAfter := useAfter, indented := indented, priority := priority } =
      { ctxInfo := ctxInfo_1, tacticInfo := tacticInfo_1, useAfter := useAfter_1, indented := indented_1,
        priority := priority_1 } →
    ctxInfo = ctxInfo_1 ∧
      tacticInfo = tacticInfo_1 ∧ useAfter = useAfter_1 ∧ indented = indented_1 ∧ priority = priority_1
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- A `R`-bialgebra homomorphism from `A[M]` is uniquely defined by its
values on the functions `single m 1` and `single 1 a`.

See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of `MonoidHom`s because `of` doesn't additivise.  -/
MonoidAlgebra.bialgHom_ext : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : Monoid M]
  ⦃φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B⦄,
  (∀ (m : M), φ₁ (MonoidAlgebra.single m 1) = φ₂ (MonoidAlgebra.single m 1)) →
    (↑φ₁).comp MonoidAlgebra.singleOneAlgHom = (↑φ₂).comp MonoidAlgebra.singleOneAlgHom → φ₁ = φ₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.var.inj : ∀ {w idx idx_1 : ℕ}, Std.Tactic.BVDecide.BVExpr.var idx = Std.Tactic.BVDecide.BVExpr.var idx_1 → idx = idx_1
-- Init.Data.Nat.Basic
Nat.mul_lt_mul_of_pos_left : ∀ {n m k : ℕ}, n < m → k > 0 → k * n < k * m
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_iff : ∀ {u : ℤ}, IsUnit u ↔ u = 1 ∨ u = -1
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.trans_apply : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R), (e₁.trans e₂) a = e₂ (e₁ a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.lt : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelMonoid α] → {s : Submonoid α} → LT (Localization s)
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : LinearOrderedCommGroupWithZero B] {f : A →*₀ B}
  (a : f.ValueGroup₀ˣ), MonoidWithZeroHom.ValueGroup₀.embedding ↑a ≠ 0
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.idem : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ (i : I), IsIdempotentElem (e i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_sigmaOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c),
  (E.sigmaOfIsColimit hc).presieve₀ =
    CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csSup_Iic : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {a : α}, sSup (Set.Iic a) = a
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.cochainComplexXIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) (n : ℤ) (k : ℕ)
  (h : ↑k = n), R.cochainComplexXIso n k h = R.cochainComplexXIso n k h
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.Mapping.mk.inj : ∀ {toNormal toSpecial toNormal_1 toSpecial_1 : Std.HashMap Char Char},
  { toNormal := toNormal, toSpecial := toSpecial } = { toNormal := toNormal_1, toSpecial := toSpecial_1 } →
    toNormal = toNormal_1 ∧ toSpecial = toSpecial_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- *Commandino's theorem* : For n-simplex, the vector from a vertex to the `centroid`
equals `n` times the vector from the `centroid` to the corresponding `faceOppositeCentroid`.  -/
Affine.Simplex.point_vsub_centroid_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i -ᵥ s.centroid = ↑n • (s.centroid -ᵥ s.faceOppositeCentroid i)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.counit_naturality_assoc : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.map f) (CategoryTheory.CategoryStruct.comp (T.ε.app Y) h) =
    CategoryTheory.CategoryStruct.comp (T.ε.app X) (CategoryTheory.CategoryStruct.comp f h)
-- Std.Internal.UV.System
/-- Returns the constrained memory limit in bytes.
 -/
Std.Internal.UV.System.constrainedMemory : IO UInt64
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.ballAddSubgroup_strictAnti : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  StrictAnti FiniteArchimedeanClass.ballAddSubgroup
-- Init.Data.Nat.Basic
Nat.not_lt_of_ge : ∀ {a b : ℕ}, b ≥ a → ¬b < a
-- Mathlib.Computability.Reduce
/-- `p` is many-one reducible to `q` if there is a computable function translating questions about `p`
to questions about `q`.
 -/
«term_≤₀_» : Lean.TrailingParserDescr
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseZoneName : (Std.Time.ZoneName → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.Topology.Algebra.InfiniteSum.Group
cauchySeq_finset_iff_tsum_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α},
  (CauchySeq fun s => ∑ b ∈ s, f b) ↔ ∀ e ∈ nhds 0, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.map_comp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} {G'' : ι → Type u_6}
  [inst_7 : (i : ι) → AddCommMonoid (G'' i)] [inst_8 : (i : ι) → Module R (G'' i)]
  {f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j} (g₁ : (i : ι) → G i →ₗ[R] G' i) (g₂ : (i : ι) → G' i →ₗ[R] G'' i)
  (hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i)
  (hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i),
  Module.DirectLimit.map g₂ hg₂ ∘ₗ Module.DirectLimit.map g₁ hg₁ = Module.DirectLimit.map (fun i => g₂ i ∘ₗ g₁ i) ⋯
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieAddGroup I' n G] (f g : ContMDiffMap I I' N G n), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map_X : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.map Polynomial.X = h.root
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.coe_pos : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β] [inst_1 : Zero β] {f : α → β},
  0 < ↑f ↔ ∀ᶠ (x : α) in ↑φ, 0 < f x
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.success.inj : ∀ {α : Type} {response response_1 : α},
  Lean.Server.ServerRequestResponse.success response = Lean.Server.ServerRequestResponse.success response_1 →
    response = response_1
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
inverse_mfderiv_mul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I (minSmoothness 𝕜 3) G]
  {g h : G}, ((mfderiv% fun b => g * b) h).inverse = (mfderiv% fun b => g⁻¹ * b) (g * h)
-- Mathlib.Data.Complex.Basic
Complex.add_re : ∀ (z w : ℂ), (z + w).re = z.re + w.re