mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filterMap_equiv_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ},
  Std.ExtHashMap.filterMap (fun k v => some (f k v)) m = Std.ExtHashMap.map f m
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.siftedSum.eq_1 : ∀ {s : BoundingSieve}, BoundingSieve.siftedSum = ∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0
-- Mathlib.Combinatorics.Graph.Basic
/-- An edge is incident with at most one pair of vertices.  -/
Graph.eq_or_eq_of_isLink_of_isLink : ∀ {α : Type u_3} {β : Type u_4} (self : Graph α β) ⦃e : β⦄ ⦃x y v w : α⦄,
  self.IsLink e x y → self.IsLink e v w → x = v ∨ x = w
-- Init.Data.Int.Compare
Int.isLE_compare : ∀ {a b : ℤ}, (compare a b).isLE = true ↔ a ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackFstFstIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  [inst_2 : CategoryTheory.Mono i₃],
  (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
        (CategoryTheory.Limits.pullback.fst f g) ⋯)
      (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
        (CategoryTheory.Limits.pullback.snd f g) ⋯)
      ⋯
-- Mathlib.GroupTheory.Congruence.Basic
Con.comapQuotientEquivOfSurj.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (c : Con M) (f : N →* M)
  (hf : Function.Surjective ⇑f),
  c.comapQuotientEquivOfSurj f hf =
    (Con.congr (MulEquiv.refl N) ⋯).trans (Con.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_ne_zero_iff : ∀ {θ : Real.Angle}, θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  m.isEmpty = true → m.get? a = none
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.dual_isColoop_iff_isLoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M✶.IsColoop e ↔ M.IsLoop e
-- Lean.DocString.Parser
Lean.Doc.Parser.instBEqOrderedListType : BEq Lean.Doc.Parser.OrderedListType
-- Mathlib.Data.Set.Defs
Set.ext : ∀ {α : Type u} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
-- Mathlib.Data.FunLike.Module
/-- A `FunLike` type with scalar multiplication that satisfies `(m • f) x = m • f x`
is a `MulAction` if `β` is a `MulAction`.  -/
FunLike.mulAction : {M : Type u_1} →
  {F : Type u_3} →
    {α : Type u_4} →
      {β : Type u_5} →
        [i : FunLike F α β] →
          [inst : SMul M F] → [inst_1 : Monoid M] → [inst_2 : MulAction M β] → [IsSMulApply M F α β] → MulAction M F
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.lintegral_lt_top_of_nnreal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X NNReal), ∫⁻ (x : X), ↑(f x) ∂μ < ⊤
-- Std.Http.Data.URI
/-- Creates an origin-form request target from a path string.
The path should start with '/' (e.g., "/api/users" or "/search?q=test").
Panics if the string is not a valid origin-form request target.
 -/
Std.Http.RequestTarget.originForm! : String → Std.Http.RequestTarget
-- Mathlib.Topology.Order
nhds_sInf : ∀ {α : Type u} {s : Set (TopologicalSpace α)} {a : α}, nhds a = ⨅ t ∈ s, nhds a
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [h : MeasureTheory.IsFiniteMeasure μ], μ.HasTemperateGrowth
-- Init.Data.List.Basic
/-- Applies a function that returns an `Option` to each element of a list, collecting the non-`none`
values.

`O(|l|)`.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterMap fun x =>
  if x > 2 then some (2 * x) else none
```
```output
[10, 14, 14]
```
 -/
List.filterMap : {α : Type u} → {β : Type v} → (α → Option β) → List α → List β
-- Mathlib.Algebra.Group.Support
Function.mulSupport_inv : ∀ {α : Type u_1} {G : Type u_3} [inst : DivisionMonoid G] (f : α → G), Function.mulSupport f⁻¹ = Function.mulSupport f
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdIntCoreE₂Cohomological : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (E : CategoryTheory.Abelian.SpectralObject C EInt),
  E.HasSpectralSequence CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_pos_iff_mem_nonZeroDivisors : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {I : Ideal S}, 0 < Ideal.absNorm I ↔ I ∈ nonZeroDivisors (Ideal S)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofHom_id : ∀ {X : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X] [inst_3 : CompactSpace X]
  [inst_4 : TotallyDisconnectedSpace X],
  ProfiniteGrp.ofHom (ContinuousMonoidHom.id X) = CategoryTheory.CategoryStruct.id (ProfiniteGrp.of X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.mk.inj : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} {bicone : CategoryTheory.Limits.BinaryBicone P Q} {isBilimit : bicone.IsBilimit}
  {bicone_1 : CategoryTheory.Limits.BinaryBicone P Q} {isBilimit_1 : bicone_1.IsBilimit},
  { bicone := bicone, isBilimit := isBilimit } = { bicone := bicone_1, isBilimit := isBilimit_1 } →
    bicone = bicone_1 ∧ isBilimit ≍ isBilimit_1
-- Init.MetaTypes
Lean.Meta.Occurrences.neg.sizeOf_spec : ∀ (idxs : List ℕ), sizeOf (Lean.Meta.Occurrences.neg idxs) = 1 + sizeOf idxs
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening.eq_1 : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.thickening δ E = {x | Metric.infEDist x E < ENNReal.ofReal δ}
-- Init.Data.Vector.MapIdx
Vector.toArray_mapFinIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {f : (i : ℕ) → α → i < n → m β}, Vector.toArray <$> xs.mapFinIdxM f = xs.toArray.mapFinIdxM fun i x h => f i x ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D] {L : C ≌ D}
  {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (α : F₀ ≅ L.functor.comp F₁),
  F₁.IsLeftKanExtension α.hom
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- Over an integral domain, the Pochhammer polynomial of degree `n` has roots *only* at
`0`, `-1`, ..., `-(n - 1)`.  -/
ascPochhammer_eval_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] [IsDomain R] (n : ℕ) (r : R),
  Polynomial.eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, ↑k = -r
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.instIterator : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [Monad m] → [Std.Iterator α m β] → Std.Iterator (Std.Iterators.Types.Drop α m β) m β
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- Deprecated: prefer `Adjunction.conjugateIsoEquiv adj1 adj2`.  -/
CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} →
          {G G' : CategoryTheory.Functor D C} → (F ⊣ G) → (F' ⊣ G') → (F ≅ F') → (G ≅ G')
-- Lean.Elab.Tactic.Conv.Basic
_private.Lean.Elab.Tactic.Conv.Basic.0.Lean.Elab.Tactic.Conv.convTarget : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 g.1)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f.2 g.2)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_comm : ∀ {α : Type u_4} {r : α → α → Prop} [inst : DecidableRel r] [Std.Symm r] (s t : Finset α),
  Rel.edgeDensity r s t = Rel.edgeDensity r t s
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_of_eqOn_of_isNoetherian : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {u v : V →ₗ[K] V₂} (A : Submodule K V)
  [quot_A_noeth : IsNoetherian K (V ⧸ A)], Set.EqOn ⇑u ⇑v ↑A → u ≈ v
-- Mathlib.Algebra.Ring.Commute
Commute.add_right : ∀ {R : Type u} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)
-- Init.Data.List.Monadic
List.forM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] [LawfulMonad m] {l : List α} {g : α → β}
  {f : β → m PUnit.{u_1 + 1}}, forM (List.map g l) f = forM l fun a => f (g a)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelMul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} [IsCancelMul M] [Nontrivial M], Nontrivial (Localization S)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A reflexive relation is a jointly monic pair of parallel morphisms `p₁, p₂ : R ⟶ X`, together
with a section `r : X ⟶ R` of both `p₁` and `p₂`.  -/
CategoryTheory.ReflexiveRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X : C} → (R ⟶ X) → (R ⟶ X) → Type v_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing_zero : ∀ {R : Type u} {ι : Type v} {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M], ContinuousMultilinearMap.mkPiRing R ι 0 = 0
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Returns `true` if the given expression is a proof and should be omitted.
This function only returns `true` if `pp.proofs` is set to `false`.

"Shallow" proofs are not omitted.
The `pp.proofs.threshold` option controls the depth threshold for what constitutes a shallow proof.
See `Lean.PrettyPrinter.Delaborator.isShallowExpression`.
 -/
Lean.PrettyPrinter.Delaborator.shouldOmitProof : Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Bool
-- Lean.Elab.DocString
Lean.Doc.WithSyntax.mk.inj : ∀ {α : Type u} {val : α} {stx : Lean.Syntax} {val_1 : α} {stx_1 : Lean.Syntax},
  { val := val, stx := stx } = { val := val_1, stx := stx_1 } → val = val_1 ∧ stx = stx_1
-- Batteries.Data.BinomialHeap.Lemmas
_private.Batteries.Data.BinomialHeap.Lemmas.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2) (rank : ℕ) (val : α)
  (c : Batteries.BinomialHeap.Imp.HeapNode α) (s : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : Unit → motive Batteries.BinomialHeap.Imp.Heap.nil)
  (h_2 :
    (rank : ℕ) →
      (val : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)),
  (match Batteries.BinomialHeap.Imp.Heap.cons rank val c s with
    | Batteries.BinomialHeap.Imp.Heap.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.Heap.cons rank val c s => h_2 rank val c s) =
    h_2 rank val c s
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.mk.sizeOf_spec : ∀ (us : List Lean.Level) (args : Array Lean.Expr) (unresolvedInsts : Array Lean.MVarId),
  sizeOf { us := us, args := args, unresolvedInsts := unresolvedInsts } =
    1 + sizeOf us + sizeOf args + sizeOf unresolvedInsts
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ.eq_def : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : List α),
  Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m l =
    match l with
    | [] => m
    | hd :: tl => Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ (m.insertIfNew hd ()) tl
-- Init.Data.BitVec.Lemmas
BitVec.msb_ushiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, (x >>> n).msb = (!decide (0 < n) && x.msb)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingEquiv.ofLeftInverseS_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {g : S → R} {f : R →+* S}
  (h : Function.LeftInverse g ⇑f) (x : R), ↑((RingEquiv.ofLeftInverseS h) x) = f x
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
  f (sSup s) = ⨆ a ∈ s, f a
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- If `F ≤ E` are two subfields of `L`, then `E` is also an intermediate field of
`L / F`. It can be viewed as an inverse to `IntermediateField.toSubfield`.  -/
Subfield.extendScalars : {L : Type u_2} → [inst : Field L] → {F E : Subfield L} → F ≤ E → IntermediateField (↥F) L
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_zero : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R), Polynomial.dickson k a 0 = 3 - ↑k
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_δ'' : ∀ {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (i.castLT ⋯)) (SimplexCategory.δ j.succ) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ i)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` has the continuous linear map `f'` as derivative along the filter `L` if
`f x₁ = f x₂ + f' (x₁ - x₂) + o (x₁ - x₂)` when `x = (x₁, x₂)` converges along the filter `L`.
This definition is designed to be specialized

- for `L = 𝓝 (x, x)` (in `HasStrictFDerivAt`),
  giving rise to the derivative in the sense of strict differentiability;
- for `L = 𝓝 x ×ˢ pure x` (in `HasFDerivAt`), giving rise to the usual notion of Fréchet derivative;
- for `L = 𝓝[s] x ×ˢ pure x` (in `HasFDerivWithinAt`),
  giving rise to the notion of Fréchet derivative along the set `s`.
 -/
HasFDerivAtFilter : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_3} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → (E →L[𝕜] F) → Filter (E × E) → Prop
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `get?_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.get?_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.filterMap f t) k = (Std.DTreeMap.Const.get? t k).bind fun x => f k x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
QuadraticMap.coeFn_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.rightUnitor_hom_apply : ∀ {X : TopCat} {x : ↑X} {p : PUnit.{u + 1}},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) (x, p) = x
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.congr_simp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C], (⊥_ C) = ⊥_ C
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanQueryModuleParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanQueryModuleParams
-- Mathlib.Order.SuccPred.CompleteLinearOrder
/-- **Alias** of `csSup_mem_of_not_isSuccPrelimit`.

---

See `csSup_mem_of_not_isSuccLimit` for the `ConditionallyCompleteLinearOrder` version.  -/
csSup_mem_of_not_isSuccPrelimit' : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, ¬Order.IsSuccPrelimit (sSup s) → sSup s ∈ s
-- Mathlib.Tactic.FieldSimp
/-- `field` is a `simp` set that clears denominators in (semi-)field (in)equalities.

The `field` simp set is a variant of the `field_simp` tactic. The latter operates recursively on
subexpressions, bringing every field-expression encountered to the form `n / d`, and then attempts
to clear the denominator. (For confluence reasons, the `field` simprocs also have a slightly
different normal form from `field_simp`'s.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific
to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is known,
etc). See `field_simp_discharge` for full details of the discharger algorithm.

* `simp [field, t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
 -/
Mathlib.Tactic.FieldSimp.proc : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.trans_homotopyHomInvId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  (f.trans g).homotopyHomInvId =
    ⋯.mpr (⋯.mp (((g.homotopyHomInvId.compRightId f.inv).compLeft f.hom).trans f.homotopyHomInvId))
-- Mathlib.Order.BooleanSubalgebra
/-- The minimum Boolean subalgebra containing a given set.  -/
BooleanSubalgebra.closure : {α : Type u_2} → [inst : BooleanAlgebra α] → Set α → BooleanSubalgebra α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.normSq_pos : ∀ (z : UpperHalfPlane), 0 < Complex.normSq ↑z
-- Mathlib.NumberTheory.Chebyshev
Nat.factorization_lcmUpto : ∀ (n : ℕ) {p : ℕ}, Nat.Prime p → n.lcmUpto.factorization p = Nat.log p n
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.SpecToEquivOfField_apply_fst : ∀ (K : Type u) [inst : Field K] (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X),
  ((AlgebraicGeometry.Scheme.SpecToEquivOfField K X) f).fst = f (IsLocalRing.closedPoint ↑(CommRingCat.of K))
-- Mathlib.Tactic.Subsingleton
/-- Elaborates the terms like how `Lean.Elab.Tactic.addSimpTheorem` does,
abstracting their metavariables.
 -/
Mathlib.Tactic.elabSubsingletonInsts : Option (Array Lean.Term) → Lean.Elab.TermElabM (Array (Lean.Term × Lean.Meta.AbstractMVarsResult))
-- Lean.Environment
Lean.instInhabitedOLeanEntries : {a : Type} → [Inhabited a] → Inhabited (Lean.OLeanEntries a)
-- Batteries.Control.Nondet.Basic
Nondet.mk.injEq : ∀ {σ : Type} {m : Type → Type} [inst : Lean.MonadBacktrack σ m] {α : Type} (toMLList toMLList_1 : MLList m (α × σ)),
  ({ toMLList := toMLList } = { toMLList := toMLList_1 }) = (toMLList = toMLList_1)
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.squash : {m : Type u → Type u} → {α : Type u} → (Unit → m (MLList.MLListImpl✝ m α)) → MLList.MLListImpl✝ m α
-- Mathlib.Algebra.Group.Action.End
/-- `AddAut.applyAddDistribAddAction` is faithful.  -/
AddAut.apply_faithfulVAdd : ∀ {M : Type u_2} [inst : AddMonoid M], FaithfulVAdd (AddAut M) M
-- Mathlib.Order.Sublattice
/-- See Note [custom simps projection].  -/
Sublattice.Simps.coe : {α : Type u_2} → [inst : Lattice α] → Sublattice α → Set α
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.instFinite : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)},
  Std.Iterators.Finite (Std.Iterators.Types.DropWhile α m β P) m
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma0Map.eq_1 : ∀ (N : ℕ), CongruenceSubgroup.Gamma0Map N = { toFun := fun g => ↑(↑↑g 1 1), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isCoprime_helper : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {r s t w : NumberField.RingOfIntegers K},
  ¬hζ.toInteger - 1 ∣ r →
    ¬hζ.toInteger - 1 ∣ s →
      (∀ {p : NumberField.RingOfIntegers K}, Prime p → p ∣ t → p ∣ w → Associated p (hζ.toInteger - 1)) →
        (∀ {q : NumberField.RingOfIntegers K}, q ∣ r → q ∣ t) →
          (∀ {q : NumberField.RingOfIntegers K}, q ∣ s → q ∣ w) → IsCoprime r s
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_3} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {M₂ : Type u_4} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_8 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_9 : RingHomInvPair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x : M), e (-x) = -e x
-- Mathlib.Logic.Pairwise
/-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`.  -/
Pairwise : {α : Type u_1} → (α → α → Prop) → Prop
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  ∃ i' hii',
    ⇑(CategoryTheory.CategoryStruct.comp (D.map hii') (CategoryTheory.Limits.pullback.lift A.a A.b ⋯)) ⁻¹'
        (↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ =
      ∅
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.const_smul : ∀ {𝕜 : 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] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F]
  [inst_7 : IsBoundedSMul R F] [inst_8 : SMulCommClass 𝕜 R F] {c : R},
  HasFPowerSeriesWithinAt f pf s x → HasFPowerSeriesWithinAt (c • f) (c • pf) s x