mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- If `(V, t, r)` is a `logSizeBallStruct` then `logSizeBallStruct.ball`
is `{x ∈ V | d(t, x) ≤ rc}`.  -/
PairReduction.logSizeBallStruct.ball : {T : Type u_1} → [PseudoEMetricSpace T] → PairReduction.logSizeBallStruct T → ENNReal → Finset T
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The category of sheaves on `X.AffineZariskiSite` is equivalent to the categories of sheaves
over `X`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.sheafEquiv : {X : AlgebraicGeometry.Scheme} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} A] →
      [∀ (U : X.Opensᵒᵖ),
            CategoryTheory.Limits.HasLimitsOfShape
              (CategoryTheory.StructuredArrow U (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op) A] →
        CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X) A ≌
          TopCat.Sheaf A ↑X.toPresheafedSpace
-- Lean.ToExpr
Lean.instToExprInt64 : Lean.ToExpr Int64
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Equiv.ofAddMonoidHom.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G} (f : E →+ E')
  (comp_inl : f.comp S.inl = S'.inl) (rightHom_comp : S'.rightHom.comp f = S.rightHom),
  AddGroupExtension.Equiv.ofAddMonoidHom f comp_inl rightHom_comp =
    { toFun := (↑f).toFun,
      invFun := fun e' =>
        have e := Function.surjInv ⋯ (S'.rightHom e');
        e + S.inl (Function.invFun (⇑S'.inl) (-f e + e')),
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Lean.Meta.Basic
Lean.Meta.Cache.synthInstance : Lean.Meta.Cache → Lean.Meta.SynthInstanceCache
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithScott α)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instIsBotOneClass : ∀ {M : Type u_1} [inst : CommMonoid M], IsBotOneClass (Associates M)
-- Aesop.Options.Public
Aesop.instReprOptions : Repr Aesop.Options
-- Mathlib.Topology.Closure
self_sdiff_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), s \ frontier s = interior s
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Continuity of interval integral with respect to a parameter, at a point within a set.
Given `F : X → ℝ → E`, assume `F x` is ae-measurable on `[a, b]` for `x` in a
neighborhood of `x₀` within `s` and at `x₀`, and assume it is bounded by a function integrable
on `[a, b]` independent of `x` in a neighborhood of `x₀` within `s`. If `(fun x ↦ F x t)`
is continuous at `x₀` within `s` for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`.  -/
intervalIntegral.continuousWithinAt_of_dominated_interval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3}
  [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ}
  {s : Set X},
  (∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousWithinAt (fun x => F x t) s x₀) →
          ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsLeftCancelAdd` across an `Equiv`  -/
Equiv.isLeftCancelAdd : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] [IsLeftCancelAdd β], IsLeftCancelAdd α
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram'.mk : CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton → LightDiagram'
-- Lean.Elab.Tactic.Try
/-- Erases duplicate tactics from `s`.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.removeDuplicates : Array (Lean.TSyntax `tactic) → Array (Lean.TSyntax `tactic)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.liftLevelM : {α : Type} → Lean.Elab.Level.LevelElabM α → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsSMulApplyInt : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsSMulApply ℤ (SchwartzMap E F) E F
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_inv_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
      CategoryTheory.Limits.coprod.inr.unop =
    CategoryTheory.Limits.prod.snd
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An equivalence of categories lifts to an equivalence of their additive monoid objects.  -/
CategoryTheory.Equivalence.mapAddMon : {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] →
            (e : C ≌ D) →
              [inst_4 : e.functor.Monoidal] →
                [inst_5 : e.inverse.Monoidal] → [e.IsMonoidal] → CategoryTheory.AddMon C ≌ CategoryTheory.AddMon D
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit.congr_simp : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (Y : D),
  L.isPointwiseRightKanExtensionRanCounit F Y = L.isPointwiseRightKanExtensionRanCounit F Y
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.toAddSubmonoid_eq_top : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S : NonUnitalSubsemiring R}, S.toAddSubmonoid = ⊤ ↔ S = ⊤
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.sepByIndentSemicolon.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
ArithmeticFunction.liouville_apply_one : ArithmeticFunction.liouville 1 = 1
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.comm_trans_rid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M = TensorProduct.lid R M
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.curry_apply : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P)
  (a : M), (TensorProduct.AlgebraTensorModule.curry f) a = (TensorProduct.curry (↑R f)) a
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
ContinuousLinearMap.mkOfIsCompactOperator_to_linearMap : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] {M₁ : Type u_3} {M₂ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommGroup M₂] [inst_7 : Module 𝕜₁ M₁]
  [inst_8 : Module 𝕜₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] [inst_10 : ContinuousConstSMul 𝕜₁ M₁]
  [inst_11 : IsTopologicalAddGroup M₂] [inst_12 : ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
  (hf : IsCompactOperator ⇑f), ↑(ContinuousLinearMap.mkOfIsCompactOperator hf) = f
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.SFinite μ],
  (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) ↔ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.compl : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet sᶜ μ
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkOrCached
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₂' : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : CategoryTheory.Limits.HasCokernel S.f],
  (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel S hg
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.mkCodomain.go.eq_def : ∀ (types : Array Lean.Expr) (u : Lean.Level) (x : Lean.Expr) (i : ℕ),
  Lean.Meta.ArgsPacker.Mutual.mkCodomain.go✝ types u x i =
    if i < types.size - 1 then do
      let __do_lift ← Lean.Meta.inferType x
      let xType ← Lean.Meta.whnfD __do_lift
      if xType.isAppOfArity `PSum 2 = true then
          have xTypeArgs := xType.getAppArgs;
          have casesOn := Lean.mkConst `PSum.casesOn (Lean.mkLevelSucc u :: xType.getAppFn.constLevels!);
          have casesOn := Lean.mkAppN casesOn xTypeArgs;
          do
          let __do_lift ← Lean.Meta.mkLambdaFVars #[x] (Lean.mkSort u)
          have casesOn : Lean.Expr := Lean.mkApp casesOn __do_lift
          have casesOn : Lean.Expr := Lean.mkApp casesOn x
          let __do_lift ← liftM (Lean.mkFreshUserName `_x)
          let minor1 ←
            Lean.Meta.withLocalDeclD __do_lift xTypeArgs[0]! fun x =>
                Lean.Meta.mkLambdaFVars #[x] (types[i]!.bindingBody!.instantiate1 x)
          let __do_lift ← liftM (Lean.mkFreshUserName `_x)
          let minor2 ←
            Lean.Meta.withLocalDeclD __do_lift xTypeArgs[1]! fun x => do
                let __do_lift ← Lean.Meta.ArgsPacker.Mutual.mkCodomain.go✝ types u x (i + 1)
                Lean.Meta.mkLambdaFVars #[x] __do_lift
          pure (Lean.mkApp2 casesOn minor1 minor2)
        else
          panicWithPosWithDecl "Lean.Meta.ArgsPacker"
            "_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.mkCodomain.go" 318 6
            ("assertion violation: " ++ "xType.isAppOfArity ``PSum 2\n      ")
    else pure (types[i]!.bindingBody!.instantiate1 x)
-- Lean.CoreM
Lean.Core.instMonadTraceCoreM : Lean.MonadTrace Lean.CoreM
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β),
  f.toFun = ⇑f
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_eq_multiplicity : ∀ {R : Type u} [inst : Ring R] [inst_1 : DecidableEq R] (p : Polynomial R) (a : R),
  Polynomial.rootMultiplicity a p = if p = 0 then 0 else multiplicity (Polynomial.X - Polynomial.C a) p
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.power.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U U_1 : CategoryTheory.Limits.FormalCoproduct C),
  U = U_1 →
    ∀ (α α_1 : Type t) (e_α : α = α_1) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
      U.power α = U_1.power α_1
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk'_X_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₀ ⟶ X₁)
  (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0),
  (CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 1 = X₁
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_a_eq_one : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 1 → P.toPoly.Monic
-- Lean.Syntax
Lean.Syntax.isAntiquotSplice : Lean.Syntax → Bool
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `deriv_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
deriv_const_smul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), deriv (c • f) x = c • deriv f x
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.HasSheafify.isRightAdjoint : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} A} [self : CategoryTheory.HasSheafify J A],
  CategoryTheory.HasWeakSheafify J A
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.G2_partial_sum_eq : ∀ (z : UpperHalfPlane) (N : ℕ),
  ∑ m ∈ Finset.Icc (-↑N) ↑N, EisensteinSeries.e2Summand m z =
    2 * riemannZeta 2 +
      ∑ m ∈ Finset.range N,
        -8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑↑n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ((m + 1) * ↑n)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_app_self : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv
      ((AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.DHashMap.Const.unitOfList l).isEmpty = l.isEmpty
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.mul_mem_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M}, s.MulSaturated → ∀ {x y : M}, x * y ∈ s ↔ x ∈ s ∧ y ∈ s
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.mul.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  ContinuousLinearMap.mul 𝕜 R = ContinuousLinearMap.mul 𝕜 R
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_singleton : ∀ {m n : ℤ}, n = m + 1 → (m...n).toArray = #[m]
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult.go.match_1.eq_2 : ∀ (motive : Option Lean.SyntaxNodeKind → Sort u_1) (x : Option Lean.SyntaxNodeKind)
  (h_1 : (kind : Lean.SyntaxNodeKind) → motive (some kind)) (h_2 : (x : Option Lean.SyntaxNodeKind) → motive x),
  (∀ (kind : Lean.SyntaxNodeKind), x = some kind → False) →
    (match x with
      | some kind => h_1 kind
      | x => h_2 x) =
      h_2 x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piMeasurableEquivTProd_symm_apply : ∀ {δ' : Type u_5} {π : δ' → Type u_6} [inst : (x : δ') → MeasurableSpace (π x)] [inst_1 : DecidableEq δ'] {l : List δ'}
  (hnd : l.Nodup) (h : ∀ (i : δ'), i ∈ l), ⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h).symm = List.TProd.elim' h
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.coe_toGL : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.unitaryGroup n α)), ↑(Matrix.UnitaryGroup.toGL A) = Matrix.UnitaryGroup.toLin' A
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul : ∀ {R : Type u_3} [inst : CommRing R] {p q : Polynomial R},
  p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
AlternatingGroup.map_subtype_of_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (m : Multiset ℕ),
  Finset.map (Function.Embedding.subtype fun x => x ∈ alternatingGroup α) {g | (↑g).cycleType = m} =
    if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.formatTerm : Lean.Syntax → Lean.CoreM Std.Format
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
UniformFun.ofFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2},
  UniformFun.ofFun = { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} → (apex : C) → (l : apex ⟶ c) → (r : apex ⟶ c') → Wₗ l → Wᵣ r → CategoryTheory.Span Wₗ Wᵣ c c'
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.termInt32 : Lean.ParserDescr
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.fvarId : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.FVarId
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.full_linearYoneda : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C], (CategoryTheory.linearYoneda R C).Full
-- Init.Data.Fin.Basic
/-- Addition modulo `n`, usually invoked via the `+` operator.

Examples:
* `(2 : Fin 8) + (2 : Fin 8) = (4 : Fin 8)`
* `(2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)`
 -/
Fin.add : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.addCommGroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : IsAddCyclic α], IsAddCyclic.addCommGroup = inferInstance
-- Mathlib.Algebra.Ring.GeomSum
sub_dvd_pow_sub_pow : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ), x - y ∣ x ^ n - y ^ n
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [inst_3 : L.IsLeftKanExtension α]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) {Z : Cᵒᵖ} (z : P.obj Z),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Presheaf.uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    {
      down :=
        CategoryTheory.CategoryStruct.comp (α.app (Opposite.unop Z)) (L.map (CategoryTheory.uliftYonedaEquiv.symm z)) }
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_inj : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] {p q : ℚ}, ↑p = ↑q ↔ p = q
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, (m.insert a).isEmpty = false
-- Mathlib.Data.List.DropRight
List.rdropWhile_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rdropWhile p l = [] ↔ ∀ x ∈ l, p x = true
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Continuous g) (hf' : IsOpenMap f)
  (hg' : IsOpenMap g) (K : TopologicalSpace.PositiveCompacts α),
  TopologicalSpace.PositiveCompacts.map (f ∘ g) ⋯ ⋯ K =
    TopologicalSpace.PositiveCompacts.map f hf hf' (TopologicalSpace.PositiveCompacts.map g hg hg' K)
-- Mathlib.Data.EReal.Basic
EReal.coe_lt_coe_iff : ∀ {x y : ℝ}, ↑x < ↑y ↔ x < y
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_self_mul_compl : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f : α → M), s.mulIndicator f * sᶜ.mulIndicator f = f
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.inv_hom_id_hom_app_assoc : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D}
  (h : (G.functor n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X)
      (CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) h) =
    h
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.isEmbedding_coe : Topology.IsEmbedding ENNReal.ofNNReal
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind.processing : Lean.Lsp.LeanFileProgressKind
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_mul : ∀ (m n : ℕ∞), ↑(m * n) = ↑m * ↑n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
OrderDual.opensMeasurableSpace : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [h : OpensMeasurableSpace α],
  OpensMeasurableSpace αᵒᵈ
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_piFinTwo : ∀ (α : Fin 2 → Type u) [inst : (i : Fin 2) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : Fin 2), MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g] (X : CategoryTheory.Subobject B)
  (h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g) (h₂ : CategoryTheory.Subobject.mk g ≤ X) {Z : C}
  (h : CategoryTheory.Subobject.underlying.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE g X h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X ⋯) h
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.instMonoSimplexCategoryMapToSimplexCategory : ∀ {n m : SemiSimplexCategory} (f : n ⟶ m), CategoryTheory.Mono (SemiSimplexCategory.toSimplexCategory.map f)
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α},
  (xs ++ ys).setIfInBounds i x = if i < n then xs.setIfInBounds i x ++ ys else xs ++ ys.setIfInBounds (i - n) x
-- Mathlib.Data.Quot
Quotient.liftOn'_mk'' : ∀ {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (f : α → φ) (h : ∀ (a b : α), s₁ a b → f a = f b) (x : α),
  (Quotient.mk'' x).liftOn' f h = f x