mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_prod_inter_eq_inter : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : DecidableEq α]
  [inst_3 : Subsingleton αˣ] (a b : α),
  UniqueFactorizationMonoid.normalizedFactors
      (UniqueFactorizationMonoid.normalizedFactors a ∩ UniqueFactorizationMonoid.normalizedFactors b).prod =
    UniqueFactorizationMonoid.normalizedFactors a ∩ UniqueFactorizationMonoid.normalizedFactors b
-- Init.Data.Repr
instReprTupleProdOfRepr : {α : Type u_1} → {β : Type u_2} → [Repr α] → [ReprTuple β] → ReprTuple (α × β)
-- Mathlib.RingTheory.RegularLocalRing.Defs
/-- A noetherian ring is regular if its localization at any prime `IsRegularLocalRing`.  -/
IsRegularRing : (R : Type u_2) → [CommRing R] → Prop
-- Mathlib.Algebra.Group.Basic
mul_right_iterate_apply_one : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ} (a : M), (fun x => x * a)^[n] 1 = a ^ n
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The isomorphism `U ≅ Spec Γ(X, U)` for an affine `U`.  -/
AlgebraicGeometry.IsAffineOpen.isoSpec : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} → AlgebraicGeometry.IsAffineOpen U → (↑U ≅ AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.Faithful.mapAddMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [F.Faithful], F.mapAddMon.Faithful
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.exists_monotone_subseq : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO → ∀ {f : ℕ → α}, (∀ (n : ℕ), f n ∈ s) → ∃ g, Monotone (f ∘ ⇑g)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousMapZero.integral_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  [inst_2 : CompactSpace Y] {R : Type u_8} [inst_3 : NormedCommRing R] [inst_4 : Zero Y] [inst_5 : NormedAlgebra ℝ R]
  [CompleteSpace R] {f : X → ContinuousMapZero Y R},
  MeasureTheory.Integrable f μ → ∀ (y : Y), (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Cache : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.goodReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasGoodReduction R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1
-- Mathlib.Analysis.Seminorm
Seminorm.coe_le_coe : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Module.Free.dfinsupp : ∀ {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)], Module.Free R (Π₀ (i : ι), M i)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_isCycle₁_iff : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (g : G)
  (a : A), (groupHomology.IsCycle₁ fun₀ | g => a) ↔ g • a = a
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R],
  ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) 1) = 1
-- Mathlib.Algebra.Torsor.Defs
/-- Convert between an equality with adding a group element to a point
and an equality of a subtraction of two points with a group element.  -/
eq_vadd_iff_vsub_eq : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ : P) (g : G) (p₂ : P),
  p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.eq_2 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f)
  (x : AdicCompletion.AdicCauchySequence I N) (n : ℕ),
  AdicCompletion.mapPreimage✝ hf x n.succ =
    match AdicCompletion.mapPreimage✝ hf x n with
    | ⟨yₙ, hyₙ⟩ =>
      match AdicCompletion.mapPreimageDelta✝ hf x ⋯ hyₙ with
      | ⟨⟨d, property⟩, p⟩ => ⟨yₙ - d, ⋯⟩
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {Φ₁ Φ₂ : S₁ ⟶ S₂}, Φ₁ = Φ₂ ↔ ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toAlgEquiv_toRingHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ↑e.toAlgEquiv = ↑e
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter : ∀ {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 : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i : Fin (n + 1)),
      SignType.sign ((s.signedInfDist i) (s.excenter signs)) = SignType.sign (s.excenterWeights signs i)
-- Mathlib.Data.PFunctor.Univariate.M
/-- For polynomial functor `F`, `M F` is its final coalgebra  -/
PFunctor.M : PFunctor.{uA, uB} → Type (max uA uB)
-- Mathlib.Algebra.Group.Prod
/-- Multiplication as a multiplicative homomorphism.  -/
mulMulHom : {α : Type u_6} → [inst : CommSemigroup α] → α × α →ₙ* α
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : LocallyBoundedMap α β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Data.Rel
SetRel.preimage_eq_dom_of_cod_subset : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β}, R.cod ⊆ t → R.preimage t = R.dom
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X Y : C),
  CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.rightDistributor f X)
        (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫
      CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) Y =
    CategoryTheory.MonoidalCategoryStruct.associator (⨁ f) X Y ≪≫
      CategoryTheory.rightDistributor f (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≪≫
        CategoryTheory.Limits.biproduct.mapIso fun x =>
          (CategoryTheory.MonoidalCategoryStruct.associator (f x) X Y).symm
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpIdIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.AddGrp C),
  (CategoryTheory.Functor.mapAddGrpIdIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Std.Async.Basic
/-- Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an error, the returned
`ETask` resolves to that error.
 -/
Std.Async.ETask.mapEIO : {α ε β : Type} →
  (α → EIO ε β) →
    Std.Async.ETask ε α →
      optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Std.Async.ETask ε β)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If a `BinaryCofan` in the opposite category is a colimit, then its `unop` is a limit.  -/
CategoryTheory.Limits.BinaryCofan.IsColimit.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)} →
        CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit c.unop
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.smul_eval_comm : ∀ (lc : Lean.Omega.LinearCombo) (i : ℤ) (v : Lean.Omega.Coeffs), (i * lc).eval v = lc.eval v * i
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.comp_det_mul_pow : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] (k : m) [inst_4 : Fintype m] [inst_5 : Fintype n]
  (f : S →+* Matrix n n R),
  ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det
-- Init.Data.UInt.Lemmas
UInt64.ofInt_neg : ∀ (x : ℤ), UInt64.ofInt (-x) = -UInt64.ofInt x
-- Mathlib.Topology.CantorBendixson
/-- A set is preperfect if and only if every stage of its iterated relative derived-set sequence
is equal to the original set.  -/
CantorBendixson.iteratedDerivedSet_constant_iff_preperfect : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Preperfect s ↔ ∀ (a : Ordinal.{u}), CantorBendixson.iteratedDerivedSet s a = s
-- Mathlib.Algebra.Order.Ring.GeomSum
Odd.geom_sum_pos : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  Odd n → 0 < ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_lift_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤)
  (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) (x : M),
  ↑((AdicCompletion.lift I f ⋯) x) n = (f n) x
-- Mathlib.Data.Vector.Defs
/-- Prepending the head of a vector to its tail gives the vector.  -/
List.Vector.cons_head_tail : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ), v.head ::ᵥ v.tail = v
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.G.mk.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x : (j : J) × ↑(F.obj j)),
  GrpCat.FilteredColimits.G.mk F x = (F.comp (CategoryTheory.forget GrpCat)).ιColimitType x.fst x.snd
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_finite : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {U : Set S} {κ : Type u_4} [Finite κ] (a : κ → ι) (V : (k : κ) → TopologicalSpace.Opens (X (a k))),
  (∀ (k : κ), IsCompact (V k).carrier) → ⋃ k, f (a k) '' ↑(V k) = U → IsCompactOpenCovered f U
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.instModuleElemForallObjCompForgetLinearMapIdCarrierSections : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) → Module R ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.finite : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} [Finite α], Finite (α ⧸ s)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_smul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (c : ℝ) (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I),
  BoxIntegral.integralSum (c • f) vol π = c • BoxIntegral.integralSum f vol π
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.of_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (f : R → Γ₀)
  {h0 : f 0 = ⊤} {h1 : f 1 = 0} {hadd : ∀ (x y : R), min (f x) (f y) ≤ f (x + y)}
  {hmul : ∀ (x y : R), f (x * y) = f x + f y} {r : R}, (AddValuation.of f h0 h1 hadd hmul) r = f r
-- Mathlib.Topology.ContinuousMap.Weierstrass
/-- The **Weierstrass Approximation Theorem**:
polynomials functions on `[a, b] ⊆ ℝ` are dense in `C([a,b],ℝ)`

(While we could deduce this as an application of the Stone-Weierstrass theorem,
our proof of that relies on the fact that `abs` is in the closure of polynomials on `[-M, M]`,
so we may as well get this done first.)
 -/
polynomialFunctions_closure_eq_top : ∀ (a b : ℝ), (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
-- Qq.Match
_private.Qq.Match.0.Qq.push : Qq.Lift✝ → StateT (Array Qq.Lift✝) Lean.MacroM Unit
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), ↑(⨅ i, f i) = ⋃ i, ↑(f i)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_smul_empty : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (w : Monoid.PushoutI.NormalWord d),
  w.prod • Monoid.PushoutI.NormalWord.empty = w
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.Internal.List.alterKey k f l).isEmpty = false →
        (Std.Internal.List.minKey! (Std.Internal.List.alterKey k f l) = k ↔
          (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.Data.Int.Basic
Int.eq_zero_of_dvd_of_nonneg_of_lt : ∀ {m n : ℤ}, 0 ≤ m → m < n → n ∣ m → m = 0
-- Mathlib.Data.Finset.Sum
Finset.toRight_monotone : ∀ {α : Type u_1} {β : Type u_2}, Monotone Finset.toRight
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (a' b' : EInt) (hab' : a' ≤ b')
  (φ :
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab) ⟶
      CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab'))
  (X : C) {Z : C} (h : (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X))
        (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a' b').hom.app X) h)) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X))
        (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)) h))
-- Mathlib.Order.Directed
IsDirected.mk : ∀ {α : Sort u_5} {r : α → α → Prop}, (∀ (a b : α), ∃ c, r a c ∧ r b c) → IsDirected α r
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- If a finset `u` is contained in the sum of two sets `s - t`, we can find two finsets
`s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' - t'`.  -/
Finset.subset_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s - t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' - t'
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange_eq_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddMonoidHom.mrange f = AddSubmonoid.map f ⊤
-- Init.Data.Float.Model.Float32
/-- Converts a `UInt16` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofUInt16 : UInt16 → Float32.Model
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.coe_le_coe_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (f g : E →L[𝕜] E), ↑f ≤ ↑g ↔ f ≤ g
-- Init.Control.Basic
/-- Returns `some x` if `f` succeeds with value `x`, else returns `none`.
 -/
optional : {f : Type u → Type v} → [Alternative f] → {α : Type u} → f α → f (Option α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.min_le_max_of_mul_le_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] {a b c d : α} [MulLeftStrictMono α] [MulRightMono α],
  a * b ≤ c * d → min a b ≤ max c d
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insert k v}, (t.insert k v)[a] = if h₂ : cmp k a = Ordering.eq then v else t[a]
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- `J` commutes with any positively-oriented isometric automorphism.  -/
Orientation.linearIsometryEquiv_comp_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
  0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x : E), φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves equicontinuity.  -/
Equicontinuous.comp : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {F : ι → X → α}, Equicontinuous F → ∀ (u : κ → ι), Equicontinuous (F ∘ u)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_lt : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a b : α},
  Lean.Grind.IntModule.OfNatModule.toQ a < Lean.Grind.IntModule.OfNatModule.toQ b ↔ a < b
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_pow_tfae : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x y : G),
  [MapClusterPt x Filter.atTop fun x => y ^ x, MapClusterPt x Filter.atTop fun x => y ^ x,
      x ∈ closure (Set.range fun x => y ^ x), x ∈ closure (Set.range fun x => y ^ x)].TFAE
-- Mathlib.Logic.Hydra
/-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself.  -/
Relation.cutExpand_fibration : ∀ {α : Type u_1} (r : α → α → Prop),
  Relation.Fibration (Prod.GameAdd (Relation.CutExpand r) (Relation.CutExpand r)) (Relation.CutExpand r) fun s =>
    s.1 + s.2
-- Mathlib.Order.CompleteLattice.Basic
/-- The symmetric case of `iSup_and`, useful for rewriting into a supremum over a conjunction  -/
iSup_and' : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p → q → α},
  ⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂ = ⨆ (h : p ∧ q), s ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_zero : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.charpoly 0 = Polynomial.X ^ Fintype.card n
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Pullback a group object along a fully faithful monoidal functor.  -/
CategoryTheory.Functor.FullyFaithful.grpObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] → F.FullyFaithful → (X : C) → [CategoryTheory.GrpObj (F.obj X)] → CategoryTheory.GrpObj X
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A locally compact normed vector space is proper.  -/
ProperSpace.of_locallyCompactSpace : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [LocallyCompactSpace E], ProperSpace E
-- Mathlib.Order.Bounds.Basic
union_upperBounds_subset_upperBounds_inter : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)
-- Init.Data.Int.OfNat
Int.Nonneg.toPoly : ∀ e ≥ 0, -1 * e ≤ 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- This is not covered by `Pi.borelSpace` as it does not require second countability.  -/
Pi.borelSpace_of_subsingleton : ∀ {ι : Type u_6} {X : ι → Type u_7} [Subsingleton ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → MeasurableSpace (X i)] [∀ (i : ι), BorelSpace (X i)], BorelSpace ((i : ι) → X i)
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_le_iff_le : ∀ {a b : ℕ} (ha : a < UInt32.size) (hb : b < UInt32.size), UInt32.ofNatLT a ha ≤ UInt32.ofNatLT b hb ↔ a ≤ b
-- Mathlib.Logic.Function.Basic
/-- `sometimes f` evaluates to some value of `f`, if it exists. This function is especially
interesting in the case where `α` is a proposition, in which case `f` is necessarily a
constant function, so that `sometimes f = f a` for all `a`.  -/
Function.sometimes : {α : Sort u_1} → {β : Sort u_2} → [Nonempty β] → (α → β) → β
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.map_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorPreCore B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf is non-negative for all `a : α`.  -/
ProbabilityTheory.condCDF_nonneg : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℝ),
  0 ≤ ↑(ProbabilityTheory.condCDF ρ a) r
-- Batteries.Data.BitVec.Lemmas
BitVec.getMsb_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnLE f).getMsb i = f i.rev
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Continuous maps out of the one point compactification of an infinite discrete space to a Hausdorff
space correspond bijectively to "convergent" maps out of the discrete space.
 -/
OnePoint.continuousMapDiscreteEquiv : (X : Type u_1) →
  [inst : TopologicalSpace X] →
    (Y : Type u_3) →
      [DiscreteTopology X] →
        [inst_2 : TopologicalSpace Y] →
          [T2Space Y] →
            [Infinite X] → C(OnePoint X, Y) ≃ { f // ∃ L, Filter.Tendsto (fun x => f x) Filter.cofinite (nhds L) }
-- Mathlib.Data.List.Basic
List.concat_eq_reverse_cons : ∀ {α : Type u} (a : α) (l : List α), l.concat a = (a :: l.reverse).reverse