mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffsIn_mul : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (M N : Submodule R S), MvPolynomial.coeffsIn σ (M * N) = MvPolynomial.coeffsIn σ M * MvPolynomial.coeffsIn σ N
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_1.eq_3 : ∀ {α α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m (Std.IterM m β)]
  {it₁ : Std.IterM m (Std.IterM m β)} (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (it₂' : Std.IterM m β) →
        (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂')) → motive ⟨Std.IterStep.yield it₁' it₂', h⟩)
  (h_2 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' it₂', h⟩ => h_1 it₁' it₂' h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.natCast_mul_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a => ↑n * a
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.tmul_mul_tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] (a₁ a₂ : A) (b₁ b₂ : B), a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_one : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.cycleFactorsFinset 1 = ∅
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M N : Submodule R A)
  {A' : Type u_1} [inst_3 : Semiring A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `S` is non-trivial and `R`-standard smooth of relative dimension, `Ω[S⁄R]` is a free
`S`-module of rank `n`.  -/
Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial S] (n : ℕ)
  [Algebra.IsStandardSmoothOfRelativeDimension n R S], Module.rank S Ω[S⁄R] = ↑n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropPrefix?_eq_map_skipPrefix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.dropPrefix? pat = Option.map s.sliceFrom (s.skipPrefix? pat)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesMonomorphisms.of_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesMonomorphisms] (f : G ⟶ F) [∀ (X : C), CategoryTheory.Mono (f.app X)],
  G.PreservesMonomorphisms
-- Mathlib.MeasureTheory.Measure.Prod
/-- **Tonelli's Theorem**: For `ℝ≥0∞`-valued almost everywhere measurable functions on `α × β`,
the integral of `f` is equal to the iterated integral.  -/
MeasureTheory.lintegral_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × β → ENNReal),
  AEMeasurable f (μ.prod ν) → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- An equivalence of the index set defines a linear isometric equivalence between the spaces
of multilinear maps.  -/
ContinuousMultilinearMap.domDomCongrₗᵢ : (𝕜 : Type u) →
  {ι : Type v} →
    {ι' : Type v'} →
      (G : Type wG) →
        (G' : Type wG') →
          [inst : Fintype ι] →
            [inst_1 : Fintype ι'] →
              [inst_2 : NontriviallyNormedField 𝕜] →
                [inst_3 : NormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : NormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        ι ≃ ι' →
                          ContinuousMultilinearMap 𝕜 (fun x => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => G) G'
-- Mathlib.Lean.Meta.Simp
/-- Construct a `Simp.Context` from a list of names.  -/
Lean.Meta.Simp.Context.ofNames : optParam (List Lean.Name) [] →
  optParam Bool false → optParam Lean.Meta.Simp.Config { } → Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Order.Filter.Pointwise
Filter.pureAddMonoidHom_apply : ∀ {α : Type u_2} [inst : AddZeroClass α] (a : α), Filter.pureAddMonoidHom a = pure a
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the centroid lies in the affine
span if the number of points is not zero.  -/
centroid_mem_affineSpan_of_card_ne_zero : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P),
  s.card ≠ 0 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ : ∀ {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) [inst_4 : F.Monoidal] (X Y : C) (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) T)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) T) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) T)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.equiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β)
  (K : TopologicalSpace.Compacts β),
  (TopologicalSpace.Compacts.equiv f).symm K = TopologicalSpace.Compacts.map ⇑f.symm ⋯ K
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.coe_smul : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β] (g : G) (f : α ↪ β),
  ⇑(g • f) = g • ⇑f
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansionFormalMultilinearSeries_apply_norm : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ),
  ‖UpperHalfPlane.qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)‖
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual
to `adjunctionOfEquivLeft`.  -/
CategoryTheory.Adjunction.adjunctionOfEquivRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G_obj : D → C} →
            (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) →
              (he :
                  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
                    (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) =
                      CategoryTheory.CategoryStruct.comp f ((e X Y) g)) →
                F ⊣ CategoryTheory.Adjunction.rightAdjointOfEquiv e he
-- Lean.Linter.UnusedVariables
/-- Returns true if this is a message produced by the unused variable linter.
This is used to give these messages an additional "faded" style in the editor.  -/
Lean.MessageData.isUnusedVariableWarning : Lean.MessageData → Bool
-- Mathlib.Tactic.ApplyWith
_private.Mathlib.Tactic.ApplyWith.0.Mathlib.Tactic.elabApplyConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.ApplyConfig
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Left.neg_of_mul_neg_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α], a * b < 0 → 0 ≤ a → b < 0
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.chromaticNumber_eq_sInf : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n → G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})
-- Mathlib.Algebra.Group.UniqueProds.Basic
Prod.instUniqueSums : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] [UniqueSums G] [UniqueSums H], UniqueSums (G × H)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.pow_succ_lt_pow : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A} [P_prime : P.IsPrime],
  P ≠ ⊥ → ∀ (i : ℕ), P ^ (i + 1) < P ^ i
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_zero : ∀ {α : Type u_1} (a : α), Multiset.replicate 0 a = 0
-- Mathlib.Algebra.Module.SpanRankOperations
IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Submodule.spanFinrank (IsLocalRing.maximalIdeal R) =
    Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''},
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (φ.comp τ) =
    CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight
          (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) τ)
        (ψ'.associator φ τ).hom)
-- Mathlib.Analysis.Matrix.Order
Matrix.le_iff : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] {A B : Matrix n n 𝕜}, A ≤ B ↔ (B - A).PosSemidef
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Quotients of locally path-connected spaces are locally path-connected.  -/
Topology.IsQuotientMap.locallyPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  {f : X → Y}, Topology.IsQuotientMap f → LocallyPathConnectedSpace Y
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
/-- Applies the given variable permutation to the given expression constraint.  -/
Nat.Internal.Linear.ExprCnstr.applyPerm : Lean.Perm → Nat.Internal.Linear.ExprCnstr → Nat.Internal.Linear.ExprCnstr
-- Lean.Elab.Command
Lean.Elab.Command.Context.ref : Lean.Elab.Command.Context → Lean.Syntax
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion : ∀ {X : AlgebraicGeometry.Scheme} [self : X.IsQuasiAffine], AlgebraicGeometry.IsImmersion X.toSpecΓ
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.Rel.smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R}
  {a : M}, TensorAlgebra.Rel R M (FreeAlgebra.ι R (r • a)) ((algebraMap R (FreeAlgebra R M)) r * FreeAlgebra.ι R a)
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convMul_apply : ∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C] (f g : WithConv (C →ₗ[R] A)) (c : C),
  (f * g).ofConv c = (LinearMap.mul' R A) ((TensorProduct.map f.ofConv g.ofConv) (CoalgebraStruct.comul c))
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.ncard_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G}, Subgroup.IsComplement (↑H) T → T.ncard = H.index
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.mk : ∀ {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} {p : P} {as : AffineSubspace ℝ P},
  p ∈ s → p ∈ as → as ≤ s.orthRadius p → s.IsTangentAt p as
-- Mathlib.Algebra.Group.Defs
DivisionMonoid.toDivInvMonoid : {G : Type u} → [self : DivisionMonoid G] → DivInvMonoid G
-- Mathlib.Data.Nat.Pairing
Nat.unpair_left_le : ∀ (n : ℕ), (Nat.unpair n).1 ≤ n
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_iff_infinitesimal_inv : ∀ {x : ℝ*}, x ≠ 0 → (x.Infinite ↔ x⁻¹.Infinitesimal)
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- See also `Ergodic.ae_empty_or_univ_of_image_ae_le`.  -/
Ergodic.ae_empty_or_univ_of_image_ae_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → f '' s ≤ᵐ[μ] s → μ s ≠ ⊤ → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Algebra.Group.Indicator
Set.indicator_union_of_notMem_inter : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {s t : Set α} {a : α},
  a ∉ s ∩ t → ∀ (f : α → M), (s ∪ t).indicator f a = s.indicator f a + t.indicator f a
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodCongr_apply : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N'),
  ⇑(e.coprodCongr e') = ⇑(Monoid.Coprod.map ↑e ↑e')
-- Init.Data.Array.Lex.Lemmas
Array.instReflLeOfIrreflLt : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Refl fun x1 x2 => x1 ≤ x2
-- Plausible.Shrinkable
Plausible.Prod.shrinkable : {α : Type u_1} →
  {β : Type u_2} → [shrA : Plausible.Shrinkable α] → [shrB : Plausible.Shrinkable β] → Plausible.Shrinkable (α × β)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_dite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι)
  (b : (x : ι) → x = a → M), (∑ x ∈ s, if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological_var : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] (a : M),
  (Module.Presentation.tautological A M).var a = a
-- Mathlib.Data.Set.Card
Set.ncard_subtype : ∀ {α : Type u_1} (P : α → Prop) (s : Set α), {x | ↑x ∈ s}.ncard = (s ∩ Set.ofPred P).ncard
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, t.contains a = false → t.getKey! a = default
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_not_measurable : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {i : Set α}, ¬MeasurableSet i → v.restrict i = 0
-- Lean.Meta.Check
Lean.Meta.throwAppTypeMismatch : {α : Type} → Lean.Expr → Lean.Expr → Lean.MetaM α
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabSimpConfigCtx.unsafe_impl_2 : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.ConfigCtx
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft_pos : ∀ (a b : ℕ), 0 < a.factorizationLCMLeft b
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_smul_not_lt : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  (r : R) (x : HahnSeries Γ V), ¬(r • x).orderTop < x.orderTop
-- Mathlib.Data.Quot
/-- Lift a constant function on `q : Trunc α`.  -/
Trunc.liftOn : {α : Sort u_1} → {β : Sort u_2} → Trunc α → (f : α → β) → (∀ (a b : α), f a = f b) → β
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.mem_domain : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  {x : M} {c : FiniteArchimedeanClass M}, x ∈ seed.stratum c → x ∈ (↑f).domain
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- See `le_expGrowthSup_mul'` for a version with swapped argument `u` and `v`.  -/
ExpGrowth.le_expGrowthSup_mul : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthSup u + ExpGrowth.expGrowthInf v ≤ ExpGrowth.expGrowthSup (u * v)
-- Init.Data.Array.Basic
Array.getElem!_toList : ∀ {α : Type u} [inst : Inhabited α] {xs : Array α} {i : ℕ}, xs.toList[i]! = xs[i]!
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_mul : ∀ {α : Type u_2} {x : NonAssocSemiring α} (f g : α →+* α), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.QuasiCompact @AlgebraicGeometry.QuasiSeparated
-- Mathlib.Order.Monotone.Basic
StrictMono.cmp_map_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictMono f → ∀ (x y : α), cmp (f x) (f y) = cmp x y
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.sub : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, s.Finite → t.Finite → (s - t).Finite
-- Mathlib.Analysis.CStarAlgebra.Spectrum
IsStarNormal.spectralRadius_eq_nnnorm : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A) [IsStarNormal a], spectralRadius ℂ a = ↑‖a‖₊
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.cocone`.

---

For any object `J : CardinalDirectedPoset κ`, this is a colimit
cocone exhibiting `J` as the colimit of its subsets
that are of cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalFilteredPoset.cocone : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet J.PropSet)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_smul_nnreal_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G) (c : NNReal), ∫ (x : α), f x ∂c • μ = c • ∫ (x : α), f x ∂μ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instReprSolverTerms : Repr Lean.Meta.Grind.SolverTerms
-- Mathlib.RingTheory.NormalClosure
/-- The normal closure of an extension of domains `R ⊆ S`. It is defined as a domain `T` such that
`R ⊆ S ⊆ T` and `Frac T / Frac R` is Galois.  -/
Ring.NormalClosure : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] → [IsDomain S] → [inst_4 : Algebra R S] → [Module.IsTorsionFree R S] → Type u_2
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (toNatTrans : CategoryTheory.NatTrans M.toFunctor N.toFunctor)
  (app_ε :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadHom.app_ε._autoParam)
  (app_δ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X))))
      CategoryTheory.ComonadHom.app_δ._autoParam)
  (toNatTrans_1 : CategoryTheory.NatTrans M.toFunctor N.toFunctor)
  (app_ε_1 :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans_1.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadHom.app_ε._autoParam)
  (app_δ_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toNatTrans_1.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (toNatTrans_1.app (M.obj X)) (N.map (toNatTrans_1.app X))))
      CategoryTheory.ComonadHom.app_δ._autoParam),
  ({ toNatTrans := toNatTrans, app_ε := app_ε, app_δ := app_δ } =
      { toNatTrans := toNatTrans_1, app_ε := app_ε_1, app_δ := app_δ_1 }) =
    (toNatTrans = toNatTrans_1)
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_eq_range : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  1 = (Algebra.linearMap R A).range
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (s : UpperSet (MulArchimedeanClass M)),
  MulArchimedeanClass.subgroup s =
    if hs : s = ⊤ then ⊥
    else
      let __src := MulArchimedeanClass.subsemigroup s;
      { toSubsemigroup := __src, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.rename_esymmAlgHom : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : Fintype τ]
  (e : σ ≃ τ),
  (↑(MvPolynomial.renameSymmetricSubalgebra e)).comp (MvPolynomial.esymmAlgHom σ R n) = MvPolynomial.esymmAlgHom τ R n
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.Std.Slice.Internal.ByteSliceData.mk.sizeOf_spec : ∀ (byteArray : ByteArray) (start stop : ℕ) (start_le_stop : start ≤ stop)
  (stop_le_size_byteArray : stop ≤ byteArray.size),
  sizeOf
      { byteArray := byteArray, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_size_byteArray := stop_le_size_byteArray } =
    1 + sizeOf byteArray + sizeOf start + sizeOf stop + sizeOf start_le_stop + sizeOf stop_le_size_byteArray
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.getAnchor : Lean.Expr → Lean.Meta.Grind.GrindM UInt64
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f ↔ ∃ n > 0, Function.IsPeriodicPt f n x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.eq_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) (t : ↑unitInterval) {x : X}, x ∈ S → F (t, x) = f₀ x