mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Options
Lean.OptionDecl : Type
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- A prime `p` is in the range of `Spec S → Spec R` if the fiber over `p` is nontrivial.  -/
PrimeSpectrum.nontrivial_iff_mem_rangeComap : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R),
  Nontrivial (TensorProduct R p.asIdeal.ResidueField S) ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The comonad induced by the Eilenberg-Moore adjunction is the original comonad.  -/
CategoryTheory.Adjunction.adjToComonadIso : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (G : CategoryTheory.Comonad C) → G.adj.toComonad ≅ G
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.field : {X Y : AlgebraicGeometry.Scheme} → {f : X ⟶ Y} → (self : AlgebraicGeometry.ValuativeCommSq f) → Field self.K
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.mk.sizeOf_spec : ∀ (all : Array Lean.Name) (numNested : ℕ),
  sizeOf { all := all, numNested := numNested } = 1 + sizeOf all + sizeOf numNested
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm extends the norm on `K` when `L/K` is finite and normal.
See also `spectralNorm_extends` for a more general result.  -/
spectralNorm_extends_of_finiteDimensional : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] (x : K),
  spectralNorm K L ((algebraMap K L) x) = ‖x‖
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.range_eq_ofSection : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : C}
  (f : CategoryTheory.yoneda.obj X ⟶ F),
  CategoryTheory.Subfunctor.range f = CategoryTheory.Subfunctor.ofSection (CategoryTheory.yonedaEquiv f)
-- Mathlib.NumberTheory.LSeries.MellinEqDirichlet
/-- Most basic version of the "Mellin transform = Dirichlet series" argument.  -/
hasSum_mellin : ∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  (∀ (i : ι), a i = 0 ∨ 0 < p i) →
    0 < s.re →
      (∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(Real.exp (-p i * t))) (F t)) →
        (Summable fun i => ‖a i‖ / p i ^ s.re) → HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = true → Std.Internal.List.getKey? a (⟨k, v⟩ :: l) = some k
-- Mathlib.Data.ZMod.Basic
ZMod.val_add_le : ∀ {n : ℕ} (a b : ZMod n), (a + b).val ≤ a.val + b.val
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
          ((AlgebraicGeometry.structureSheafInType
                  ↑(Opposite.unop (Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))))
                  ↑(Opposite.unop (Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))))).obj.obj
            (Opposite.op (PrimeSpectrum.basicOpen r)))))
      (X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r))) =
    X.toToΓSpecMapBasicOpen r
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_image' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {s : Finset κ}
  {g : κ → ι} (h : κ → M), (∀ i ∈ s, f (g i) = ∏ j ∈ s with g j = g i, h j) → ∏ a ∈ Finset.image g s, f a = ∏ i ∈ s, h i
-- Mathlib.Analysis.Convex.Exposed
exposedPoints_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A : Set E}, Set.exposedPoints 𝕜 A ⊆ A
-- Mathlib.RingTheory.TensorProduct.Basic
/-- If `M` is a `B`-module that is also an `A`-module, the canonical map
`M →ₗ[A] B ⊗[A] M` is injective.  -/
Algebra.TensorProduct.mk_one_injective_of_isScalarTower : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M],
  Function.Injective ⇑((TensorProduct.mk R S M) 1)
-- Mathlib.Data.NNRat.Defs
NNRat.add_def : ∀ (q r : ℚ≥0), q + r = NNRat.divNat (q.num * r.den + r.num * q.den) (q.den * r.den)
-- Init.Meta.Defs
/-- Extracts the non-separator elements of a separated array.
 -/
Lean.Syntax.TSepArray.getElems : {k : Lean.SyntaxNodeKinds} → {sep : String} → Lean.Syntax.TSepArray k sep → Lean.TSyntaxArray k
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofLeftAdjoint.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  {left : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone G)}
  {right : CategoryTheory.Functor (CategoryTheory.Limits.Cocone G) (CategoryTheory.Limits.Cocone F)}
  (adj : right ⊣ left) {c : CategoryTheory.Limits.Cocone G} (t : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Limits.IsColimit.ofLeftAdjoint adj t =
    CategoryTheory.Limits.IsColimit.mkCoconeMorphism (fun s => (adj.homEquiv' s c) (t.descCoconeMorphism (left.obj s)))
      ⋯
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_eq_of_fixedPoint_or_zero : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  x ≤ f x → ∀ (o : Ordinal.{u}), OrdinalApprox.lfpApprox f x o = x ↔ f x = x ∨ o = 0
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone fun x => Set.Ici (f x)
-- Init.Meta.Defs
Lean.Meta.Rewrite.Config.mk.sizeOf_spec : ∀ (transparency : Lean.Meta.TransparencyMode) (offsetCnstrs : Bool) (occs : Lean.Meta.Occurrences)
  (newGoals : Lean.Meta.Rewrite.NewGoals),
  sizeOf { transparency := transparency, offsetCnstrs := offsetCnstrs, occs := occs, newGoals := newGoals } =
    1 + sizeOf transparency + sizeOf offsetCnstrs + sizeOf occs + sizeOf newGoals
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_congr : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : ℕ → MeasureTheory.Measure α},
  (∀ (n : ℕ), μ n = ν n) → MeasureTheory.Measure.sum μ = MeasureTheory.Measure.sum ν
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow.
 -/
Std.Time.PlainDateTime.subMilliseconds : Std.Time.PlainDateTime → Std.Time.Millisecond.Offset → Std.Time.PlainDateTime
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_Q : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).Q = F.obj h.Q
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H : CategoryTheory.Functor D E} [inst_3 : H.Full] [inst_4 : H.Faithful] (comp_iso : F.comp H ≅ G.comp H) (X : C),
  (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.appLE : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  P f →
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
      Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Augmented.stdSimplex_obj_hom_app : ∀ (Δ : SimplexCategory) (x : SimplexCategoryᵒᵖ),
  (SSet.Augmented.stdSimplex.obj Δ).hom.app x =
    CategoryTheory.Limits.terminal.from
      (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x)
-- Mathlib.CategoryTheory.Action.Continuous
/-- Continuous version of `Functor.mapActionComp`.  -/
CategoryTheory.Functor.mapContActionComp : {V : Type u_5} →
  {W : Type u_6} →
    [inst : CategoryTheory.Category.{v_2, u_5} V] →
      {FV : V → V → Type u_7} →
        {CV : V → Type u_8} →
          [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory V FV] →
              [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
                [inst_4 : CategoryTheory.Category.{v_3, u_6} W] →
                  {FW : W → W → Type u_9} →
                    {CW : W → Type u_10} →
                      [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] →
                        [inst_6 : CategoryTheory.ConcreteCategory W FW] →
                          [inst_7 : CategoryTheory.HasForget₂ W TopCat] →
                            (G : Type u_11) →
                              [inst_8 : Monoid G] →
                                [inst_9 : TopologicalSpace G] →
                                  {T : Type u_12} →
                                    [inst_10 : CategoryTheory.Category.{v_4, u_12} T] →
                                      {FT : T → T → Type u_13} →
                                        {CT : T → Type u_14} →
                                          [inst_11 : (X Y : T) → FunLike (FT X Y) (CT X) (CT Y)] →
                                            [inst_12 : CategoryTheory.ConcreteCategory T FT] →
                                              [inst_13 : CategoryTheory.HasForget₂ T TopCat] →
                                                (F : CategoryTheory.Functor V W) →
                                                  (H :
                                                      ∀ (X : ContAction V G),
                                                        ((F.mapAction G).obj X.obj).IsContinuous) →
                                                    (F' : CategoryTheory.Functor W T) →
                                                      (H' :
                                                          ∀ (X : ContAction W G),
                                                            ((F'.mapAction G).obj X.obj).IsContinuous) →
                                                        CategoryTheory.Functor.mapContAction G (F.comp F') ⋯ ≅
                                                          (CategoryTheory.Functor.mapContAction G F H).comp
                                                            (CategoryTheory.Functor.mapContAction G F' H')
-- Mathlib.Algebra.Exact.Basic
LinearMap.surjective_range_liftQ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : f.range ≤ g.ker),
  Function.Surjective ⇑g → Function.Surjective ⇑(f.range.liftQ g h)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A `fin_strongly_measurable` function such that `f =ᵐ[μ] hf.mk f`. See lemmas
`fin_strongly_measurable_mk` and `ae_eq_mk`.  -/
MeasureTheory.AEFinStronglyMeasurable.mk : {α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : TopologicalSpace β] →
          [inst_1 : Zero β] → (f : α → β) → MeasureTheory.AEFinStronglyMeasurable f μ → α → β
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangleRotateShortComplex φ).f = (CochainComplex.mappingCone.triangle φ).rotate.mor₁
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenConj_sq : Real.goldenConj ^ 2 = Real.goldenConj + 1
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable.  -/
MDifferentiableAt.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {EM : Type u_6} [inst_12 : NormedAddCommGroup EM] [inst_13 : NormedSpace ℝ EM] {HM : Type u_7}
  [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [inst_15 : TopologicalSpace M]
  [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)}
  {x : M},
  (MDiffAt fun m => ⟨b m, v m⟩) x → (MDiffAt fun m => ⟨b m, w m⟩) x → (MDiffAt fun b_1 => inner ℝ (v b_1) (w b_1)) x
-- Init.Data.Array.Subarray
/-- Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.
 -/
Std.Slice.Internal.SubarrayData : Type u → Type u
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- If `x` is a point in the basic open set `D(f)` where `f` is a homogeneous element of positive
degree, then the homogeneously localized ring `A⁰ₓ` has the universal property of the localization
of `A⁰_f` at `φ(x)` where `φ : Proj|D(f) ⟶ Spec A⁰_f` is the morphism of locally ringed space
constructed as above.
 -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) {m : ℕ},
  f ∈ 𝒜 m →
    0 < m →
      IsLocalization
        ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base)
              x).asIdeal.primeCompl
        (HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.associator_monoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) X₃
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) Y₃)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃))
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) Y₁
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₃))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
          (CategoryTheory.MonoidalCategory.tensorμ X₂ X₃ Y₂ Y₃)))
-- Mathlib.Logic.Equiv.List
/-- Explicit encoding function for `List α`  -/
Encodable.encodeList : {α : Type u_1} → [Encodable α] → List α → ℕ
-- Lean.Message
Lean.instInhabitedMessageData : Inhabited Lean.MessageData
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instInhabitedOfYear : {leap : Bool} → Inhabited (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_add_const_iff`. -/
Wbtw.add_const : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R x y z → Wbtw R (x + v) (y + v) (z + v)
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
 -/
Polynomial.degree_prod : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R)
  [Nontrivial R], (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_expChar_of_commute : ∀ {R : Type u_1} [inst : Ring R] {x y : R} (p : ℕ) [hR : ExpChar R p], Commute x y → (x - y) ^ p = x ^ p - y ^ p
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- Precomposition by a fixed continuous linear map, as a continuous linear map when all spaces
of continuous linear maps are equipped with the weak operator topology.  -/
ContinuousLinearMapWOT.postcompCLM : {𝕜₁ : Type u_5} →
  {𝕜₂ : Type u_6} →
    {𝕜₃ : Type u_7} →
      {E : Type u_9} →
        {F : Type u_10} →
          {G : Type u_11} →
            [inst : NormedField 𝕜₁] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : NormedField 𝕜₃] →
                  {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                    {σ₁₃ : 𝕜₁ →+* 𝕜₃} →
                      {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : TopologicalSpace E] →
                              [inst_6 : Module 𝕜₁ E] →
                                [inst_7 : AddCommGroup F] →
                                  [inst_8 : TopologicalSpace F] →
                                    [inst_9 : Module 𝕜₂ F] →
                                      [inst_10 : AddCommGroup G] →
                                        [inst_11 : TopologicalSpace G] →
                                          [inst_12 : Module 𝕜₃ G] →
                                            [inst_13 : IsTopologicalAddGroup F] →
                                              [inst_14 : ContinuousConstSMul 𝕜₂ F] →
                                                [inst_15 : IsTopologicalAddGroup G] →
                                                  [inst_16 : ContinuousConstSMul 𝕜₃ G] →
                                                    [RingHomSurjective σ₂₃] →
                                                      [RingHomIsometric σ₂₃] →
                                                        (F →SWOT[σ₂₃] G) → (E →SWOT[σ₁₂] F) →SL[σ₂₃] E →SWOT[σ₁₃] G
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (s : Set α) (t : Set β), ⋃ a ∈ s, a • t = s • t
-- Std.Async.Signal
/-- Trace/breakpoint trap.
 -/
Std.Async.Signal.sigtrap : Std.Async.Signal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β)
  (k : α),
  t.get? k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match h : compare k k' with
      | Ordering.lt => l.get? k
      | Ordering.gt => r.get? k
      | Ordering.eq => some (cast ⋯ v')
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- `Matrix.toLinearMap₂ b₁ b₂` is the same as `Matrix.toLinearMapₛₗ₂ b₁ b₂` but with
`σ₁ := RingHom.id R` to avoid having to specify it.  -/
Matrix.toLinearMap₂ : {R : Type u_1} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      {N₂ : Type u_10} →
        {n : Type u_11} →
          {m : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M₁] →
                [inst_2 : Module R M₁] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M₂] →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Module R N₂] →
                          [Fintype n] →
                            [Fintype m] →
                              [DecidableEq m] →
                                [DecidableEq n] →
                                  Module.Basis n R M₁ → Module.Basis m R M₂ → Matrix n m N₂ ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] N₂
-- Mathlib.MeasureTheory.PiSystem
/-- If `π` is a family of π-systems, then `piiUnionInter π S` is a π-system.  -/
isPiSystem_piiUnionInter : ∀ {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)),
  (∀ (x : ι), IsPiSystem (π x)) → ∀ (S : Set ι), IsPiSystem (piiUnionInter π S)
-- Mathlib.Algebra.Order.Group.End
OrderHom.one_eq_id : ∀ {α : Type u_1} [inst : Preorder α], 1 = OrderHom.id
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_injOn_Ioc : ∀ {a b : ℝ}, b - a ≤ 2 * Real.pi → Set.InjOn (⇑Circle.exp) (Set.Ioc a b)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_top : ∀ {G : Type u_2} [inst : AddGroup G], -⊤ = ⊤
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.range_polarization_domRestrict_le_span_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  (P.Polarization.domRestrict (P.rootSpan R)).range ≤ P.corootSpan R
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?.eq_1 : ∀ {s : String.Slice} (pos : s.Pos), pos.get? = if h : pos = s.endPos then none else some (pos.get h)
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_counit_smul : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A} (𝓡 : Coalgebra.Repr R a ι),
  ∑ x ∈ 𝓡.index, CoalgebraStruct.counit (𝓡.left x) • 𝓡.right x = a
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.toReal : ∀ {p q : ENNReal} (r : ENNReal),
  0 < p.toReal → 0 < q.toReal → ∀ [p.HolderTriple q r], p.toReal.HolderTriple q.toReal r.toReal
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.slice_le_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  q.slice p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ String.Slice.Pos.ofSlice p
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContDiffOn.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞},
  ContDiffOn ℝ (↑n) f s → ContDiffOn ℝ (↑n) (fun x => Real.arsinh (f x)) s
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprNoopConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.NoopConfig