mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode_eq : Denumerable.ofNat Nat.Partrec.Code = Nat.Partrec.Code.ofNatCode
-- Mathlib.Data.EReal.Operations
EReal.neg_eq_bot_iff : ∀ {x : EReal}, -x = ⊥ ↔ x = ⊤
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_zero_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R), MvPolynomial.coeff 0 (MvPolynomial.C a) = a
-- Mathlib.Topology.Inseparable
SeparationQuotient.isQuotientMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsQuotientMap SeparationQuotient.mk
-- Mathlib.Order.Minimal
OrderIso.map_maximal_mem : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t)
  (hx : Maximal (fun x => x ∈ s) x), Maximal (fun x => x ∈ t) ↑(f ⟨x, ⋯⟩)
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_smul : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] (c : M) (x y : X),
  nndist (c • x) (c • y) = nndist x y
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd₂.toMeasurableAdd : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Add M] [MeasurableAdd₂ M], MeasurableAdd M
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The matrix that gives the representation on `stdBasis` of the image by `commMap` of an
element `x` of `(K →+* ℂ) → ℂ` fixed by the map `x_φ ↦ conj x_(conjugate φ)`,
see `stdBasis_repr_eq_matrixToStdBasis_mul`.  -/
NumberField.mixedEmbedding.matrixToStdBasis : (K : Type u_1) → [inst : Field K] → Matrix (NumberField.mixedEmbedding.index K) (NumberField.mixedEmbedding.index K) ℂ
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_1 : PosNum.one.testBit 0 = true
-- Mathlib.Analysis.Calculus.MeanValue
/-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
bounded by `C` satisfies `‖f x - f a‖ ≤ C * (x - a)`, `derivWithin`
version.  -/
norm_image_sub_le_of_norm_deriv_le_segment : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C : ℝ},
  DifferentiableOn ℝ f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
-- Batteries.Data.List.Basic
List.swapAtTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (v : α) (a : ℕ) (a_1 : Array α), List.swapAtTR.go l v [] a a_1 = (v, l)
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function `g` is strongly measurable with respect to the pullback along some function `f`,
then to prove `g x = g y` it is enough to prove `f x = f y`.

If `Z` is not empty there exists `h : Y → Z` such that `g = h ∘ f`.
If `Z` is also completely metrizable, the factorization map `h` can be taken to be measurable
(see `exists_eq_measurable_comp`).  -/
MeasureTheory.StronglyMeasurable.factorsThrough : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z}
  [inst : TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z],
  MeasureTheory.StronglyMeasurable g → Function.FactorsThrough g f
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
RingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ⇑f → α →+* β
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_mem : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] [WellFoundedLT α] [Nonempty ι] (f : ι → α),
  iInf f ∈ Set.range f
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities.mk.inj : ∀ {completionItem? completionItem?_1 : Option Lean.Lsp.CompletionItemCapabilities},
  { completionItem? := completionItem? } = { completionItem? := completionItem?_1 } →
    completionItem? = completionItem?_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.TreeMap.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.ext' : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M}, (∀ (x : M), x ∈ s₁ ↔ x ∈ s₂) → s₁ = s₂
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.toList_copy_take : ∀ {s : String.Slice} {n : ℕ}, (s.take n).copy.toList = List.take n s.copy.toList
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_le_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.limsSup_le_of_le._auto_1 →
    (∀ᶠ (n : α) in f, n ≤ a) → f.limsSup ≤ a
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.intersecting_iff_pairwise_not_disjoint : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α},
  s.Intersecting ↔ (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
-- Mathlib.Algebra.Ring.Parity
/-- **Alias** of `Nat.Odd.sub_odd`. -/
Odd.tsub_odd : ∀ {m n : ℕ}, Odd m → Odd n → Even (m - n)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_sdiff : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f s μ →
      t ⊆ s → ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
-- Mathlib.Data.Real.ConjExponents
NNReal.holderConjugate_one_div : ∀ {a b : NNReal}, 0 < a → 0 < b → a + b = 1 → (1 / a).HolderConjugate (1 / b)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_1 ()
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`.  -/
hasProd_prod_support_of_ne_finset_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {s : Finset β},
  (∀ b ∈ L.support, b ∉ s → f b = 1) →
    ∀ [L.HasSupport] [inst_3 : DecidablePred fun x => x ∈ L.support], HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map : ∀ {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂}
  [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (x x_1 : C),
  (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map x x_1 = TypeCat.ofHom fun f => F.map f
-- Mathlib.Algebra.Algebra.Operations
Submodule.span_singleton_eq_one_iff : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  {x : A}, R ∙ x = 1 ↔ ∃ r, x = (algebraMap R A) ↑r
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ m₂ m₁₂ : ℤ) (h₁₂ : n₁₂ + 1 = m₁₂)
  (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂),
  CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) =
    z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The effect of a stack action on the local variables, given the value of the stack.  -/
Turing.TM2to1.stVar : {K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → σ → List (Γ k) → Turing.TM2to1.StAct K Γ σ k → σ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_eq_zero : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, Metric.externalCoveringNumber ε A = 0 ↔ A = ∅
-- Mathlib.Algebra.Torsor.Defs
/-- If dividing two points produces 1, they are equal.  -/
eq_of_sdiv_eq_one : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ : P}, p₁ /ₛ p₂ = 1 → p₁ = p₂
-- Init.Data.List.Perm
List.perm_nil : ∀ {α : Type u_1} {l₁ : List α}, l₁.Perm [] ↔ l₁ = []
-- Mathlib.Algebra.Module.Torsion.Basic
/-- In a `p ^ ∞`-torsion module (that is, a module where all elements are cancelled by scalar
multiplication by some power of `p`), the smallest `n` such that `p ^ n • x = 0`.  -/
Submodule.pOrder : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : DistribMulAction R M] →
          {p : R} → Module.IsTorsion' M ↥(Submonoid.powers p) → (x : M) → [(n : ℕ) → Decidable (p ^ n • x = 0)] → ℕ
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_singleton_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Submodule.torsionBySet R M {a} = Submodule.torsionBy R M a
-- Mathlib.Topology.Algebra.GroupCompletion
/-- The map from a group to its completion as a group hom.  -/
UniformSpace.Completion.toCompl : {α : Type u_3} →
  [inst : UniformSpace α] → [inst_1 : AddGroup α] → [inst_2 : IsUniformAddGroup α] → α →+ UniformSpace.Completion α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 2 → H) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 2)) x) =
    ((Rep.Hom.hom φ).compLeft (G × G))
      ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f))
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).hom) x))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Control.Monad.Cont
MonadCont.Label : Type w → (Type u → Type v) → Type u → Type (max v w)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.digamma_zero : Complex.digamma 0 = 0
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.ext_iff : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {f g : SlashInvariantForm Γ k},
  f = g ↔ ∀ (x : UpperHalfPlane), f x = g x
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctor_op_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {K L : Cᵒᵖ}
  (φ : K ⟶ L) (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.shiftFunctor_op_map._auto_1),
  (CategoryTheory.shiftFunctor Cᵒᵖ n).map φ =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m).map φ.unop).op
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app L))
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map.eq_1 : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.map f = Polynomial.eval₂ (Polynomial.C.comp f) Polynomial.X
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.addCompletionInfo : Lean.Elab.ConfigEval.ConfigItem → Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSMulSubtypeMem : {R : Type u} → {M : Type v} → [inst : SMul R M] → (p : SubMulAction R M) → SMul R ↥p
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.hasExactColimitsOfShape_discrete_finite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] (J : Type u_1) [inst_3 : Finite J],
  CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv Y)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv) h
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddZeroClass` across an `Equiv`  -/
Equiv.addZeroClass : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddZeroClass β] → AddZeroClass α
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` is closed under addition.  -/
AddSubgroup.add_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → y ∈ H → x + y ∈ H
-- Mathlib.Data.Quot
/-- The `bind` operator for the `Trunc` monad.  -/
Trunc.bind : {α : Sort u_1} → {β : Sort u_2} → Trunc α → (α → Trunc β) → Trunc β
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_surjective : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  Function.Surjective ⇑f → (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank B
-- Mathlib.Analysis.Convex.Between
wbtw_const_sub_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R (v - x) (v - y) (v - z) ↔ Wbtw R x y z
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
contMDiffAt_inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] [ContMDiffInv₀ I n G]
  {x : G}, x ≠ 0 → ContMDiffAt I I n (fun y => y⁻¹) x
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (ρ : MeasureTheory.Measure (α × β)), ρ.fst = MeasureTheory.Measure.map Prod.fst ρ
-- Mathlib.CategoryTheory.Functor.Currying
/-- The uncurrying of `F.flip` is isomorphic to
swapping the factors followed by the uncurrying of `F`.  -/
CategoryTheory.Functor.uncurryObjFlip : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) →
              CategoryTheory.Functor.uncurry.obj F.flip ≅
                (CategoryTheory.Prod.swap D C).comp (CategoryTheory.Functor.uncurry.obj F)
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
CategoryTheory.instPreservesFiniteLimitsHomologicalComplexMapHomologicalComplexOfHasFiniteLimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_5 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteLimits (F.mapHomologicalComplex c)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal),
  f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given a category `C` that has a coseparator (`HasCoseparator C`), `coseparator C` is an arbitrarily
chosen coseparator of `C`.
 -/
CategoryTheory.coseparator : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.HasCoseparator C] → C
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_iSup_map_of_injective : ∀ {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] {ι : Type u_5} {f : F},
  Function.Injective ⇑f → ∀ (S : ι → Submonoid M), Submonoid.comap f (⨆ i, Submonoid.map f (S i)) = iSup S
-- Std.Http.Protocol.H1.Error
/-- Invalid or malformed header.
 -/
Std.Http.Protocol.H1.Error.invalidHeader : Std.Http.Protocol.H1.Error
-- Mathlib.Algebra.Order.Group.End
RelHom.one_def : ∀ {α : Type u_1} {r : α → α → Prop}, 1 = RelHom.id r
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories which preserves kernels preserves that an
arbitrary binary fan is a limit.
 -/
CategoryTheory.Functor.isLimitMapConeBinaryFanOfPreservesKernels : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  (π₁ : Z ⟶ X) →
                    (π₂ : Z ⟶ Y) →
                      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair π₂ 0) F] →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk π₁ π₂) →
                          CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.BinaryFan.mk π₁ π₂))
-- Lean.Meta.Basic
Lean.Meta.Diagnostics.mk.sizeOf_spec : ∀ (unfoldCounter unfoldAxiomCounter heuristicCounter instanceCounter : Lean.PHashMap Lean.Name ℕ)
  (synthPendingFailures : Lean.PHashMap Lean.Expr Lean.MessageData),
  sizeOf
      { unfoldCounter := unfoldCounter, unfoldAxiomCounter := unfoldAxiomCounter, heuristicCounter := heuristicCounter,
        instanceCounter := instanceCounter, synthPendingFailures := synthPendingFailures } =
    1 + sizeOf unfoldCounter + sizeOf unfoldAxiomCounter + sizeOf heuristicCounter + sizeOf instanceCounter +
      sizeOf synthPendingFailures
-- Lean.Parser.Command
Lean.Parser.Command.axiom : Lean.Parser.Parser
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalTermAbelMode : Lean.Elab.ConfigEval.EvalTerm Mathlib.Tactic.Abel.AbelMode
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.leadingCoeff_pos_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : LinearOrder R]
  {x : Lex (HahnSeries Γ R)}, 0 < (ofLex x).leadingCoeff ↔ 0 < x
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTraceMessage : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsRightCancelMul.mulRightStrictMono_of_mulRightMono : ∀ (N : Type u_2) [inst : Mul N] [IsRightCancelMul N] [inst_2 : PartialOrder N] [MulRightMono N], MulRightStrictMono N
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefViewElabHeaderData : Inhabited Lean.Elab.DefViewElabHeaderData
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.instTotallyDisconnectedSpaceCarrierToTop : ∀ {X : Profinite}, TotallyDisconnectedSpace ↑X.toTop
-- Init.Data.Int.ToString
_private.Init.Data.Int.ToString.0.Int.repr.eq_1 : ∀ (m : ℕ), (Int.ofNat m).repr = m.repr
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a + b).imJ = a.imJ + b.imJ
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.mk : Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.Context✝
-- Mathlib.LinearAlgebra.Matrix.WithConv
instMulWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Mul α] → Mul (WithConv (Matrix m n α))
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.empty : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  MonovaryOn f g ∅
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Array.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Lean.Util.Diff
Lean.Diff.instReprAction : Repr Lean.Diff.Action
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The inclusion of the bounded below derived category.  -/
DerivedCategory.Plus.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (DerivedCategory.Plus C) (DerivedCategory C)
-- Mathlib.RingTheory.LocalRing.LocalSubring
isLocalRing_top : ∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R], IsLocalRing ↥⊤
-- Init.Data.Order.MinMaxOn
minOn_eq_left : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x y : α},
  f x ≤ f y → minOn f x y = x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_leftUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (self.mapComp (CategoryTheory.CategoryStruct.id a) f))
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_orthogonal_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E), U ⟂ Uᗮ
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_freeOn : ∀ {α : Type u_1} {X Y : Set α}, X ⊆ Y → (Matroid.freeOn Y).eRk X = X.encard
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.toList_uLift : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [inst_2 : Monad n] {it : Std.IterM m β} [inst_3 : MonadLiftT m (Std.Iterators.ULiftT n)]
  [Std.Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).toList = (fun l => List.map ULift.up l.down) <$> (monadLift it.toList).run
-- Std.Http.Internal.Char
Std.Http.Internal.Char.qdtext.eq_3 : Std.Http.Internal.Char.qdtext '!' = (true || decide ('#' ≤ '!' ∧ '!' ≤ '[') || decide (']' ≤ '!' ∧ '!' ≤ '~'))
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : PredOrder α] (a : α), Order.pred a = ⨆ b, ⨆ (_ : a > b), b