mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- This enables the instance `Zero (Weight R H L)`.  -/
LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] [Nontrivial ↥H], Nontrivial ↥(LieModule.genWeightSpace L 0)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.Eventually.exists_measurable_mem_of_smallSets : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : Set α → Prop},
  (∀ᶠ (s : Set α) in f.smallSets, p s) → ∃ s ∈ f, MeasurableSet s ∧ p s
-- Mathlib.Logic.Equiv.PartialEquiv
Set.BijOn.toPartialEquiv_source : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (t : Set β) (hf : Set.BijOn f s t),
  (Set.BijOn.toPartialEquiv f s t hf).source = s
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.coeff_trunc : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (φ : PowerSeries R),
  ((PowerSeries.trunc n) φ).coeff m = if m < n then (PowerSeries.coeff m) φ else 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.zero_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y : C) (n : ℕ) [inst_3 : HasDerivedCategory C],
  CategoryTheory.Abelian.Ext.hom 0 = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.const_nsmul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : AddMonoid β]
  [ContinuousAdd β], MeasureTheory.StronglyMeasurable f → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (n • f)
-- Mathlib.Order.BoundedOrder.Basic
not_isBot_iff_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ¬IsBot a ↔ a ≠ ⊥
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instOne : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [One G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] → One (ContMDiffMap I I' N G n)
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `b.coord i` is the linear function giving the `i`-th coordinate of a vector
with respect to the basis `b`.

`b.coord i` is an element of the dual space. In particular, for
finite-dimensional spaces it is the `ι`th basis vector of the dual space.
 -/
Module.Basis.coord : {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → ι → M →ₗ[R] R
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_inj : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  {x y : G i}, RestrictedProduct.single A i x = RestrictedProduct.single A i y ↔ x = y
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.mk.inj : ∀ {mctx : Lean.MetavarContext} {nextMacroScope : Lean.MacroScope} {ngen : Lean.NameGenerator}
  {cache : Std.HashMap Lean.ExprStructEq Lean.Expr} {mctx_1 : Lean.MetavarContext} {nextMacroScope_1 : Lean.MacroScope}
  {ngen_1 : Lean.NameGenerator} {cache_1 : Std.HashMap Lean.ExprStructEq Lean.Expr},
  { mctx := mctx, nextMacroScope := nextMacroScope, ngen := ngen, cache := cache } =
      { mctx := mctx_1, nextMacroScope := nextMacroScope_1, ngen := ngen_1, cache := cache_1 } →
    mctx = mctx_1 ∧ nextMacroScope = nextMacroScope_1 ∧ ngen = ngen_1 ∧ cache = cache_1
-- Mathlib.RepresentationTheory.Invariants
Rep.instAdditiveModuleCatInvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G], (Rep.invariantsFunctor k G).Additive
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.mk : {α : Type u} →
  {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
    α → Std.Tactic.BVDecide.BVExpr.Cache aig → Std.Tactic.BVDecide.BVExpr.WithCache α aig
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Given any morphism `k : Y ⟶ W` such that `f ≫ k = 0`, `k` factors through `cokernel.π f`
via `cokernel.desc : cokernel f ⟶ W`.  -/
CategoryTheory.Limits.cokernel.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {W : C} → (k : Y ⟶ W) → CategoryTheory.CategoryStruct.comp f k = 0 → (CategoryTheory.Limits.cokernel f ⟶ W)
-- Mathlib.Analysis.Fourier.Convolution
SchwartzMap.convolution_flip : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace ℂ F₁]
  [inst_8 : NormedSpace 𝕜 F₁] [inst_9 : SMulCommClass ℂ 𝕜 F₁] [inst_10 : NormedAddCommGroup F₂]
  [inst_11 : NormedSpace ℂ F₂] [inst_12 : NormedSpace 𝕜 F₂] [inst_13 : SMulCommClass ℂ 𝕜 F₂]
  [inst_14 : NormedAddCommGroup F₃] [inst_15 : NormedSpace ℂ F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂),
  ((SchwartzMap.convolution B.flip) g) f = ((SchwartzMap.convolution B) f) g
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.E.inj : ∀ {B : Type v} {a a_1 : B}, CartanMatrix.Generators.E a = CartanMatrix.Generators.E a_1 → a = a_1
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
is a linear map between `M₁` and `M₂` that commutes with the quadratic forms.  -/
QuadraticMap.Isometry.«term_→qᵢ_» : Lean.TrailingParserDescr
-- Init.Core
/-- The analogue of `Quot.inductionOn`: every element of `Quotient s` is of the form `Quotient.mk s a`.  -/
Quotient.inductionOn : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s), (∀ (a : α), motive ⟦a⟧) → motive q
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.chains₁ToCoinvariantsKer_surjective : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (groupHomology.chains₁ToCoinvariantsKer A))
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits of `K.leftOp : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : Cᵒᵖ ⥤ D`
preserves limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesLimit_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimit K.leftOp F.rightOp],
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toBilinForm_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (L : E →L[𝕜] E →L[𝕜] 𝕜) (v w : E), (L.toBilinForm v) w = (L v) w
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.continuous : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (h : ContinuousMap.HomotopyEquiv X Y), Continuous ⇑h.toFun
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : CompleteSpace E] (μ : MeasureTheory.Measure E),
  ProbabilityTheory.covarianceOperator μ =
    InnerProductSpace.continuousLinearMapOfBilin
      ((ProbabilityTheory.uncenteredCovarianceBilinDual μ).bilinearComp
        (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- Convergence a.e. implies convergence in measure in a finite measure space.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_ae : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
      MeasureTheory.TendstoInMeasure μ f Filter.atTop g
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.le_of_inf_neBot : ∀ {α : Type u} (f : Ultrafilter α) {g : Filter α}, (↑f ⊓ g).NeBot → ↑f ≤ g
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_4 : ∀ (f fs : Turing.ToPartrec.Code),
  (f.cons fs).eval = fun v => do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_disjoint_Ioc_of_le : ∀ {α : Type u_2} {a b c : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {d : α},
  b ≤ c → Disjoint (Finset.Ioc a b) (Finset.Ioc c d)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.equivQuotientZPowOfEquiv_trans : ∀ {A B C : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] [inst_2 : CommGroup C] (e : A ≃* B) (d : B ≃* C) (n : ℤ),
  (QuotientGroup.equivQuotientZPowOfEquiv e n).trans (QuotientGroup.equivQuotientZPowOfEquiv d n) =
    QuotientGroup.equivQuotientZPowOfEquiv (e.trans d) n
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff : ∀ {n : ℕ} (S : Finset (Fin (n + 1))) (i : Fin (n + 1)),
  SSet.stdSimplex.obj₀Equiv.symm i ∈ (SSet.stdSimplex.face S).obj (Opposite.op { len := 0 }) ↔ i ∈ S
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_succ : ∀ (n : ℕ), (n + 1).primesBelow = if Nat.Prime n then insert n n.primesBelow else n.primesBelow
-- Init.Data.UInt.BasicAux
/-- Converts a word-sized unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
 -/
USize.toNat : USize → ℕ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instTop.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instTop = { top := { toAddSubgroup := ⊤, isOpen' := ⋯ } }
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.mk.inj : ∀ {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.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.AddMonObj A} {X : D} {addMod : CategoryTheory.AddModObj A X} {X_1 : D}
  {addMod_1 : CategoryTheory.AddModObj A X_1},
  { X := X, addMod := addMod } = { X := X_1, addMod := addMod_1 } → X = X_1 ∧ addMod ≍ addMod_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_bot : ∀ {α : Type u} [inst : AddGroup α], ⊥.toTopologicalSpace = ⊥
-- Init.Data.List.Lemmas
List.getElem?_singleton : ∀ {α : Type u_1} {a : α} {i : ℕ}, [a][i]? = if i = 0 then some a else none
-- Mathlib.Analysis.Fourier.ZMod
ZMod.invDFT_apply : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Ψ : ZMod N → E)
  (k : ZMod N), ZMod.dft.symm Ψ k = (↑N)⁻¹ • ∑ j, ZMod.stdAddChar (j * k) • Ψ j
-- Init.Data.SInt.Lemmas
Int64.toInt_toInt8 : ∀ (x : Int64), x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.cast_rfl_rfl : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path.Homotopic.Quotient x y), γ.cast ⋯ ⋯ = γ
-- Mathlib.Topology.Order.IsLUB
IsGLB.exists_seq_antitone_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} {x : α}
  [(nhds x).IsCountablyGenerated],
  IsGLB t x →
    t.Nonempty → ∃ u, Antitone u ∧ (∀ (n : ℕ), x ≤ u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
-- Mathlib.NumberTheory.FLT.Four
Int.isCoprime_of_sq_sum' : ∀ {r s : ℤ}, IsCoprime r s → IsCoprime (r ^ 2 + s ^ 2) (r * s)
-- Mathlib.Geometry.Euclidean.Sphere.Ptolemy
/-- **Ptolemy’s Theorem**.  -/
EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c d p : P},
  EuclideanGeometry.Cospherical {a, b, c, d} →
    EuclideanGeometry.angle a p c = Real.pi →
      EuclideanGeometry.angle b p d = Real.pi → dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.closure_mul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {t : Set G},
  IsOpen t → ∀ (s : Set G), closure s * t = s * t
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  -Set.Iio a = Set.Ioi (-a)
-- Lean.Data.Lsp.Basic
/-- Identifier for annotated edit.

`WorkspaceEdit` has a `changeAnnotations` field that maps these identifiers to a `ChangeAnnotation`.
By annotating an edit you can add a description of what the edit will do and also control whether the
user is presented with a prompt before applying the edit.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textEdit).
 -/
Lean.Lsp.TextEdit.annotationId? : Lean.Lsp.TextEdit → Option String
-- Lean.Parser.Basic
/-- The name of a declaration which will be used as the target of
go-to-definition queries and from which doc strings will be extracted.
This is a dummy declaration of type `Lean.Parser.Category`
created by `declare_syntax_cat`, but for builtin categories the declaration
is made manually and passed to `registerBuiltinParserAttribute`.  -/
Lean.Parser.ParserCategory.declName : Lean.Parser.ParserCategory → Lean.Name
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.lintegral_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {μ ν : MeasureTheory.Measure M}
  [MeasureTheory.SFinite ν] {f : M → ENNReal},
  Measurable f → ∫⁻ (z : M), f z ∂μ.mconv ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Context.mk : Lean.Meta.Sym.Simp.Config → ℕ → ℕ → Lean.Meta.Sym.Simp.Context
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t₁ t₂ : Set β}, s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
-- Mathlib.Order.Bounds.Basic
isGreatest_himp : ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.coe_bot : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : T1Space E], ↑⊥ = {0}
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_intCast_atBot_cobounded : ∀ {α : Type u_1} [inst : NormedRing α] [NormSMulClass ℤ α] [Nontrivial α],
  Filter.Tendsto Int.cast Filter.atBot (Bornology.cobounded α)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.lift_symm_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (F : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A), QuaternionAlgebra.lift.symm F = (QuaternionAlgebra.Basis.self R).compHom F
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isZeroAt_infty_iff : ∀ {f : UpperHalfPlane → ℂ} {k : ℤ}, OnePoint.infty.IsZeroAt f k ↔ UpperHalfPlane.IsZeroAtImInfty f
-- Mathlib.Order.Circular
/-- **Alias** of `sbtw_trans_right`. -/
SBtw.sbtw.trans_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b d
-- Mathlib.Control.Basic
joinM_map_joinM : ∀ {m : Type u → Type u} [inst : Monad m] [LawfulMonad m] {α : Type u} (a : m (m (m α))),
  joinM (joinM <$> a) = joinM (joinM a)
-- Init.Data.Int.Basic
/-- The canonical homomorphism `Int → R`. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.

`IntCast` and `NatCast` exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent `simp` normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
`IntCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
`IntCast R` instance) whenever `R` is an additive group with a `1`.
 -/
Int.cast : {R : Type u} → [IntCast R] → ℤ → R
-- Lean.Elab.Binders
Lean.Elab.Term.LetConfig.mk.injEq : ∀ (nondep usedOnly zeta postponeValue generalize : Bool) (eq? : Option Lean.Ident)
  (nondep_1 usedOnly_1 zeta_1 postponeValue_1 generalize_1 : Bool) (eq?_1 : Option Lean.Ident),
  ({ nondep := nondep, usedOnly := usedOnly, zeta := zeta, postponeValue := postponeValue, generalize := generalize,
        eq? := eq? } =
      { nondep := nondep_1, usedOnly := usedOnly_1, zeta := zeta_1, postponeValue := postponeValue_1,
        generalize := generalize_1, eq? := eq?_1 }) =
    (nondep = nondep_1 ∧
      usedOnly = usedOnly_1 ∧ zeta = zeta_1 ∧ postponeValue = postponeValue_1 ∧ generalize = generalize_1 ∧ eq? = eq?_1)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_iff_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable b → b ≤ a → (a - b < c ↔ a < c + b)
-- Mathlib.Analysis.CStarAlgebra.Basic
Metric.star_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ),
  star (Metric.ball x r) = Metric.ball (star x) r
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `isClosed_setOfPred_specializes`. -/
isClosed_setOf_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], IsClosed {p | p.1 ⤳ p.2}
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_weightedOrder_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} (n : ℕ),
  n • MvPowerSeries.weightedOrder w f ≤ MvPowerSeries.weightedOrder w (f ^ n)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- [Stacks Tag 09FN](https://stacks.math.columbia.edu/tag/09FN) (Generalized from fields to division rings.) -/
Module.Free.of_divisionRing : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V], Module.Free K V
-- Lean.Data.Lsp.Internal
Lean.Lsp.instOrdRefIdent.ord : Lean.Lsp.RefIdent → Lean.Lsp.RefIdent → Ordering
-- Init.Data.ToString.Basic
instToStringUInt8 : ToString UInt8
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The `G`-valued integral of `E`-valued function and the `F`-valued vector measure `μ` with linear
paring `B : E →L[ℝ] F →L[ℝ] G` . This is set to be `0` if `G` is not complete or if `f` is not
integrable with respect to `(μ.transpose B).variation`. Notation `∫ᵛ x, f x ∂[B; μ]`.

When `μ` is `G`-valued, to get the integral in `G` of a real-valued function, take
`B = ContinousLinearMap.lsmul ℝ ℝ`. Notation `∫ᵛ x, f x ∂•μ`.
When `μ` is a signed measure, to get the integral in `G` of a `G`-valued function, take
`B = (ContinousLinearMap.lsmul ℝ ℝ).flip`. Notation `∫ᵛ x, f x ∂<•μ`.
 -/
MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂[_;_]» : Lean.ParserDescr
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`, unless `a` is a top
element.  -/
closure_Ioi' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Ioi a).Nonempty → closure (Set.Ioi a) = Set.Ici a
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_zero : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F], star (WithConv.toConv 0) = WithConv.toConv 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
-- Mathlib.Computability.Partrec
Nat.Partrec.none : Nat.Partrec fun x => Part.none
-- Mathlib.Topology.Category.TopCat.EpiMono
TopCat.mono_iff_injective : ∀ {X Y : TopCat} (f : X ⟶ Y), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.Convex.PathConnected
Path.range_segment : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b : E), Set.range ⇑(Path.segment a b) = segment ℝ a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.congr_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Algebra.Ring.Defs
/-- Negation is right distributive over multiplication  -/
HasDistribNeg.mul_neg : ∀ {α : Type u_1} {inst : Mul α} [self : HasDistribNeg α] (x y : α), x * -y = -(x * y)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sumIsoExt_hom_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor (A ⊕ B) C}
  (e₁ : (CategoryTheory.Sum.inl_ A B).comp F ≅ (CategoryTheory.Sum.inl_ A B).comp G)
  (e₂ : (CategoryTheory.Sum.inr_ A B).comp F ≅ (CategoryTheory.Sum.inr_ A B).comp G) (a : A),
  (CategoryTheory.Functor.sumIsoExt e₁ e₂).hom.app (Sum.inl a) = e₁.hom.app a
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.anyM.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()