mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.uniform_continuity : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f : C(α, β)) (ε : ℝ), 0 < ε → ∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_isoBot : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i],
  (SSet.relativeCellComplexOfMono i).isoBot =
    SSet.Subcomplex.eqToIso ⋯ ≪≫ (CategoryTheory.asIso (SSet.Subcomplex.toRange i)).symm
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The functor used to define the equivalence `ofCommaFstEquivalence`.  -/
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c)
                    (CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instMulDistribMulActionUnits : {R : Type uR} →
  {A₁ : Type uA₁} →
    [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ
-- Mathlib.Analysis.Analytic.IteratedFDeriv
FormalMultilinearSeries.iteratedFDerivSeries_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {k n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots_iff_aeval_eq_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {x : R},
  p ≠ 0 → (x ∈ p.roots ↔ (Polynomial.aeval x) p = 0)
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteAddMonoid : ∀ (M : Type u_2) [inst : AddCommMonoid M], IsDedekindFiniteAddMonoid M
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsOneApplyEqSelf.one_apply_eq_self`. -/
one_apply_eq_self : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : One F} [self : IsOneApplyEqSelf F α]
  (x : α), 1 x = x
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSystem_coroot_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α : ↥LieSubalgebra.root),
  (LieAlgebra.IsKilling.rootSystem H).coroot α = LieAlgebra.IsKilling.coroot ↑α
-- Init.Data.Rat.Lemmas
Rat.divInt_add_divInt : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℤ},
  d₁ ≠ 0 → d₂ ≠ 0 → Rat.divInt n₁ d₁ + Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ + n₂ * d₁) (d₁ * d₂)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly (-F) (-f) l
-- Mathlib.Data.List.InsertIdx
List.get_insertIdx_of_lt : ∀ {α : Type u} (l : List α) (x : α) (n k : ℕ),
  k < n →
    ∀ (hk : k < l.length) (hk' : autoParam (k < (l.insertIdx n x).length) List.get_insertIdx_of_lt._auto_1),
      (l.insertIdx n x).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.ext_iff : ∀ {X : SSet} (x y : X.N), x = y ↔ x.toS = y.toS
-- Mathlib.LinearAlgebra.Prod
Submodule.range_fst : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.fst R M M₂).range = ⊤
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.prod_multisetInfinitePlace_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : CommMonoid M]
  (f : AbsoluteValue K ℝ → M), (Multiset.map f (NumberField.multisetInfinitePlace K)).prod = ∏ v, f ↑v ^ v.mult
-- Init.Data.Bool
Bool.instCommutativeOr : Std.Commutative fun x1 x2 => x1 || x2
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_push : ∀ {m n : ℕ}, m < n → (m<...=n).toArray = (m<...=n - 1).toArray.push n
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Subsemiring.isHomogeneous_iff_subset_iInter : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] (R : Subsemiring A),
  DirectSum.SetLike.IsHomogeneous 𝒜 R ↔ ↑R ⊆ ⋂ i, ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑R
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_conj : ∀ (x : ℂ), Complex.exp ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.exp x)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.const` as a `MulHom`.  -/
Pi.constMulHom : (α : Type u_5) → (β : Type u_6) → [inst : Mul β] → β →ₙ* α → β
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.apply_covBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  f a ⋖ f b ↔ a ⋖ b
-- Mathlib.Order.Filter.TendstoCofinite
Filter.tendstoCofinite_iff_finite_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Filter.TendstoCofinite f ↔ ∀ (b : β), (f ⁻¹' {b}).Finite
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite =
  { hom := fun {X Y} f => f.hom', ofHom := fun {X Y} f => { hom' := f },
    hom_ofHom :=
      @instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_1,
    ofHom_hom :=
      @instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_2,
    id_apply :=
      @instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_3,
    comp_apply :=
      @instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_4 }
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.faithful : ∀ {G : Type u_1} (A : Type u_2) {B : Type u_4} {inst : Group G} {inst_1 : CommSemiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra A B} {inst_4 : MulSemiringAction G B} [self : IsGaloisGroup G A B], FaithfulSMul G B
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_sum_sum : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H₁ H₂ : AddSubgroup G)
  (K₁ K₂ : AddSubgroup G'), ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instAlgebraInteger : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {ΓR : Type u_6} →
            {ΓA : Type u_7} →
              [inst_3 : LinearOrderedCommGroupWithZero ΓR] →
                [inst_4 : LinearOrderedCommGroupWithZero ΓA] →
                  {vR : Valuation R ΓR} → {vA : Valuation A ΓA} → [vR.HasExtension vA] → Algebra ↥vR.integer ↥vA.integer
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error.
 -/
CategoryTheory.GrothendieckTopology.map_yonedaEquiv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F)
  (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app Y)) g.unop
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A bilinear form is nonnegative if and only if it is nonnegative as a sesquilinear form.  -/
LinearMap.BilinForm.isNonneg_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsNonneg ↔ LinearMap.IsNonneg B
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulZeroClassAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : SMul M α] →
              [MeasurableConstSMul M α] →
                [MeasureTheory.SMulInvariantMeasure M α μ] → [inst_5 : Zero β] → SMulZeroClass Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C)
  {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  (X.ofRestrict h).hom.base = f
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Ioo_eq_of_Icc_succ_pred_eq : ∀ {m n : ℤ} {s : Finset ℤ}, Finset.Icc (m + 1) (n - 1) = s → Finset.Ioo m n = s
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalTorsorProd : ∀ {V : Type u_1} {W : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : CommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : Torsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] [inst_5 : CommGroup W]
  [inst_6 : TopologicalSpace W] [inst_7 : Torsor W Q] [inst_8 : TopologicalSpace Q] [IsTopologicalTorsor Q],
  IsTopologicalTorsor (P × Q)
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The quotient of `P` as an `S`-submodule is the same as the quotient of `P` as an `R`-submodule,
where `P : Submodule R M`.
 -/
Submodule.Quotient.restrictScalarsEquiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (S : Type u_3) →
            [inst_3 : Ring S] →
              [inst_4 : SMul S R] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower S R M] → (P : Submodule R M) → (M ⧸ Submodule.restrictScalars S P) ≃ₗ[S] M ⧸ P
-- Mathlib.Lean.Meta.Tactic.Rewrite
/-- Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.

Rewrites with a fresh metavariable as the ambient goal.
Fails if the rewrite produces any subgoals.
 -/
Lean.Expr.rewrite : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The range of a `MonoidHom` is a `Submonoid`. See Note [range copy pattern].  -/
MonoidHom.mrange : {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 → Submonoid N
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instBEqConfig : BEq Mathlib.Meta.FunProp.Config
-- Mathlib.Order.Filter.Pointwise
/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Filter`. See Note [pointwise nat action].  -/
Filter.instZPow : {α : Type u_2} → [One α] → [Mul α] → [Inv α] → Pow (Filter α) ℤ
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprHeader : Repr Std.Time.TimeZone.TZif.Header
-- Init.Data.Nat.Basic
Nat.sub_one_mul : ∀ (n m : ℕ), (n - 1) * m = n * m - m
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the base of a pretrivialization from a nonempty set to the whole space.  -/
Bundle.Trivialization.codExtend : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] →
            {s : Set B} →
              IsOpen s →
                s.Nonempty →
                  {proj : Z → ↑s} → Bundle.Trivialization F proj → Bundle.Trivialization F (Subtype.val ∘ proj)
-- Mathlib.Algebra.Group.Ext
DivInvMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : DivInvMonoid M⦄, HMul.hMul = HMul.hMul → Inv.inv = Inv.inv → m₁ = m₂
-- Mathlib.RingTheory.Etale.Finite
/-- If `k` is a field, this is the `Spec` functor sending a finite étale `k`-algebra `R`
to its finite prime spectrum.  -/
CommAlgCat.FiniteEtale.finiteSpec : (k : Type u) → [inst : Field k] → CategoryTheory.Functor (CommAlgCat.FiniteEtale k)ᵒᵖ FintypeCat
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((f x.1) x.2)
-- Lean.Meta.Instances
Lean.Meta.Instances.mk : Lean.Meta.InstanceTree → Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry → Lean.PHashSet Lean.Name → Lean.Meta.Instances
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk.inj : ∀ {M : Type u_1} {inst : CommMonoid M} {S : Submonoid M} {N : Type u_2} {inst_1 : CommMonoid N} {toMulHom : M →ₙ* N}
  {isLocalizationMap : S.IsLocalizationMap toMulHom.toFun} {toMulHom_1 : M →ₙ* N}
  {isLocalizationMap_1 : S.IsLocalizationMap toMulHom_1.toFun},
  { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap } =
      { toMulHom := toMulHom_1, isLocalizationMap := isLocalizationMap_1 } →
    toMulHom = toMulHom_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_nonneg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ a - b ↔ b ≤ a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_iff_eq_right : ∀ {s : Set ℕ}, ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.eq_prime_pow_mul_coprime : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I : Ideal T},
  I ≠ ⊥ →
    ∀ (P : Ideal T) [hpm : P.IsMaximal],
      ∃ Q, P ⊔ Q = ⊤ ∧ I = P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) * Q
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsTrivialBlock.preimage : ∀ {M : Type u_3} {α : Type u_4} {N : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α]
  [inst_2 : AddMonoid N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Injective ⇑f → ∀ {B : Set β}, AddAction.IsTrivialBlock B → AddAction.IsTrivialBlock (⇑f ⁻¹' B)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.toPiLocalization_bijective : ∀ {R : Type u} [inst : CommSemiring R] [DiscreteTopology (PrimeSpectrum R)],
  Function.Bijective ⇑(PrimeSpectrum.toPiLocalization R)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.incl.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithTerminal.incl =
    { obj := CategoryTheory.WithTerminal.of, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → (ι → ℕ) → ι → ℕ
-- Lean.MonadEnv
Lean.matchConst : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [Lean.MonadEnv m] → Lean.Expr → (Unit → m α) → (Lean.ConstantInfo → List Lean.Level → m α) → m α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {A : Type u_4} [inst_2 : CategoryTheory.Category.{v_4, u_4} A]
  (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [inst_5 : G.IsContinuous J K],
  (G.sheafPushforwardContinuous A J K).Faithful
-- Init.Data.List.Lemmas
List.eraseDups_append : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {as bs : List α},
  (as ++ bs).eraseDups = as.eraseDups ++ (bs.removeAll as).eraseDups
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism to an initial object is epi.  -/
CategoryTheory.Limits.IsInitial.epi_to : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X)
  (f : Y ⟶ X), CategoryTheory.Epi f
-- Mathlib.Data.List.Dedup
List.dedup_cons_of_mem' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l.dedup → (a :: l).dedup = l.dedup
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_base_mul : ∀ {b m : ℕ}, 1 < b → 0 < m → b.digits (b * m) = 0 :: b.digits m
-- Mathlib.Order.SuccPred.Basic
Set.OrdConnected.succOrder : {α : Type u_3} → [inst : PartialOrder α] → {s : Set α} → [s.OrdConnected] → [SuccOrder α] → SuccOrder ↑s
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_interior_face_iff_pos : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [IsOrderedAddMonoid k] {n : ℕ} (s : Affine.Simplex k P n)
  {fs : Finset (Fin (n + 1))} {m : ℕ} [NeZero m] (h : fs.card = m + 1) {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).interior ↔
      (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0)
-- Mathlib.NumberTheory.Modular
ModularGroup.stabilizer_ρ : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  g • UpperHalfPlane.ρ = UpperHalfPlane.ρ ↔
    g ∈
      {1, -1, ModularGroup.S * ModularGroup.T, -(ModularGroup.S * ModularGroup.T), ModularGroup.T⁻¹ * ModularGroup.S,
        -(ModularGroup.T⁻¹ * ModularGroup.S)}
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
/-- Let `K` be a finite field of cardinality `p ^ f` and let `P` be an irreducible factor of the
`n`-th cyclotomic polynomial over `K`, where `p` and `n` are coprime. Then the degree of `P` is
the multiplicative order of `p ^ f` modulo `n`.  -/
Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ} {P : Polynomial K},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)],
      P ∣ Polynomial.cyclotomic n K → Irreducible P → P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_not_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  (Filter.blimsup u f fun x => ¬p x) ⊔ Filter.blimsup u f p = Filter.limsup u f
-- Mathlib.Order.Disjoint
disjoint_right_comm : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α}, Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.hasOpNorm : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] → [inst_5 : NormedSpace 𝕜₂ F] → {σ₁₂ : 𝕜 →+* 𝕜₂} → Norm (E →SL[σ₁₂] F)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.toSubmonoid_mono : ∀ {R : Type u} [inst : NonAssocSemiring R], Monotone Subsemiring.toSubmonoid
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.le_norm_of_le_abs_repr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ) (i : ι),
  ↑n ≤ |(b.repr x) i| → ZLattice.normBound b * ↑n ≤ ‖x‖
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.limitCommGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] →
        CommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommGrpCat))).pt
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ι_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε P.ι =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_1.eq_1 : ∀ (motive : Num × Num → Sort u_1) (q r₁ : Num) (h_1 : (q r₁ : Num) → motive (q, r₁)),
  (match (q, r₁) with
    | (q, r₁) => h_1 q r₁) =
    h_1 q r₁
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- If a function is the greatest lower bound of countably many measurable functions on a measurable
set `s`, and coincides with a measurable function outside of `s`, then it is measurable.  -/
Measurable.isGLB_of_mem : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α} {g g' : δ → α},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {s : Set δ},
      MeasurableSet s → (∀ b ∈ s, IsGLB {a | ∃ i, f i b = a} (g b)) → Set.EqOn g g' sᶜ → Measurable g' → Measurable g
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Write a list of `Bool`s on the tape.  -/
Turing.TM1to1.write : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      List Bool → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt.inj : ∀ {a b toIntThm : Lean.Expr} {lhs rhs : Int.Internal.Linear.Expr} {a_1 b_1 toIntThm_1 : Lean.Expr}
  {lhs_1 rhs_1 : Int.Internal.Linear.Expr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a b toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a_1 b_1 toIntThm_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_dvd_ordCompl_iff_dvd : ∀ (a b : ℕ), (∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b
-- Std.Time.Format.DateFormat
/-- `DayPeriodSymbols` holds the four locale strings used by the `b` pattern: AM, PM, noon, midnight.
 -/
Std.Time.DayPeriodSymbols : Type
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_neg : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  (-s).singularPart μ = -s.singularPart μ
-- Mathlib.SetTheory.Lists
Lists'.cons'.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] {b : Bool} (a : Lists' α b) (a_1 : Lists' α true),
  sizeOf (a.cons' a_1) = 1 + sizeOf b + sizeOf a + sizeOf a_1