mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Flat.Localization
instFlatAtPrimeOfIsLiesOverAlgebra : ∀ {A : Type u_4} {B : Type u_5} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Flat A B]
  (p : Ideal A) [inst_4 : p.IsPrime] (P : Ideal B) [inst_5 : P.IsPrime] [inst_6 : P.LiesOver p]
  [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [Localization.AtPrime.IsLiesOverAlgebra p P],
  Module.Flat (Localization.AtPrime p) (Localization.AtPrime P)
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.tag.injEq : ∀ {α : Type u} (a : α) (a_1 : Lean.Widget.TaggedText α) (a_2 : α) (a_3 : Lean.Widget.TaggedText α),
  (Lean.Widget.TaggedText.tag a a_1 = Lean.Widget.TaggedText.tag a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- We show that the forgetful functor `AddCommMonCat ⥤ AddMonCat` creates limits.

All we need to do is notice that the limit point has an `AddCommMonoid` instance available,
and then reuse the existing limit.  -/
AddCommMonCat.forget₂CreatesLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {α' : Type u_7} {β : Type u_8} [uβ : UniformSpace β] {u : κ → UniformSpace α'}
  {F : ι → β → α'} {S : Set β}, UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S
-- Mathlib.CategoryTheory.Action.Limits
Action.instLinear : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.Preadditive V] →
          {R : Type u_3} → [inst_3 : Semiring R] → [CategoryTheory.Linear R V] → CategoryTheory.Linear R (Action V G)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorHom_def : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ ⟶ X₂)
  (g : Y₁ ⟶ Y₂) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂] [inst_5 : X₂.HasTensor Y₁],
  CategoryTheory.GradedObject.Monoidal.tensorHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight f Y₁)
      (CategoryTheory.GradedObject.Monoidal.whiskerLeft X₂ g)
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.eq_one_of_mem_of_inv_mem' : ∀ {G : Type u_1} [inst : CommGroup G] (self : GroupCone G) {a : G}, a ∈ self.carrier → a⁻¹ ∈ self.carrier → a = 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.id_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.Oplax.StrongTrans.id F).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_connected : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.toSubgraph.Connected
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.Equiv t₂ → t₁.getKeyLTD k fallback = t₂.getKeyLTD k fallback
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.FoldM : Type → Type
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData.mk.injEq : ∀ (clsName : Lean.Name) (privateSpecs : Bool) (clsName_1 : Lean.Name) (privateSpecs_1 : Bool),
  ({ clsName := clsName, privateSpecs := privateSpecs } = { clsName := clsName_1, privateSpecs := privateSpecs_1 }) =
    (clsName = clsName_1 ∧ privateSpecs = privateSpecs_1)
-- Lean.Meta.GeneralizeVars
Lean.Meta.getFVarsToGeneralize : Array Lean.Expr → optParam Lean.FVarIdSet ∅ → optParam Bool false → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.nnHolderNorm_smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  {α : Type u_3} [inst_2 : NormedRing α] [inst_3 : Module α Y] [NormSMulClass α Y],
  MemHolder r f → ∀ (c : α), nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
-- Mathlib.Topology.Order.IsLUB
IsLUB.exists_seq_strictMono_tendsto_of_notMem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} {x : α}
  [(nhds x).IsCountablyGenerated],
  IsLUB t x →
    x ∉ t →
      t.Nonempty →
        ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.contDiffWithinAt_extendCoordChange : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ∀ {x : E},
        x ∈ (ModelWithCorners.extendCoordChange e e').source →
          ContDiffWithinAt 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (Set.range ↑I) x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.not_irreducible_C : ∀ {R : Type u} [inst : Field R] (x : R), ¬Irreducible (Polynomial.C x)
-- Init.Data.BitVec.Basic
/-- `BitVec` representation.  -/
BitVec.repr : {n : ℕ} → BitVec n → Std.Format
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_iff_exists_lt : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α},
  s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
-- Mathlib.Computability.Reduce
/-- **Alias** of `isTrans_manyOneReducible`. -/
transitive_manyOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], IsTrans (α → Prop) ManyOneReducible
-- Mathlib.Tactic.Tauto
_private.Mathlib.Tactic.Tauto.0.Mathlib.Tactic.Tauto.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Tauto.Config
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.leftHomologyData_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.leftHomologyData.K = S.X₁
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map_comp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_3}
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)),
  FundamentalGroupoid.map (g.comp f) = (FundamentalGroupoid.map f).comp (FundamentalGroupoid.map g)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_id_real : ∀ (r : ℝ), (↑r).st = r
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S],
  Subring.center (R × S) = (Subring.center R).prod (Subring.center S)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_zero_of_not_mdifferentiableWithinAt : ∀ {𝕜 : 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'} {x : M} {s : Set M},
  ¬MDiffAt[s] f x → mfderiv[s] f x = 0
-- Mathlib.Topology.Order.CountableSeparating
HasCountableSeparatingOn.range_Iic : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {s : Set X}, HasCountableSeparatingOn X (fun x => x ∈ Set.range Set.Iic) s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_preimage_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {t : Set M} {x : M},
  x ∈ f.source → t ∈ nhds x → ↑(f.extend I).symm ⁻¹' t ∈ nhds (↑(f.extend I) x)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.sub` -/
InnerProductSpace.HarmonicContOnCl.fun_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f₁ s →
    InnerProductSpace.HarmonicContOnCl f₂ s → InnerProductSpace.HarmonicContOnCl (fun i => f₁ i - f₂ i) s
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObjEquiv_symm_naturality : ∀ {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (g : C(↑(stdSimplex ℝ (Fin (m.len + 1))), ↑X)),
  (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) ((X.toSSetObjEquiv (Opposite.op m)).symm g) =
    (X.toSSetObjEquiv (Opposite.op n)).symm
      (g.comp { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })
-- Mathlib.Topology.Order.HullKernel
/-- When `α` is complete, a set is closed in the relative lower topology if and only if it is of the
form `hull T a` for some `a` in `α`.  -/
PrimitiveSpectrum.isClosed_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) → ∀ {S : Set ↑T}, IsClosed S ↔ ∃ a, S = PrimitiveSpectrum.hull T a
-- Mathlib.Analysis.Normed.Operator.Mul
/-- The norm of `lsmul x` equals `‖x‖` in any nontrivial normed group.

This is `ContinuousLinearMap.opNorm_lsmul_apply_le` as an equality.  -/
ContinuousLinearMap.opNorm_lsmul_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E] {a : R},
  ‖(ContinuousLinearMap.lsmul 𝕜 R) a‖ = ‖a‖
-- Lean.Data.Options
Lean.Option.Decl : Type → Type
-- Init.Meta.Defs
/-- Creates a literal of the given kind. It is the caller's responsibility to ensure that the provided
literal is a valid atom for the provided kind.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkLit : (kind : Lean.SyntaxNodeKind) → String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.TSyntax kind
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux_zero : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ), SchwartzMap.seminormAux✝ k n 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_sum : ∀ {ι : Type u_1} {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (s : Finset ι)
  (f : ι → Matrix n n R), (∑ i ∈ s, f i).trace = ∑ i ∈ s, (f i).trace
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKey? k = none
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.continuous_sumAssoc : ∀ (X : Type u) (Y : Type v) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z], Continuous ⇑(Equiv.sumAssoc X Y Z)
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.normal.sizeOf_spec : sizeOf Lean.Server.FileWorker.Hover.RWState.normal✝ = 1
-- Mathlib.CategoryTheory.Enriched.HomCongr
/-- The inverse map defined by `eHomCongr` respects composition of morphisms.  -/
CategoryTheory.Iso.eHomCongr_inv_comp_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) {Z_1 : V}
  (h : (X ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y)
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
              (CategoryTheory.Iso.eHomCongr V β γ).inv))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)))
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (Φ : Subgroup (G →* Mˣ)) (g : G),
  g ∈ (CommGroup.subgroupOrderIsoSubgroupMonoidHom G M).symm (OrderDual.toDual Φ) ↔ ∀ φ ∈ Φ, φ g = 1
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_map : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (a : Fin n),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).map a = (⇑finSumFinEquiv.symm ∘ ⇑(finCongr hn)) a
-- Mathlib.Analysis.Convolution
/-- The convolution of two functions with respect to a bilinear operation `L` and the volume.  -/
Convolution.«term_⋆[_]_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.w_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i j : ι) (X : TopPair)
  {Z : C} (h : (HP'.H j).obj X.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HP.δ i j).app X) (CategoryTheory.CategoryStruct.comp ((f.hom j).app X.left) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app X) ((HP'.δ i j).app X)) h
-- Mathlib.Order.PrimeIdeal
Order.Ideal.isPrime_of_mem_or_compl_mem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {I : Order.Ideal P} [I.IsProper], (∀ {x : P}, x ∈ I ∨ xᶜ ∈ I) → I.IsPrime
-- Lean.Meta.Basic
/-- Projections `s.i` are reduced at `whnfCore`, and `whnf` is used at `s` during the process.
Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
 -/
Lean.Meta.ProjReductionKind.yesWithDelta : Lean.Meta.ProjReductionKind
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncFinset_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (p : MvPowerSeries σ R),
  x ∉ s → MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) p) = 0
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- Eta-expanded form of `AbsolutelyContinuousOnInterval.add` -/
AbsolutelyContinuousOnInterval.fun_add : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (fun i => f i + g i) a b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_mul : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R},
  Polynomial.eval x (p * q) = Polynomial.eval x p * Polynomial.eval x q
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.natDegree_smul_of_smul_regular : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] {k : S} (p : Polynomial R),
  IsSMulRegular R k → (k • p).natDegree = p.natDegree
-- Lean.Parser.Do
Lean.Parser.Term.doForward.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instMul : (M : Type u_4) → [inst : AddZero M] → Mul (AddMonoid.End M)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of `-x` is the same as that of `x`.  -/
Height.mulHeight₁_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.mulHeight₁ (-x) = Height.mulHeight₁ x
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.isLetDeclToUnfold : Lean.Meta.SimpTheorems → Lean.FVarId → Bool
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.nil_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (hwp : w ∈ p.support),
  (p.takeUntil w hwp).Nil ↔ u = w
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_smul : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] {S : NonUnitalSubalgebra R A} [inst_3 : SMul R' R] [inst_4 : SMul R' A]
  [inst_5 : IsScalarTower R' R A] (r : R') (x : ↥S), ↑(r • x) = r • ↑x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_hasSum_exp : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  HasSum (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) (NormedSpace.exp x)
-- Mathlib.Data.Int.ModEq
/-- **Alias** of the reverse direction of `Int.modEq_iff_dvd`. -/
Int.modEq_of_dvd : ∀ {n a b : ℤ}, n ∣ b - a → a ≡ b [ZMOD n]
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.δ_index : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (hxy.index hd))) (y.cast ⋯).simplex =
    (x.cast hd).simplex
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_refl : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.refl G) = 1
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularEpi.effectiveEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B X : C} {f : X ⟶ B} (h : CategoryTheory.RegularEpi f),
  CategoryTheory.EffectiveEpi f
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofBitVec : ∀ (b : BitVec System.Platform.numBits), { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }
-- Mathlib.Order.Fin.Basic
Fin.succ_top : ∀ (n : ℕ) [inst : NeZero n], ⊤.succ = ⊤
-- Mathlib.Algebra.GCDMonoid.Basic
instStrongNormalizationMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [Subsingleton αˣ] → StrongNormalizationMonoid α
-- Mathlib.Algebra.Group.Basic
inv_div_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a⁻¹ / b = b⁻¹ / a
-- Mathlib.Algebra.CharP.Algebra
/-- Given `R →+* A`, where `R` is a domain with `char R > 0`, then `char A = char R`.  -/
CharP.of_ringHom_of_ne_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [NoZeroDivisors R] [inst_2 : NonAssocSemiring A]
  [Nontrivial A] (f : R →+* A) (p : ℕ), p ≠ 0 → ∀ [CharP R p], CharP A p
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- The projection out of `SecondCountableTopologyEither`  -/
SecondCountableTopologyEither.out : ∀ {α : Type u_6} {β : Type u_7} {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β}
  [self : SecondCountableTopologyEither α β], SecondCountableTopology α ∨ SecondCountableTopology β
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.union_cylinder_same : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S₁ S₂ : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S₁ ∪ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∪ S₂)
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of any finset is `0`.  -/
schnirelmannDensity_finset : ∀ (A : Finset ℕ), schnirelmannDensity ↑A = 0
-- Mathlib.Order.Closure
LowerAdjoint.closure_top : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : Preorder β] {u : β → α}
  (l : LowerAdjoint u), u (l.toFun ⊤) = ⊤
-- Mathlib.Order.Filter.NAry
Filter.map₂_map_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β} (m : γ → β → δ) (n : α → γ),
  Filter.map₂ m (Filter.map n f) g = Filter.map₂ (fun a b => m (n a) b) f g
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds_of_size_le_left : ∀ {α : Type u_1} {xs : Array α} {i j k : ℕ},
  xs.size ≤ i → ∀ (hk : k < (xs.swapIfInBounds i j).size), (xs.swapIfInBounds i j)[k] = xs[k]
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_pair_mul_span_pair : ∀ {R : Type u} [inst : Semiring R] (w x y z : R) [(Ideal.span {w, x}).IsTwoSided],
  Ideal.span {w, x} * Ideal.span {y, z} = Ideal.span {w * y, w * z, x * y, x * z}
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
MeasurableEquiv.Simps.apply : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → α ≃ᵐ β → α → β
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_eq_zero_of_notMem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∉ Function.periodicPts f → Function.minimalPeriod f x = 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_monomial_of_ne : ∀ {R : Type u} [inst : Semiring R] {m n : ℕ} (c : R), m ≠ n → ((Polynomial.monomial n) c).coeff m = 0
-- Mathlib.Data.Int.Cast.Defs
/-- An `AddGroupWithOne` is an `AddGroup` with a 1. It also contains data for the unique
homomorphisms `ℕ → R` and `ℤ → R`.  -/
AddGroupWithOne : Type u → Type u
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_symm_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P), (LinearEquiv.lTensor M f).symm (m ⊗ₜ[R] p) = m ⊗ₜ[R] f.symm p
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_inv : ∀ (b x : ℝ), Real.logb b x⁻¹ = -Real.logb b x
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.toSubring_mono : ∀ {R : Type u_1} [inst : CommRing R], Monotone LocalSubring.toSubring
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The object property on `Under X` induced by a morphism property.  -/
CategoryTheory.MorphismProperty.underObj : {T : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} T] →
    CategoryTheory.MorphismProperty T → {X : T} → CategoryTheory.ObjectProperty (CategoryTheory.Under X)