mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_appTop : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop g) (AlgebraicGeometry.Scheme.Hom.appTop f)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The identity morphism of this category  -/
CategoryTheory.EnrichedCategory.id : {V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} →
        [self : CategoryTheory.EnrichedCategory V C] →
          (X : C) → CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.add.match_1.splitter : {F : Type u_1} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} →
      (motive : W.Point → W.Point → Sort u_2) →
        (x x_1 : W.Point) →
          ((P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P) →
            ((P : W.Point) →
                (P = WeierstrassCurve.Affine.Point.zero → False) → motive P WeierstrassCurve.Affine.Point.zero) →
              ((x₁ y₁ : F) →
                  (h₁ : W.Nonsingular x₁ y₁) →
                    (x₂ y₂ : F) →
                      (h₂ : W.Nonsingular x₂ y₂) →
                        motive (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁)
                          (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)) →
                motive x x_1
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Dual to `Monad.PreservesColimitOfIsReflexivePair`.  -/
CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_tProd_elim' : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (i : δ) → MeasurableSpace (X i)] [inst_1 : DecidableEq δ] {l : List δ}
  (h : ∀ (i : δ), i ∈ l), Measurable (List.TProd.elim' h)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instCommRing : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → CommRing (TruncatedWittVector p n R)
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
Projectivization.isEmpty_of_subsingleton : ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [Subsingleton V], IsEmpty (Projectivization k V)
-- Mathlib.Algebra.Ring.Prod
RingHom.prod_comp_prodMap : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S']
  [inst_4 : NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S'),
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Hom.sum_comp_sumComm : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G →g G') (g : H →g H'),
  (f.sum g).comp SimpleGraph.Iso.sumComm.toHom = SimpleGraph.Iso.sumComm.toHom.comp (g.sum f)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
IsUnit.stronglyMeasurable_const_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Type u_5} [inst : TopologicalSpace β] [inst_1 : Monoid M]
  [inst_2 : MulAction M β] [ContinuousConstSMul M β] {x : MeasurableSpace α} {c : M},
  IsUnit c → ((MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_sInf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α} {S : Set (BooleanSubalgebra α)}, a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_eq_card_sub_one : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
  G.degree v = Fintype.card V - 1 ↔ G.IsUniversal v
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind.processing.sizeOf_spec : sizeOf Lean.Lsp.LeanFileProgressKind.processing = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams : Type
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram `D` to `F` is limit
of `F` evaluated at `D`. This variant is for covariant diagrams, see
`colimitCoyonedaHomIsoLimit` for a covariant version.  -/
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor I C) →
          (F : CategoryTheory.Functor C (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.op.comp CategoryTheory.coyoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus\{j\}} → X)$.  -/
GenLoop.toLoop : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} → [DecidableEq N] → (i : N) → ↑(GenLoop N X x) → LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → fderiv 𝕜 (fun y => f y + g y) x = fderiv 𝕜 f x + fderiv 𝕜 g x
-- Mathlib.Data.SetLike.Basic
/-- **Alias** of `SetLike.coe_injective`.

---

The coercion from a term of a `SetLike` to its corresponding `Set` is injective.  -/
SetLike.coe_injective' : ∀ {A : Type u_1} {B : outParam (Type u_2)} [self : SetLike A B], Function.Injective SetLike.coe
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_ofProp_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)]
  {φ₁ φ₂ : Prop},
  Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp (φ₁ → φ₂))
    (Lean.Order.himp (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withoutErrToSorryImp : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Init.Data.List.Lemmas
List.mem_of_getElem? : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, l[i]? = some a → a ∈ l
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- An argument to skip, like an implicit argument.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.skip : Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.RingTheory.SimpleModule.Isotypic
isFullyInvariant_iff_le_imp_isotypicComponent_le : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  {m : Submodule R M}, m.IsFullyInvariant ↔ ∀ S ≤ m, ∀ [IsSimpleModule R ↥S], isotypicComponent R M ↥S ≤ m
-- Lean.Elab.Term.TermElabM
/-- Make sure `e` is a type by inferring its type and making sure it is an `Expr.sort`
or is unifiable with `Expr.sort`, or can be coerced into one.  -/
Lean.Elab.Term.ensureType : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

---

`range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.range_mem_invtSubmodule : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → f ∘ₗ T ∘ₗ f = T ∘ₗ f → f.range ∈ Module.End.invtSubmodule T
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
interior_ae_eq_of_null_frontier : ∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s : Set α'}, μ (frontier s) = 0 → interior s =ᵐ[μ] s
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommGroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : CommGroup α], Shrink.instCommGroup = (equivShrink α).symm.commGroup
-- Mathlib.RingTheory.Ideal.Colon
/-- A variant for arbitrary sets in commutative semirings  -/
Submodule.bot_colon' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M},
  ⊥.colon S = (Submodule.span R S).annihilator
-- Lean.Data.Options
Lean.Option.registerBuiltinOption : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instPartialOrder : {E : Type u_3} → [inst : AddGroup E] → PartialOrder (NonarchAddGroupSeminorm E)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_inj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] ⦃s t : ContMDiffSection I F n V⦄,
  ⇑s = ⇑t → s = t
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B} (y : E b),
  (Bundle.Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e ⟨b, y⟩).2 else 0
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.length_cycle : ∀ {n : ℕ}, (SimpleGraph.cycleGraph.cycle n).length = n + 3
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ ∪ t₂)[k]! = t₂.getD k t₁[k]!
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.ennrealPreVariation_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) (hf : MeasureTheory.IsSigmaSubadditiveSetFun f)
  (hf' : f ∅ = 0) (s : Set X), (MeasureTheory.ennrealPreVariation f hf hf') s = MeasureTheory.preVariationFun f s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_id : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_227✝ → cfcₙ id a = a
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_eq_true_iff_exists_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {p : α → Bool},
  m.any p = true ↔ ∃ a ∈ m, p a = true
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_shiftLeft_mod : ∀ (a : BitVec 32) (b : ℕ), { toBitVec := a <<< (b % 32) } = { toBitVec := a } <<< UInt32.ofNat b
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed_def : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E),
  f.normed μ x = ↑f x / ∫ (x : E), ↑f x ∂μ
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- A (random) isomorphism between an algebraic closure of `R` and an algebraic closure of
an algebraic extension of `R`  -/
IsAlgClosure.equivOfAlgebraic' : (R : Type u) →
  (S : Type u_3) →
    (L : Type v) →
      (M : Type w) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Field L] →
              [inst_3 : Field M] →
                [inst_4 : Algebra R M] →
                  [inst_5 : Module.IsTorsionFree R M] →
                    [IsAlgClosure R M] →
                      [inst_7 : Algebra S L] →
                        [inst_8 : Module.IsTorsionFree S L] →
                          [IsAlgClosure S L] →
                            [inst_10 : Algebra R S] →
                              [inst_11 : Algebra R L] →
                                [IsScalarTower R S L] →
                                  [IsDomain R] →
                                    [IsDomain S] → [Module.IsTorsionFree R S] → [Algebra.IsAlgebraic R L] → L ≃ₐ[R] M
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.isDenseEmbedding : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → DenseRange f → IsDenseEmbedding f
-- Mathlib.Algebra.Quandle
/-- The homomorphism `toEnvelGroup.map f` is the unique map that fits into the commutative
triangle in `toEnvelGroup.univ`.
 -/
Rack.toEnvelGroup.univ_uniq : ∀ (R : Type u_1) [inst : Rack R] (G : Type u_2) [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  (g : Rack.EnvelGroup R →* G), f = (Quandle.Conj.map g).comp (Rack.toEnvelGroup R) → g = Rack.toEnvelGroup.map f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.insert : Lean.Lsp.InsertReplaceEdit → Lean.Lsp.Range
-- Mathlib.Data.Set.Finite.Lattice
iInf_iSup_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Antitone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
-- Mathlib.Data.Num.Bitwise
/-- Sign of a `NzsNum`.  -/
NzsNum.sign : NzsNum → Bool
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The composition of an isomorphism between equivalent additive group extensions and a section  -/
AddGroupExtension.Section.equivComp : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] →
        {E : Type u_3} →
          [inst_2 : AddGroup E] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : AddGroup E'] → {S' : AddGroupExtension N E' G} → S.Section → S.Equiv S' → S'.Section
-- Init.Data.List.Basic
List.map.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (head : α) (tail : List α),
  List.map f (head :: tail) = f head :: List.map f tail
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instIsScalarTower : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommGroup M] [inst_3 : CommRing A] [inst_4 : SMul R S] [inst_5 : Algebra R A] [inst_6 : Algebra S A]
  [inst_7 : Module R M] [inst_8 : Module S M] [inst_9 : Module A M] [inst_10 : IsScalarTower R A M]
  [inst_11 : IsScalarTower S A M] [IsScalarTower R S A] (Q : QuadraticForm A M), IsScalarTower R S (CliffordAlgebra Q)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonMulHom : ∀ {α : Type u_2} [inst : Mul α], ⇑Set.singletonMulHom = singleton
-- Std.Time.Format.Modifier
Std.Time.Modifier.Y.sizeOf_spec : ∀ (presentation : Std.Time.Year), sizeOf (Std.Time.Modifier.Y presentation) = 1 + sizeOf presentation
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 1).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.mk.inj : ∀ {visited : Std.HashSet UInt64} {found : Lean.FVarIdSet} {visited_1 : Std.HashSet UInt64} {found_1 : Lean.FVarIdSet},
  { visited := visited, found := found } = { visited := visited_1, found := found_1 } →
    visited = visited_1 ∧ found = found_1
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_ineq : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (a : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_right_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_right_split_ineq_cert p₁ p₂ (↑k) a p' = true →
      Int.Internal.Linear.Poly.denote' ctx p' ≤ 0
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.isPWO_iUnion_support : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α), (⋃ a, (s a).support).IsPWO
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleParams.mk : Lean.JsonRpc.RequestID → Array Lean.Lsp.LeanModuleQuery → Lean.Lsp.LeanQueryModuleParams
-- Init.Data.UInt.Lemmas
UInt64.right_eq_add : ∀ {a b : UInt64}, b = a + b ↔ a = 0
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- For nonzero `a : F`, `quadraticChar F a = 1 ↔ IsSquare a`.  -/
quadraticChar_one_iff_isSquare : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  a ≠ 0 → ((quadraticChar F) a = 1 ↔ IsSquare a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Jacobian R} →
      {point : WeierstrassCurve.Jacobian.PointClass R} → W'.NonsingularLift point → W'.Point
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_1.go : {ε : Type u} →
  {α : Type v} →
    {motive_1 : Lean.AsyncList ε α → Sort u_1} →
      {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
        {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
          {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1} →
            (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) →
              ((t : Lean.AsyncList ε α) → t.below → motive_1 t) →
                ((t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t) →
                  ((t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t) →
                    ((t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t) →
                      motive_2 t ×' Lean.AsyncList.below_1 t
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.image.lift_fac : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (ModuleCat.image.lift F') F'.m = ModuleCat.image.ι f
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v), Module.Basis.span hli = Module.Basis.mk ⋯ ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y),
  (P.fullsubcategory.map f).toFunctor = P.map f
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
MulOpposite.instSMulZeroClass : {M : Type u_1} → {α : Type u_2} → [inst : AddMonoid α] → [SMulZeroClass M α] → SMulZeroClass M αᵐᵒᵖ
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.instOfNonemptyOfIndiscreteTopology : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [Nonempty Y] [IndiscreteTopology Y], ContractibleSpace Y
-- Init.Data.List.Attach
List.attach_nil : ∀ {α : Type u_1}, [].attach = []
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.sign_eq_abs_ediv : ∀ (a : ℤ), a.sign = |a| / a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_ite_eq' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => b = x] (a : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  (∑'[L] (b' : β), if b = b' then a b' else 0) = a b
-- Mathlib.Order.SuccPred.Basic
PredOrder.ofPredLeIff.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (succ : α → α) (hsucc_le_iff : ∀ {a b : α}, b ≤ succ a ↔ b < a),
  PredOrder.ofPredLeIff succ hsucc_le_iff = { pred := succ, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
-- Mathlib.Algebra.GCDMonoid.Multiset
/-- Least common multiple of a multiset  -/
Multiset.lcm : {α : Type u_1} → [inst : CommMonoidWithZero α] → [NormalizedGCDMonoid α] → Multiset α → α
-- Mathlib.Data.EReal.Basic
/-- Extension for the `positivity` tactic: cast from `ℝ` to `EReal`.  -/
Mathlib.Meta.Positivity.evalRealToEReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
AlgEquiv.fieldRange_eq_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (f : E ≃ₐ[F] K), (↑f).fieldRange = ⊤
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv_refl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v),
  hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_measure : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ ν : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f ν a b → μ ≤ ν → IntervalIntegrable f μ a b
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.instInhabitedForwardRuleMatches : Inhabited Aesop.ForwardRuleMatches
-- Init.Data.SInt.Lemmas
Int32.zero_mod : ∀ {a : Int32}, 0 % a = 0
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_add_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (p m n : ℕ) [inst_1 : ExpChar R p] (x : R),
  (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra hom `f : P →ₐ[R] S` with square-zero kernel `I`,
and a section `g : S →ₐ[R] P` (as algebra homs),
we get a retraction of the injection `I → S ⊗[P] Ω[P/R]`.
 -/
retractionOfSectionOfKerSqZero : {R : Type u_1} →
  {P : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                [inst_5 : Algebra R S] →
                  [inst_6 : IsScalarTower R P S] →
                    (g : S →ₐ[R] P) →
                      RingHom.ker (algebraMap P S) ^ 2 = ⊥ →
                        (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S →
                          TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_algebraMap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (r : R),
  (CliffordAlgebra.changeForm h) ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q')) r