mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.leftHomotopyClassToHom_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] {X Y : C} (f : X ⟶ Y),
  HomotopicalAlgebra.leftHomotopyClassToHom L (HomotopicalAlgebra.LeftHomotopyClass.mk f) = L.map f
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_prod_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι}, m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.algebraMap_injective : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K],
  Function.Injective ⇑(algebraMap (Polynomial F) ↥(FunctionField.ringOfIntegers F K))
-- Mathlib.Order.RelSeries
RelSeries.apply_last : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.toFun (Fin.last x.length) = x.last
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C}, Monotone (CategoryTheory.Presieve.map F)
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.faithful_constantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [inst_3 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_6 : CategoryTheory.HasWeakSheafify J A], (CategoryTheory.constantSheaf J A).Faithful
-- Init.Data.SInt.Lemmas
Int32.toISize_ne_neg_one : ∀ (a : Int32), a ≠ -1 → a.toISize ≠ -1
-- Lean.Log
/-- A widget for displaying error names and explanation links.
 -/
Lean.errorDescriptionWidget : Lean.Widget.Module
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.isPullback_opens_inf : ∀ {X : AlgebraicGeometry.Scheme} (U V : X.Opens), CategoryTheory.IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) U.ι V.ι
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq' : ∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [inst : AddCommMonoid β] (n : ℕ),
  MeasureTheory.stoppedProcess u τ n =
    {a | ↑n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a | τ a = ↑i}.indicator (u i)
-- Mathlib.Data.Finset.Max
/-- A version of `Finset.min'_image` with LHS and RHS reversed.
Also, this version assumes that `s` is nonempty, not its image.  -/
Monotone.map_finset_min' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f → ∀ {s : Finset α} (h : s.Nonempty), f (s.min' h) = (Finset.image f s).min' ⋯
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_trans : ∀ {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] {F F' F'' : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G),
  CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj2).hom (adj2.leftAdjointUniq adj3).hom =
    (adj1.leftAdjointUniq adj3).hom
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_comm : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y ↔ IsCoprime y x
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.fork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂),
  (CategoryTheory.Subfunctor.equalizer.fork f g).ι = CategoryTheory.Subfunctor.equalizer.ι f g
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vle_mul_iff_left`. -/
ValuativeRel.vle_mul_right_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → (x * z ≤ᵥ y * z ↔ x ≤ᵥ y)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod.inj : ∀ {k : ℤ} {y? : Option Int.Internal.Linear.Var} {c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {k_1 : ℤ}
  {y?_1 : Option Int.Internal.Linear.Var} {c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod k y? c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod k_1 y?_1 c_1 →
    k = k_1 ∧ y? = y?_1 ∧ c = c_1
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.hole.inj : ∀ {mvarId mvarId_1 : Lean.MVarId}, Lean.Elab.InfoTree.hole mvarId = Lean.Elab.InfoTree.hole mvarId_1 → mvarId = mvarId_1
-- Mathlib.Algebra.Homology.Augment
ChainComplex.truncate_obj_X : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i : ℕ), (ChainComplex.truncate.obj C).X i = C.X (i + 1)
-- Std.Data.DTreeMap.Iterator
/-- Returns a finite iterator over the entries of a dependent tree map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.iter : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.Iter ((a : α) × β a)
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_jointly_surjective : ∀ (D : TopCat.GlueData) (x : ↑D.glued), ∃ i y, (CategoryTheory.ConcreteCategory.hom (D.ι i)) y = x
-- Mathlib.Topology.Order.WithTop
WithBot.tendsto_nhds_bot_iff : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] {α : Type u_2}
  {f : Filter α} (x : α → WithBot ι), Filter.Tendsto x f (nhds ⊥) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, x a < ↑i
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `K / E / F` is a field extension tower such that `K / F` is purely inseparable,
then `K / E` is also purely inseparable.  -/
IsPurelyInseparable.tower_top : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [h : IsPurelyInseparable F K],
  IsPurelyInseparable E K
-- Mathlib.RingTheory.Ideal.Span
Ideal.isCompactElement_top : ∀ {α : Type u} [inst : Semiring α], IsCompactElement ⊤
-- Mathlib.Order.SymmDiff
symmDiff_right_injective : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Injective fun x => symmDiff a x
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throwThe : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {e : ε} {Q : Std.Do.PostCond α ps}
  [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps],
  (Std.Do.wp (throwThe ε e)).apply Q = (Std.Do.wp (MonadExceptOf.throw e)).apply Q
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_eq_empty_iff : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioc a b = ∅ ↔ ¬a < b
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
AlgebraicIndependent.liftAlgHom_comp_reprField : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (hx : AlgebraicIndependent F x),
  (IsFractionRing.liftAlgHom ⋯).comp hx.reprField = (IntermediateField.adjoin F (Set.range x)).val
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [inst_1 : F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  (hf' : CategoryTheory.Sieve.ofArrows X' f' ∈ J S) {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃i : ι⦄ ⦃Y : C⦄ (q : Y ⟶ X i) ⦃j : ι'⦄ (a : Y ⟶ X' j)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i))
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.map_hom._auto_1✝),
  (F.map q.op.toLoc).toFunctor.map (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i) =
    CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a fac
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.instComonadHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (m : CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B) → CategoryTheory.Bicategory.Comonad m.hom
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Any functor from a finite category to `Type*` that only involves finite objects,
has a finite colimit.  -/
CategoryTheory.Limits.FintypeCat.finite_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  {K : CategoryTheory.Functor J (Type u)} [∀ (j : J), Finite (K.obj j)] {c : CategoryTheory.Limits.Cocone K}
  (hc : CategoryTheory.Limits.IsColimit c), Finite c.pt
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.ofHom_apply : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : Finite X] [inst_2 : AddGroup Y] [inst_3 : Finite Y] (f : X →+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (FiniteAddGrp.ofHom f)) x = f x
-- Init.SimpLemmas
Bool.not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b
-- Mathlib.Order.SymmDiff
symmDiff_sup_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b ⊔ a ⊓ b = a ⊔ b
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.IsArithmetic.mk : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)}, 𝒢.Commensurable (Matrix.SpecialLinearGroup.mapGL ℝ).range → 𝒢.IsArithmetic
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.specTargetImageRingHom_surjective : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.specTargetImageRingHom f))
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectSuccessorOf.below.refl : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {a : Std.Iter β}
  {motive : (a_1 : Std.Iter β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop},
  Std.Iter.IsPlausibleIndirectSuccessorOf.below ⋯
-- Mathlib.Data.Set.Insert
Set.eq_singleton_iff_unique_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.comonEquivalence_counitIso : ∀ (R : Type u) [inst : CommRing R],
  (CoalgCat.comonEquivalence R).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl (((CoalgCat.ofComon R).comp (CoalgCat.toComon R)).obj x)) ⋯
-- Mathlib.Combinatorics.Hindman
Hindman.FP_drop_subset_FP : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (n : ℕ), Hindman.FP (Stream'.drop n a) ⊆ Hindman.FP a
-- Lean.Elab.AutoBound
Lean.Elab.AutoBoundImplicitContext.mk.injEq : ∀ (autoImplicitEnabled : Bool) (boundVariables : Lean.PArray Lean.Expr) (autoImplicitEnabled_1 : Bool)
  (boundVariables_1 : Lean.PArray Lean.Expr),
  ({ autoImplicitEnabled := autoImplicitEnabled, boundVariables := boundVariables } =
      { autoImplicitEnabled := autoImplicitEnabled_1, boundVariables := boundVariables_1 }) =
    (autoImplicitEnabled = autoImplicitEnabled_1 ∧ boundVariables = boundVariables_1)
-- Mathlib.Geometry.Euclidean.Altitude
/-- A line through a vertex is the altitude through that vertex if and
only if it is orthogonal to the opposite face.  -/
Affine.Simplex.affineSpan_pair_eq_altitude_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) (p : P),
  line[ℝ, p, s.points i] = s.altitude i ↔
    p ≠ s.points i ∧
      p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ
-- Aesop.Forward.RuleInfo
Aesop.ForwardRuleInfo.mk.sizeOf_spec : ∀ (numPremises numLevelParams : ℕ) (slotClusters : Array (Array Aesop.Slot)) (conclusionDeps : Array Aesop.PremiseIndex)
  (rulePatternInfo? : Option (Aesop.RulePattern × Aesop.PremiseIndex)),
  sizeOf
      { numPremises := numPremises, numLevelParams := numLevelParams, slotClusters := slotClusters,
        conclusionDeps := conclusionDeps, rulePatternInfo? := rulePatternInfo? } =
    1 + sizeOf numPremises + sizeOf numLevelParams + sizeOf slotClusters + sizeOf conclusionDeps +
      sizeOf rulePatternInfo?
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- A functor `F : A ⥤ B` preserves the sheafification for the Grothendieck
topology `J` on a category `C` if whenever a morphism of presheaves `f : P₁ ⟶ P₂`
in `Cᵒᵖ ⥤ A` is such that becomes an iso after sheafification, then it is
also the case of `whiskerRight f F : P₁ ⋙ F ⟶ P₂ ⋙ F`.  -/
CategoryTheory.GrothendieckTopology.PreservesSheafification : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} B] → CategoryTheory.Functor A B → Prop
-- Mathlib.Algebra.Group.PUnit
PUnit.instNeg_mathlib.eq_1 : PUnit.instNeg_mathlib = { neg := fun x => PUnit.unit }
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.ext_iff : ∀ {𝕜 : Type u_6} {E : Type u_7} {inst : NormedField 𝕜} {inst_1 : SeminormedAddCommGroup E} {x y : NormedSpace 𝕜 E},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hasForgetToMagmaCat : CategoryTheory.HasForget₂ Semigrp MagmaCat
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.newParamNames : Lean.MetavarContext.UnivMVarParamResult → Array Lean.Name
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_left_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f.right F),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).left.as = PUnit.unit
-- Mathlib.LinearAlgebra.Ray
/-- The ray given by the negation of a nonzero vector.  -/
neg_rayOfNeZero : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (v : M) (h : v ≠ 0), -rayOfNeZero R v h = rayOfNeZero R (-v) ⋯
-- Mathlib.RingTheory.Jacobson.Ring
/-- A variant of `isJacobsonRing_iff_sInf_maximal` with a different spelling of "maximal or `⊤`".  -/
isJacobsonRing_iff_sInf_maximal' : ∀ {R : Type u_1} [inst : CommRing R],
  IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M, (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M
-- Mathlib.Tactic.Linarith.Datatypes
/-- A shorthand for getting the types of a list of proofs terms, to trace.  -/
Mathlib.Tactic.Linarith.linarithGetProofsMessage : List Lean.Expr → Lean.MetaM Lean.MessageData
-- Lean.DocString.Parser
/-- Parses some number of blank lines followed by zero or more blocks.
 -/
Lean.Doc.Parser.document : optParam Lean.Doc.Parser.BlockCtxt { } → Lean.Parser.ParserFn
-- Mathlib.Logic.Function.Defs
/-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates
`g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation
from `β` to `α`.  -/
Function.term_On_ : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} {f g : X ⟶ Y},
  f = g ↔ CategoryTheory.StructuredArrow.Hom.right f = CategoryTheory.StructuredArrow.Hom.right g
-- Mathlib.Data.PNat.Factors
instAddCommMonoidPrimeMultiset : AddCommMonoid PrimeMultiset
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If an additive content is σ-additive on a set ring, then it is σ-subadditive.  -/
MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum : ∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetRing C →
    (∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) →
          ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)) →
      m.IsSigmaSubadditive
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.piPremeasure_pi_eval : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)}
  {s : Set ((i : ι) → α i)},
  MeasureTheory.piPremeasure m (Set.univ.pi fun i => Function.eval i '' s) = MeasureTheory.piPremeasure m s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.op_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F), c.op.ι = CategoryTheory.NatTrans.op c.π
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.step_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n},
  (xs.iterM m).step =
    pure
      (Std.Shrink.deflate
        (if h : 0 < n then Std.PlausibleIterStep.yield (xs.iterFromIdxM m 1) xs[0] ⋯ else Std.PlausibleIterStep.done ⋯))
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.uniformizer_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R],
  ValuativeRel.uniformizer R < 1
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First Derivative test, minimum version.  -/
isLocalMin_of_deriv : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    (∀ᶠ (x : ℝ) in nhdsWithin b {b}ᶜ, DifferentiableAt ℝ f x) →
      (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), deriv f x ≤ 0) →
        (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), 0 ≤ deriv f x) → IsLocalMin f b
-- Lean.Meta.Tactic.Generalize
_private.Lean.Meta.Tactic.Generalize.0.Lean.Meta.generalizeCore.go' : Array Lean.Meta.GeneralizeArg → Array Lean.Expr → Lean.Expr → ℕ → Lean.MetaM (List Lean.Expr × Lean.Expr)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.plus : {v : Lean.Level} → {M : Q(Type v)} → Mathlib.Tactic.FieldSimp.Sign M
-- Mathlib.CategoryTheory.Galois.Basic
/-- The fiber of a connected object is nonempty.  -/
CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected X], Nonempty (F.obj X).obj
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.algebraMap_coxeterWeightIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_7)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : P.IsValuedIn S] (i j : ι),
  (algebraMap S R) (P.coxeterWeightIn S i j) = P.coxeterWeight i j
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k : α}, List.find? (fun x => x.1 == k) (Std.DHashMap.Raw.Const.toList m) = none ↔ m.contains k = false
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Enable `a ^ y` notation for `CFC.rpow`. This is a low-priority instance to make sure it does
not take priority over other instances when they are available (such as `Pow ℝ ℝ`).  -/
CFC.instPowReal : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : Ring A] →
      [inst_2 : StarRing A] →
        [inst_3 : TopologicalSpace A] →
          [StarOrderedRing A] →
            [inst_5 : Algebra ℝ A] →
              [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → [NonnegSpectrumClass ℝ A] → Pow A ℝ
-- Mathlib.Tactic.Polynomial.Basic
/-- A cleanup routine, which simplifies normalized expressions to a more human-friendly format.
This is the `algebra_nf` cleanup routine with a little extra work to turn scalar multiplication
into `(MV)Polynomial.C`  -/
Mathlib.Tactic.Polynomial.cleanup : Mathlib.Tactic.RingNF.Config → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_sub_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp f p μ →
    1 ≤ p → MeasureTheory.lpNorm (f - g) p μ ≤ MeasureTheory.lpNorm f p μ + MeasureTheory.lpNorm g p μ
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory CommMonCat fun x1 x2 => ↑x1 →* ↑x2
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Return `(f, g)` if `e` is definitionally equal to `f ⊗ g`.  -/
Mathlib.Tactic.Monoidal.comp? : Lean.Expr →
  Mathlib.Tactic.Monoidal.MonoidalM (Option (Mathlib.Tactic.BicategoryLike.Mor₁ × Mathlib.Tactic.BicategoryLike.Mor₁))
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_iff_eq_maxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ},
  List.maxIdxOn f xs h = i ↔
    ∃ (hi : i < xs.length), xs[i] = List.maxOn f xs h ∧ ∀ (j : ℕ) (hj : j < i), f xs[j] < f (List.maxOn f xs h)
-- Mathlib.Algebra.Module.FinitePresentation
/-- If `M` is a finite `R`-module, and the localization `Mₛ` at some submonoid `S` of `R`
is finitely presented, then `Mₛ = M[1/r]` for some `r ∈ S`.  -/
IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  {M' : Type u_1} [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  [Module.Finite R M] [Module.FinitePresentation R M'], ∃ r ∈ S, IsLocalizedModule.Away r f
-- Mathlib.Data.Fintype.Card
/-- Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses
that `Sum.inl` is an injection, but there's no clear inverse if `α` is empty.  -/
Fintype.sumLeft : {α : Type u_4} → {β : Type u_5} → [Fintype (α ⊕ β)] → Fintype α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)),
  (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₁) *
      (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₂) =
    (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯)