mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h =
    CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_powerset : ∀ (x : PSet.{u_1}), x.powerset.rank = Order.succ x.rank
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.comp_aemeasurable : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β},
  AEMeasurable g (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → AEMeasurable (g ∘ f) μ
-- Mathlib.Algebra.Group.Defs
ZSMul.ofSMul : {M : Type u_2} → [SMul ℤ M] → ZSMul M
-- Mathlib.RingTheory.Regular.RegularSequence
LinearEquiv.isRegular_congr : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (e : M ≃ₗ[R] M₂) (rs : List R),
  RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ rs
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMapIdIso_hom_app : ∀ (V : Type u_1) [inst : Quiver V] (X : CategoryTheory.Paths V),
  (CategoryTheory.Cat.freeMapIdIso V).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrdered.exists_monotone_subseq : ∀ {α : Type u_1} {r : α → α → Prop} [IsPreorder α r],
  WellQuasiOrdered r → ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) {Z : CommRingCat} (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.residue (f x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.residue x) h)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roo_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toArray[i]? = none ↔ (n - (m + 1)).toNat ≤ i
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_eq_zero_tfae : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V),
  [f.normDet = 0, f.ker ≠ ⊥, Module.finrank 𝕜 ↥f.range ≠ Module.finrank 𝕜 U,
      Module.finrank 𝕜 ↥f.range < Module.finrank 𝕜 U, IsEmpty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range),
      ¬Function.Injective ⇑f].TFAE
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : BorelSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.covarianceBilinDual μ = ProbabilityTheory.covarianceBilinDual μ_1
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_smul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (a : A) (f : σ.IntertwiningMap τ),
  Representation.IntertwiningMap.rTensor ρ (a • f) = a • Representation.IntertwiningMap.rTensor ρ f
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The `OrderIso` between the fiber of `PrimeSpectrum S → PrimeSpectrum R` at a prime
ideal `p : PrimeSpectrum R` and the prime spectrum of `κ(p) ⊗[R] S`.  -/
PrimeSpectrum.preimageOrderIsoFiber : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : PrimeSpectrum R) → ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃o PrimeSpectrum (p.asIdeal.Fiber S)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the condition that the denominator belongs to the given morphism property  -/
CategoryTheory.MorphismProperty.RightFraction.hs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (self : W.RightFraction X Y), W self.s
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.Red.enum.sound : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  L₂ ∈ List.filter (fun b => decide (FreeGroup.Red L₁ b)) L₁.sublists → FreeGroup.Red L₁ L₂
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.eq_of_measure_of_tendsto_atBot : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (g : StieltjesFunction R) {l : ℝ},
  f.measure = g.measure → Filter.Tendsto (↑f) Filter.atBot (nhds l) → Filter.Tendsto (↑g) Filter.atBot (nhds l) → f = g
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.modify.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : β → β) (sz : ℕ) (k' : α) (v' : β)
  (l' r' : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.modify k f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k' v' (Std.DTreeMap.Internal.Impl.Const.modify k f l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.inner sz k' v' l' (Std.DTreeMap.Internal.Impl.Const.modify k f r')
    | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k (f v') l' r'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PullbackObjObj` of `f₁ : Arrow C₁` and `f₃ : Arrow C₃`, a `PullbackObjObj` of `f₁` and
`f₃' : Arrow C₃`, and an isomorphism `f₃ ≅ f₃'`, this defines an isomorphism of the induced
pullback maps.  -/
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {f₁ : CategoryTheory.Arrow C₁} →
                {f₃ f₃' : CategoryTheory.Arrow C₃} →
                  (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) →
                    (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) →
                      (f₃ ≅ f₃') → (CategoryTheory.Arrow.mk sq₁₃.π ≅ CategoryTheory.Arrow.mk sq₁₃'.π)
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_sub : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f g : ι → G),
  Fintype.balance (f - g) = Fintype.balance f - Fintype.balance g
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α},
  k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Sigma.fst l).contains k = true
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.hasForgetToMon : CategoryTheory.HasForget₂ GrpWithZero MonCat
-- Mathlib.Algebra.Order.Monoid.Units
Units.instLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α],
  Units.instLinearOrder = Function.Injective.linearOrder Units.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofObjects.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) (X : C),
  CategoryTheory.Sieve.ofObjects Y X = { arrows := fun Z x => ∃ i, Nonempty (Z ⟶ Y i), downward_closed := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsImmersion
-- Mathlib.Algebra.Category.Grp.IsFinite
AddCommGrpCat.instIsSerreClassIsFinite : AddCommGrpCat.isFinite.IsSerreClass
-- Mathlib.Order.Zorn
zorn_le₀ : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  (∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) → ∃ m, Maximal (fun x => x ∈ s) m
-- Init.System.IO
IO.FS.instReprMetadata : Repr IO.FS.Metadata
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.op.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.op =
    { toFun := fun f => { toFun := MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯ },
      invFun := fun f => { toFun := MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op, map_one' := ⋯, map_mul' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.unique_affineSpan_singleton : (k : Type u_1) →
  (V : Type u_2) →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [S : AddTorsor V P] → (p : P) → Unique ↥(affineSpan k {p})
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Iterated Frobenius map (ring homomorphism) for purely inseparable field extension with exponent.
If `n ≥ exponent K L`, it acts like `x ↦ x ^ p ^ n` but the codomain is the base field `K`.  -/
IsPurelyInseparable.iterateFrobenius : (K : Type u_2) →
  (L : Type u_3) →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [inst_3 : IsPurelyInseparable.HasExponent K L] →
            (p : ℕ) → [ExpChar K p] → {n : ℕ} → IsPurelyInseparable.exponent K L ≤ n → L →+* K
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.comp_ker_incl : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] {f : M →ₗ⁅R,L⁆ N}, f.comp f.ker.incl = 0
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↑0 = 0
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- **Alias** of `MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_sdiff`.

---

The everywhere positive subset of a set is obtained by removing an open set.  -/
MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  ∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
CategoryTheory.FunctorToTypes.mem_fromOverSubfunctor_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (x : F.obj X)
  {U : CategoryTheory.Over X} (u : F.obj U.left),
  u ∈ (CategoryTheory.FunctorToTypes.fromOverSubfunctor F x).obj U ↔
    (CategoryTheory.ConcreteCategory.hom (F.map U.hom)) u = x
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupSeminormClass.toSeminormedAddCommGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddCommGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  (f : F),
  AddGroupSeminormClass.toSeminormedAddCommGroup f =
    { toNorm := (AddGroupSeminormClass.toSeminormedAddGroup f).toNorm,
      toAddGroup := (AddGroupSeminormClass.toSeminormedAddGroup f).toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := (AddGroupSeminormClass.toSeminormedAddGroup f).toPseudoMetricSpace, dist_eq := ⋯ }
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt : Lean.Compiler.LCNF.Purity → Type
-- Init.Data.UInt.Lemmas
USize.toFin_inj : ∀ {a b : USize}, a.toFin = b.toFin ↔ a = b
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c, ↑c + (↑b₂ + a₁) = ↑c + (↑a₂ + b₁)
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.nsmul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn f (n • g) s
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (e.homEquiv.symm y) g =
    e.homEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map g)) y)
-- Mathlib.Data.Multiset.UnionInter
/-- `s ∪ t` is the multiset such that the multiplicity of each `a` in it is the maximum of the
multiplicity of `a` in `s` and `t`. This is the supremum of multisets.  -/
Multiset.union : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α → Multiset α
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.limsup_mu_le : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ {s : ℕ → ℕ},
      (∀ (n : ℕ), s n ≤ n) →
        ∀ {x : R} {a : ℝ},
          a ∈ Set.Icc 0 1 →
            ∀ {ψ : ℕ → ℕ},
              StrictMono ψ →
                Filter.Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) Filter.atTop (nhds a) →
                  Filter.limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) Filter.atTop ≤ smoothingFun μ x ^ a
-- Mathlib.CategoryTheory.Distributive.Cartesian
/-- A category `C` with finite products is Cartesian distributive if it is monoidal distributive
with respect to the Cartesian monoidal structure.  -/
CategoryTheory.IsCartesianDistributive : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.Algebra.CharP.Defs
CharP.cast_eq_iff_mod_eq : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R], ↑a = ↑b ↔ a % p = b % p
-- Mathlib.Data.List.Permutation
id.eq_def : ∀ {α : Sort u} (a : α), id a = a
-- Mathlib.Data.Part
Part.instMul.eq_1 : ∀ {α : Type u_1} [inst : Mul α], Part.instMul = { mul := fun a b => (fun x1 x2 => x1 * x2) <$> a <*> b }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Only assumes left strict covariance  -/
Left.add_lt_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightMono α] {a b c d : α},
  a < b → c < d → a + c < b + d
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instMax : {V : Type u} → {G : SimpleGraph V} → Max G.Finsubgraph
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.readonly : Lean.Lsp.SemanticTokenModifier
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderIsomorphisms],
  P.strictColimitsOfShape J ≤ P → P.IsClosedUnderColimitsOfShape J
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribInvOfBasis.congr_simp : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} {inst : DecidableEq ι}
  [inst_1 : DecidableEq ι] {inst_2 : DecidableEq κ} [inst_3 : DecidableEq κ] [inst_4 : Fintype ι] [inst_5 : Fintype κ]
  [inst_6 : CommSemiring R] [inst_7 : AddCommMonoid M] [inst_8 : AddCommMonoid N] [inst_9 : Module R M]
  [inst_10 : Module R N] (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ (c c_1 : Module.Basis κ R N),
      c = c_1 → TensorProduct.dualDistribInvOfBasis b c = TensorProduct.dualDistribInvOfBasis b_1 c_1
-- Lean.Data.Position
Lean.instToJsonPosition.toJson : Lean.Position → Lean.Json
-- Mathlib.Topology.MetricSpace.Bounded
/-- A version of the **Extreme Value Theorem**: if the set where a continuous function `f`
into a linearly ordered space takes values `≥ f x₀` is bounded for some `x₀`,
then `f` has a global maximum (under suitable topological assumptions).

This is a convenient combination of `Continuous.exists_forall_ge'` and
`Metric.isCompact_of_isClosed_isBounded`.  -/
Continuous.exists_forall_ge_of_isBounded : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α]
  [inst_3 : PseudoMetricSpace β] [ProperSpace β] {f : β → α},
  Continuous f → ∀ (x₀ : β), Bornology.IsBounded {x | f x₀ ≤ f x} → ∃ x, ∀ (y : β), f y ≤ f x
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Raw.Const.unitOfArray : {α : Type u} →
  Array α →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.Const.unitOfArray._auto_1) →
      Std.DTreeMap.Raw α (fun x => Unit) cmp
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.param.sizeOf_spec : sizeOf Lean.Meta.FunIndParamKind.param = 1
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExists.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E'),
  DiscreteConvolution.AddConvolutionExists L f g = ∀ (x : M), DiscreteConvolution.AddConvolutionExistsAt L f g x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.iInf_span_singleton_natCast : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [inst_1 : Fintype ι] {I : ι → ℕ},
  (Pairwise fun i j => (I i).Coprime (I j)) → ⨅ i, Ideal.span {↑(I i)} = Ideal.span {↑(∏ i, I i)}
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_ne : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R₂ E₂] [inst_4 : NormedAddCommGroup F]
  [inst_5 : Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F}, x ≠ y → f₁ x ≠ f₁ y
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.univ_umax : Cardinal.univ.{u, max (u + 1) v} = Cardinal.univ.{u, v}
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.pendingHead : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Option Std.Http.Request.Head
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : δ → α → m δ} {init : δ}, Std.TreeSet.Raw.foldlM f init t = Array.foldlM f init t.toArray
-- Mathlib.RingTheory.Polynomial.Basic
/-- The multivariate polynomial ring in finitely many variables over a Noetherian ring
is itself a Noetherian ring.  -/
MvPolynomial.isNoetherianRing : ∀ {R : Type u} {σ : Type v} [inst : CommRing R] [Finite σ] [IsNoetherianRing R], IsNoetherianRing (MvPolynomial σ R)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.inst : {B : Type u} → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Bicategory (CategoryTheory.Bicategory.Adj B)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Weird.eq_1 : ∀ (n : ℕ), n.Weird = (n.Abundant ∧ ¬n.Pseudoperfect)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mk.inj : ∀ {C₀ : Type u₀} {C : Type u} {inst : CategoryTheory.Category.{v₀, u₀} C₀} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {S : C} {toPreOneHypercoverDenseData : F.PreOneHypercoverDenseData S}
  {mem₀ : toPreOneHypercoverDenseData.toPreOneHypercover.sieve₀ ∈ J S}
  {mem₁₀ :
    ∀ (i₁ i₂ : toPreOneHypercoverDenseData.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData.X i₁)
      (p₂ : W₀ ⟶ toPreOneHypercoverDenseData.X i₂),
      CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData.f i₁) =
          CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData.f i₂) →
        toPreOneHypercoverDenseData.sieve₁₀ p₁ p₂ ∈ J₀ W₀}
  {toPreOneHypercoverDenseData_1 : F.PreOneHypercoverDenseData S}
  {mem₀_1 : toPreOneHypercoverDenseData_1.toPreOneHypercover.sieve₀ ∈ J S}
  {mem₁₀_1 :
    ∀ (i₁ i₂ : toPreOneHypercoverDenseData_1.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData_1.X i₁)
      (p₂ : W₀ ⟶ toPreOneHypercoverDenseData_1.X i₂),
      CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData_1.f i₁) =
          CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData_1.f i₂) →
        toPreOneHypercoverDenseData_1.sieve₁₀ p₁ p₂ ∈ J₀ W₀},
  { toPreOneHypercoverDenseData := toPreOneHypercoverDenseData, mem₀ := mem₀, mem₁₀ := mem₁₀ } =
      { toPreOneHypercoverDenseData := toPreOneHypercoverDenseData_1, mem₀ := mem₀_1, mem₁₀ := mem₁₀_1 } →
    toPreOneHypercoverDenseData = toPreOneHypercoverDenseData_1
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.message? : Lean.DeprecatedModuleEntry → Option String
-- Init.Data.UInt.Lemmas
UInt32.div_zero : ∀ {a : UInt32}, a / 0 = 0
-- Mathlib.RingTheory.Perfection
Perfection.coe_pthRootMonoidHom_eq_powMulEquiv_symm : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ},
  ⇑(Perfection.pthRootMonoidHom M p) = ⇑(powMulEquiv (Perfection M p) p).symm
-- Mathlib.Data.Nat.Factorial.Basic
Nat.self_le_factorial : ∀ (n : ℕ), n ≤ n.factorial
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast : {lo : ℤ} → {n k : ℕ} → OfNat (Std.Time.Internal.Bounded.LE lo (lo + ↑k)) n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.deprecated.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.deprecated = 1
-- Mathlib.Algebra.Group.Action.End
/-- Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of `MulAction.toPermHom`.  -/
MulDistribMulAction.toMulAut : (G : Type u_1) → (M : Type u_2) → [inst : Group G] → [inst_1 : Monoid M] → [MulDistribMulAction G M] → G →* MulAut M
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimits_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sInfHomClass F α β], CategoryTheory.Limits.PreservesLimits (↑f).toFunctor
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_finTwoProd_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (a b c d : R) (x : R × R),
  ((Matrix.toLin (Module.Basis.finTwoProd R) (Module.Basis.finTwoProd R)) !![a, b; c, d]) x =
    (a * x.1 + b * x.2, c * x.1 + d * x.2)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.sub_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x y : WithCStarModule A ((i : ι) → E i)) (i : ι)
  [inst : (i : ι) → AddCommGroup (E i)], (x - y) i = x i - y i
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, (∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e) → AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e