mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `F : ComposableArrows C n` and all maps `F.obj i.castSucc ⟶ F.obj i.succ`
are in `W`, then `F.hom : F.left ⟶ F.right` is a transfinite composition of
shape `Fin (n + 1)` of morphisms in `W`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {n : ℕ} →
        (F : CategoryTheory.ComposableArrows C n) →
          (∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))) → W.TransfiniteCompositionOfShape (Fin (n + 1)) F.hom
-- Mathlib.Algebra.Order.Field.Basic
div_pos_of_neg_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → 0 < a / b
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.instSMul : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [SMul R S] → SMul { c // 0 ≤ c } S
-- Lean.Elab.Binders
/-- Eliminate the `let` if it is unused by the body.  -/
Lean.Elab.Term.LetConfig.usedOnly : Lean.Elab.Term.LetConfig → Bool
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify a `BirdDet.birdDet n A` call.  -/
Mathlib.Tactic.Determinant.certBirdDet : {u : Lean.Level} →
  {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.Hom.ext : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} {f g : A ⟶ B},
  f.left = g.left → f.right = g.right → f = g
-- Init.Data.Array.Extract
Array.extract_push : ∀ {α : Type u_1} {as : Array α} {b : α} {start stop : ℕ},
  (as.push b).extract start stop =
    if stop ≤ as.size then as.extract start stop else if start ≤ as.size then (as.extract start).push b else #[]
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.instInvolutiveInv : {α : Type u} → [InvolutiveInv α] → InvolutiveInv (WithOne α)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactlyChars.go : Std.Internal.Parsec.String.Parser Char → ℕ → String → ℕ → Std.Internal.Parsec.String.Parser String
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00Q9](https://stacks.math.columbia.edu/tag/00Q9) -/
Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p], Algebra.ZariskisMainProperty R p
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_c₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The unit fork is a limit provided `F` coreflects it.  -/
CategoryTheory.Comonad.ComonadicityInternal.unitEqualizerOfCoreflectsEqualizer : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              (B : C) →
                [CategoryTheory.Limits.ReflectsLimit
                      (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B)))
                        (adj.unit.app (G.obj (F.obj B))))
                      F] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_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) (n : N), (LinearEquiv.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.I_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ) (n : ℤ),
  (CochainComplex.cm5b.I K).X n = CategoryTheory.Injective.under (K.X n)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → Option (γ a)} {k : α}, k ∈ Std.DTreeMap.filterMap f t → k ∈ t
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valued_toVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (r : R), Valued.v (WithVal.toVal v r) = v r
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_pos_of_mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f → 0 < Function.minimalPeriod f x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.of.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G],
  IsFreeGroup.of = (IsFreeGroup.mulEquiv G).toFun ∘ FreeGroup.of
-- Lean.Meta.InferType
/-- Infers the types of the next `n` parameters that `e` expects. See `arrowDomainsN`.
 -/
Lean.Meta.inferArgumentTypesN : ℕ → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f f' g h : C}
  {η : f ⟶ f'}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj f g ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj f' g}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) h ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f' g) h}
  {η₃ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) h ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj f' (CategoryTheory.MonoidalCategoryStruct.tensorObj g h)}
  {η₄ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g h) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj f' (CategoryTheory.MonoidalCategoryStruct.tensorObj g h)},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight η g = η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight η₁ h = η₂ →
      CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategoryStruct.associator f' g h).hom = η₃ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f g h).inv η₃ = η₄ →
          CategoryTheory.MonoidalCategoryStruct.whiskerRight η (CategoryTheory.MonoidalCategoryStruct.tensorObj g h) =
            η₄
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_val_assemble₂ : ∀ {w x : UInt8} (c : Char),
  ByteArray.utf8DecodeChar?.assemble₂ w x = some c →
    c.val.toBitVec = BitVec.setWidth 32 (BitVec.setWidth 5 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec)
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by setting the lower bound to zero and the maximum value to (m - n).
 -/
Std.Time.Internal.Bounded.LE.truncate : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → Std.Time.Internal.Bounded.LE 0 (m - n)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.uniqueIso_default : ∀ {A : Type u} (x y : CategoryTheory.Codiscrete A), default = x.iso y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toOrderHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], Function.Injective OrderMonoidHom.toOrderHom
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.SzemerediRegularity.pairwiseDisjoint_distinctPairs : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  (↑P.parts.offDiag.attach).PairwiseDisjoint (SzemerediRegularity.distinctPairs✝ hP G ε)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.isCauSeq : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} (f : CauSeq β abv), IsCauSeq abv ↑f
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.id_coe : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⇑LinearMap.id = id
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyEq.countable_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋃ i, s i =ᶠ[l] ⋃ i, t i
-- Init.Data.SInt.Lemmas
ISize.le_trans : ∀ {a b c : ISize}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_le_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α},
  BddBelow (Set.range f) → ∀ (c : ι), f c ≤ a → iInf f ≤ a
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodX_ext_to : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι}
  {f g : A ⟶ (K ⊞ L).X i},
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) =
      CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i) →
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i) →
      f = g
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.range_liftAux : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r),
  (TrivSqZeroExt.lift f g hg hfg hgf).range = f.range ⊔ Algebra.adjoin S (Set.range ⇑g)
-- Mathlib.Algebra.Divisibility.Basic
pow_dvd_pow : ∀ {α : Type u_1} [inst : Monoid α] {m n : ℕ} (a : α), m ≤ n → a ^ m ∣ a ^ n
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplex.eq_1 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  Λ.chainComplex X =
    ChainComplex.mk' (Λ.F.obj X) (Λ.F.obj (CategoryTheory.Limits.kernel (Λ.π.app X)))
      (ι.preimage
        (CategoryTheory.CategoryStruct.comp (Λ.π.app (CategoryTheory.Limits.kernel (Λ.π.app X)))
          (CategoryTheory.Limits.kernel.ι (Λ.π.app X))))
      fun {X₀ X₁} f =>
      ⟨Λ.F.obj (CategoryTheory.Limits.kernel (ι.map f)),
        ⟨ι.preimage
            (CategoryTheory.CategoryStruct.comp (Λ.π.app (CategoryTheory.Limits.kernel (ι.map f)))
              (CategoryTheory.Limits.kernel.ι (ι.map f))),
          ⋯⟩⟩
-- Std.Http.Server.Config
/-- Connection limits configuration with validation.
 -/
Std.Http.Config : Type
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.inclusion_apply : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) (a : ↥L),
  (BooleanSubalgebra.inclusion h) a = Set.inclusion h a
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_comp : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} {N' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup N']
  [inst_6 : Module R N'] (f : M →ₗ[R] N) (g : N →ₗ[R] N'),
  exteriorPower.map n (g ∘ₗ f) = exteriorPower.map n g ∘ₗ exteriorPower.map n f
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore'_eq_sSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
  Ideal.homogeneousCore' 𝒜 I = sSup {J | Ideal.IsHomogeneous 𝒜 J ∧ J ≤ I}
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Icc_iff : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ b₁ → (Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- A monoidal functor between skeletal monoidal categories induces a monoid homomorphism.  -/
CategoryTheory.Skeletal.monoidHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                (hC : CategoryTheory.Skeletal C) →
                  (hD : CategoryTheory.Skeletal D) →
                    have x := CategoryTheory.monoidOfSkeletalMonoidal hC;
                    have x_1 := CategoryTheory.monoidOfSkeletalMonoidal hD;
                    C →* D
-- Mathlib.Algebra.BigOperators.Pi
Pi.list_prod_apply : ∀ {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → Monoid (M a)] (a : α) (l : List ((a : α) → M a)),
  l.prod a = (List.map (fun f => f a) l).prod
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- A sum of extended nonnegative reals which is finite can have only finitely many terms
above any positive threshold.  -/
ENNReal.finite_const_le_of_tsum_ne_top : ∀ {ι : Type u_4} {a : ι → ENNReal}, ∑' (i : ι), a i ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → {i | ε ≤ a i}.Finite
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_of_factorization_le_one : ∀ {n : ℕ}, n ≠ 0 → (∀ (p : ℕ), n.factorization p ≤ 1) → Squarefree n
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `y ∈ S`, `- (f y)` is unique.  -/
AddSubmonoid.LocalizationMap.neg_unique : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y : ↥S} {z : N},
  f ↑y + z = 0 → ↑(-(IsAddUnit.liftRight (f.domRestrict S) h) y) = z
-- Mathlib.RingTheory.TensorProduct.Maps
LinearMap.tensorProduct_apply : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] (a : TensorProduct R A (M →ₗ[R] N)),
  (LinearMap.tensorProduct R A M N) a =
    (TensorProduct.liftAux
        (↑R { toFun := fun a => a • LinearMap.baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ }))
      a
-- Std.Data.TreeSet.Raw.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.Raw.get! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.Topology.MetricSpace.Thickening
Disjoint.exists_cthickenings : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Disjoint s t → IsCompact s → IsClosed t → ∃ δ, 0 < δ ∧ Disjoint (Metric.cthickening δ s) (Metric.cthickening δ t)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg : ∀ {w : ℕ} {x : BitVec w}, (-x).toInt = (-x.toInt).bmod (2 ^ w)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.isoApp_symm : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y),
  CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_apply_mul_eqOn_Ici : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → Set.EqOn (fun t => p.rpowIntegrand₀₁ (x * t) x * x) (fun t => p.rpowIntegrand₀₁ t 1 * x ^ p) (Set.Ici 0)
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssocProd_symm_apply_snd : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : (a : α) × (b : β) × γ a b),
  (Equiv.sigmaAssocProd.symm a).snd = ((Equiv.sigmaAssoc γ).symm a).snd
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] {d : n → α} {m : ℕ}
  [inst_3 : m.AtLeastTwo], Matrix.diagonal d = OfNat.ofNat m ↔ d = OfNat.ofNat m
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_prodExtendRight : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (a : α) (σ : Equiv.Perm β), Equiv.Perm.sign (Equiv.Perm.prodExtendRight a σ) = Equiv.Perm.sign σ
-- Mathlib.Analysis.RCLike.Basic
RCLike.instCStarRing : ∀ {K : Type u_1} [inst : RCLike K], CStarRing K
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskeringLeft_δ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} E] [inst_3 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (X Y : CategoryTheory.Functor D E) (X_1 : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ ((CategoryTheory.Functor.whiskeringLeft C D E).obj F) X Y).app X_1 =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (X.obj (F.obj X_1)) (Y.obj (F.obj X_1)))
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.instMonoδ₀Iter : ∀ (i : ℕ) {n m : ℕ} (hi : n + i = m), CategoryTheory.Mono (SimplexCategory.δ₀Iter i hi)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `S₀` is a "semigroup with zero” if it is a semigroup with zero element, and `0` is left
and right absorbing.  -/
SemigroupWithZero : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.normalizedChainComplexFunctorObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (R : C) {X Y : SSet} (f : X ⟶ Y),
  (SSet.normalizedChainComplexFunctorObj R).map f = SSet.normalizedChainComplexMap f R
-- Mathlib.NumberTheory.Divisors
Nat.divisors_filter_dvd_of_dvd : ∀ {n m : ℕ}, n ≠ 0 → m ∣ n → {d ∈ n.divisors | d ∣ m} = m.divisors
-- Mathlib.Data.Complex.Basic
Complex.inv_zero : 0⁻¹ = 0
-- Mathlib.Data.Num.Basic
/-- Greatest Common Divisor (GCD) of two `ZNum`s.  -/
ZNum.gcd : ZNum → ZNum → Num
-- Mathlib.Util.Notation3
Mathlib.Notation3.expandFoldl : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_int16ToInt : ∀ (x : Int16), Int64.ofIntClamp x.toInt = x.toInt64
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Mathlib.Order.Filter.Lift
Filter.lift'_inf_le : ∀ {α : Type u_1} {β : Type u_2} (f g : Filter α) (s : Set α → Set β), (f ⊓ g).lift' s ≤ f.lift' s ⊓ g.lift' s
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instLiftingFunctorUniq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] →
                      CategoryTheory.Localization.Lifting L₁ W' L₂ (CategoryTheory.Localization.uniq L₁ L₂ W').functor
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The triangle inequality for an `AbsoluteValue` applied to a list.  -/
AbsoluteValue.listSum_le : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [AddLeftMono S] (l : List R), abv l.sum ≤ (List.map (⇑abv) l).sum
-- Init.Data.List.Monadic
/-- Applies the monadic action `f` on every element in the list, left-to-right, and returns the list of
results.

This is a non-tail-recursive variant of `List.mapM` that's easier to reason about. It cannot be used
as the main definition and replaced by the tail-recursive version because they can only be proved
equal when `m` is a `LawfulMonad`.
 -/
List.mapM' : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → m β) → List α → m (List β)
-- Mathlib.Algebra.Ring.Defs
Ring.zsmul_neg' : ∀ {R : Type u} [self : Ring R] (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
-- Mathlib.Order.RelClasses
/-- A connected order is one satisfying the condition `a < c → a < b ∨ b < c`.
This is recognizable as an intuitionistic substitute for `a ≤ b ∨ b ≤ a` on
the constructive reals, and is also known as negative transitivity,
since the contrapositive asserts transitivity of the relation `¬ a < b`.  -/
IsOrderConnected : (α : Type u) → (α → α → Prop) → Prop
-- Mathlib.RingTheory.PrincipalIdealDomain
top_isPrincipal : ∀ {R : Type u} [inst : Semiring R], ⊤.IsPrincipal
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  (CategoryTheory.Limits.BinaryFan.map F s).fst = F.map s.fst
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  {x y : A.Hom B}, x = y ↔ x.f = y.f
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.natCast_log : ∀ (m n : ℕ), ↑(Nat.log m n) = Ordinal.log ↑m ↑n
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toComon_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.Comon (CategoryTheory.Mon C)),
  ((CategoryTheory.Bimon.toComon C).obj A).X = A.X.X
-- Init.Data.String.Iterator
Substring.toIterator : Substring.Raw → String.Legacy.Iterator
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.measurable : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module R E] [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_5 : SeminormedAddCommGroup F]
  [inst_6 : Module R F] [inst_7 : MeasurableSpace F] [BorelSpace F] (L : E →L[R] F), Measurable ⇑L
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_compl_mul_prod : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), (∏ i ∈ sᶜ, f i) * ∏ i ∈ s, f i = ∏ i, f i