mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.instPartialOrder : {L : FirstOrder.Language} → {T : L.Theory} → {α : Type w} → PartialOrder (T.CompleteType α)
-- Init.Data.String.Basic
/-- Decodes a sequence of characters from their UTF-8 representation. Returns `none` if the bytes are
not a sequence of Unicode scalar values.
 -/
ByteArray.utf8Decode? : ByteArray → Option (Array Char)
-- Init.Prelude
of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → γ},
  Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.map f t) =
    List.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- for every pair of parallel morphisms there exists a morphism to the right
so the compositions are equal  -/
CategoryTheory.IsFilteredOrEmpty.cocone_maps : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] ⦃X Y : C⦄
  (f g : X ⟶ Y), ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioo_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (b : α i), Pi.single i '' Set.Ioo 0 b = Set.Ioo 0 (Pi.single i b)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `P` is stable under restriction to a basic open set of global sections.  -/
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X Y : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  P f → P (f ∣_ Y.basicOpen r)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.lift.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H],
  IsFreeAddGroup.lift = (IsFreeAddGroup.basis G).lift
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.implicitBinderF : Lean.Parser.Parser
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.isoCocycles₂ A =
    CategoryTheory.ShortComplex.cyclesMapIso' (groupCohomology.isoShortComplexH2 A)
      (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 2).leftHomologyData
      (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.r_of_le : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (x : (i : ι) × F i) (i : ι)
  (h : x.fst ≤ i), (DirectLimit.setoid f) x ⟨i, (f x.fst i h) x.snd⟩
-- Mathlib.Data.Rat.Floor
/-- `norm_num` extension for `Int.floor`  -/
Rat.evalIntFloor : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {M : CategoryTheory.Functor C MonCat}
  {obj : (U : C) → Submonoid ↑(M.obj U)}
  {map :
    autoParam (∀ {U V : C} (i : U ⟶ V), obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj V))
      CategoryTheory.SubmonoidFunctor.map._autoParam}
  {obj_1 : (U : C) → Submonoid ↑(M.obj U)}
  {map_1 :
    autoParam (∀ {U V : C} (i : U ⟶ V), obj_1 U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj_1 V))
      CategoryTheory.SubmonoidFunctor.map._autoParam},
  { obj := obj, map := map } = { obj := obj_1, map := map_1 } → obj = obj_1
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.tendsto_right_iff : ∀ {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β}
  {f : α → β}, lb.HasBasis pb sb → (Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.append : ∀ {left right : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis left →
    Tactic.ComputeAsymptotics.WellFormedBasis right →
      (∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[Filter.atTop] (Real.log ∘ f)) →
        Tactic.ComputeAsymptotics.WellFormedBasis (left ++ right)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- The pullback functor `SheafOfModules S ⥤ SheafOfModules R` induced by
a morphism of sheaves of rings `S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R`,
defined as the left adjoint functor to the pushforward, when it exists.  -/
SheafOfModules.pullback : {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 : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [(SheafOfModules.pushforward φ).IsRightAdjoint] →
                        CategoryTheory.Functor (SheafOfModules S) (SheafOfModules R)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false}, Std.Internal.List.containsKey (Std.Internal.List.maxKey l he) l = true
-- Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
/-- A prime natural number is prime in `ℤ[i]` if and only if it is `3` mod `4`  -/
GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime : ∀ (p : ℕ) [Fact (Nat.Prime p)], Prime ↑p ↔ p % 4 = 3
-- Init.Data.SInt.Lemmas
Int16.toInt_toInt64 : ∀ (x : Int16), x.toInt64.toInt = x.toInt
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toCommGrpIso_hom : ∀ {X Y : CommGrpCat} (e : ↑X ≃* ↑Y), e.toCommGrpIso.hom = CommGrpCat.ofHom e.toMonoidHom
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoMiddle_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : b ⟶ c),
  (CategoryTheory.Bicategory.associatorNatIsoMiddle f h).inv.app X = (CategoryTheory.Bicategory.associator f X h).inv
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuous_primitive : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ],
  (∀ (a b : ℝ), IntervalIntegrable f μ a b) → ∀ (a : ℝ), Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_left_eball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal),
  (fun x => a * x) ⁻¹' Metric.eball b r = Metric.eball (a⁻¹ * b) r
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.wellPowered_of_essentiallySmall_monoOver : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C],
  (∀ (X : C), CategoryTheory.EssentiallySmall.{w, v, max u₁ v} (CategoryTheory.MonoOver X)) →
    CategoryTheory.WellPowered.{w, v, u₁} C
-- Lean.Elab.PreDefinition.FixedParams
/-- The dependencies among the parameters. See `FixedParams.Info.revDeps`.
We need this for the `FixedParamsPerm.erase` operation.
 -/
Lean.Elab.FixedParamPerms.revDeps : Lean.Elab.FixedParamPerms → Array (Array (Array ℕ))
-- Std.Time.Format.Modifier
Std.Time.instReprText.repr : Std.Time.Text → ℕ → Std.Format
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivOfCompEqX_apply : ∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X)
  (hqp : q.comp p = Polynomial.X) (a : Polynomial R), (p.algEquivOfCompEqX q hpq hqp) a = (Polynomial.aeval p) a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Int.castDef.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.mk : Array Lean.Json.CompressWorkItemKind✝ → Array Lean.Json → Array String → Lean.Json.CompressWorkItemQueue✝
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isComplete_range : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  [CompleteSpace α], AntilipschitzWith K f → UniformContinuous f → IsComplete (Set.range f)
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space which is Lipschitz on a set
is differentiable almost everywhere in this set. For the general Rademacher theorem assuming
that the source space is finite dimensional, see `LipschitzOnWith.ae_differentiableWithinAt`.  -/
LipschitzOnWith.ae_differentiableWithinAt_real : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal}
  {f : ℝ → V} {s : Set ℝ},
  LipschitzOnWith C f s → MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
-- Mathlib.CategoryTheory.Action.Basic
Action.isIso_hom_mk : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M.V ⟶ N.V) [CategoryTheory.IsIso f]
  (w : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f = CategoryTheory.CategoryStruct.comp f (N.ρ g)),
  CategoryTheory.IsIso { hom := f, comm := w }
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_rco : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_rco._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
    List.filter (fun e => decide ((cmp e.1 lowerBound).isGE = true ∧ (cmp e.1 upperBound).isLT = true)) t.toList
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  [inst_5 : J.WEqualsLocallyBijective AddCommGrpCat] {F : PresheafOfModules R.obj}
  (hF : CategoryTheory.Presheaf.IsSheaf J F.presheaf) (f : M₀ ⟶ (PresheafOfModules.restrictScalars α).obj F),
  CategoryTheory.CategoryStruct.comp φ
      ((PresheafOfModules.toPresheaf R.obj).map ((PresheafOfModules.sheafifyHomEquiv' α φ hF).symm f)) =
    (PresheafOfModules.toPresheaf R₀).map f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.bit1.sizeOf_spec : sizeOf Turing.PartrecToTM2.Γ'.bit1 = 1
-- Lean.Meta.GetUnfoldableConst
/-- Implements the `TransparencyMode` hierarchy for unfolding decisions.
See `TransparencyMode` and `ReducibilityStatus` for the design rationale.
 -/
Lean.Meta.canUnfoldDefault : Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instContinuousLinearMapClass : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  ContinuousSemilinearMapClass (E →SWOT[σ] F) σ E F
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instEpiFunctorGShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), CategoryTheory.Epi Φ.shortComplex.g
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
IsSelfAdjoint.norm_eq_max_norm_posPart_negPart : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : NormedSpace ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A]
  [inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (IsSelfAdjoint a) IsSelfAdjoint.norm_eq_max_norm_posPart_negPart._auto_1 → ‖a‖ = max ‖a⁺‖ ‖a⁻‖
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonAssocSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [AddZeroClass M] → NonAssocSemiring (AddMonoidAlgebra R M)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- If `f` is multiplicative and summable, then its values at natural numbers `> 1`
have norm strictly less than `1`.  -/
Summable.norm_lt_one : ∀ {F : Type u_1} [inst : NormedDivisionRing F] [CompleteSpace F] {f : ℕ →* F},
  Summable ⇑f → ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.setIntegral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν →
    ∀ (a : α) {s : Set β}, MeasurableSet s → ∀ (q : ℚ), ∫ (b : β) in s, f (a, b) q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
/-- The cocone `colimitCocone F` is colimit for any `F : J ⥤ PresheafOfModules.{v} R`.  -/
PresheafOfModules.isColimitColimitCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [inst_2 :
                ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
                  CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
                    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] →
              [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] →
                CategoryTheory.Limits.IsColimit (PresheafOfModules.colimitCocone F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The left unitor isomorphism for categorical cospan transformations.  -/
CategoryTheory.Limits.CatCospanTransform.«termλ_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_le_ceil : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (a : R), ⌊a⌋₊ ≤ ⌈a⌉₊
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- If `f` is a box-additive map, then so is the map sending `I` to the scalar multiplication
by `f I` as a continuous linear map from `E` to itself.  -/
BoxIntegral.BoxAdditiveMap.toSMul : {ι : Type u_1} →
  {I₀ : WithTop (BoxIntegral.Box ι)} →
    {E : Type u_4} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] → BoxIntegral.BoxAdditiveMap ι ℝ I₀ → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] E) I₀
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
/-- **Alias** of `cfcHom_mem_elemental`. -/
cfcHom_apply_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] {a : A}
  (ha : p a) (f : C(↑(spectrum 𝕜 a), 𝕜)), (cfcHom ha) f ∈ StarAlgebra.elemental 𝕜 a
-- Mathlib.Data.Set.Finite.Monad
Finite.Set.finite_seq : ∀ {α : Type u} {β : Type v} (f : Set (α → β)) (s : Set α) [Finite ↑f] [Finite ↑s], Finite ↑(f.seq s)
-- Lean.Parser.Extension
Lean.Parser.ParserAttributeHook.mk.inj : ∀ {postAdd postAdd_1 : Lean.Name → Lean.Name → Bool → Lean.AttrM Unit},
  { postAdd := postAdd } = { postAdd := postAdd_1 } → postAdd = postAdd_1
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.factor₁.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing.factor₁ m k hn p =
    (↑((MvPolynomial.universalFactorizationMapLiftEquiv R (Polynomial.UniversalFactorizationRing m k hn p) n m k hn
            (Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p))
          ⟨Polynomial.UniversalFactorizationRing.fromTensor m k hn p, ⋯⟩)).1
-- Mathlib.Algebra.Field.GeomSum
geom₂_sum : ∀ {K : Type u_2} [inst : Field K] {x y : K},
  x ≠ y → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Lean.Parser.Term
Lean.Parser.Term.byTactic'.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Analytic.CPolynomial
/-- Formal multilinear series associated to a linear map into multilinear maps.  -/
ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear : {𝕜 : Type u_1} →
  {F : Type u_3} →
    {G : Type u_4} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace 𝕜 F] →
            [inst_3 : NormedAddCommGroup G] →
              [inst_4 : NormedSpace 𝕜 G] →
                {ι : Type u_5} →
                  {Em : ι → Type u_6} →
                    [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] →
                      [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)] →
                        [Fintype ι] →
                          (G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) → FormalMultilinearSeries 𝕜 (G × ((i : ι) → Em i)) F
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.Equiv.foldM_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Std.Iterator α₁ m β] [Std.Iterator α₂ m β]
  [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m]
  [inst_4 : Monad m] [inst_5 : LawfulMonad m] [inst_6 : Monad n] [LawfulMonad n] [inst_8 : Std.IteratorLoop α₁ m n]
  [Std.LawfulIteratorLoop α₁ m n] [inst_10 : Std.IteratorLoop α₂ m n] [Std.LawfulIteratorLoop α₂ m n]
  [inst_12 : MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ} {f : γ → β → n γ} {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → Std.IterM.foldM f init ita = Std.IterM.foldM f init itb
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
real number in the domain of absolute convergence, then the `n`th iterated derivative
of the associated L-series is nonnegative real when `n` is even and nonpositive real
when `n` is odd.  -/
LSeries.iteratedDeriv_alternating : ∀ {a : ℕ → ℂ},
  0 ≤ a → ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a < ↑x → ∀ (n : ℕ), 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.merge : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₂ → t₃.Equiv t₄ → (t₁.merge t₃).Equiv (t₂.merge t₄)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n : ℕ)
  (f₁ f₂ : L.BoundedFormula α _n) (h_1 : (_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_n l : ℕ) →
      (_R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts))
  (h_4 : (_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂))
  (h_5 : (_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all),
  (match _n, f₁.imp f₂ with
    | _n, FirstOrder.Language.BoundedFormula.falsum => h_1 _n
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _n t₁ t₂
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => h_3 _n l _R ts
    | _n, f₁.imp f₂ => h_4 _n f₁ f₂
    | _n, f.all => h_5 _n f) =
    h_4 _n f₁ f₂
-- Mathlib.Order.Monotone.Defs
StrictMono.comp_strictMonoOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, StrictMono g → StrictMonoOn f s → StrictMonoOn (g ∘ f) s
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] {Cg rg : NNReal} {g : Y → Z},
  HolderWith Cg rg g → ∀ {Cf rf : NNReal} {f : X → Y}, HolderWith Cf rf f → HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.op_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).op = β_ (Opposite.op Y) (Opposite.op X)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.mk.sizeOf_spec : ∀ (modified : Bool) (mvarId : Lean.MVarId) (entries : Array Lean.Meta.SimpAll.Entry) (ctx : Lean.Meta.Simp.Context)
  (simprocs : Lean.Meta.Simp.SimprocsArray) (usedTheorems : Lean.Meta.Simp.UsedSimps)
  (diag : Lean.Meta.Simp.Diagnostics),
  sizeOf
      { modified := modified, mvarId := mvarId, entries := entries, ctx := ctx, simprocs := simprocs,
        usedTheorems := usedTheorems, diag := diag } =
    1 + sizeOf modified + sizeOf mvarId + sizeOf entries + sizeOf ctx + sizeOf simprocs + sizeOf usedTheorems +
      sizeOf diag
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.le_traceDual_traceDual : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I : Submodule B L},
  I ≤ Submodule.traceDual A K (Submodule.traceDual A K I)
-- Mathlib.Algebra.RingQuot
RingQuot.mkRingHom_surjective : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), Function.Surjective ⇑(RingQuot.mkRingHom r)
-- Std.Async.Basic
/-- Creates an `EAsync` computation that immediately returns the given value.
 -/
Std.Async.EAsync.pure : {α ε : Type} → α → Std.Async.EAsync ε α
-- Mathlib.Algebra.Ring.Parity
Odd.pow_add_pow_eq_zero : ∀ {α : Type u_2} [inst : Semiring α] {a b : α} {n : ℕ} [IsCancelAdd α], Odd n → a + b = 0 → a ^ n + b ^ n = 0