mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.IsSupported
/-- If `K : HomologicalComplex C c'`, then `K.IsStrictlySupportedOutside e` holds for
an embedding `e : c.Embedding c'` of complex shapes if `K.X (e.f i)` is zero for all `i`.  -/
HomologicalComplex.IsStrictlySupportedOutside : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → HomologicalComplex C c' → c.Embedding c' → Prop
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) →
              ∀ {t : Set Ω},
                MeasurableSet t →
                  ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω => 1 | m] ω = 0 ∨ μ[t.indicator fun ω => 1 | m] ω = 1
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.sigmaFinite_trim_bot_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.SigmaFinite (μ.trim ⋯) ↔ MeasureTheory.IsFiniteMeasure μ
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.smul_extend : ∀ {R : Type u_1} {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) [inst : Semiring R] [IsDomain R]
  [inst_2 : Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R},
  c ≠ 0 → c • MeasureTheory.extend m = MeasureTheory.extend fun s h => c • m s h
-- Init.Data.Option.Lemmas
Option.guard_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α}, p a = true → Option.guard p a = some a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.instAddCommGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F G : CochainComplex C ℤ) → (n : ℤ) → AddCommGroup (CochainComplex.HomComplex.Cocycle F G n)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkip?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos res : s.Pos},
  pos.revSkip? pat = some res ↔ String.Slice.Pattern.Model.IsLongestRevMatchAt pat res pos
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_toList_rco : ∀ {m n : ℕ}, (m...=n).toList = (m...n + 1).toList
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f] (x : ↥X),
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth →
    ∃ U,
      ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
        ∃ V,
          ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
            x ∈ V ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)).Smooth
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_one_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Zero M], (AddMonoidAlgebra.coeff 1) 0 = 1
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.mkHomFromDouble_f₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁) {K : HomologicalComplex C c} (φ₀ : X₀ ⟶ K.X i₀) (φ₁ : X₁ ⟶ K.X i₁)
  (comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
  (hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0),
  (HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₀ f hi₀₁).hom φ₀
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.nnHolderNorm_nsmul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  [NormedSpace ℝ Y] (n : ℕ), MemHolder r f → nnHolderNorm r (n • f) = n • nnHolderNorm r f
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_eq_self : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid N},
  S ≤ MonoidHom.mrange f → Submonoid.map f (Submonoid.comap f S) = S
-- Init.Data.Nat.Basic
/-- Deprecated alias for `Nat.lt_iff_le_and_not_ge`.  -/
Nat.lt_iff_le_not_le : ∀ {m n : ℕ}, m < n ↔ m ≤ n ∧ ¬n ≤ m
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.instSelfAdjointDecompose : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A],
  SelfAdjointDecompose A
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instPow : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : Monoid N] → Pow (OneHom M N) ℕ
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- Auxiliary definition for `CliffordAlgebra.foldr'`  -/
CliffordAlgebra.foldr'Aux : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (Q : QuadraticForm R M) →
                  (M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) → M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- `IsDedekindDomainInv A` implies that fractional ideals over it form a commutative group with
zero.  -/
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.IsDedekindDomainInv.commGroupWithZero : {A : Type u_2} →
  (K : Type u_3) →
    [inst : CommRing A] →
      [inst_1 : Field K] →
        [inst_2 : Algebra A K] →
          [IsFractionRing A K] →
            [inst_4 : IsDomain A] → IsDedekindDomainInv✝ A → CommGroupWithZero (FractionalIdeal (nonZeroDivisors A) K)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.size : Lean.Meta.Simp.UsedSimps → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.lt_iff : ∀ {X : SSet} {x y : X.N}, x < y ↔ x.subcomplex < y.subcomplex
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.pointReflection_fixed_iff_of_module : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [Invertible 2] {x y : P₁}, (AffineEquiv.pointReflection k x) y = y ↔ y = x
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the subgroup of units of `S` and the type of units of `S`.  -/
Submonoid.unitsEquivUnitsType : {M : Type u_1} → [inst : Monoid M] → (S : Submonoid M) → ↥S.units ≃* (↥S)ˣ
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.coe_of : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [inst_1 : CommRing X] [inst_2 : Algebra R X], ↑(CommAlgCat.of R X) = X
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- Given an exact sequence of `G`-representations `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0`, this expresses an
`n`-chain `x : Gⁿ →₀ X₁` such that `f ∘ x ∈ Bₙ(G, X₂)` as a cycle. Stated for readability of
`δ_apply`.  -/
groupHomology.cyclesMkOfCompEqD : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact →
          {i j : ℕ} →
            {y : (Fin i → G) →₀ ↑X.X₂} →
              {x : (Fin j → G) →₀ ↑X.X₁} →
                (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x =
                    (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y →
                  ↑(groupHomology.cycles X.X₁ j)
-- Mathlib.Topology.Algebra.Algebra
continuous_algebraMap : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [ContinuousSMul R A], Continuous ⇑(algebraMap R A)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDHashMap.Const.insertMany m l).getKey! k = m.getKey! k
-- Init.Data.Array.Monadic
Array.foldlM_filter : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Bool}
  {g : β → α → m β} {xs : Array α} {init : β} {w : stop = (Array.filter p xs).size},
  Array.foldlM g init (Array.filter p xs) 0 stop =
    Array.foldlM (fun x y => if p y = true then g x y else pure x) init xs
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.isStronglyProgressive_of_tendsto`. -/
MeasureTheory.progMeasurable_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β] {U : ℕ → ι → Ω → β},
  (∀ (l : ℕ), MeasureTheory.IsStronglyProgressive f (U l)) →
    Filter.Tendsto U Filter.atTop (nhds u) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.exists_of₂ : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] [Nonempty ι] [IsDirectedOrder ι] (z w : Module.DirectLimit G f),
  ∃ i x y, (Module.DirectLimit.of R ι G f i) x = z ∧ (Module.DirectLimit.of R ι G f i) y = w
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.hasDerivAtFilter : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} {L' : Filter 𝕜},
  HasGradientAtFilter g g' u L' → HasDerivAtFilter g ((starRingEnd 𝕜) g') (L' ×ˢ pure u)
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- **Fundamental theorem of algebra**: every nonconstant complex polynomial
has a root.  -/
Complex.exists_root : ∀ {f : Polynomial ℂ}, 0 < f.degree → ∃ z, f.IsRoot z
-- Mathlib.RingTheory.PrincipalIdealDomain
IsPrime.to_maximal_ideal : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : S.IsPrime],
  S ≠ ⊥ → S.IsMaximal
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The function from `S.leftAdd` to `S` sending an element to its right additive
inverse in `S`. This is an `AddMonoidHom` when `M` is commutative.  -/
AddSubmonoid.fromLeftNeg : {M : Type u_1} → [inst : AddMonoid M] → (S : AddSubmonoid M) → ↥S.leftNeg → ↥S
-- Batteries.Data.List.Basic
/-- Optimized version of `dropSlice`.  -/
List.dropSliceTR : {α : Type u_1} → ℕ → ℕ → List α → List α
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K]
  [inst_6 : IsFractionRing R K],
  FractionalIdeal.absNorm =
    { toFun := fun I => ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|, map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Order.Category.Frm
Frm.hom_inv_apply : ∀ {X Y : Frm} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Topology.Order.IntermediateValue
isConnected_uIoc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a ≠ b → IsConnected (Set.uIoc a b)
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- If `b` is strictly between `a` and `c`, and `p -ᵥ a` is orthogonal to `b -ᵥ a`,
then `p` is closer to `b` than to `c`.  -/
EuclideanGeometry.dist_lt_of_sbtw_of_inner_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p : P}, Sbtw ℝ a b c → inner ℝ (p -ᵥ a) (b -ᵥ a) = 0 → dist p b < dist p c
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a')
  {Z : F.obj a ⟶ a'}
  (h :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (G.obj a)) f) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom h)))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roc α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.op_commShiftIso_hom_app_assoc : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ)
  (h : n + m = 0) {Z : Dᵒᵖ} (h_1 : (CategoryTheory.shiftFunctor Dᵒᵖ n).obj (F.op.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).hom.app X) h_1 =
    CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F m).inv.app (Opposite.unop X)).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X))))
          h_1))
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f` is bounded, then its `LSeries` is summable at `s : ℝ` when `s > 1`.  -/
LSeriesSummable_of_bounded_of_one_lt_real : ∀ {f : ℕ → ℂ} {m : ℝ}, (∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m) → ∀ {s : ℝ}, 1 < s → LSeriesSummable f ↑s
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Endowing the space `WithLp p (α × β)` with the `L^p` edistance. We register this instance
separate from `WithLp.instProdPseudoEMetric` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future emetric-like structure on `WithLp p (α × β)` for
`p < 1` satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*.  -/
WithLp.instProdEDist : (p : ENNReal) → (α : Type u_2) → (β : Type u_3) → [EDist α] → [EDist β] → EDist (WithLp p (α × β))
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.nnreal_le_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ spectrum NNReal a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, ↑r ≤ x
-- Init.Data.SInt.Basic
instDecidableEqInt8 : DecidableEq Int8
-- Mathlib.Topology.Separation.Basic
/-- If a function to a `T1Space` tends to some limit `y` at some point `x`, then necessarily
`y = f x`.  -/
eq_of_tendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {f : X → Y}
  {x : X} {y : Y}, Filter.Tendsto f (nhds x) (nhds y) → f x = y
-- Mathlib.Data.Set.Image
Set.eq_preimage_iff_image_eq : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → ∀ {s : Set α} {t : Set β}, s = f ⁻¹' t ↔ f '' s = t
-- Mathlib.Topology.Connected.PathConnected
PathConnectedSpace.exists_path_through_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PathConnectedSpace X] {n : ℕ} (p : Fin (n + 1) → X),
  ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_zero : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, ¬IsOfFinOrder x → orderOf x = 0
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq.eq_3 : ∀ (x x_1 : Lean.Grind.AC.Seq),
  (∀ (a b : Lean.Grind.AC.Var), x = Lean.Grind.AC.Seq.var a → x_1 = Lean.Grind.AC.Seq.var b → False) →
    (∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
        x = Lean.Grind.AC.Seq.cons a a_1 → x_1 = Lean.Grind.AC.Seq.cons b b_1 → False) →
      Lean.Grind.AC.instBEqSeq.beq x x_1 = false
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk.inj : ∀ {R : Type u} {inst : LE R} {inst_1 : AddCommMonoid R} {inst_2 : One R} {M : Type v} {weights : M →₀ R}
  {nonneg : 0 ≤ weights} {total : (weights.sum fun x r => r) = 1} {weights_1 : M →₀ R} {nonneg_1 : 0 ≤ weights_1}
  {total_1 : (weights_1.sum fun x r => r) = 1},
  { weights := weights, nonneg := nonneg, total := total } =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 } →
    weights = weights_1
-- Mathlib.Geometry.Convex.Cone.Dual
/-- Duality with respect to a general bilinear map can be expressed as duality using the
identity pairing.  -/
PointedCone.dual_eq_dual_id_map : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (C : PointedCone R M),
  PointedCone.dual p ↑C = PointedCone.dual LinearMap.id ↑(PointedCone.map p C)
-- Mathlib.GroupTheory.GroupAction.Basic
Finite.finite_mulAction_orbit : ∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] [Finite M] (a : α), (MulAction.orbit M a).Finite
-- Mathlib.GroupTheory.IsSubnormal
/-- The quotient of a subnormal additive subgroup by a normal additive subgroup is subnormal.  -/
AddSubgroup.IsSubnormal.quotient : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [inst_1 : K.Normal],
  H.IsSubnormal → (AddSubgroup.map (QuotientAddGroup.mk' K) H).IsSubnormal
-- Lean.Server.Requests
Lean.Server.ServerRequestEmitter : Type
-- Mathlib.Topology.Order.Compact
CompactIccSpace.mk' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  (∀ {a b : α}, a ≤ b → IsCompact (Set.Icc a b)) → CompactIccSpace α
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_shiftRight : ∀ (a : BitVec 32), ∀ b < 32, { toBitVec := a >>> b } = { toBitVec := a } >>> UInt32.ofNat b
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {a a' : M} {b : R} [inst_1 : Decidable (a = a')],
  (AddMonoidAlgebra.single a b).coeff a' = if a = a' then b else 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_ofNat : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : α → β} (n : ℕ) [inst_1 : n.AtLeastTwo],
  WithBot.map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.instIsIsoF' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i : D.J),
  CategoryTheory.IsIso (D.f' i i)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toPreimages_map : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) {X Y : J} (g : X ⟶ Y),
  (F.toPreimages s).map g =
    TypeCat.ofHom
      (Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom (F.map g)))
        (⋂ f, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' s)
        (⋂ f, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' s) ⋯)
-- Lean.Meta.Eqns
Lean.Meta.EqnsExtState.mk : Lean.PHashMap Lean.Name Lean.Name → Lean.Meta.EqnsExtState
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The free monic polynomial of degree `n`, as a polynomial in `R[X₁,...,Xₙ][X]`.  -/
Polynomial.freeMonic : (R : Type u_1) → [inst : CommRing R] → (n : ℕ) → Polynomial (MvPolynomial (Fin n) R)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.InftyValuation.map_one' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], RatFunc.inftyValuationDef F 1 = 1
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_smul_inv : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M), c • f x = f (σ' c • x)
-- Mathlib.Data.Set.Card
Set.ncard_union_le : ∀ {α : Type u_1} (s t : Set α), (s ∪ t).ncard ≤ s.ncard + t.ncard
-- Mathlib.Algebra.Homology.Monoidal
/-- Auxiliary definition for `leftUnitor`.  -/
HomologicalComplex.leftUnitor' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  {c : ComplexShape I} →
                    [inst_7 : c.TensorSigns] →
                      (K : HomologicalComplex C c) →
                        [inst_8 : DecidableEq I] →
                          [inst_9 :
                              ∀ (X₂ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                            ((HomologicalComplex.tensorUnit C c).tensorObj K).X ≅ K.X
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ioc_eq_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → nhdsWithin b (Set.Ioc b a) = nhdsWithin b (Set.Ioi b)