mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- Let `I` be a fractional ideal of `K`. Assume that `B : ℝ` is such that
`minkowskiBound K I < volume (convexBodySum K B)` where `convexBodySum K B` is the set of points
`x` such that `∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B` (see `convexBodySum_volume` for
the computation of this volume), then there exists a nonzero algebraic number `a` in `I` such
that `|Norm a| < (B / d) ^ d` where `d` is the degree of `K`.  -/
NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) {B : ℝ},
  NumberField.mixedEmbedding.minkowskiBound K I ≤ MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) →
    ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(Module.finrank ℚ K)) ^ Module.finrank ℚ K
-- Std.Data.ExtDHashMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.ExtDHashMap.insert : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → (a : α) → β a → Std.ExtDHashMap α β
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Measurability of the action of the additive topological group `G` on the
left-coset space `G / Γ`.  -/
QuotientAddGroup.measurableVAdd : ∀ {G : Type u_1} [inst : AddGroup G] {Γ : AddSubgroup G} [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [BorelSpace (G ⧸ Γ)], MeasurableVAdd G (G ⧸ Γ)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- The support of an element of the field of fractions of a Dedekind domain
is finite.
 -/
IsDedekindDomain.HeightOneSpectrum.Support.finite : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (k : K), (IsDedekindDomain.HeightOneSpectrum.Support R k).Finite
-- Init.Prelude
Nat.add_pos_right : ∀ {b : ℕ} (a : ℕ), 0 < b → 0 < a + b
-- Batteries.Data.List.Basic
/-- Left-biased version of `List.zipWith`. `zipWithLeft f as bs` applies `f` to each pair
`aᵢ ∈ as` and `bᵢ ‌∈ bs`. If `bs` is shorter than `as`, `f` is applied to `none`
for the remaining `aᵢ`.
```
zipWithLeft prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipWithLeft prod.mk [1] ['a', 'b'] = [(1, some 'a')]
zipWithLeft f as bs = (zipWithLeft' f as bs).fst
```
 -/
List.zipWithLeft : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.of_subsingleton : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [Subsingleton E] [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.IsGaussian μ
-- Lean.Compiler.IR.Format
Lean.IR.formatArray : {α : Type} → [Std.ToFormat α] → Array α → Std.Format
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.views : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Elab.Command.InductiveView
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.instIsUniformAddGroup : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : WithIdeal R], IsUniformAddGroup R
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
_private.Lean.Meta.Tactic.Grind.EMatchTheoremParam.0.Lean.Meta.Grind.globalDeclToGrindLemmaSyntax : Lean.Name →
  Lean.Meta.Grind.EMatchTheoremKind →
    Bool → Lean.MetaM (Lean.TSyntax [`Lean.Parser.Tactic.grindLemma, `Lean.Parser.Tactic.grindLemmaMin])
-- Mathlib.CategoryTheory.Functor.Category
/-- The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
 -/
CategoryTheory.Functor.rightUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → F.comp (CategoryTheory.Functor.id D) ≅ F
-- Mathlib.FieldTheory.SeparableClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same
separable degree over `F`.  -/
Field.lift_sepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K),
  Cardinal.lift.{w, v} (Field.sepDegree F E) = Cardinal.lift.{v, w} (Field.sepDegree F K)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M},
  ContMDiffOn I I' (↑⊤) f s ↔ ∀ (n : ℕ), ContMDiffOn I I' (↑n) f s
-- Mathlib.Condensed.Discrete.Basic
LightCondensed.discrete_obj : ∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  [inst_1 : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] (X : C),
  (LightCondensed.discrete C).obj X =
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).obj
      ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).obj X)
-- Std.Data.HashMap.RawLemmas
_private.Std.Data.HashMap.RawLemmas.0.Std.HashMap.Raw.ext : ∀ {α : Type u} {β : Type v} {m m' : Std.HashMap.Raw α β}, m.inner = m'.inner → m = m'
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.isPartition_splitCenter : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι), (BoxIntegral.Prepartition.splitCenter I).IsPartition
-- Mathlib.Algebra.Group.Pi.Basic
Pi.monoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Monoid (f i)],
  Pi.monoid =
    { toSemigroup := Pi.semigroup, toOne := Pi.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n x i => x i ^ n, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation and is right-continuous at a point, then the variation on
small closed intervals to the right of this point tends to `0`.  -/
BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    ∀ (x : α),
      ContinuousWithinAt f (s ∩ Set.Ici x) x →
        Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc x y)) (nhdsWithin x s) (nhds 0)
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (K L : CochainComplex C ℤ)
  (n : ℤ)
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [K.IsKProjective], Function.Bijective CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.MorphismProperty.LeftFraction₂.map_add : ∀ {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.Preadditive C]
  {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) (F : CategoryTheory.Functor C D)
  (hF : W.IsInvertedBy F) [inst_3 : CategoryTheory.Preadditive D] [F.Additive],
  φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF
-- Batteries.Data.String.Lemmas
String.takeWhileAux_of_valid : ∀ (p : Char → Bool) (l m r : List Char),
  Substring.Raw.takeWhileAux (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l + String.utf8Len m } p
      { byteIdx := String.utf8Len l } =
    { byteIdx := String.utf8Len l + String.utf8Len (List.takeWhile p m) }
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M'),
  b.prod b' = { repr := b.repr.prodCongr b'.repr ≪≫ₗ (Finsupp.sumFinsuppLEquivProdFinsupp R).symm }
-- Mathlib.Topology.Separation.Regular
Topology.IsEmbedding.t3Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T3Space Y] {f : X → Y},
  Topology.IsEmbedding f → T3Space X
-- Mathlib.Data.Multiset.Filter
Multiset.count_filter_of_pos : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] {a : α} {s : Multiset α},
  p a → Multiset.count a (Multiset.filter p s) = Multiset.count a s
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.coe_op : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R), ↑S.op = MulOpposite.unop ⁻¹' ↑S
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.toHomeomorph_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsEmbedding f) (a : X), ↑(hf.toHomeomorph a) = f a
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} [inst_2 : SizeOf C] (f₀ : S₁.L₀ ⟶ S₂.L₀) (f₁ : S₁.L₁ ⟶ S₂.L₁)
  (f₂ : S₁.L₂ ⟶ S₂.L₂) (f₃ : S₁.L₃ ⟶ S₂.L₃)
  (comm₀₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam),
  sizeOf { f₀ := f₀, f₁ := f₁, f₂ := f₂, f₃ := f₃, comm₀₁ := comm₀₁, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
    1 + sizeOf f₀ + sizeOf f₁ + sizeOf f₂ + sizeOf f₃ + sizeOf comm₀₁ + sizeOf comm₁₂ + sizeOf comm₂₃
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The exchange of the two fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction₂.symm : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → W.LeftFraction₂ X Y
-- Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
/-- The underlying category of the `Cat`-enriched ordinary category of quasicategories is
equivalent to `QCat`.  -/
SSet.QCat.forgetEnrichment.equiv : CategoryTheory.ForgetEnrichment CategoryTheory.Cat SSet.QCat ≌ SSet.QCat
-- Mathlib.Data.WSeq.Defs
/-- Returns `true` if any element of `s` satisfies `p`  -/
Stream'.WSeq.any : {α : Type u} → Stream'.WSeq α → (α → Bool) → Computation Bool
-- Lean.Declaration
Lean.ConstantInfo.name : Lean.ConstantInfo → Lean.Name
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.le_mul_inv_iff`. -/
Units.le_mul_inv_of_mul_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a * ↑u ≤ b → a ≤ b * ↑u⁻¹
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst._auto_3)
  {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f' g')
      (CategoryTheory.CategoryStruct.comp γ₁ h)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.mkHomeomorph.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  DomMulAct.mkHomeomorph = { toEquiv := DomMulAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Std.Async.TCP
/-- Enables TCP keep-alive for all client sockets accepted by this server socket.
 -/
Std.Async.TCP.Socket.Server.keepAlive : Std.Async.TCP.Socket.Server →
  Bool →
    (delay : Std.Time.Second.Offset) → autoParam (delay.val ≥ 1) Std.Async.TCP.Socket.Server.keepAlive._auto_1 → IO Unit
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology : CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget LightProfinite)
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `A` induces a short exact sequence of
`G`-representations `0 ⟶ Ker(mk) ⟶ A ⟶ A_S ⟶ 0` where `mk` is the quotient map to the
`S`-coinvariants `A_S`.  -/
Rep.coinvariantsShortComplex : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        Rep.{w, u, v} k G → (S : Subgroup G) → [S.Normal] → CategoryTheory.ShortComplex (Rep.{w, u, v} k G)
-- Mathlib.Probability.Distributions.Binomial
_private.Mathlib.Probability.Distributions.Binomial.0.ProbabilityTheory.condVar_of_hasLaw_binomial : {Ω : Type u_2} →
  {m : MeasurableSpace Ω} →
    {n : ℕ} →
      {p : ↑unitInterval} →
        {X : Ω → ℝ} →
          {m₀ : MeasurableSpace Ω} →
            m ≤ m₀ →
              {P : MeasureTheory.Measure Ω} →
                ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) P →
                  ProofWanted (ProbabilityTheory.condVar m X P =ᵐ[P] P[X | m] * P[1 - X | m])
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.getEqDefDecl? : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instInhabited : (α : Type u_2) → [inst : Min α] → [inst_1 : Top α] → Inhabited (InfTopHom α α)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Sets of subtype are σ-compact iff the image under a coercion is.  -/
Subtype.isSigmaCompact_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { a // p a }},
  IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' s)
-- Mathlib.Tactic.NormNum.BigOperators
/-- Either show the expression `s : Q(Finset α)` is empty, or remove one element from it.

Fails if we cannot determine which of the alternatives apply to the expression.
 -/
Mathlib.Meta.Finset.proveEmptyOrCons : {u : Lean.Level} → {α : Q(Type u)} → (s : Q(Finset «$α»)) → Lean.MetaM (Mathlib.Meta.Finset.ProveEmptyOrConsResult s)
-- Lean.Meta.Tactic.Simp.Types
/-- Local declarations to propagate to `Meta.Context`  -/
Lean.Meta.Simp.Context.zetaDeltaSet : Lean.Meta.Simp.Context → Lean.FVarIdSet
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonneg : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → ℝ} {a b : ℝ} {g : ℝ → F},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, 0 ≤ f' x) →
        a ≤ b → ∫ (x : ℝ) in Set.Icc a b, f' x • g (f x) = ∫ (u : ℝ) in Set.Icc (f a) (f b), g u
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsBigOEventuallyEq : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] →
          {l : Filter α} → Trans (fun x1 x2 => x1 =O[l] x2) (fun x1 x2 => x1 =ᶠ[l] x2) fun x1 x2 => x1 =O[l] x2
-- Mathlib.Computability.DFA
DFA.eval.eq_1 : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.eval = M.evalFrom M.start
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ}, S.Exact → S.unop.Exact
-- Init.Data.Ord.Basic
Ordering.ne_eq_of_eq_gt : ∀ {o : Ordering}, o = Ordering.gt → o ≠ Ordering.eq
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.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₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} [inst_1 : SizeOf C] [inst_2 : SizeOf ι] (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalAddGroup.IsSES.isClosedEmbedding : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C},
  TopologicalAddGroup.IsSES φ ψ → Topology.IsClosedEmbedding ⇑φ
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inr_descShortComplex_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) {Z : CochainComplex C ℤ} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S) h) =
    CategoryTheory.CategoryStruct.comp S.g h
-- Lean.Data.NameTrie
Lean.instEmptyCollectionNameTrie : {β : Type u_1} → EmptyCollection (Lean.NameTrie β)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk_coe : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M)
  (h₁ : Function.LeftInverse f (↑e).toFun) (h₂ : Function.RightInverse f (↑e).toFun),
  { toLinearMap := ↑e, invFun := f, left_inv := h₁, right_inv := h₂ } = e
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.eta_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g), t.eta.inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey_eq_getKeyₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β)
  {h : Std.DTreeMap.Internal.Impl.contains k l = true} (h' : (l.getKey?ₘ k).isSome = true),
  l.getKey k h = l.getKeyₘ k h'
-- Mathlib.AlgebraicTopology.CechNerve
/-- The morphism between Čech nerves associated to a morphism of arrows.  -/
CategoryTheory.Arrow.mapCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] →
          (f ⟶ g) → (f.cechNerve ⟶ g.cechNerve)
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveLimit.measure_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)},
  MeasureTheory.IsProjectiveLimit μ P →
    ∀ (I : Finset ι) {s : Set ((i : ↥I) → α ↑i)}, MeasurableSet s → μ (MeasureTheory.cylinder I s) = (P I) s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The underlying seminormed abelian group.  -/
SemiNormedGrp₁.carrier : SemiNormedGrp₁ → Type u
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The forward direction of `Comon (Mon C) ≌ Mon (Comon C)`  -/
CategoryTheory.Bimon.toMonComon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.Bimon C) (CategoryTheory.Mon (CategoryTheory.Comon C))
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  p.copy hu hv = hu ▸ hv ▸ p
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- `spineToSimplex` is a left inverse to `spine X m`.  -/
SSet.Truncated.StrictSegal.spineToSimplex_spine : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (self : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1),
  self.spineToSimplex m ⋯ ∘ X.spine m h = id
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Function.Injective ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.instHAdd : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ ν : MeasureTheory.Measure α}
  [μ.InnerRegular] [ν.InnerRegular], (μ + ν).InnerRegular
-- Mathlib.Data.Int.Log
Int.clog_mono_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ} {r₁ r₂ : R}, 0 < r₁ → r₁ ≤ r₂ → Int.clog b r₁ ≤ Int.clog b r₂
-- Mathlib.Topology.Bases
/-- The product of a countable family of separable spaces is a separable space.  -/
TopologicalSpace.instSeparableSpaceForallOfCountable : ∀ {ι : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), TopologicalSpace.SeparableSpace (X i)] [Countable ι], TopologicalSpace.SeparableSpace ((i : ι) → X i)