mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Submersion
/-- Given a submersion `f` at `x`, this is a choice of complement which lives in the same universe
as the model space for the domain of `f`: this is useful to avoid universe restrictions.  -/
Manifold.IsSubmersionAtOfComplement.smallComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} → Manifold.IsSubmersionAtOfComplement F I J n f x → Type u
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometry.strictConvexSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [StrictConvexSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F), StrictConvexSpace 𝕜 E
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.X₁ = S.L₀.X₂
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.IsComplete.mk : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv],
  (∀ (s : CauSeq β abv), ∃ b, s ≈ CauSeq.const abv b) → CauSeq.IsComplete β abv
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The image of a splitting of simplicial object by a functor which preserves
finite coproducts  -/
CategoryTheory.SimplicialObject.Splitting.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {X : CategoryTheory.SimplicialObject C} →
          X.Splitting →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.Limits.PreservesFiniteCoproducts F] →
                CategoryTheory.SimplicialObject.Splitting (CategoryTheory.Functor.comp X F)
-- Mathlib.Analysis.Complex.Basic
RCLike.complexRingEquiv_apply : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (x : 𝕜),
  (RCLike.complexRingEquiv h) x = ↑(RCLike.re x) + ↑(RCLike.im x) * Complex.I
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.denote : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Power → α
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.arrow.sizeOf_spec : sizeOf Lean.Meta.LazyDiscrTree.Key.arrow = 1
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.take.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, [] with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_2 n
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Combine a family of multilinear maps with the same domain and codomains `M' i` into a
multilinear map taking values in the space of functions `∀ i, M' i`.  -/
MultilinearMap.pi : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
          [inst_2 : (i : ι) → Module R (M₁ i)] →
            {ι' : Type u_1} →
              {M' : ι' → Type u_2} →
                [inst_3 : (i : ι') → AddCommMonoid (M' i)] →
                  [inst_4 : (i : ι') → Module R (M' i)] →
                    ((i : ι') → MultilinearMap R M₁ (M' i)) → MultilinearMap R M₁ ((i : ι') → M' i)
-- Mathlib.Order.Category.PartOrdEmb
/-- Turn a morphism in `PartOrdEmb` back into a `OrderEmbedding`.  -/
PartOrdEmb.Hom.hom : {X Y : PartOrdEmb} → X.Hom Y → ↑X ↪o ↑Y
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.instNSMul.eq_1 : ∀ {M : Type u_5} [inst : AddMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] (S : A),
  AddSubmonoidClass.instNSMul S = { smul := fun n a => ⟨n • ↑a, ⋯⟩ }
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
/-- Given a set `s` of affine-independent points belonging to an open set `u`, we may extend `s` to
an affine basis, all of whose elements belong to `u`.  -/
IsOpen.exists_between_affineIndependent_span_eq_top : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s u : Set P},
  IsOpen u →
    s ⊆ u →
      s.Nonempty →
        AffineIndependent ℝ Subtype.val → ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobiMatrix_naive : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R} (a : ι → σ)
  (ha : Function.Injective a) (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
  [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i j : ι),
  (Algebra.PreSubmersivePresentation.naive a ha s hs).jacobiMatrix i j = (MvPolynomial.pderiv (a i)) (v j)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.act.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] (a : Turing.TM0.Stmt Γ) (a_1 : Λ),
  sizeOf (Turing.TM0to1.Λ'.act a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.AC
Lean.Data.AC.Expr.toList.eq_2 : ∀ (l r : Lean.Data.AC.Expr), (l.op r).toList = l.toList.append r.toList
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_min : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s t : Set E}, s ⊆ t → AbsConvex 𝕜 t → (absConvexHull 𝕜) s ⊆ t
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.toQuadraticMap_associated : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N),
  ((QuadraticMap.associatedHom S) Q).toQuadraticMap = Q
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointIdIso.eq_1 : ∀ {C₀ : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C₀] {F G : CategoryTheory.Functor C₀ C₀} (adj : F ⊣ G)
  (e : G ≅ CategoryTheory.Functor.id C₀),
  adj.leftAdjointIdIso e = (CategoryTheory.conjugateIsoEquiv CategoryTheory.Adjunction.id adj).symm e.symm
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.neg_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (-x).1 = -x.1
-- Mathlib.RingTheory.ZMod
instIsReducedZModOfFactSquarefreeNat : ∀ {n : ℕ} [Fact (Squarefree n)], IsReduced (ZMod n)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_top : ∀ {G : Type u_1} [inst : AddGroup G], Nat.card ↥⊤ = Nat.card G
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHomClass.toAddMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [inst_3 : AddMonoidHomClass F M N] (f : F), ↑f = { toFun := (↑f).toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Meta.Tactic.Grind.Cases
/-- Returns `true` if `declName` is the name of inductive type/predicate that
even `grind only` case splits on.
Remark: we added support for them to reduce the noise in the tactic generated by
`grind?`
 -/
Lean.Meta.Grind.isBuiltinEagerCases : Lean.Name → Bool
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_inter_distrib_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z_1 : C} (h : Q.complex.X 1 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm)
      (CategoryTheory.CategoryStruct.comp (Q.complex.d 2 1) h) =
    CategoryTheory.CategoryStruct.comp
      (f.f 1 -
        CategoryTheory.CategoryStruct.comp (P.complex.d 1 0)
          (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm))
      h
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofErrorNameInfo.injEq : ∀ (i i_1 : Lean.Elab.ErrorNameInfo), (Lean.Elab.Info.ofErrorNameInfo i = Lean.Elab.Info.ofErrorNameInfo i_1) = (i = i_1)
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.uncurryBilinear_apply : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (m : Fin 2 → E × F),
  f.uncurryBilinear m = (f (m 0).1) (m 1).2
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_inf : ∀ {K : Type u} [inst : DivisionRing K] (p p' : Subfield K), ↑(p ⊓ p') = p.carrier ∩ p'.carrier
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_exchange_iff : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α},
  e ∈ M.closure (insert f X) \ M.closure X ↔ f ∈ M.closure (insert e X) \ M.closure X
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.hasStrictFDerivAt_rightFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (self : ImplicitFunctionData 𝕜 E F G),
  HasStrictFDerivAt self.rightFun self.rightDeriv self.pt
-- Init.Data.UInt.Lemmas
UInt8.ofNat_usizeSize_sub_one : UInt8.ofNat (USize.size - 1) = 255
-- Mathlib.Data.Ordmap.Ordset
/-- O(1). Construct a singleton set containing value `a`.  -/
Ordset.singleton : {α : Type u_1} → [inst : Preorder α] → α → Ordset α
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_one : Cardinal.lift.{u_2, u_1} 1 = 1
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.ofSubtype_swap_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] (x y : Subtype p),
  Equiv.Perm.ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_pos_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ {s : Set α}, 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s)
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.re_inner_nonneg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 x (T x))
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.single.addMonoidHom_apply_coeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (a : Γ) (r : R) (j : Γ),
  ((HahnSeries.single.addMonoidHom a) r).coeff j = Pi.single a r j
-- Mathlib.Algebra.Group.Defs
Group.toDivInvMonoid : {G : Type u} → [self : Group G] → DivInvMonoid G
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.toFun_map : Char.map✝.toFun = Char.ordinal
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  IsClosed (B.polar s)
-- Init.Data.ByteArray.Bootstrap
List.toByteArray.eq_1 : ∀ (bs : List UInt8), bs.toByteArray = List.toByteArray.loop bs ByteArray.empty
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.vecMulBilin.congr_simp : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] [inst_8 : Fintype m],
  Matrix.vecMulBilin R S = Matrix.vecMulBilin R S
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.ext_inv : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) CategoryTheory.Limits.Cofork.ext._auto_1),
  (CategoryTheory.Limits.Cofork.ext i w).inv = CategoryTheory.Limits.Cofork.mkHom i.inv ⋯
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → ∀ (c : β), MeasureTheory.Integrable (fun x => f x • c) μ
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is continuous
at `x₀`, and eventually `a x` satisfies the predicate `p` associated to `𝕜` and has quasispectrum
contained in `s`, then `fun x ↦ cfcₙ f (a x)` is continuous at `x₀`.  -/
ContinuousAt.cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X},
      ContinuousAt a x₀ →
        (∀ᶠ (x : X) in nhds x₀, quasispectrum 𝕜 (a x) ⊆ s) →
          (∀ᶠ (x : X) in nhds x₀, p (a x)) →
            autoParam (ContinuousOn f s) ContinuousAt.cfcₙ._auto_1 →
              autoParam (f 0 = 0) ContinuousAt.cfcₙ._auto_3 → ContinuousAt (fun x => cfcₙ f (a x)) x₀
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pow_rpow_inv_natCast : ∀ {x : ℝ} {n : ℕ}, 0 ≤ x → n ≠ 0 → (x ^ n) ^ (↑n)⁻¹ = x
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of the forward direction of `Matroid.isColoop_iff_sdiff_not_spanning`. -/
Matroid.IsColoop.sdiff_not_spanning : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e → ¬M.Spanning (M.E \ {e})
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.subsingleton_iff : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Subsingleton B], IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}
-- Init.SizeOfLemmas
Char.toNat.eq_1 : ∀ (c : Char), c.toNat = c.val.toNat
-- Mathlib.Algebra.Group.Conj
addConj_nsmul : ∀ {α : Type u} [inst : AddGroup α] {i : ℕ} {a b : α}, i • (a + b + -a) = a + i • b + -a
-- Init.Data.String.Basic
String.Slice.Pos.prevAux_lt_rawEndPos : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prevAux h < s.rawEndPos
-- Init.Prelude
/-- Evaluates a value from monad `m` into monad `n`.  -/
MonadEval.monadEval : {m : semiOutParam (Type u → Type v)} → {n : Type u → Type w} → [self : MonadEval m n] → {α : Type u} → m α → n α
-- Mathlib.RingTheory.FreeCommRing
/-- `is_supported x s` means that all monomials showing up in `x` have variables in `s`.  -/
FreeCommRing.IsSupported : {α : Type u} → FreeCommRing α → Set α → Prop
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal : ∀ {R₁ : Type u_3} [inst : CommRing R₁] (K : Type u_4) [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {I J : Ideal R₁} {x y : R₁} (hy : y ∈ nonZeroDivisors R₁),
  FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (IsLocalization.mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔
    Ideal.span {x} * I = Ideal.span {y} * J
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instInhabited : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Inhabited (Derivation R A M)
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instAddGroupWithOne : {R : Type u_1} → [AddGroupWithOne R] → AddGroupWithOne Rᵒᵈ
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.toFractionRing_injective : ∀ {K : Type u} [inst : CommRing K], Function.Injective RatFunc.toFractionRing
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_smul_measure_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {c : ENNReal}, c ≠ 0 → (AEMeasurable f (c • μ) ↔ AEMeasurable f μ)
-- Lean.Environment
Lean.Kernel.Exception.declHasFVars.inj : ∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {expr : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {name_1 : Lean.Name} {expr_1 : Lean.Expr},
  Lean.Kernel.Exception.declHasFVars env name expr = Lean.Kernel.Exception.declHasFVars env_1 name_1 expr_1 →
    env = env_1 ∧ name = name_1 ∧ expr = expr_1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_positive : ∀ (R : Type u_1) (E : Type u_2) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : PartialOrder E] [inst_5 : IsOrderedAddMonoid E] [inst_6 : Module R E]
  [inst_7 : PosSMulMono R E], ↑(PointedCone.positive R E) = Set.Ici 0
-- Mathlib.Topology.Algebra.Constructions
AddUnits.continuous_val : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Continuous AddUnits.val
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_toAddSubmonoid : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ), H.unop.toAddSubmonoid = H.unop
-- Mathlib.Algebra.Algebra.Basic
Module.IsTorsionFree.trans_faithfulSMul : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [FaithfulSMul R A] [Nontrivial R] [IsCancelMulZero A] [inst_6 : AddCommMonoid M] [inst_7 : Module A M]
  [inst_8 : Module R M] [Module.IsTorsionFree A M] [IsScalarTower R A M], Module.IsTorsionFree R M
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_union_Ioc_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  a ≤ b → b ≤ c → Finset.Ioc a b ∪ Finset.Ioc b c = Finset.Ioc a c
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.instDecidableEq : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → DecidableEq (Monoid.CoprodI.Word M)
-- Mathlib.Algebra.Order.Star.Basic
/-- A class to encode that self-adjoint elements may be expressed as the
difference of nonnegative elements. This is satisfied by any type with a
`NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint` instance.
However, it can also be satisfied by continuous linear functionals equipped
with the intrinsic star operation.

This type class can be used to guarantee `PositiveLinearMap` is a `StarHomClass`.  -/
SelfAdjointDecompose : (R : Type u_3) → [AddGroup R] → [Star R] → [PartialOrder R] → Prop
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- Any `1`-separated set in the ball of radius `2` has cardinality at most `5 ^ dim`. This is
useful to show that the supremum in the definition of `Besicovitch.multiplicity E` is
well behaved.  -/
Besicovitch.card_le_of_separated : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Finset E),
  (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) → s.card ≤ 5 ^ Module.finrank ℝ E
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.mk : Option Lean.Lsp.Range → Lean.Lsp.DocumentUri → Lean.Lsp.Range → Lean.Lsp.Range → Lean.Lsp.LocationLink
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLp.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) (p : ENNReal)
  [inst_4 : Fact (1 ≤ p)], StrongDual.toLp μ p = { toLinearMap := StrongDual.toLpₗ μ p, cont := ⋯ }
-- Aesop.Forward.State
/-- Find hyps in `slot` whose substitutions are compatible with `subst`.
Precondition: `slot.common` is nonempty and each variable contained in it is
also contained in `subst`.  -/
Aesop.VariableMap.findHyps : Aesop.VariableMap → Aesop.Slot → Aesop.Substitution → Aesop.BaseM (Std.HashSet Aesop.Hyp)
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.snoc : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X}
  {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s₁) x₁}
  {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s₂) x₂},
  s₁.Equivalent s₂ →
    JordanHolderLattice.Iso (RelSeries.last s₁, x₁) (RelSeries.last s₂, x₂) →
      CompositionSeries.Equivalent (RelSeries.snoc s₁ x₁ hsat₁) (RelSeries.snoc s₂ x₂ hsat₂)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.add.match_1.eq_1 : ∀ (motive : ONote → ONote → Sort u_1) (o : ONote) (h_1 : (o : ONote) → motive ONote.zero o)
  (h_2 : (e : ONote) → (n : ℕ+) → (a o : ONote) → motive (e.oadd n a) o),
  (match ONote.zero, o with
    | ONote.zero, o => h_1 o
    | e.oadd n a, o => h_2 e n a o) =
    h_1 o
-- Mathlib.Algebra.Module.Presentation.Finite
Module.Presentation.finitePresentation : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (pres : Module.Presentation A M) [Finite pres.G] [Finite pres.R], Module.FinitePresentation A M
-- Mathlib.Algebra.Order.Kleene
add_eq_left_iff_le : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, a + b = a ↔ b ≤ a