mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.numeratorHom_surjective_of_finite : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] [Finite ↥S],
  Function.Surjective ⇑OreLocalization.numeratorHom
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.whiskerRight_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂)
  (Y : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).f =
    CategoryTheory.Limits.prod.map f.f (CategoryTheory.CategoryStruct.id Y.src)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.HasSeparator C] (α : C ≌ D), CategoryTheory.HasSeparator D
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (X_1 : CategoryTheory.Sheaf J (Type v)),
  (J.yonedaOpCompCoyoneda.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.largeCurriedYonedaLemma.inv.app X).app X_1.obj)
      (CategoryTheory.CategoryStruct.comp
        (TypeCat.ofHom fun g =>
          CategoryTheory.CategoryStruct.comp (J.yonedaCompSheafToPresheaf.hom.app (Opposite.unop X)) g)
        ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.hom.app
              (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app
          X_1))
-- Mathlib.Order.Ideal
Order.Ideal.mem_principal : ∀ {P : Type u_1} [inst : Preorder P] {x y : P}, x ∈ Order.Ideal.principal y ↔ x ≤ y
-- Mathlib.Topology.Defs.Basic
WithTopology.ext : ∀ {X : Type u_1} {t : TopologicalSpace X} {x y : WithTopology X t}, x.ofTopology = y.ofTopology → x = y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The polynomial `W(X, Y, Z) := Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³)` associated to a
Weierstrass curve `W` over a ring `R` in projective coordinates.

This is represented as a term of type `MvPolynomial (Fin 3) R`, where `X`, `Y`, and `Z`
represent `X`, `Y`, and `Z` respectively.  -/
WeierstrassCurve.Projective.polynomial : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → MvPolynomial (Fin 3) R
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.mk.sizeOf_spec : ∀ {α α₂ β : Type w} {m : Type w → Type u_1} [inst : SizeOf α] [inst_1 : SizeOf α₂] [inst_2 : SizeOf β]
  [inst_3 : (a : Type w) → SizeOf (m a)] (it₁ : Std.IterM m (Std.IterM m β)) (it₂ : Option (Std.IterM m β)),
  sizeOf { it₁ := it₁, it₂ := it₂ } = 1 + sizeOf it₁ + sizeOf it₂
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_twice : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D)
  {H K : CategoryTheory.Functor D E} (α : H ≅ K),
  F.isoWhiskerLeft (G.isoWhiskerLeft α) = (F.associator G H).symm ≪≫ (F.comp G).isoWhiskerLeft α ≪≫ F.associator G K
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.instCategoryComp : {I : Type w₀} →
  (C : I → Type u₁) →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₁} → (f : J → I) → (j : J) → CategoryTheory.Category.{v₁, u₁} ((C ∘ f) j)
-- Mathlib.Computability.Ackermann
ack_inj_right : ∀ {m n₁ n₂ : ℕ}, ack m n₁ = ack m n₂ ↔ n₁ = n₂
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.conjugate' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] {x : R},
  x ∈ skewAdjoint R → ∀ (z : R), star z * x * z ∈ skewAdjoint R
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.eq_1 : ∀ {α : Type u_1} (op : Stream'.Seq α → Stream'.Seq α),
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op = LipschitzWith 1 op
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_localizationToStalk : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x)
      (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x) =
    CategoryTheory.CategoryStruct.id ((AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.sliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos →
    ∀ (p : s.Pos) (hp : p ≤ pos), String.Slice.Pattern.Model.IsLongestRevMatch pat (p.sliceFrom pos hp)
-- Init.Data.Vector.Zip
Vector.zipWith_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n},
  Vector.zipWith f as bs = Vector.zipWith (fun b a => f a b) bs as
-- Mathlib.CategoryTheory.Elements
/-- The equivalence `F.Elementsᵒᵖ ≅ (yoneda, F)` given by yoneda lemma.  -/
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) → F.Elementsᵒᵖ ≌ CategoryTheory.CostructuredArrow CategoryTheory.yoneda F
-- Init.Data.Nat.Fold
Nat.all_congr : ∀ {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → Bool), n.all f = m.all fun i h => f i ⋯
-- Lean.Elab.Do.Legacy
/-- A code block, and the collection of variables updated by it.  -/
Lean.Elab.Term.Do.CodeBlock : Type
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instFaithfulRestrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), (ModuleCat.restrictScalars f).Faithful
-- Mathlib.Topology.Sheaves.Presheaf
/-- A homeomorphism of spaces gives an equivalence of categories of presheaves.  -/
TopCat.Presheaf.presheafEquivOfIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : TopCat} → (X ≅ Y) → (TopCat.Presheaf C X ≌ TopCat.Presheaf C Y)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabDoElems : Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Syntax)
-- Init.Data.Int.Lemmas
Int.subNatNat_self : ∀ (n : ℕ), Int.subNatNat n n = 0
-- Mathlib.Order.Hom.Basic
OrderIso.prodAssoc_symm_apply : ∀ (α : Type u_6) (β : Type u_7) (γ : Type u_8) [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (p : α × β × γ),
  (RelIso.symm (OrderIso.prodAssoc α β γ)) p = ((p.1, p.2.1), p.2.2)
-- Std.Http.Protocol.H1.Event
/-- Indicates readiness to process the next message.
 -/
Std.Http.Protocol.H1.Event.next : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind.fatalError.sizeOf_spec : sizeOf Lean.Lsp.LeanFileProgressKind.fatalError = 1
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.restrict_scalars' : ∀ {ι : Type u'} (R : Type u_2) {K : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring K] [inst_4 : SMulWithZero R K] [inst_5 : Module K M] [IsScalarTower R K M]
  [FaithfulSMul R K] [IsScalarTower R K K] {v : ι → M}, LinearIndependent K v → LinearIndependent R v
-- Mathlib.Geometry.Manifold.IsManifold.Basic
isManifold_of_contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u_4) [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
  (∀ (e e' : OpenPartialHomeomorph M H),
      e ∈ atlas H M →
        e' ∈ atlas H M →
          ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm.trans e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm.trans e').source ∩ Set.range ↑I)) →
    IsManifold I n M
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) {β : Type u_3} (f : β ≃ α)
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape β C] (X : (i : α) → I i),
  (CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct F f).hom.app X =
    CategoryTheory.Limits.Pi.map' ⇑f.symm fun k => CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.Multiplicity
dvd_iff_multiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, 0 < multiplicity a b ↔ a ∣ b
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_two : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 2 = 1
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The isomorphism `obj F X ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
              (X : C) →
                (i : ↑(Set.Iic j)) → CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨↑i, ⋯⟩ ≅ F.obj i
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasFiniteProducts : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteProducts V], CategoryTheory.Limits.HasFiniteProducts (Action V G)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastVar : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (var : Std.Tactic.BVDecide.BVExpr.bitblast.BVVar w)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (idx : ℕ) (hidx : idx < w),
  ⟦assign.toAIGAssignment,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig var).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig var).vec.get idx hidx }⟧ =
    (Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var var.ident)).getLsbD idx
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.instReprLiteral : Repr BitVec.Literal✝
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.integralClosure_eq_bot_iff : ∀ {R : Type u_1} (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Function.Injective ⇑(algebraMap R A) → (integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- A bimodule object for a pair of monoid objects, all internal to some monoidal category.  -/
Bimod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon C → CategoryTheory.Mon C → Type (max u₁ v₁)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_comp : ∀ {n : Type u} {S S' S'' : AlgebraicGeometry.Scheme} (f : S ⟶ S') (g : S' ⟶ S''),
  AlgebraicGeometry.AffineSpace.map n (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f) (AlgebraicGeometry.AffineSpace.map n g)
-- Mathlib.RingTheory.LinearDisjoint
/-- Two subalgebras `A`, `B` in a commutative ring are linearly disjoint if and only if
`Subalgebra.mulMap A B` is injective.  -/
Subalgebra.linearDisjoint_iff_injective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B ↔ Function.Injective ⇑(A.mulMap B)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.integrable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Submartingale f ℱ μ → ∀ (i : ι), MeasureTheory.Integrable (f i) μ
-- Mathlib.Topology.UniformSpace.Basic
comap_uniformity_addOpposite : ∀ {α : Type ua} [inst : UniformSpace α],
  Filter.comap (fun p => (AddOpposite.op p.1, AddOpposite.op p.2)) (uniformity αᵃᵒᵖ) = uniformity α
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.of_comp_lift : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L),
  ⇑((FreeLieAlgebra.lift R) f) ∘ FreeLieAlgebra.of R = f
-- Mathlib.Order.Sublocale
Sublocale.instCompleteLattice : {X : Type u_1} → [inst : Order.Frame X] → CompleteLattice (Sublocale X)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The forgetful functor from presheaves of modules over a presheaf of rings `R` to presheaves of
`R(X)`-modules where `X` is an initial object.

The functor is implemented as, on object level `M ↦ (c ↦ M(c))` where the `R(X)`-module structure
on `M(c)` is given by restriction of scalars along the unique morphism `R(c) ⟶ R(X)`; and on
morphism level `(f : M ⟶ N) ↦ (c ↦ f(c))`.
 -/
PresheafOfModules.forgetToPresheafModuleCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (X : Cᵒᵖ) →
        CategoryTheory.Limits.IsInitial X →
          CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X)))
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- If `P` is a sheaf, then `P` is isomorphic to `sheafify J P`.  -/
CategoryTheory.isoSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {P : CategoryTheory.Functor Cᵒᵖ D} → CategoryTheory.Presheaf.IsSheaf J P → (P ≅ CategoryTheory.sheafify J P)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.instHashableCall : Hashable Lean.Meta.FunInd.Call
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
QuadraticMap.coeFn_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.one_le_iff_one_le : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, 1 ≤ v₁ x ↔ 1 ≤ v₂ x
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.dominatedFinMeasAdditive_transpose_cbmApplyMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  MeasureTheory.DominatedFinMeasAdditive (μ.transpose B).variation (⇑(μ.transpose B)) 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_subset_iff : ∀ {α : Type u_2} [inst : Add α] {s t u : Set α}, s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.bdd_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜},
  MeasureTheory.Integrable f μ →
    ∀ (C : ℝ), MeasureTheory.AEStronglyMeasurable φ μ → (∀ᵐ (a : α) ∂μ, ‖φ a‖ ≤ C) → MeasureTheory.Integrable (φ • f) μ
-- Mathlib.GroupTheory.NoncommCoprod
AddHom.comp_noncommCoprod : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : AddSemigroup P] (f : M →ₙ+ P)
  (g : N →ₙ+ P) {Q : Type u_4} [inst_3 : AddSemigroup Q] (h : P →ₙ+ Q)
  (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)),
  h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- (Implementation): Inverse for `TensorProduct.piScalarRight`.  -/
TensorProduct.piScalarRightInv : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    (ι : Type u_4) → [Fintype ι] → [DecidableEq ι] → (ι → N) →ₗ[S] TensorProduct R N (ι → R)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.homMk_eta : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U ⟶ V)
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) V.hom = U.hom),
  CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left f) h = f
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.sub_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g g₂ : M [⋀^ι]→ₗ[R] N') (m : ι → M),
  (g - g₂) m = g m - g₂ m
-- Init.Prelude
HOr.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HOr α β γ
-- Mathlib.RingTheory.DualNumber
DualNumber.isNilpotent_eps : ∀ {R : Type u_1} [inst : Semiring R], IsNilpotent DualNumber.eps
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- Commutativity of a square is preserved when taking quotients by an ideal.  -/
Ideal.comp_quotientMap_eq_of_comp_eq : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {R' : Type u_5} {S' : Type u_6} [inst_2 : Ring R']
  [inst_3 : Ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f)
  (I : Ideal S') [inst_4 : I.IsTwoSided],
  have leq := ⋯;
  (Ideal.quotientMap I g' ⋯).comp (Ideal.quotientMap (Ideal.comap g' I) f ⋯) =
    (Ideal.quotientMap I f' ⋯).comp (Ideal.quotientMap (Ideal.comap f' I) g leq)
-- Mathlib.GroupTheory.Index
Subgroup.index_iInf_le : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → Subgroup G),
  (⨅ i, f i).index ≤ ∏ i, (f i).index
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- If a multivariate formal power series is invertible,
then so is its constant coefficient.  -/
MvPowerSeries.isUnit_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R),
  IsUnit φ → IsUnit (MvPowerSeries.constantCoeff φ)
-- Mathlib.Analysis.Convex.Combination
mem_convexHull_pi : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [Finite ι] [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : (i : ι) → AddCommGroup (E i)] [inst_4 : (i : ι) → Module 𝕜 (E i)] {s : Set ι}
  {t : (i : ι) → Set (E i)} {x : (i : ι) → E i}, (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → x ∈ (convexHull 𝕜) (s.pi t)
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- **Cartan's formula** in the case where `0 < meromorphicOrderAt f 0`.
 -/
ValueDistribution.characteristic_top_eq_circleAverage_of_meromorphicOrderAt_pos : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    0 < meromorphicOrderAt f 0 →
      R ≠ 0 →
        ValueDistribution.characteristic f ⊤ R =
          Real.circleAverage (fun x => ValueDistribution.logCounting f (↑x) R) 0 1
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Lean.Parser.Command
/-- Debugging command. Runs the following command in an exported context just like elaboration of
declaration signatures.
 -/
Lean.Parser.Command.withExporting : Lean.Parser.Parser
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two : CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
    (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
      SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two._proof_1) =
  CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.δ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
    (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
      SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two._proof_1)
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.select.injEq : ∀ (finished finished_1 : Std.Async.Waiter Unit),
  (Std.CancellationToken.Consumer.select finished = Std.CancellationToken.Consumer.select finished_1) =
    (finished = finished_1)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instCommutativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.Semiring α], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Analysis.Fourier.PoissonSummation
isBigO_norm_Icc_restrict_atBot : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)} {b : ℝ},
  0 < b →
    (⇑f =O[Filter.atBot] fun x => |x| ^ (-b)) →
      ∀ (R S : ℝ), (fun x => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atBot] fun x => |x| ^ (-b)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] {x : R} {s : Set R},
  x ∈ Subsemiring.closure s ↔ ∀ (S : Subsemiring R), s ⊆ ↑S → x ∈ S
-- Mathlib.RingTheory.Perfectoid.BDeRham
_private.Mathlib.RingTheory.Perfectoid.BDeRham.0.«term𝔹_dR^+(_)» : Lean.ParserDescr
-- Mathlib.Data.PNat.Defs
PNat.mod_coe : ∀ (m k : ℕ+), ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_mul_le_sum_comp_perm_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f (σ i) * g i
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roo_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toArray.getD i fallback = m + 1 + ↑i