mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
isAdjointPair_toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {n' : Type u_13} [inst : CommRing R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂]
  [inst_5 : Fintype n] [inst_6 : Fintype n'] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis n' R M₂) (J : Matrix n n R)
  (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [inst_7 : DecidableEq n] [inst_8 : DecidableEq n'],
  ((Matrix.toLinearMap₂ b₁ b₁) J).IsAdjointPair ((Matrix.toLinearMap₂ b₂ b₂) J') ⇑((Matrix.toLin b₁ b₂) A)
      ⇑((Matrix.toLin b₂ b₁) A') ↔
    J.IsAdjointPair J' A A'
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
nonzero derivative `f'` at `f.symm a` in the strict sense, then `f.symm` has the derivative `f'⁻¹`
at `a` in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.hasStrictDerivAt_symm : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜},
  a ∈ f.target → f' ≠ 0 → HasStrictDerivAt (↑f) f' (↑f.symm a) → HasStrictDerivAt (↑f.symm) f'⁻¹ a
-- Init.Meta.Defs
/-- Creates a hole (`_`). The hole's position is copied from `ref`.
 -/
Lean.mkHole : Lean.Syntax → optParam Bool false → Lean.Term
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.sle_iff_rotate_le_rotate : ∀ {n : ℕ} {x y : BitVec n}, x.sle y = true ↔ BitVec.Signed.rotate✝ x ≤ BitVec.Signed.rotate✝ y
-- Mathlib.FieldTheory.Normal.Defs
Normal.toIsAlgebraic : ∀ {F : Type u_1} {K : Type u_2} {inst : Field F} {inst_1 : Field K} {inst_2 : Algebra F K} [self : Normal F K],
  Algebra.IsAlgebraic F K
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.equiv_symm_apply_toCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (toCLM : E →SL[σ] F),
  (ContinuousLinearMapWOT.equiv.symm toCLM).toCLM = toCLM
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_unique : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) (j : S →+* Q),
  (∀ (x : R), j ((algebraMap R S) x) = (algebraMap P Q) (g x)) → IsLocalization.map Q g hy = j
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.fac_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : a ⟶ b') [inst_3 : p.IsHomLift f φ'] {Z : 𝒳} (h : b' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCocartesian.map p f φ φ') h) =
    CategoryTheory.CategoryStruct.comp φ' h
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eval_derivative_eq_eval_mul_sum : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R},
  f.Splits →
    ∀ {x : R},
      Polynomial.eval x f ≠ 0 →
        Polynomial.eval x (Polynomial.derivative f) =
          Polynomial.eval x f * (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
-- Mathlib.RingTheory.Multiplicity
multiplicity_pow_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p : α},
  p ≠ 0 → ¬IsUnit p → ∀ (n : ℕ), multiplicity p (p ^ n) = n
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.epi_iff_range_eq_top : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y), CategoryTheory.Epi f ↔ (ModuleCat.Hom.hom f).range = ⊤
-- Batteries.Lean.Meta.UnusedNames
/-- Obtain a name `n` such that `n` is unused in the current local context and
`suggestion` is a prefix of `n`.
 -/
Lean.Meta.getUnusedUserName : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → Lean.Name → m Lean.Name
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_multiset_prod_le : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (m : Multiset E), ‖m.prod‖₊ ≤ (Multiset.map (fun x => ‖x‖₊) m).sum
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.comp_obj : ∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C),
  (CategoryTheory.CategoryStruct.comp F G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans F G) (θ : CategoryTheory.Lax.LaxTrans G H)
  {a b : B} {f g : a ⟶ b} (β : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (η.vCompNaturality θ f)
      (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β))
      (η.vCompNaturality θ g)
-- Mathlib.Order.Concept
/-- The intent of a concept.  -/
Concept.intent : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Concept α β r → Set β
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk : (coe : ℂ) → 0 < coe.im → UpperHalfPlane
-- Mathlib.Algebra.Group.Prod
/-- Multiplying by the trivial monoid doesn't change the structure.

This is the `MulEquiv` version of `Equiv.prodUnique`.  -/
MulEquiv.prodUnique : {M : Type u_3} → {N : Type u_4} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [Unique N] → M × N ≃* M
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq.eq_2 : ∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
  Lean.Grind.AC.instBEqSeq.beq (Lean.Grind.AC.Seq.cons a a_1) (Lean.Grind.AC.Seq.cons b b_1) =
    (a == b && Lean.Grind.AC.instBEqSeq.beq a_1 b_1)
-- Mathlib.Topology.Separation.Hausdorff
eqOn_closure₂ : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_3} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z},
  (∀ x ∈ s, ∀ y ∈ t, f x y = g x y) →
    Continuous (Function.uncurry f) → Continuous (Function.uncurry g) → ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The characteristic map of the `n`-cell given by the index `i`.
This map is a bijection when restricting to `ball 0 1`, where we consider `(Fin n → ℝ)`
endowed with the maximum metric.  -/
Topology.CWComplex.map : {X : Type u} →
  {inst : TopologicalSpace X} →
    {C : Set X} → [self : Topology.CWComplex C] → (n : ℕ) → Topology.CWComplex.cell C n → PartialEquiv (Fin n → ℝ) X
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart.eq_1 : ∀ {Ω : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m0 : MeasurableSpace Ω}
  (f : ℕ → Ω → E) (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) (n : ℕ),
  MeasureTheory.martingalePart f ℱ μ n = f n - MeasureTheory.predictablePart f ℱ μ n
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_one : ∀ (S : Type u_2) [inst : Semiring S] (n : ℕ), Polynomial.eval 1 (ascPochhammer S n) = ↑n.factorial
-- Lean.Elab.InfoTree.Types
/-- Name of the field as written.  -/
Lean.Elab.FieldInfo.fieldName : Lean.Elab.FieldInfo → Lean.Name
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `smul_apply`. -/
CuspForm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.HasExponent.mk : ∀ {K : Type u_2} {L : Type u_3} [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L],
  (∃ e, ∀ (a : L), a ^ ringExpChar K ^ e ∈ (algebraMap K L).range) → IsPurelyInseparable.HasExponent K L
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.splits : ∀ (n : ℕ) {K : Type u} [inst : Field K] (f : Polynomial K),
  f.natDegree = n → (Polynomial.map (algebraMap K (Polynomial.SplittingFieldAux n f)) f).Splits
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushExcept.match_1.splitter : {α ε : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Alternatization of a continuous multilinear map.  -/
ContinuousMultilinearMap.alternatization : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      [inst_7 : IsTopologicalAddGroup N] →
                        [Fintype ι] → [DecidableEq ι] → ContinuousMultilinearMap R (fun x => M) N →+ M [⋀^ι]→L[R] N
-- Mathlib.Data.Finset.Sups
Finset.sups_infs_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] (s t u : Finset α), s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
-- Mathlib.Algebra.GCDMonoid.Basic
instSubsingletonStrongNormalizedGCDMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [Subsingleton αˣ], Subsingleton (StrongNormalizedGCDMonoid α)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mem_sInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {f : Set (SaturatedAddSubmonoid M)} {x : M}, x ∈ sInf f ↔ ∀ s ∈ f, x ∈ s
-- Mathlib.RingTheory.WittVector.WittPolynomial
bind₁_wittPolynomial_xInTermsOfW : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (n : ℕ),
  (MvPolynomial.bind₁ (wittPolynomial p R)) (xInTermsOfW p R n) = MvPolynomial.X n
-- Init.Data.Nat.Basic
Nat.eq_self_sub_one : ∀ {n : ℕ}, n = n - 1 ↔ n = 0
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The natural embedding of L^p into tempered distributions.  -/
MeasureTheory.Lp.toTemperedDistributionCLM : {E : Type u_3} →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [CompleteSpace F] →
              [inst_5 : MeasurableSpace E] →
                [BorelSpace E] →
                  (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.Lp.toTemperedDistributionCLM._auto_1) →
                    [μ.HasTemperateGrowth] →
                      (p : ENNReal) → [hp : Fact (1 ≤ p)] → ↥(MeasureTheory.Lp F p μ) →L[ℂ] TemperedDistribution E F
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x + y, - x)` is measure-preserving.  -/
MeasureTheory.measurePreserving_add_prod_neg_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] [ν.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, -z.1)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual : {α : Type u_1} → [LinearOrderedCommMonoidWithZero α] → LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ)
-- Mathlib.Data.ZMod.Basic
ZMod.val_cast_zmod_lt : ∀ {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m), a.cast.val < m
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.FormallyUnramified f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- A single term of a Mahler series, given by the product of the scalar-valued continuous map
`mahler n : ℤ_[p] → ℤ_[p]` with a constant vector in some normed `ℤ_[p]`-module.
 -/
PadicInt.mahlerTerm : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {E : Type u_1} →
      [inst : NormedAddCommGroup E] → [inst_1 : Module ℤ_[p] E] → [IsBoundedSMul ℤ_[p] E] → E → ℕ → C(ℤ_[p], E)
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkMVars.checkNormMVars : Lean.Meta.SavedState → Aesop.Goal → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_iUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {s : β → Set α},
  (∀ (i : β), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ltAddSubgroup_le_leAddSubgroup : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : Γ₀ˣ), v.ltAddSubgroup γ ≤ v.leAddSubgroup ↑γ
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.effectiveEpiFamily_of_jointly_surjective : ∀ {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B),
  (∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) → CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Order.Disjointed
disjointed_succ : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : SuccOrder ι] (f : ι → α) {i : ι},
  ¬IsMax i → disjointed f (Order.succ i) = f (Order.succ i) \ (partialSups f) i
-- Mathlib.Algebra.Group.Int.Even
Int.even_coe_nat : ∀ (n : ℕ), Even ↑n ↔ Even n
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.pushforwardIso_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] [inst_1 : P.ContainsIdentities]
  [inst_2 : P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y)
  [inst_3 : CategoryTheory.IsIso f] (x : 𝒰.I₀), (𝒰.pushforwardIso f).X x = 𝒰.X x
-- Mathlib.RingTheory.Jacobson.Semiprimary
/-- The Jacobson radical of a ring annihilates every semisimple module.  -/
IsSemisimpleModule.jacobson_le_annihilator : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], Ring.jacobson R ≤ Module.annihilator R M
-- Mathlib.Order.Partition.Basic
Partition.parts_top : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α], s ≠ ⊥ → ↑⊤ = {s}
-- Mathlib.RingTheory.Ideal.Span
IsIdempotentElem.ker_toSpanSingleton_eq_span : ∀ {R : Type u_1} [inst : CommRing R] {e : R},
  IsIdempotentElem e → (LinearMap.toSpanSingleton R R e).ker = Ideal.span {1 - e}
-- Mathlib.Order.Disjointed
disjointed_partialSups : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : PartialOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α), disjointed ⇑(partialSups f) = disjointed f
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.assertHypothesis : Lean.MVarId → Lean.Meta.Hypothesis → Lean.Meta.TransparencyMode → Aesop.Script.TacticBuilder
-- Mathlib.Analysis.Distribution.Distribution
Distribution.delta_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞}
  (x : E) (f : TestFunction Ω ℝ n), (Distribution.delta x) f = f x
-- Mathlib.Combinatorics.Hindman
Hindman.exists_FS_of_large : ∀ {M : Type u_1} [inst : AddSemigroup M] (U : Ultrafilter M), U + U = U → ∀ s₀ ∈ U, ∃ a, Hindman.FS a ⊆ s₀
-- Mathlib.Order.RelSeries
RelSeries.eraseLast_toFun : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length - 1 + 1)), p.eraseLast.toFun i = p.toFun ⟨↑i, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.hasZeroObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → CategoryTheory.Limits.HasZeroObject C
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability.  -/
uniqueDiffOn_convex : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} [IsTopologicalAddGroup E], Convex ℝ s → (interior s).Nonempty → UniqueDiffOn ℝ s
-- Mathlib.Order.RelClasses
instAntisymmGe : ∀ {α : Type u} [inst : PartialOrder α], Std.Antisymm fun x1 x2 => x2 ≤ x1
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Adjunction.toKleisli_map_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Kleisli.Adjunction.toKleisli T).map f).of = CategoryTheory.CategoryStruct.comp f (T.η.app Y)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNeg.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M),
  S.leftNeg = { carrier := {x | ∃ y, x + ↑y = 0}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Analysis.MellinTransform
/-- The Mellin transform of the indicator function of `Ioc 0 1`.  -/
hasMellin_one_Ioc : ∀ {s : ℂ}, 0 < s.re → HasMellin ((Set.Ioc 0 1).indicator fun x => 1) s (1 / s)
-- Mathlib.Order.Hom.Bounded
/-- Composition of `TopHom`s as a `TopHom`.  -/
TopHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Top α] → [inst_1 : Top β] → [inst_2 : Top γ] → TopHom β γ → TopHom α β → TopHom α γ
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.severity : Lean.ErrorExplanation.Metadata → Lean.MessageSeverity
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `f : M →* N` and `k : M →* P` are Localization maps for a Submonoid `S`, we get an
isomorphism of `N` and `P`.  -/
Submonoid.LocalizationMap.mulEquivOfLocalizations : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} → [inst_2 : CommMonoid P] → S.LocalizationMap N → S.LocalizationMap P → N ≃* P
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} [inst_1 : SizeOf C]
  [inst_2 : SizeOf ι] (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom :
    (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j))
  (pullHom'_hom_self :
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i)))
  (pullHom'_hom_comp :
    ∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
            ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯
            ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯
          ⋯),
  sizeOf { obj := obj, hom := hom, pullHom'_hom_self := pullHom'_hom_self, pullHom'_hom_comp := pullHom'_hom_comp } = 1
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.paramsStructure : (α : Type w') → (A : Set α) → (FirstOrder.Language.constantsOn ↑A).Structure α
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.integrable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : MeasureTheory.Measure α} {f : β → E},
  MeasureTheory.AEStronglyMeasurable f (μ.bind ⇑κ) →
    (MeasureTheory.Integrable f (μ.bind ⇑κ) ↔
      (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable f (κ x)) ∧ MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f y‖ ∂κ x) μ)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The restriction of a presheafed space along an open embedding into the space.
 -/
AlgebraicGeometry.PresheafedSpace.restrict : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {U : TopCat} →
      (X : AlgebraicGeometry.PresheafedSpace C) →
        {f : U ⟶ ↑X} →
          Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → AlgebraicGeometry.PresheafedSpace C
-- Mathlib.Algebra.Order.Sub.Defs
tsub_right_comm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  a - b - c = a - c - b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.cast : {aig1 aig2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  Std.Tactic.BVDecide.BVExpr.Cache aig1 → aig1.decls.size ≤ aig2.decls.size → Std.Tactic.BVDecide.BVExpr.Cache aig2
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.eq_4 : ∀ (motive : Turing.PartrecToTM2.Cont' → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k))
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive k.cons₂)
  (h_3 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k))
  (h_5 : Unit → motive Turing.PartrecToTM2.Cont'.halt),
  (match Turing.PartrecToTM2.Cont'.fix f k with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k => h_1 fs k
    | k.cons₂ => h_2 k
    | Turing.PartrecToTM2.Cont'.comp f k => h_3 f k
    | Turing.PartrecToTM2.Cont'.fix f k => h_4 f k
    | Turing.PartrecToTM2.Cont'.halt => h_5 ()) =
    h_4 f k
-- Mathlib.Order.Lattice
lt_sup_of_lt_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c < b → c < a ⊔ b
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α}, s.Nonempty → (a • s).Nonempty
-- Mathlib.Topology.Order.Priestley
exists_isClopen_lower_of_not_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [PriestleySpace α] {x y : α},
  ¬x ≤ y → ∃ U, IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ y ∈ U