mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_mapsTo : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {x : M} {f : M → M'},
  Set.MapsTo (writtenInExtChartAt I I' x f)
    ((extChartAt I x).target ∩ f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) (extChartAt I' (f x)).target
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateConstImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu →
    Lean.Name → List Lean.Level → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Lean.Meta.Basic
Lean.Meta.isExprDefEqAux : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.UInt.Lemmas
UInt8.ofNat_lt_iff : ∀ {n : UInt8} {m : ℕ}, m < UInt8.size → (UInt8.ofNat m < n ↔ m < n.toNat)
-- Mathlib.CategoryTheory.Sites.Closed
/-- The topology given by the closure operator `J.close` on a Grothendieck topology is the same as `J`.
 -/
CategoryTheory.topologyOfClosureOperator_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.topologyOfClosureOperator J₁.closureOperator ⋯ = J₁
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.forward.inj : ∀ {n n_1 : Lean.Name},
  Batteries.Tactic.Alias.AliasInfo.forward n = Batteries.Tactic.Alias.AliasInfo.forward n_1 → n = n_1
-- Mathlib.Algebra.Category.Grp.AB
instHasSeparatorAddCommGrpCat : CategoryTheory.HasSeparator AddCommGrpCat
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J),
  CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
      ⟨(j, 0), ⋯⟩ =
    CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
      (e.hom.app (X j))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : β k → β k},
  (t.modify k f).getD k fallback = (Option.map f (t.get? k)).getD fallback
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {ι : Type u_3}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit c →
    ∀ (i j : CategoryTheory.Discrete ι),
      i ≠ j →
        CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i))
          (CategoryTheory.Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- If an `R`-module `M` is the direct sum of fully invariant submodules `Nᵢ`,
then `End R M` is isomorphic to `Πᵢ End R Nᵢ` as an algebra.  -/
iSupIndep.algEquiv : (R₀ : Type u_1) →
  {R : Type u_2} →
    {M : Type u} →
      [inst : CommSemiring R₀] →
        [inst_1 : Ring R] →
          [inst_2 : Algebra R₀ R] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                {ι : Type u_5} →
                  [DecidableEq ι] →
                    {N : ι → Submodule R M} →
                      iSupIndep N →
                        ⨆ i, N i = ⊤ →
                          (∀ (i : ι), (N i).IsFullyInvariant) →
                            [inst_6 : Module R₀ M] →
                              [inst_7 : IsScalarTower R₀ R M] → Module.End R M ≃ₐ[R₀] (i : ι) → Module.End R ↥(N i)
-- Mathlib.RingTheory.PrincipalIdealDomainOfPrime
/-- `Submodule.IsPrincipal` is an Oka predicate.  -/
Ideal.isOka_isPrincipal : ∀ {R : Type u_1} [inst : CommSemiring R], Ideal.IsOka Submodule.IsPrincipal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.cos_arctan : ∀ (x : ℝ), Real.cos (Real.arctan x) = 1 / √(1 + x ^ 2)
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_comm : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A B : Rep.{u_1, u, v} k ↥S} (f : A ⟶ B) (g₁ g₂ : G) (a : ↑A),
  (B.indToCoindAux g₁) ((Rep.Hom.hom f) a) g₂ = (Rep.Hom.hom f) ((A.indToCoindAux g₁) a g₂)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- **Thales' theorem**: The angle inscribed in a semicircle is a right angle.  -/
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P},
  s.IsDiameter p₁ p₃ → (EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.isFiniteMeasure_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → (MeasureTheory.IsFiniteMeasure P ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- A function on `Box ι` is called box additive if for every box `J` and a partition `π` of `J`
we have `f J = ∑ Ji ∈ π.boxes, f Ji`. A function is called box additive on subboxes of `I : Box ι`
if the same property holds for `J ≤ I`. We formalize these two notions in the same definition
using `I : WithBot (Box ι)`: the value `I = ⊤` corresponds to functions box additive on the whole
space.  -/
BoxIntegral.BoxAdditiveMap : (ι : Type u_3) → (M : Type u_4) → [AddCommMonoid M] → WithTop (BoxIntegral.Box ι) → Type (max u_3 u_4)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `ENNReal.tendsto_finsetProd_of_ne_top`. -/
ENNReal.tendsto_finset_prod_of_ne_top : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α → ENNReal} {x : Filter α} {a : ι → ENNReal} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) →
    (∀ i ∈ s, a i ≠ ⊤) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentColorOptions.fromJson : Lean.Json → Except String Lean.Lsp.DocumentColorOptions
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B]
  (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C] [inst_4 : CategoryTheory.FinitaryExtensive C]
  [h : ∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
  [CategoryTheory.Limits.PreservesFiniteLimits s], (CategoryTheory.coherentTopology C).HasSheafCompose s
-- Mathlib.Probability.Distributions.Pareto
/-- Measure defined by the Pareto distribution.  -/
ProbabilityTheory.paretoMeasure : ℝ → ℝ → MeasureTheory.Measure ℝ
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.Spec_map_left : ∀ (S : AlgebraicGeometry.Scheme)
  {X Y : CategoryTheory.MorphismProperty.CostructuredArrow @AlgebraicGeometry.Etale ⊤ AlgebraicGeometry.Scheme.Spec S}
  (f : X ⟶ Y), ((AlgebraicGeometry.Scheme.AffineEtale.Spec S).map f).left = AlgebraicGeometry.Spec.map f.left.unop
-- Mathlib.Logic.Equiv.Prod
/-- A product of types can be split as the binary product of one of the types and the product
of all the remaining types.  -/
Equiv.piSplitAt : {α : Type u_9} → [DecidableEq α] → (i : α) → (β : α → Type u_10) → ((j : α) → β j) ≃ β i × ((j : { j // j ≠ i }) → β ↑j)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.tendsto_coe_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  Filter.Tendsto OnePoint.some (Filter.coclosedCompact X) (nhds OnePoint.infty)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `completedHurwitzZetaOdd` as a Dirichlet series in the convergence range.  -/
HurwitzZeta.hasSum_int_completedHurwitzZetaOdd : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2)
      (HurwitzZeta.completedHurwitzZetaOdd (↑a) s)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.instStarMul : {R : Type u_1} → {R' : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing R'] → [StarRing R'] → StarMul (MulChar R R')
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.rank F ↥⊥ = 1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_sigma : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f],
  CategoryTheory.IsSeparator (∐ f) ↔ (CategoryTheory.ObjectProperty.ofObj f).IsSeparating
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- The cocone `coconeOfHasLimitEval F` is colimit.  -/
HomologicalComplex.isColimitCoconeOfHasColimitEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] →
                  CategoryTheory.Limits.IsColimit (HomologicalComplex.coconeOfHasColimitEval F)
-- Mathlib.Data.Multiset.AddSub
/-- `s - t` is the multiset such that `count a (s - t) = count a s - count a t` for all `a`.
(note that it is truncated subtraction, so `count a (s - t) = 0` if `count a s ≤ count a t`).  -/
Multiset.sub : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α → Multiset α
-- Mathlib.Logic.Equiv.Multiset
/-- If `α` is denumerable, then so is `Multiset α`. Warning: this is *not* the same encoding as used
in `Multiset.encodable`.  -/
Denumerable.multiset : {α : Type u_1} → [Denumerable α] → Denumerable (Multiset α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_mapPullbackAdj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f],
  CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f = CategoryTheory.Over.mapPullbackAdj f
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedRuleSets.default : Aesop.Frontend.RuleSets
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_congr_identDistrib : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ},
  ProbabilityTheory.IdentDistrib X Y μ μ' → ProbabilityTheory.complexMGF X μ = ProbabilityTheory.complexMGF Y μ'
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succ : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) {n : ℕ},
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg (n + 1) =
    max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1))
      (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)
-- Init.Data.List.SplitOn.Basic
/-- Split a list at every occurrence of a separator element. The separators are not in the result.

Examples:

* `[1, 1, 2, 3, 2, 4, 4].splitOn 2 = [[1, 1], [3], [4, 4]]`
 -/
List.splitOn : {α : Type u_1} → [BEq α] → α → List α → List (List α)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.infDist_eq_radius_iff_isTangent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as]
  [as.direction.HasOrthogonalProjection], Metric.infDist s.center ↑as = s.radius ↔ s.IsTangent as
-- Batteries.Lean.NameMapAttribute
Lean.NameMapAttributeImpl.mk : {α : Type} →
  Lean.Name →
    autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam →
      String → (Lean.Name → Lean.Syntax → Lean.AttrM α) → Lean.NameMapAttributeImpl α
-- Std.Data.ExtDHashMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDHashMap.getKey : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → (m : Std.ExtDHashMap α β) → (a : α) → a ∈ m → α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_le_iff_le_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S} {s : Subring R}
  {t : Subring S}, Subring.map f s ≤ t ↔ s ≤ Subring.comap f t
-- Mathlib.Data.Finset.Sort
Finset.pairwise_sort : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], List.Pairwise r (s.sort r)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Postcomposing by an isomorphism induces an isomorphism on the image.  -/
CategoryTheory.Limits.image.compIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        {Z : C} →
          (g : Y ⟶ Z) →
            [CategoryTheory.Limits.HasEqualizers C] →
              [inst_2 : CategoryTheory.Limits.HasImage f] →
                [inst_3 : CategoryTheory.IsIso g] →
                  CategoryTheory.Limits.image f ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- `Module.IsTrivialRelation` is equivalent to the predicate `TensorProduct.VanishesTrivially`
defined in `Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean`.  -/
Module.isTrivialRelation_iff_vanishesTrivially : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Fintype ι] {f : ι → R} {x : ι → M}, Module.IsTrivialRelation f x ↔ TensorProduct.VanishesTrivially R f x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_if : ∀ {m n : ℤ}, (m<...=n).toArray = if m + 1 ≤ n then #[m + 1] ++ ((m + 1)<...=n).toArray else #[]
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_left_mk' : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ),
  Turing.Tape.move Turing.Dir.left (Turing.Tape.mk' L R) = Turing.Tape.mk' L.tail (Turing.ListBlank.cons L.head R)
-- Mathlib.Topology.DiscreteSubset
/-- Criterion for a subset `S ⊆ X` to be closed and discrete in terms of the punctured
neighbourhood filter at an arbitrary point of `X`. (Compare `isDiscrete_iff_nhds_ne`.)  -/
isClosed_and_discrete_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X},
  IsClosed S ∧ IsDiscrete S ↔ ∀ (x : X), Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal S)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.completedCosZeta₀_zero : ∀ (s : ℂ), HurwitzZeta.completedCosZeta₀ 0 s = completedRiemannZeta₀ s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKeyD k fallback =
    if (f (Std.DHashMap.Const.get? m k)).isSome = true then k else fallback
-- Lean.DocString.Extension
/-- Returns the Verso module docs for the current main module.

During elaboration, this will return the modules docs that have been added thus far, rather than
those for the entire module.
 -/
Lean.getMainVersoModuleDocs : Lean.Environment → Lean.VersoModuleDocs
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.mk_algebraMap : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] (x : R₁), (Ideal.Quotient.mk I) ((algebraMap R₁ A) x) = (algebraMap R₁ (A ⧸ I)) x
-- Mathlib.Topology.Order
isClosed_sSup_iff : ∀ {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)}, IsClosed s ↔ ∀ t ∈ T, IsClosed s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.termZ : Lean.ParserDescr
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_eq_of_associated : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, Associated x y → Ring.ord R x = Ring.ord R y
-- Plausible.Testable
Plausible.Testable.forallTypesULiftTestable : {var : String} →
  {f : Type u → Prop} →
    [Plausible.Testable (f (ULift.{u, 0} ℤ))] → Plausible.Testable (Plausible.NamedBinder var (∀ (x : Type u), f x))
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isVonNBounded_iff : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
-- Mathlib.Tactic.Abel
/-- Construct the normal form representing zero.  -/
Mathlib.Tactic.Abel.NormalExpr.zero' : Mathlib.Tactic.Abel.M Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.zero_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G H : CategoryTheory.Grp C), CategoryTheory.InducedCategory.Hom.hom 0 = 0
-- Mathlib.Data.Nat.Pairing
Set.iUnion_unpair_prod : ∀ {α : Type u_1} {β : Type u_2} {s : ℕ → Set α} {t : ℕ → Set β},
  ⋃ n, s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.pow_le_one_of_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, a ≤ 1 → ∀ (n : ℕ), a ^ n ≤ 1
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The image of a monoid object under a lax monoidal functor is a monoid object.  -/
CategoryTheory.Functor.monObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.LaxMonoidal] → (X : C) → [CategoryTheory.MonObj X] → CategoryTheory.MonObj (F.obj X)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_iInter_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (s : Set α) (t : ι → Set β),
  s • ⋂ i, t i ⊆ ⋂ i, s • t i
-- Mathlib.Order.Bounds.Basic
IsLeast.mono : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a b : α}, IsLeast s a → IsLeast t b → s ⊆ t → b ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.s_r_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.s (CategoryTheory.CategoryStruct.comp s.r h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_le_not_ge`. -/
LE.le.lt_of_not_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.smul_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst_1 : AddCommMonoid M] [inst_2 : SMul R M]
  {f : ArithmeticFunction R} {g : ArithmeticFunction M} {n : ℕ}, (f • g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 • g x.2
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Star projection operators are equal iff their range are.  -/
LinearMap.IsStarProjection.ext_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {S T : E →ₗ[𝕜] E},
  IsStarProjection S → IsStarProjection T → (S = T ↔ S.range = T.range)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h : k' ∈ Std.HashMap.ofList l}, (Std.HashMap.ofList l).getKey k' h = k
-- Init.Data.Vector.Lemmas
Vector.toList_empty : ∀ {α : Type u_1}, #v[].toList = []
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.op_apply_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β) (a : βᵃᵒᵖ),
  (AddEquiv.op f).symm a = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a
-- Mathlib.Analysis.Analytic.Inverse
_private.Mathlib.Analysis.Analytic.Inverse.0.FormalMultilinearSeries.leftInv.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.pullback_map_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f] (g : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.map f).obj g) = g
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_iff_smul_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  (P.reflectionPerm i) j = j ↔ P.pairing j i • P.root i = 0
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `locallyLipschitzOn_inv_iff`. -/
LocallyLipschitzOn.of_inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E} {s : Set α},
  LocallyLipschitzOn s f⁻¹ → LocallyLipschitzOn s f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.mk.injEq : ∀ (c? c_ww? c_wl? c_wr? c?_1 c_ww?_1 c_wl?_1 c_wr?_1 : Option Lean.Expr),
  ({ c? := c?, c_ww? := c_ww?, c_wl? := c_wl?, c_wr? := c_wr? } =
      { c? := c?_1, c_ww? := c_ww?_1, c_wl? := c_wl?_1, c_wr? := c_wr?_1 }) =
    (c? = c?_1 ∧ c_ww? = c_ww?_1 ∧ c_wl? = c_wl?_1 ∧ c_wr? = c_wr?_1)