mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lattice.Congruence
LatticeCon.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : SizeOf α] (toSetoid : Setoid α)
  (inf : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊓ y) (x ⊓ z))
  (sup : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊔ y) (x ⊔ z)),
  sizeOf { toSetoid := toSetoid, inf := inf, sup := sup } = 1 + sizeOf toSetoid
-- Mathlib.Combinatorics.Quiver.Path
/-- Composition of paths.  -/
Quiver.Path.comp : {V : Type u} → [inst : Quiver V] → {a b c : V} → Quiver.Path a b → Quiver.Path b c → Quiver.Path a c
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabEnsureTypeOf : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.Nilpotent.Exp
Module.End.commute_exp_left_of_commute : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module ℚ M] [inst_6 : Module ℚ N] {fM : Module.End R M}
  {fN : Module.End R N} {g : M →ₗ[R] N},
  IsNilpotent fM → IsNilpotent fN → fN ∘ₗ g = g ∘ₗ fM → IsNilpotent.exp fN ∘ₗ g = g ∘ₗ IsNilpotent.exp fM
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of the reverse direction of `commute_star_comm`. -/
Commute.star_left : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute x (star y) → Commute (star x) y
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.rnDeriv_conv' : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SigmaFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [MeasureTheory.SigmaFinite ν₁] [MeasureTheory.SigmaFinite ν₂],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ → (ν₁.conv ν₂).rnDeriv μ =ᵐ[μ] MeasureTheory.lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautologicalRelations_relation : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (x : Module.Presentation.tautological.R A M),
  (Module.Presentation.tautologicalRelations A M).relation x =
    match x with
    | Module.Presentation.tautological.R.add m₁ m₂ => ((fun₀ | m₁ => 1) + fun₀ | m₂ => 1) - fun₀ | m₁ + m₂ => 1
    | Module.Presentation.tautological.R.smul a m => (a • fun₀ | m => 1) - fun₀ | a • m => 1
-- Batteries.Data.List.Lemmas
List.modify_eq_set_getElem? : ∀ {α : Type u_1} (f : α → α) (n : ℕ) (l : List α), l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
CategoryTheory.Limits.colimit_eq_iff : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4}
  [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_3 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J C)
  [CategoryTheory.IsFilteredOrEmpty J] [inst_6 : CategoryTheory.Limits.HasColimit F] {i j : J}
  {xi : CategoryTheory.ToType (F.obj i)} {xj : CategoryTheory.ToType (F.obj j)},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) xi =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) xj ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getLTInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isIso_pOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.prev j = i → K.d i j = 0 → ∀ [inst_2 : K.HasHomology j], CategoryTheory.IsIso (K.pOpcycles j)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (self : S₁.Hom S₂) (n : ℕ) {Z : C} (h : S₂.X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S₁.s.ι n)
      (CategoryTheory.CategoryStruct.comp (self.F.app (Opposite.op { len := n })) h) =
    CategoryTheory.CategoryStruct.comp (self.f n) (CategoryTheory.CategoryStruct.comp (S₂.s.ι n) h)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [inst_1 : IsDomain R] [inst_2 : NeZero ↑n],
  { val := (Polynomial.cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R
-- Mathlib.Algebra.Group.Pi.Units
Pi.isAddUnit_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] {x : (i : ι) → M i},
  IsAddUnit x ↔ ∀ (i : ι), IsAddUnit (x i)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The functor `F.DescentData' sq sq₃ ⥤ F.DescentData f`.  -/
CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)) →
                (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) →
                  CategoryTheory.Functor (F.DescentData' sq sq₃) (F.DescentData f)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.error? : Lean.ParseImports.State → Option String
-- Lean.Parser.Basic
Lean.Parser.hygieneInfoNoAntiquot : Lean.Parser.Parser
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- The map taking a space to its compact coherentification.  -/
CompactCoherentification.mk : (X : Type u_1) → X ≃ CompactCoherentification X
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_neg_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.S R (-n - 2) = -Polynomial.Chebyshev.S R n
-- Init.Data.UInt.Lemmas
UInt64.eq_of_toFin_eq : ∀ {a b : UInt64}, a.toFin = b.toFin → a = b
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) →
    ∀ (a b : M), f a * f b + f b * f a = (algebraMap R A) (QuadraticMap.polar (⇑Q) a b)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An embedding from a topological space to a pseudometric space is an isometry with respect to the
induced pseudometric space structure on the source space.  -/
Topology.IsEmbedding.to_isometry : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β}
  (h : Topology.IsEmbedding f), Isometry f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Mathlib.GroupTheory.ResiduallyFinite
Group.residuallyFinite_iff_exists_finiteIndexNormalSubgroup : ∀ {G : Type u_1} [inst : Group G], Group.ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Noncomputable model function returning the end point of the longest match starting at the given
position, or `none` if there is no match.
 -/
String.Slice.Pattern.Model.matchAt? : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Option s.Pos
-- Std.Time.Zoned.Database.TzIf
/-- The array indicating whether each transition time uses universal time or local time.
 -/
Std.Time.TimeZone.TZif.TZifV1.utLocalIndicators : Std.Time.TimeZone.TZif.TZifV1 → Array Bool
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The composition for the `J ⥤ V`-enrichment of the category `J ⥤ C`.  -/
CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ F₃ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                    [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃] →
                      [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃] →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj
                            (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
                            (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₂ F₃) ⟶
                          CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₃
-- Mathlib.Algebra.Free
FreeSemigroup.instSemigroup : {α : Type u} → Semigroup (FreeSemigroup α)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.isIso_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.unop
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_subset_range_lift : ∀ {α : Type u} {β : Type v} (f : α → β),
  ∀ s ⊆ Set.range f, Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s))
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.parse : Lean.Syntax → Lean.MVarId → Lean.Elab.TermElabM Aesop.Frontend.TacticConfig
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.nil : ∀ (R : Type u_1) (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  RingTheory.Sequence.IsWeaklyRegular M []
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_eq_sqrt_norm_inner_self : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] (x : E), ‖x‖ = √‖inner A x x‖
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatTrans_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G H : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] [inst_4 : H.IsContinuous J K] (α : F ⟶ G) (β : G ⟶ H)
  (φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S),
  SheafOfModules.pushforwardNatTrans φ (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pushforwardNatTrans φ β)
      (CategoryTheory.CategoryStruct.comp
        (SheafOfModules.pushforwardNatTrans
          (CategoryTheory.CategoryStruct.comp φ
            ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans β RingCat J K).app S))
          α)
        (SheafOfModules.pushforwardCongr ⋯).hom)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- A finite group action is always properly discontinuous.  -/
Finite.to_properlyDiscontinuousSMul : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T] [Finite Γ],
  ProperlyDiscontinuousSMul Γ T
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.eventually : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x → ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFPowerSeriesOnBall f p x r
-- Mathlib.Data.Fintype.Option
/-- If `Option α` is a `Fintype` then so is `α`  -/
fintypeOfOption : {α : Type u_3} → [Fintype (Option α)] → Fintype α
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_of_gt'_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) (x : S.obj (Opposite.op { len := n + 1 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S (j.castLT ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S (i.pred ⋯))) x)
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_mul : ∀ {p q : ℚ}, 0 ≤ p → (p * q).toNNRat = p.toNNRat * q.toNNRat
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to M.  -/
OrderMonoidHom.fst : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → α × β →*o α
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instIsScalarTower_circle : IsScalarTower Circle Complex.UnitDisc Complex.UnitDisc
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.of_comp_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D),
  (CategoryTheory.FreeGroupoid.of C).comp (CategoryTheory.FreeGroupoid.map F) =
    F.comp (CategoryTheory.FreeGroupoid.of D)
-- Mathlib.Logic.Equiv.Defs
Equiv.rightInverse_symm : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ⇑f.symm ⇑f
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- There is a unique path from the root to any other vertex.  -/
Quiver.Arborescence.uniquePath : {V : Type u} →
  {inst : Quiver V} → [self : Quiver.Arborescence V] → (b : V) → Unique (Quiver.Path Quiver.Arborescence.root b)
-- Mathlib.Data.List.Intervals
/-- `Ico n m` is the list of natural numbers `n ≤ x < m`.
(Ico stands for "interval, closed-open".)

See also `Mathlib/Order/Interval/Basic.lean` for modelling intervals in general preorders, as well
as sibling definitions alongside it such as `Set.Ico`, `Multiset.Ico` and `Finset.Ico`
for sets, multisets and finite sets respectively.
 -/
List.Ico : ℕ → ℕ → List ℕ
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffAt I I' n f x → ContMDiffWithinAt I I' n f s x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound.  -/
MeasureTheory.tendsto_of_integral_tendsto_of_monotone : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    MeasureTheory.Integrable F μ →
      Filter.Tendsto (fun i => ∫ (a : α), f i a ∂μ) Filter.atTop (nhds (∫ (a : α), F a ∂μ)) →
        (∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) →
          (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) →
            ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
-- Lean.LocalContext
Lean.LocalDecl.hasExprMVar : Lean.LocalDecl → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItemTag.default : Lean.Lsp.CompletionItemTag
-- Mathlib.Analysis.InnerProductSpace.Trace
InnerProductSpace.trace_rankOne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (x y : E), (LinearMap.trace 𝕜 E) ↑(((InnerProductSpace.rankOne 𝕜) x) y) = inner 𝕜 y x
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- Every irreducible polynomial can be contracted to a separable polynomial.  -/
Irreducible.hasSeparableContraction : ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hF : ExpChar F q] {f : Polynomial F},
  Irreducible f → Polynomial.HasSeparableContraction q f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedCounters.default : Lean.Meta.Grind.Counters
-- Mathlib.Algebra.Group.Commute.Defs
IsLeftRegular.commute_mul_left_iff : ∀ {S : Type u_3} [inst : Semigroup S] {a b : S}, IsLeftRegular a → (Commute (a * b) a ↔ Commute a b)
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressMarkupContentFast : String → Lean.Lsp.MarkupContent → String
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Construct a cocone on `F` from an object of the category `(F ↓ Δ)`. This is part of an
equivalence, see `Cocone.equivStructuredArrow`.  -/
CategoryTheory.Limits.Cocone.fromStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Functor (CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J))
            (CategoryTheory.Limits.Cocone F)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- If `f : 𝒜 →+*ᵍ ℬ` is a graded ring homomorphism and `I` is a prime ideal of `A` and
`J` is a prime ideal of `B` and `f⁻¹ J = I` then we have a map `AtPrime 𝒜 I →+* AtPrime ℬ J`.  -/
HomogeneousLocalization.localRingHom : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} →
                  [inst_5 : GradedRing 𝒜] →
                    {B : Type u_4} →
                      {τ : Type u_5} →
                        [inst_6 : CommRing B] →
                          [inst_7 : SetLike τ B] →
                            [inst_8 : AddSubgroupClass τ B] →
                              {ℬ : ι → τ} →
                                [inst_9 : GradedRing ℬ] →
                                  (f : 𝒜 →+*ᵍ ℬ) →
                                    (I : Ideal A) →
                                      [inst_10 : I.IsPrime] →
                                        (J : Ideal B) →
                                          [inst_11 : J.IsPrime] →
                                            I = Ideal.comap f J →
                                              HomogeneousLocalization.AtPrime 𝒜 I →+*
                                                HomogeneousLocalization.AtPrime ℬ J
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- **The Radon-Nikodym theorem**: Given two measures `μ` and `ν`, if
`HaveLebesgueDecomposition μ ν`, then `μ` is absolutely continuous to `ν` if and only if
`ν.withDensity (rnDeriv μ ν) = μ`.  -/
MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν ↔ ν.withDensity (μ.rnDeriv ν) = μ
-- Mathlib.RingTheory.IsTensorProduct
/-- Algebra version of `IsPushout.cancelBaseChange`.  -/
Algebra.IsPushout.cancelBaseChangeAlg : (R : Type u_1) →
  (S : Type v₃) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (A : Type u_8) →
            (B : Type u_9) →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [Algebra.IsPushout R S A B] →
                                (C : Type u_11) →
                                  [inst_12 : CommRing C] →
                                    [inst_13 : Algebra R C] →
                                      [inst_14 : Algebra A C] →
                                        [IsScalarTower R A C] → TensorProduct A B C ≃ₐ[S] TensorProduct R S C
-- Lean.Meta.ForEachExpr
/-- Remove user facing name for metavariables in `toReset`.
This a low-level method for "undoing" the effect of `setMVarUserNamesAt`
 -/
Lean.Meta.resetMVarUserNames : Array Lean.MVarId → Lean.MetaM Unit
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_eq_of_isFractionRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] (K : Type u_4) (L : Type u_5) [inst_6 : Field K]
  [inst_7 : Field L] [inst_8 : Algebra (R ⧸ p) K] [IsFractionRing (R ⧸ p) K] [inst_10 : Algebra (S ⧸ q) L]
  [IsFractionRing (S ⧸ q) L] [inst_12 : Algebra R K] [IsScalarTower R (R ⧸ p) K] [inst_14 : Algebra S L]
  [IsScalarTower S (S ⧸ q) L] [inst_16 : Algebra R L] [IsScalarTower R S L] [inst_18 : Algebra K L]
  [IsScalarTower R K L], q.inertiaDeg R = Module.finrank K L
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_nonpos : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {n : ℤ}, ↑n ≤ 0 ↔ n ≤ 0
-- Mathlib.Order.UpperLower.Prod
UpperSet.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : UpperSet α) (t : UpperSet β),
  ↑(s ×ˢ t) = ↑s ×ˢ ↑t
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), f.toFun = ⇑f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_piCurry : ∀ {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8}
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], Measurable ⇑(Equiv.piCurry X)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Algebra.Group.Conj
ConjClasses.mem_carrier_mk : ∀ {α : Type u} [inst : Monoid α] {a : α}, a ∈ (ConjClasses.mk a).carrier