mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_sum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) (s : Set α),
  ∑' (i : ι), (f i) s ≤ (MeasureTheory.Measure.sum f) s
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `prod F G` is a limit cone.  -/
CategoryTheory.FunctorToTypes.binaryProductLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Limits.IsLimit (CategoryTheory.FunctorToTypes.binaryProductCone F G)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.mabs_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Group (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → Lattice (α i)] (i : ι), |f|ₘ i = |f i|ₘ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Turn a right exact functor into an object of the category `RightExactFunctor C D`.  -/
CategoryTheory.RightExactFunctor.of : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [CategoryTheory.Limits.PreservesFiniteColimits F] → C ⥤ᵣ D
-- Mathlib.Data.Nat.Size
/-- **Alias** of `Nat.shiftLeft'_true_eq_mul_pow`. -/
Nat.shiftLeft'_tt_eq_mul_pow : ∀ (m n : ℕ), Nat.shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.norm_nonneg : ∀ (x : GaussianInt), 0 ≤ Zsqrtd.norm x
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : Fintype Ω] {s : Set Ω},
  (ProbabilityTheory.uniformOn Set.univ) s = MeasureTheory.Measure.count s / ↑(Fintype.card Ω)
-- Mathlib.Order.WithBot
WithTop.map_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ},
  g₁ ∘ f₁ = g₂ ∘ f₂ → ∀ (a : α), WithTop.map g₁ (WithTop.map f₁ ↑a) = WithTop.map g₂ (WithTop.map f₂ ↑a)
-- Mathlib.NumberTheory.Multiplicity
Int.two_pow_sub_pow' : ∀ {x y : ℤ} (n : ℕ), 4 ∣ x - y → ¬2 ∣ x → emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity 2 ↑n
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.functor : Functor Ultrafilter
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
SubmodulesRingBasis.toSubmodulesBasis : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] {B : ι → Submodule R A},
  SubmodulesRingBasis B → (∀ (m : A) (i : ι), ∀ᶠ (a : R) in nhds 0, a • m ∈ B i) → SubmodulesBasis B
-- Mathlib.Order.Filter.Lift
/-- If `(p : ι → Prop, s : ι → Set α)` is a basis of a filter `f`, `g` is a monotone function
`Set α → Filter γ`, and for each `i`, `(pg : β i → Prop, sg : β i → Set α)` is a basis
of the filter `g (s i)`, then
`(fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (i : ι) (x : β i) ↦ sg i x)` is a basis
of the filter `f.lift g`.

This basis is parametrized by `i : ι` and `x : β i`, so in order to formulate this fact using
`Filter.HasBasis` one has to use `Σ i, β i` as the index type, see `Filter.HasBasis.lift`.
This lemma states the corresponding `mem_iff` statement without using a sigma type.  -/
Filter.HasBasis.mem_lift_iff : ∀ {α : Type u_1} {γ : Type u_3} {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
  f.HasBasis p s →
    ∀ {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {g : Set α → Filter γ},
      (∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) →
        Monotone g → ∀ {s : Set γ}, s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.max_sum_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  {s : Multiset ι} {f g : ι → α},
  max (Multiset.map f s).sum (Multiset.map g s).sum ≤ (Multiset.map (fun i => max (f i) (g i)) s).sum
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- The image of a morphism which is equal to zero is the zero object.  -/
CategoryTheory.Limits.imageZero' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X Y : C} →
          {f : X ⟶ Y} → f = 0 → [inst_3 : CategoryTheory.Limits.HasImage f] → CategoryTheory.Limits.image f ≅ 0
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.intCast_neg : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (i : ℤ),
  Lean.Grind.Ring.OfSemiring.intCast (-i) = Lean.Grind.Ring.OfSemiring.neg (Lean.Grind.Ring.OfSemiring.intCast i)
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.Prod.upMulHom : (G : Type u) → (H : Type v) → [inst : Mul G] → [inst_1 : Mul H] → G × H →ₙ* (b : Bool) → I✝ G H b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X₁ ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f)
        CategoryTheory.AddMonObj.add) =
    f
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Given a `UpperSet` of `ArchimedeanClass`,
all group elements belonging to these classes form a subsemigroup.
This is not yet a subgroup because it doesn't contain the identity if `s = ⊤`.  -/
ArchimedeanClass.subsemigroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → UpperSet (ArchimedeanClass M) → AddSubsemigroup M
-- Mathlib.GroupTheory.Divisible
Prod.rootableBy.eq_1 : ∀ {β : Type u_3} {B : Type u_4} {B' : Type u_5} [inst : Pow B β] [inst_1 : Pow B' β] [inst_2 : Zero β]
  [inst_3 : Monoid B] [inst_4 : Monoid B'] [inst_5 : RootableBy B β] [inst_6 : RootableBy B' β],
  Prod.rootableBy =
    { root := fun p n => (RootableBy.root p.1 n, RootableBy.root p.2 n), root_zero := ⋯, root_cancel := ⋯ }
-- Init.Data.Array.Lemmas
/-- Variant of `foldl_reverse` with a side condition for the `stop` argument.  -/
Array.foldl_reverse' : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {b : β} {stop : ℕ},
  stop = xs.size → Array.foldl f b xs.reverse 0 stop = Array.foldr (fun x y => f y x) b xs
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x : M × M₂),
  (f.prodMap g) x = (f x.1, g x.2)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_eq_of_degree_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {q : Polynomial S},
  p.degree = q.degree → p.natDegree = q.natDegree
-- Init.Data.FloatArray.Basic
/-- We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
This is similar to the `Array` version.
 -/
FloatArray.forInUnsafe : {β : Type v} → {m : Type v → Type w} → [Monad m] → FloatArray → β → (Float → β → m (ForInStep β)) → m β
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_eq_zero : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {B : LinearMap.BilinMap R M N},
  B.toQuadraticMap = 0 ↔ LinearMap.IsAlt B
-- Mathlib.Data.List.Basic
List.ext_get_iff : ∀ {α : Type u} {l₁ l₂ : List α},
  l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
-- Init.Data.UInt.Lemmas
UInt64.neg_add : ∀ {a b : UInt64}, -(a + b) = -a - b
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X Y : CochainComplex C ℤ) (a b : ℤ),
  a < b → ∀ [X.IsStrictlyLE a] [Y.IsStrictlyGE b], Subsingleton (DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_smul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A]
  [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [inst_9 : Module ℝ A] [inst_10 : SMulCommClass ℝ A A]
  [inst_11 : IsScalarTower ℝ A A] [inst_12 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarModule 𝕜 A] [StarModule ℝ A]
  [IsScalarTower ℝ 𝕜 A] (r : 𝕜) (a : A), CFC.abs (r • a) = ‖r‖ • CFC.abs a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α} {fallback : Unit},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l) k fallback = ()
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- A linear equivalence which is a homothety is a continuous linear equivalence.  -/
ContinuousLinearEquiv.ofHomothety : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} →
                      {σ₂₁ : 𝕜₂ →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ] →
                            (f : E ≃ₛₗ[σ] F) → (a : ℝ) → 0 < a → (∀ (x : E), ‖f x‖ = a * ‖x‖) → E ≃SL[σ] F
-- Mathlib.RingTheory.AdicCompletion.Functoriality
LinearMap.reduceModIdeal_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M),
  (LinearMap.reduceModIdeal I f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
-- Mathlib.Data.Sum.Order
Sum.inl_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], StrictMono Sum.inl
-- Mathlib.Algebra.Order.Group.End
RelIso.coe_mul : ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r), ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h.leftHomologyIso.hom h.homologyIso.inv = S.leftHomologyIso.hom
-- Lean.Meta.BinderNameHint
_private.Lean.Meta.BinderNameHint.0.Lean.enterScope : Lean.Name → Array Lean.Name → Array Lean.Name
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Spec_stalkClosedPointIso : ∀ (R : CommRingCat) [inst : IsLocalRing ↑R],
  AlgebraicGeometry.Spec.map (AlgebraicGeometry.stalkClosedPointIso R).inv =
    (AlgebraicGeometry.Spec R).fromSpecStalk (IsLocalRing.closedPoint ↑R)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_lt_encard_iff_dep : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite],
  autoParam (X ⊆ M.E) Matroid.eRk_lt_encard_iff_dep._auto_1 → (M.eRk X < X.encard ↔ M.Dep X)
-- Init.Prelude
/-- Sequences the effects of two terms, discarding the value of the first. This function is usually
invoked via the `*>` operator.

Given `x : f α` and `y : f β`, `x *> y` runs `x`, then runs `y`, and finally returns the result of
`y`.

The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `*>` in identifiers is `seqRight`. -/
SeqRight.seqRight : {f : Type u → Type v} → [self : SeqRight f] → {α β : Type u} → f α → (Unit → f β) → f β
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_iSup_of_directed : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → AddSubmonoid M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_natCast_cpow_of_re_ne_zero : ∀ (n : ℕ) {s : ℂ}, s.re ≠ 0 → ‖↑n ^ s‖ = ↑n ^ s.re
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_lt_top : ∀ {n : ℕ∞}, ↑n < ⊤ ↔ n < ⊤
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanFileProgressParams : Lean.ToJson Lean.Lsp.LeanFileProgressParams
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_coe : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), ⇑↑f = ⇑f
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (F : Set X) (x y : X), JoinedIn F x y = ∃ γ, ∀ (t : ↑unitInterval), γ t ∈ F
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' fallback : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then k else fallback
        else t.getKeyD k' fallback
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrLemma.mk.inj : ∀ {keys : List Mathlib.Tactic.GCongr.GCongrKey} {declName : Lean.Name}
  {mainSubgoals : Array Mathlib.Tactic.GCongr.GCongrHyp} {numHyps prio numVarying : ℕ} {forGrw : Bool}
  {keys_1 : List Mathlib.Tactic.GCongr.GCongrKey} {declName_1 : Lean.Name}
  {mainSubgoals_1 : Array Mathlib.Tactic.GCongr.GCongrHyp} {numHyps_1 prio_1 numVarying_1 : ℕ} {forGrw_1 : Bool},
  { keys := keys, declName := declName, mainSubgoals := mainSubgoals, numHyps := numHyps, prio := prio,
        numVarying := numVarying, forGrw := forGrw } =
      { keys := keys_1, declName := declName_1, mainSubgoals := mainSubgoals_1, numHyps := numHyps_1, prio := prio_1,
        numVarying := numVarying_1, forGrw := forGrw_1 } →
    keys = keys_1 ∧
      declName = declName_1 ∧
        mainSubgoals = mainSubgoals_1 ∧
          numHyps = numHyps_1 ∧ prio = prio_1 ∧ numVarying = numVarying_1 ∧ forGrw = forGrw_1
-- Mathlib.Topology.Maps.Proper.Basic
/-- If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a closed map.  -/
isClosedMap_snd_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X],
  IsClosedMap Prod.snd
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The isomorphism `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`, where `Rₚ` satisfies
`IsLocalization.AtPrime Rₚ p`. In particular, localization preserves the residue field.  -/
IsLocalization.AtPrime.equivQuotMaximalIdeal : {R : Type u_7} →
  [inst : CommRing R] →
    (p : Ideal R) →
      [inst_1 : p.IsMaximal] →
        (Rₚ : Type u_8) →
          [inst_2 : CommRing Rₚ] →
            [inst_3 : Algebra R Rₚ] →
              [IsLocalization.AtPrime Rₚ p] → [inst_5 : IsLocalRing Rₚ] → R ⧸ p ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tprodCoeff.eq_1 : ∀ {ι : Type u_1} (R : Type u_4) [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i),
  PiTensorProduct.tprodCoeff R r f = (addConGen (PiTensorProduct.Eqv R fun i => s i)).mk' (FreeAddMonoid.of (r, f))
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), (↑n).imJ = 0
-- Mathlib.Order.Defs.Unbundled
Minimal.eq_1 : ∀ {α : Type u_1} [inst : LE α] (P : α → Prop) (x : α), Minimal P x = (P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x ≤ y)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- Left unit cancellation `1 ⊗ X ≅ X` in `Dial C`.  -/
CategoryTheory.Dial.leftUnitorImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (X : CategoryTheory.Dial C) → CategoryTheory.Dial.tensorUnitImpl.tensorObjImpl X ≅ X
-- Mathlib.Algebra.Colimit.Ring
Field.DirectLimit.inv_mul_cancel : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  [inst_3 : (i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f},
  p ≠ 0 → Field.DirectLimit.inv G f p * p = 1
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.preserveOrder : Lean.MetavarContext.MkBinding.M Bool
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Unfolds `ofMulDistribMulAction`; useful to keep track of additivity.  -/
Rep.toAdditive : {M : Type u_1} →
  {G : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : CommGroup G] → [inst_2 : MulDistribMulAction M G] → ↑(Rep.ofMulDistribMulAction M G) ≃+ Additive G
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
/-- The additive subgroup generated by an element.  -/
AddSubgroup.zmultiples : {G : Type u_1} → [inst : AddGroup G] → G → AddSubgroup G
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffWithinAt_fst : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {s : Set (M × N)} {p : M × N},
  ContMDiffWithinAt (I.prod J) I n Prod.fst s p
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited β] {a : α}, ∅[a]! = default
-- Mathlib.Topology.Bornology.BoundedOperation
isBounded_sub : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Sub R] [BoundedSub R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_density_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) {s : Set β}, MeasurableSet s → ∀ (a : α), Measurable fun x => κ.density ν a x s
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mk.sizeOf_spec : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : SizeOf J] [inst_4 : SizeOf K]
  [inst_5 : SizeOf C] (obj : (j : J) → CategoryTheory.Limits.Cone (F.obj j))
  (map : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj j) ⟶ obj j')
  (id :
    autoParam
      (∀ (j : J),
        (map (CategoryTheory.CategoryStruct.id j)).hom =
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (obj j)).pt)
      CategoryTheory.Limits.DiagramOfCones.id._autoParam)
  (comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCones.comp._autoParam),
  sizeOf { obj := obj, map := map, id := id, comp := comp } = 1
-- Lean.Widget.TaggedText
Lean.Widget.instFromJsonTaggedText : {α : Type} → [Lean.FromJson α] → Lean.FromJson (Lean.Widget.TaggedText α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.zero_cochain_comp_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0)
  (z₂ : CochainComplex.HomComplex.Cochain G K n) (p q : ℤ) (hpq : p + n = q),
  (z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p p ⋯) (z₂.v p q hpq)
-- Init.Data.Vector.Basic
/-- Computes the sum of the elements of a vector.

Examples:
* `#v[a, b, c].sum = a + (b + (c + 0))`
* `#v[1, 2, 5].sum = 8`
 -/
Vector.sum : {α : Type u_1} → {n : ℕ} → [Add α] → [Zero α] → Vector α n → α
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_minFac_2 : ∀ {a a' : ℕ}, Mathlib.Meta.NormNum.IsNat a a' → a' % 2 = 0 → Mathlib.Meta.NormNum.IsNat a.minFac 2
-- Init.Data.Array.Nat
Array.sum_eq_foldl_nat : ∀ {xs : Array ℕ}, xs.sum = Array.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  m.WF → (Std.DHashMap.Raw.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback
-- Mathlib.CategoryTheory.Skeletal
/-- For each `x : ThinSkeleton C`, we promote `map₂ObjMap F x` to a functor  -/
CategoryTheory.ThinSkeleton.map₂Functor : {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] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) →
              CategoryTheory.ThinSkeleton C →
                CategoryTheory.Functor (CategoryTheory.ThinSkeleton D) (CategoryTheory.ThinSkeleton E)
-- Mathlib.Logic.UnivLE
/-- A class expressing a universe inequality. `UnivLE.{u, v}` expresses that `u ≤ v`.

There used to be a stronger definition `∀ α : Type max u v, Small.{v} α` that immediately implies
`Small.{v} ((α : Type u) → (β : Type v))` which is essential for proving that `Type v` has
`Type u`-indexed limits when `u ≤ v`. However the current weaker condition
`∀ α : Type u, Small.{v} α` also implies the same, so we switched to use it for
its simplicity and transitivity.

The strong definition easily implies the weaker definition (see below),
but we cannot prove the reverse implication.
This is because in Lean's type theory, while `max u v` is at least at big as `u` and `v`,
it could be bigger than both!
See also `Mathlib/CategoryTheory/UnivLE.lean` for the statement that the stronger definition is
equivalent to `EssSurj (uliftFunctor : Type v ⥤ Type max u v)`.
 -/
UnivLE : Prop