mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_edgeSet_sdiff_eq_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), G.restrict (G.edgeSet \ F) = G.deleteEdges F
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C]
  [inst_3 : P.IsStableUnderBraiding] (c : CategoryTheory.WideSubcategory P) [inst_4 : CategoryTheory.ComonObj c.obj]
  [CategoryTheory.IsCommComonObj c.obj] [inst_6 : P.IsStableUnderComonoid c.obj], CategoryTheory.IsCommComonObj c
-- Mathlib.Tactic.DefEqAbuse
/-- Find the deepest failing `Meta.isDefEq` trace nodes (leaf failures).
Skips `onFailure` retry nodes and ignores ✅️ branches (recovered failures aren't root causes).  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.findLeafFailures : Lean.MessageData → BaseIO (Array Lean.MessageData)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Creates the stream of integer and fractional parts of a value `v` needed to obtain the continued
fraction representation of `v` in `GenContFract.of`. More precisely, given a value `v : K`, it
recursively computes a stream of option `ℤ × K` pairs as follows:
- `stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩`
- `stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`,
  if `stream v n = some ⟨_, frₙ⟩` and `frₙ ≠ 0`
- `stream v (n + 1) = none`, otherwise

For example, let `(v : ℚ) := 3.4`. The process goes as follows:
- `stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩ = some ⟨3, 0.4⟩`
- `stream v 1 = some ⟨⌊0.4⁻¹⌋, 0.4⁻¹ - ⌊0.4⁻¹⌋⟩ = some ⟨⌊2.5⌋, 2.5 - ⌊2.5⌋⟩ = some ⟨2, 0.5⟩`
- `stream v 2 = some ⟨⌊0.5⁻¹⌋, 0.5⁻¹ - ⌊0.5⁻¹⌋⟩ = some ⟨⌊2⌋, 2 - ⌊2⌋⟩ = some ⟨2, 0⟩`
- `stream v n = none`, for `n ≥ 3`
 -/
GenContFract.IntFractPair.stream : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] → [FloorRing K] → K → Stream' (Option (GenContFract.IntFractPair K))
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instStrictBackwardPatternForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.StrictBackwardPattern p
-- Mathlib.Data.List.NodupEquivFin
List.Nodup.getEquiv_symm_apply_val : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (H : l.Nodup) (x : { x // x ∈ l }),
  ↑((List.Nodup.getEquiv l H).symm x) = List.idxOf (↑x) l
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M], Function.mulSupport 1 = ∅
-- Mathlib.Tactic.Linarith.Datatypes
/-- `mkSingleCompZeroOf c h` assumes that `h` is a proof of `t R 0`.
It produces a pair `(R', h')`, where `h'` is a proof of `c*t R' 0`.
Typically `R` and `R'` will be the same, except when `c = 0`, in which case `R'` is `=`.
If `c = 1`, `h'` is the same as `h` -- specifically, it does *not* change the type to `1*t R 0`.
 -/
Mathlib.Tactic.Linarith.mkSingleCompZeroOf : ℕ → Lean.Expr → Lean.MetaM (Mathlib.Ineq × Lean.Expr)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {W : Submodule R M},
  B.IsRefl → W ⊓ B.orthogonal W ≤ Submodule.map W.subtype (LinearMap.ker (B.restrict W))
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_div : ∀ {R : Type u} [inst : EuclideanDomain R] {x y z : R}, y ∣ x → z ∣ x / y → x / y / z = x / (y * z)
-- Init.System.FilePath
_private.Init.System.FilePath.0.System.FilePath.afterRootDirectory : (p : System.FilePath) → p.toString.Pos
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set at `x`, then it is the uniform limit
of the partial sums of this power series on strict subdisks of the disk of convergence, i.e.,
`f (x + y)` is the uniform limit of `p.partialSum n y` there.  -/
HasFPowerSeriesWithinOnBall.tendstoUniformlyOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ↑r' < r →
      TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop
        ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')
-- Mathlib.Algebra.Field.Defs
/-- `a / b := a * b⁻¹`  -/
Semifield.div_eq_mul_inv : ∀ {K : Type u_2} [self : Semifield K] (a b : K), a / b = a * b⁻¹
-- Mathlib.Data.Finset.Sort
Finset.mem_sort : ∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] {a : α}, a ∈ s.sort r ↔ a ∈ s
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplex_unitIso : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.dgoEquivHomologicalComplex b V).unitIso = HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPNumericTypes : Lean.Options → Bool
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.autEquivPow_apply : ∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] (L : Type u_2) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K))
  (a : L ≃ₐ[K] L), (IsCyclotomicExtension.autEquivPow L h) a = (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun a
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.starProjection_apply_eq_isComplProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (x : E), K.starProjection x = (K.projection Kᗮ ⋯) x
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.finsetSum_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [inst : SeminormedAddCommGroup β] {ι : Type u_8} {s : Finset ι}
  (hs : s.Nonempty) (μ : ι → MeasureTheory.Measure α) (T : ι → Set α → β) (C : ι → ℝ),
  (∀ (i : ι), MeasureTheory.DominatedFinMeasAdditive (μ i) (T i) (C i)) →
    MeasureTheory.DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C)
-- Mathlib.Algebra.Star.Basic
star_natCast : ∀ {R : Type u} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (n : ℕ), star ↑n = ↑n
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.bind_diag_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] {X : C}
  (P : CategoryTheory.Limits.ColimitPresentation J X)
  (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j))
  [inst_3 : ∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [inst_4 : ∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)]
  (k : CategoryTheory.Limits.ColimitPresentation.Total Q), (P.bind Q).diag.obj k = (Q k.fst).diag.obj k.snd
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The diagram sending each pointed Galois object to its automorphism group
as an object of `C`.  -/
CategoryTheory.PreGaloisCategory.autGaloisSystem : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        CategoryTheory.Functor (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) GrpCat
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom =
    TypeCat.ofHom Sum.inr
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Inner product defined by the `InnerProductSpace.Core` structure. We can't reuse
`InnerProductSpace.Core.toInner` because it takes `InnerProductSpace.Core` as an explicit
argument.  -/
InnerProductSpace.Core.toInner' : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [cd : InnerProductSpace.Core 𝕜 F] → Inner 𝕜 F
-- Mathlib.Algebra.Group.Finsupp
/-- When ι is finite and M is an AddMonoid,
then Finsupp.equivFunOnFinite gives an AddEquiv  -/
Finsupp.addEquivFunOnFinite : {M : Type u_3} → [inst : AddZeroClass M] → {ι : Type u_8} → [Finite ι] → (ι →₀ M) ≃+ (ι → M)
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr_apply : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) (a : α₂),
  (e₁.arrowCongr e₂) f a = (⇑e₂ ∘ f ∘ ⇑e₁.symm) a
-- Mathlib.Order.Hom.Basic
OrderIso.isCompl_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : α ≃o β) {x y : α}, IsCompl x y ↔ IsCompl (f x) (f y)
-- Mathlib.Topology.Defs.Basic
/-- Notation for `IsOpen` with respect to a non-standard topology.  -/
Topology.IsOpen_of : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ)
  {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F.op n).inv.app
          (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Dᵒᵖ n).map
            ((CategoryTheory.Functor.commShiftIso F n).hom.app (Opposite.unop X)).op).unop
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app
              (Opposite.op (F.obj (Opposite.unop X)))).unop
          h))
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_symm_apply_snd : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (a : B × F),
  (↑(Bundle.Trivial.trivialization B F).symm a).snd = a.2
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.zero_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  (CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁.right h₂.right
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmodule.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B B_1 : LinearMap.BilinForm S M),
  B = B_1 → ∀ (N N_1 : Submodule R M), N = N_1 → B.dualSubmodule N = B_1.dualSubmodule N_1
-- Mathlib.Data.ZMod.Units
/-- `unitsMap_val` shows that coercing from `(ZMod m)ˣ` to `ZMod n` gives the same result
when going via `(ZMod n)ˣ` and `ZMod m`.  -/
ZMod.unitsMap_val : ∀ {n m : ℕ} (h : n ∣ m) (a : (ZMod m)ˣ), ↑((ZMod.unitsMap h) a) = (↑a).cast
-- Mathlib.Tactic.DeriveFintype
Mathlib.Deriving.Fintype.mkFintypeInstanceHandler : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  [SecondCountableTopology α] [OrderClosedTopology α], Measurable fun p => p.1 < p.2
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instHasDistribNeg : {R : Type u_1} → [inst : Mul R] → [HasDistribNeg R] → HasDistribNeg Rᵒᵈ
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_le_prod_top : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex), A.prod B ≤ A.prod ⊤
-- Mathlib.Data.Fintype.Quotient
Trunc.finLiftOn_empty : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} {β : Sort u_3} [e : IsEmpty ι]
  (q : (i : ι) → Trunc (α i)), Trunc.finLiftOn q = fun f x => f fun a => e.elim a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α}, BddBelow s → b ∈ s → b ≤ a → sInf s ≤ a
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toRingHom_fromOpposite : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  ↑(f.fromOpposite hf) = (↑f).fromOpposite hf
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.nonneg : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  0 ≤ (f i) x
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_ofColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Colex α}, IsAddRegular (ofColex a) ↔ IsAddRegular a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_support_finsetSum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {s : Finset ι} {h : ι → α →₀ M},
  ∀ a ∈ (∑ c ∈ s, h c).support, ∃ c ∈ s, a ∈ (h c).support
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The evaluation at a point, as a continuous linear map from `α →ᵇ β` to `β`.  -/
BoundedContinuousFunction.evalCLM : {α : Type u} →
  {β : Type v} →
    (𝕜 : Type u_2) →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : Semiring 𝕜] →
              [inst_4 : AddCommMonoid β] →
                [inst_5 : Module 𝕜 β] →
                  [inst_6 : IsBoundedSMul 𝕜 β] →
                    [inst_7 : BoundedAdd β] → [inst_8 : ContinuousAdd β] → α → BoundedContinuousFunction α β →L[𝕜] β
-- Aesop.Index.RulePattern
/-- Build a rule pattern substitution map from an array of substitutions.  -/
Aesop.RulePatternSubstMap.ofArray : Array (Aesop.RuleName × Aesop.Substitution) → Aesop.RulePatternSubstMap
-- Init.Data.SInt.Lemmas
Int16.ofNat_bitVecToNat : ∀ (n : BitVec 16), Int16.ofNat n.toNat = Int16.ofBitVec n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A coequalizer that is a monomorphism is an isomorphism.  -/
CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Cofork f g}
  (h : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Mono c.π], CategoryTheory.IsIso c.π
-- Mathlib.Order.Directed
Std.Total.directedOn : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (s : Set α), DirectedOn r s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_inter_eq_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.Algebra.Group.Defs
inv_mul_cancel_comm_assoc : ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a⁻¹ * (b * a) = b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.mk x = 0 ↔ x ∈ CochainComplex.HomComplex.coboundaries K L n
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- `C` has all limits over any type `J` whose objects and morphisms lie in the same universe
and which has countably many objects and morphisms  -/
CategoryTheory.Limits.HasCountableColimits.out : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableColimits C]
  (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_odd : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.Ψ (2 * m + 1) =
    W.Ψ (m + 2) * W.Ψ m ^ 3 - W.Ψ (m - 1) * W.Ψ (m + 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        Polynomial.C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3 else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3)
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the forward direction of `isLowerSet_iff_Iic_subset`. -/
IsLowerSet.Iic_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s
-- Std.Http.Internal.String
/-- Quotes `s` as an HTTP `quoted-string`: `DQUOTE *( qdtext / quoted-pair ) DQUOTE`.

If every character is a `tchar` and the string is non-empty, the string is returned as-is (it is
already a valid token). Otherwise the string is wrapped in double quotes, escaping `"` and `\`
as `quoted-pair`.

Requires a proof that every character passes `quotedStringChar`.
 -/
Std.Http.Internal.quoteHttpString : (s : String) → s.toList.all Std.Http.Internal.Char.quotedStringChar = true → String
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (κ.singularPart η) a = 0 ↔ (κ a).AbsolutelyContinuous (η a)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalNonAssocRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalNonAssocRing R] → NonUnitalNonAssocRing (HahnSeries Γ R)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_inf : ∀ {M : Type u_1} [inst : Mul M] (p p' : Subsemigroup M), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.quotientCompQhIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) {Z : DerivedCategory C}
  (h : DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f)
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).inv.app L) h) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).inv.app K)
      (CategoryTheory.CategoryStruct.comp
        (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f)) h)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_const_mul : ∀ {𝕜 : Type u_2} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜]
  (r : 𝕜) (f : ℝ → 𝕜), ∫ (x : ℝ) in a..b, r * f x ∂μ = r * ∫ (x : ℝ) in a..b, f x ∂μ
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.contains : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Bool
-- Mathlib.Order.Std
/-- The `Min` instance of the order. This can always be automatically derived.  -/
LinearOrder.OfStdArgs.min : {α : Type u_1} →
  (self : LinearOrder.OfStdArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    Min α
-- Init.Data.List.Sort.Lemmas
/-- If the input list is already sorted, then `mergeSort` does not change the list.
 -/
List.mergeSort_of_pairwise : ∀ {α : Type u_1} {le : α → α → Bool} {l : List α}, List.Pairwise (fun a b => le a b = true) l → l.mergeSort le = l
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.coe_pointwise_smul : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (m : M)
  (S : AddSubmonoid A), ↑(m • S) = m • ↑S
-- Mathlib.Order.Category.Preord
_private.Mathlib.Order.Category.Preord.0.Preord.Hom.mk.sizeOf_spec : ∀ {X Y : Preord} (hom' : ↑X →o ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.handlerDispatched : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Bool
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instCoeSortType : (R : Type u) → [inst : CommRing R] → CoeSort (AlgCat R) (Type v)
-- Mathlib.Algebra.Order.ZeroLEOne
Int.instZeroLEOneClass : ZeroLEOneClass ℤ
-- Mathlib.Data.Finsupp.Defs
/-- **Alias** of `Finsupp.embDomain_of_notMem_range`. -/
Finsupp.embDomain_notin_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M),
  ∀ a ∉ Set.range ⇑f, (Finsupp.embDomain f v) a = 0
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits SemiRingCat
-- Lean.Expr
Lean.Expr.mdata.inj : ∀ {data : Lean.MData} {expr : Lean.Expr} {data_1 : Lean.MData} {expr_1 : Lean.Expr},
  Lean.Expr.mdata data expr = Lean.Expr.mdata data_1 expr_1 → data = data_1 ∧ expr = expr_1
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The pre-path object object obtained from a cylinder in the opposite category.  -/
HomotopicalAlgebra.Precylinder.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Cᵒᵖ} → HomotopicalAlgebra.Precylinder A → HomotopicalAlgebra.PrepathObject (Opposite.unop A)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.elimExpr : Lean.Meta.ElimInfo → Lean.Expr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape.eq_1 : ∀ {Γ : Type u_1} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (T : Turing.Tape Γ),
  Turing.TM1to1.trTape enc0 T = Turing.TM1to1.trTape' enc0 T.left T.right₀
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.succFn_le_of_lt : ∀ {ι : Type u_1} [inst : LinearOrder ι] (i j : ι), i < j → LinearLocallyFiniteOrder.succFn i ≤ j
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x) = ⋃₀ ↑J
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_smul_iff : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {𝕜 : Type u_7} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 E] {f : α → E} (c : 𝕜),
  MeasureTheory.IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ MeasureTheory.IntegrableAtFilter f l μ