mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r r' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size)) →
          ((ℓ : Std.DTreeMap.Internal.Impl α β) →
              (hℓ₁ : ℓ.Balanced) →
                (hℓ₂ : ℓ.size = r'.size + r.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
            motive x
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The replacement expression obtained from the rewrite  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.replacementString : Mathlib.Tactic.LibraryRewrite.RewriteInterface → String
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.projective_iff_injective_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C},
  CategoryTheory.Projective P ↔ CategoryTheory.Injective (Opposite.op P)
-- Mathlib.RingTheory.SimpleModule.Basic
/-- The Jacobson density theorem for a module finite over its endomorphism ring.  -/
Module.Finite.toModuleEnd_moduleEnd_surjective : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite (Module.End R M) M], Function.Surjective ⇑(Module.toModuleEnd (Module.End R M) M)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.instMonoidalLinear : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.MonoidalLinear R (ModuleCat R)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.squarefree_of_dvd_prodPrimes : ∀ {s : BoundingSieve} {d : ℕ}, d ∣ s.prodPrimes → Squarefree d
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.mono_of_mono_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsMonomorphisms] {X Y : C} {f : Y ⟶ X},
  CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.conjugatesOfSet_subset_normalClosure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Group.conjugatesOfSet s ⊆ ↑(Subgroup.normalClosure s)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C →
    ∀ (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
      ⊤ ≤
          Submodule.span ℤ
            (Set.range
              (Profinite.NobelingProof.GoodProducts.eval
                (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))) →
        LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.C' C ho)) →
          LinearIndependent (ι := ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) ℤ
            (⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho))) ∘
              Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inr)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.addEntry : Lean.Meta.Grind.ExtensionState → Lean.Meta.Grind.Entry → Lean.Meta.Grind.ExtensionState
-- Mathlib.Data.Int.Order.Basic
/-- **Alias** of the reverse direction of `Int.ofNat_lt`. -/
Int.ofNat_lt_ofNat_of_lt : ∀ {n m : ℕ}, n < m → ↑n < ↑m
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C)
  (X_1 : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj X_1))
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- The abbreviation for `⟦f⟧`.  -/
CategoryTheory.FreeMonoidalCategory.homMk : {C : Type u} → {X Y : CategoryTheory.FreeMonoidalCategory C} → X.Hom Y → (X ⟶ Y)
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Relations.adE.eq_1 : ∀ (R : Type u) {B : Type v} [inst : CommRing R] (CM : Matrix B B ℤ),
  CartanMatrix.Relations.adE R CM =
    Function.uncurry fun i j =>
      ((LieAlgebra.ad R (FreeLieAlgebra R (CartanMatrix.Generators B)))
            ((FreeLieAlgebra.of R ∘ CartanMatrix.Generators.E) i) ^
          (-CM i j).toNat)
        ⁅(FreeLieAlgebra.of R ∘ CartanMatrix.Generators.E) i, (FreeLieAlgebra.of R ∘ CartanMatrix.Generators.E) j⁆
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → m.modify a f = m_1.modify a f_1
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.gcd_eq : ∀ {m a b : ℕ}, a ≡ b [MOD m] → a.gcd m = b.gcd m
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.regular.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.ModObj.regular M = { smul := CategoryTheory.MonObj.mul, one_smul := ⋯, mul_smul := ⋯ }
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.Simps.apply.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (h : α ≃+o β), OrderAddMonoidIso.Simps.apply h = ⇑h
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying monoid homomorphism.  -/
CommMonCat.Hom.hom' : {A B : CommMonCat} → A.Hom B → ↑A →* ↑B
-- Std.Sat.AIG.Basic
/-- Add a new constant node to `aig`. Note that this version is only meant for proving,
for production purposes use `AIG.mkConstCached` and equality theorems to this one.
 -/
Std.Sat.AIG.mkConst : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Bool → Std.Sat.AIG.Entrypoint α
-- Mathlib.Topology.Algebra.Group.Basic
Topology.IsInducing.continuousInv : ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] [ContinuousInv H] {f : G → H},
  Topology.IsInducing f → (∀ (x : G), f x⁻¹ = (f x)⁻¹) → ContinuousInv G
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∉ t → t.get? a = none
-- Init.Data.Range.Polymorphic.Iterators
Std.Roi.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLT α] →
            [Monad m] → [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] → ForIn' m (Std.Roi α) α inferInstance
-- Init.Data.Range.Polymorphic.PRange
/-- A range of elements of `α` with an open lower bound and a closed upper bound.

`a<...=b` is the range of all values greater than `a : α` and less than or equal to
`b : α`. This is notation for `Roc.mk a b`.
 -/
Std.Roc : Type u → Type u
-- Mathlib.Order.Bounded
Set.bounded_gt_inter_ge : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 > x2) (s ∩ {b | b ≤ a}) ↔ Set.Bounded (fun x1 x2 => x1 > x2) s
-- Lean.Elab.Calc
Lean.Elab.Term.CalcStepView.mk : Lean.Syntax → Lean.Term → Lean.Term → Lean.Elab.Term.CalcStepView
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebraFin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [inst_1 : SeminormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [NormOneClass A], ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map.

Monadically computes a value by folding the given function over the mappings in the hash
map in the reverse order used by `foldM`.
 -/
Std.DHashMap.Raw.Internal.foldRevM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} → {m : Type w → Type w'} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DHashMap.Raw α β → m δ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The identity rational map.  -/
AlgebraicGeometry.Scheme.RationalMap.id : (X : AlgebraicGeometry.Scheme) → X.RationalMap X
-- Mathlib.LinearAlgebra.Reflection
Module.reflection_symm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (h : f x = 2), (Module.reflection h).symm = Module.reflection h
-- Mathlib.Order.SuccPred.Limit
/-- Predecessor limits aren't maximal.  -/
Order.IsPredLimit.not_isMax : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Order.IsPredLimit a → ¬IsMax a
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_diag : ∀ (n : ℕ) (i : Fin n), CartanMatrix.D n i i = 2
-- Lean.Server.Completion
_private.Lean.Server.Completion.0.Lean.Server.Completion.filterDuplicateCompletionItems : Array Lean.Lsp.ResolvableCompletionItem → Array Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffOn_piLp' : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {t : Set H}, (∀ (i : ι), ContDiffOn 𝕜 n (fun x => (f x).ofLp i) t) → ContDiffOn 𝕜 n f t
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace.eq_1 : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (A : Matrix n n R),
  A.trace = ∑ i, A.diag i
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `NatModule`. We support them using the envelope `OfNatModule.Q`  -/
Lean.Meta.Grind.Arith.Linear.State.natStructs : Lean.Meta.Grind.Arith.Linear.State → Array Lean.Meta.Grind.Arith.Linear.NatStruct
-- Mathlib.GroupTheory.Focal
/-- Isomorphism theorem: `G / ker(V) ≅ P / P*`.  -/
Subgroup.transferFocal.quotientKerMulEquivQuotientFocalSubroupOf : {G : Type u_1} →
  [inst : Group G] →
    {p : ℕ} →
      [Fact (Nat.Prime p)] →
        (P : Sylow p G) → [inst_2 : (↑P).FiniteIndex] → G ⧸ (↑P).transferFocal.ker ≃* ↥↑P ⧸ (↑P).focalSubgroupOf
-- Mathlib.Analysis.Normed.Ring.Lemmas
antilipschitzWith_mul_right : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [NormMulClass α] {a : α},
  a ≠ 0 → AntilipschitzWith ‖a‖₊⁻¹ fun x => x * a
-- Mathlib.Algebra.Group.Basic
div_mul_cancel_right : ∀ {G : Type u_3} [inst : Group G] (a b : G), a / (b * a) = b⁻¹
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.inScope : String → Lean.MetaM Bool
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_monotone : ∀ {u v : ℕ → EReal}, u ≤ v → LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthInf v
-- Mathlib.Algebra.Quaternion
Quaternion.coe_mul : ∀ {R : Type u_3} [inst : CommRing R] (x y : R), ↑(x * y) = ↑x * ↑y
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- One direction of `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, but where all derivatives are
taken within the same set. Version for partial derivatives / functions with parameters. If `f x` is
a `C^n+1` family of functions and `g x` is a `C^n` family of points, then the derivative of `f x` at
`g x` depends in a `C^n` way on `x`. We give a general version of this fact relative to sets which
may not have unique derivatives, in the following form.  If `f : E × F → G` is `C^n+1` at
`(x₀, g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`,
then there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
sufficiently close to `x₀` within `s ∪ {x₀}` the function `y ↦ f x y` has derivative `f' x` at `g x`
within `t ⊆ F`.  For convenience, we return an explicit set of `x`'s where this holds that is a
subset of `s ∪ {x₀}`.  We need one additional condition, namely that `t` is a neighborhood of
`g(x₀)` within `g '' s`.  -/
ContDiffWithinAt.hasFDerivWithinAt_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} {f : E → F → G} {g : E → F}
  {t : Set F},
  n ≠ ↑⊤ →
    ∀ {x₀ : E},
      ContDiffWithinAt 𝕜 (n + 1) (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀) →
        ContDiffWithinAt 𝕜 n g s x₀ →
          t ∈ nhdsWithin (g x₀) (g '' s) →
            ∃ v ∈ nhdsWithin x₀ (insert x₀ s),
              v ⊆ insert x₀ s ∧
                ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun x => f' x) s x₀
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1NormedRing : {R : Type u_3} →
  {M : Type u_4} →
    [inst : NormedRing R] →
      [inst_1 : NormedAddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] →
            [IsBoundedSMul R M] → [IsBoundedSMul Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → NormedRing (TrivSqZeroExt R M)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.merge.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a₂ : α) (c₂ sibling : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.merge le Batteries.PairingHeapImp.Heap.nil
      (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling) =
    Batteries.PairingHeapImp.Heap.node a₂ c₂ Batteries.PairingHeapImp.Heap.nil
-- Mathlib.Computability.Primrec.List
Primrec.vector_get : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec₂ List.Vector.get
-- ProofWidgets.Util
/-- Delaborate the elements of an array literal separately, calling `elem` on each.  -/
Lean.PrettyPrinter.Delaborator.delabArrayLiteral : {α : Type} → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM (Array α)
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.getArrowArity : Lean.Expr → ℕ
-- Mathlib.Data.Set.Prod
Set.insert_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} (i : ι) (s : Set ι) (t : (i : ι) → Set (α i)),
  (insert i s).pi t = Function.eval i ⁻¹' t i ∩ s.pi t
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- The key step: show that the norm of a suitable function is constant if the norm takes
a positive minimum and condition `H` below is satisfied.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.norm_eq_of_isMinOn_of_forall_le : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] [inst_2 : SeminormedAddCommGroup E]
  {f : X → E} {M : ℝ} {x : X},
  0 < M →
    ‖f x‖ = M →
      IsMinOn (fun x => ‖f x‖) Set.univ x →
        Continuous f →
          (∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)) → ∀ (y : X), ‖f y‖ = M
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b)
  {Z : C} (h : (E.sigmaOfIsColimit hc hd).X b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (d.inj i)
      (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₂ r) h) =
    CategoryTheory.CategoryStruct.comp (E.p₂ i.snd) (CategoryTheory.CategoryStruct.comp (c.inj i.fst.2) h)
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.one_le_unop : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : αᵐᵒᵖ}, 1 ≤ MulOpposite.unop a ↔ 1 ≤ a
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Ico : ∀ (a b : ℝ), Real.exp '' Set.Ico a b = Set.Ico (Real.exp a) (Real.exp b)
-- Mathlib.RingTheory.Valuation.RankOne
ValuativeRel.isRankLeOne_iff_mulArchimedean : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R],
  ValuativeRel.IsRankLeOne R ↔ MulArchimedean (ValuativeRel.ValueGroupWithZero R)
-- Std.Http.Server.Config
/-- Maximum length of reason phrase (default: 512 bytes)
 -/
Std.Http.Config.maxReasonPhraseLength : Std.Http.Config → ℕ
-- Mathlib.Algebra.Group.Units.Equiv
/-- When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`.  -/
AddEquiv.neg : (G : Type u_6) → [inst : SubtractionCommMonoid G] → G ≃+ G
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.mk : {X : SSet} →
  (spineToSimplex : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n })) →
    (∀ (n : ℕ), X.spine n ∘ spineToSimplex = id) → (∀ (n : ℕ), spineToSimplex ∘ X.spine n = id) → X.StrictSegal
-- Lean.Data.Lsp.Extra
/-- `$/lean/plainGoal` client->server request.

If there is a tactic proof at the specified position, returns the current goals.
Otherwise returns `null`.  -/
Lean.Lsp.PlainGoalParams : Type
-- Mathlib.Data.Rat.Floor
Rat.fract_inv_num_lt_num_of_pos : ∀ {q : ℚ}, 0 < q → (Int.fract q⁻¹).num < q.num
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert!_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare ((Std.DTreeMap.Internal.Impl.insert! k v t).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  G.toLocalizationPresheaf.app U = CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U)))
-- Init.Data.SInt.Lemmas
Int8.ne_iff_ofBitVec_ne : ∀ {a b : BitVec 8}, a ≠ b ↔ Int8.ofBitVec a ≠ Int8.ofBitVec b
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_trans_apply : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] {T : Type u_9}
  [inst_10 : CommRing T] [inst_11 : IsDomain T] (M : Type u_10) [inst_12 : CommRing M] [inst_13 : Algebra T M]
  [inst_14 : IsFractionRing T M] (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal (nonZeroDivisors R) K),
  (FractionalIdeal.ringEquivOfRingEquiv K M (f.trans g)) I =
    (FractionalIdeal.ringEquivOfRingEquiv L M g) ((FractionalIdeal.ringEquivOfRingEquiv K L f) I)
-- Mathlib.Data.Nat.ModEq
Nat.right_modEq_add_iff : ∀ {n a b : ℕ}, b ≡ a + b [MOD n] ↔ n ∣ a
-- Mathlib.Order.Minimal
maximalFor_iff_forall_gt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i : ι},
  MaximalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f i < f j → ¬Q j
-- Mathlib.Algebra.Order.Archimedean.Hom
OrderRingHom.eq_id : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α),
  f = OrderRingHom.id α
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instHashableExtTheorem.hash : Lean.Meta.Ext.ExtTheorem → UInt64
-- Init.Data.BitVec.Lemmas
BitVec.append_zero_width : ∀ {w : ℕ} (x : BitVec w) (y : BitVec 0), x ++ y = x
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_filterM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : List α), Lean.Order.monotone f → Lean.Order.monotone fun x => List.filterM (f x) xs
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf : ∀ {X : AlgebraicGeometry.Scheme}, CategoryTheory.Limits.PreservesLimits (AlgebraicGeometry.Scheme.Modules.toPresheaf X)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSolverTerms.default : Lean.Meta.Grind.SolverTerms
-- Lean.Declaration
Lean.Declaration.inductDecl.inj : ∀ {lparams : List Lean.Name} {nparams : ℕ} {types : List Lean.InductiveType} {isUnsafe : Bool}
  {lparams_1 : List Lean.Name} {nparams_1 : ℕ} {types_1 : List Lean.InductiveType} {isUnsafe_1 : Bool},
  Lean.Declaration.inductDecl lparams nparams types isUnsafe =
      Lean.Declaration.inductDecl lparams_1 nparams_1 types_1 isUnsafe_1 →
    lparams = lparams_1 ∧ nparams = nparams_1 ∧ types = types_1 ∧ isUnsafe = isUnsafe_1
-- Init.Data.BitVec.Lemmas
BitVec.neg_add_mul_eq_mul_not : ∀ {w : ℕ} {x y : BitVec w}, -(x + x * y) = x * ~~~y
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.whiskerRight_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B),
  (CategoryTheory.Lax.LaxTrans.whiskerRight Γ ι).as.app a =
    CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Mathlib.Computability.Partrec
/-- Partially recursive partial functions `α → σ` between `Primcodable` types  -/
Partrec : {α : Type u_1} → {σ : Type u_2} → [Primcodable α] → [Primcodable σ] → (α →. σ) → Prop
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.toSpanSingleton_one_eq_algebraLinearMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  LinearMap.toSpanSingleton R A 1 = Algebra.linearMap R A
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} {f g : X ⟶ Y}, f = g ↔ f.1 = g.1 ∧ f.2 = g.2
-- Mathlib.Topology.Constructions
Sigma.discreteTopology : ∀ {ι : Type u_5} {Y : ι → Type v} [inst : (i : ι) → TopologicalSpace (Y i)] [h : ∀ (i : ι), DiscreteTopology (Y i)],
  DiscreteTopology (Sigma Y)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mk.injEq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (map : Polynomial R →ₐ[R] S) (map_surjective : Function.Surjective ⇑map) (ker_map : RingHom.ker map = Ideal.span {f})
  (map_1 : Polynomial R →ₐ[R] S) (map_surjective_1 : Function.Surjective ⇑map_1)
  (ker_map_1 : RingHom.ker map_1 = Ideal.span {f}),
  ({ map := map, map_surjective := map_surjective, ker_map := ker_map } =
      { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 }) =
    (map = map_1)
-- Mathlib.Control.LawfulFix
/-- `Sigma.uncurry` as a monotone function.  -/
Pi.monotoneUncurry : (α : Type u_1) →
  (β : α → Type u_2) →
    (γ : (a : α) → β a → Type u_3) →
      [inst : (x : α) → (y : β x) → Preorder (γ x y)] →
        ((a : α) → (b : β a) → γ a b) →o (x : (a : α) × β a) → γ x.fst x.snd
-- Init.Data.Int.Basic
Int.ofNat_two : ↑2 = 2
-- Init.Data.UInt.BasicAux
/-- Converts an 8-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.toNat : UInt8 → ℕ