mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_sin_neg_pi_div_two : Filter.Tendsto Real.sin (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhds (-1))
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_one_substInvOfIsUnit : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) (hP' : IsUnit ((PowerSeries.coeff 1) P)),
  (PowerSeries.coeff 1) (P.substInvOfIsUnit hP') = ↑hP'.unit⁻¹
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.const_comp : ∀ (x : SimplexCategory) {y z : SimplexCategory} (f : y ⟶ z) (i : Fin (y.len + 1)),
  CategoryTheory.CategoryStruct.comp (x.const y i) f = x.const z ((SimplexCategory.Hom.toOrderHom f) i)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv
      (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) =
    CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i
-- Std.Data.DTreeMap.Internal.Def
/-- (Implementation detail)  -/
Std.DTreeMap.Internal.Impl.inner : {α : Type u} →
  {β : α → Type v} →
    ℕ → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier : Lean.Lsp.FileSource Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {x y : D₁.Hom D₂},
  x = y ↔ x.hom = y.hom
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The intersection between the fundamental cone and the `idealLattice` defined by the image of
the integral ideal `J`.  -/
NumberField.mixedEmbedding.fundamentalCone.idealSet : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Right multiplication of a column stochastic matrix by a non-negative vector
gives a non-negative vector.  -/
Matrix.nonneg_mulVec_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.colStochastic R n → (∀ (i : n), 0 ≤ x i) → ∀ (j : n), 0 ≤ M.mulVec x j
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.continuous_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → ∀ {e₁ : E}, Continuous fun e₂ => f (e₁, e₂)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  (toLatticeHom : LatticeHom α β) (map_top' : toLatticeHom.toFun ⊤ = ⊤)
  (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b)
  (toLatticeHom_1 : LatticeHom α β) (map_top'_1 : toLatticeHom_1.toFun ⊤ = ⊤)
  (map_sdiff'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a \ b) = toLatticeHom_1.toFun a \ toLatticeHom_1.toFun b),
  ({ toLatticeHom := toLatticeHom, map_top' := map_top', map_sdiff' := map_sdiff' } =
      { toLatticeHom := toLatticeHom_1, map_top' := map_top'_1, map_sdiff' := map_sdiff'_1 }) =
    (toLatticeHom = toLatticeHom_1)
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-open right-closed.

The type of the resulting slices is `γ`.
 -/
Std.Roc.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Algebra.Order.Monoid.Units
Units.orderEmbeddingVal.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α],
  Units.orderEmbeddingVal = { toFun := Units.val, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The direct map in `rTensor.equiv`  -/
rTensor.toFun : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  TensorProduct R N Q ⧸ (LinearMap.rTensor Q f).range →ₗ[R] TensorProduct R P Q
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.toBotHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β), f.toBotHom = { toFun := f.toFun, map_bot' := ⋯ }
-- Init.Omega.Constraint
/-- Normalize a constraint, by dividing through by the GCD.  -/
Lean.Omega.normalize : Lean.Omega.Constraint × Lean.Omega.Coeffs → Lean.Omega.Constraint × Lean.Omega.Coeffs
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instHashableDecl : {α : Type} → [Hashable α] → Hashable (Std.Sat.AIG.Decl α)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (p₁ p₂ : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a b p₁ p₂) = 1 + sizeOf a + sizeOf b + sizeOf p₁ + sizeOf p₂
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- `Irreducible p` states that `p` is non-unit and only factors into units.

We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
monoid allows us to reuse irreducible for associated elements. 

[Wikidata Q2989575](https://www.wikidata.org/wiki/Q2989575) -/
Irreducible : {M : Type u_1} → [Monoid M] → M → Prop
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.exportedConstInfo : Lean.Environment.ConstPromiseVal✝ → Lean.ConstantInfo
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.keys_eq_nil_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys = [] ↔ t = ∅
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- Turn a perfect pairing between `M` and `N` into an isomorphism between `M` and the dual of `N`.
 -/
LinearMap.toPerfPair : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_5} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup N] →
          [inst_2 : CommRing R] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → (p : M →ₗ[R] N →ₗ[R] R) → [p.IsPerfPair] → M ≃ₗ[R] Module.Dual R N
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- **Alias** of `Set.iUnion_vadd_eq_ofPred_exists`. -/
Set.iUnion_vadd_eq_setOf_exists : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β},
  ⋃ g, g +ᵥ s = {a | ∃ g, g +ᵥ a ∈ s}
-- Mathlib.LinearAlgebra.Projection
Submodule.projection.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (hpq : IsCompl p q), p.projection q hpq = p.subtype ∘ₗ p.projectionOnto q hpq
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.eqToHom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X = Y) (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eqToHom f) Z = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Group.Action.Defs
AddDistribAddAction.ext : ∀ {M : Type u_9} {N : Type u_10} {inst : AddMonoid M} {inst_1 : AddMonoid N} {x y : AddDistribAddAction M N},
  VAdd.vadd = VAdd.vadd → x = y
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- The change of charts from `e` to `e'` in the model vector space `E`.  -/
ModelWithCorners.extendCoordChange : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {M : Type u_3} →
      {H : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : TopologicalSpace H] →
                [inst_4 : TopologicalSpace M] →
                  {I : ModelWithCorners 𝕜 E H} →
                    OpenPartialHomeomorph M H → OpenPartialHomeomorph M H → PartialEquiv E E
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- Tensor products distribute over a direct sum on the left .  -/
TensorProduct.directSumLeft : (R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₁ : Type v₁} →
            [DecidableEq ι₁] →
              (M₁ : ι₁ → Type w₁) →
                (M₂' : Type w₂') →
                  [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] →
                    [inst_5 : AddCommMonoid M₂'] →
                      [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] →
                        [inst_7 : Module R M₂'] →
                          [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] →
                            [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] →
                              TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) M₂' ≃ₗ[S]
                                DirectSum ι₁ fun i => TensorProduct R (M₁ i) M₂'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k fallback : α},
  t.WF → (Std.TreeMap.Raw.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.Tactic.Ring.Basic
/-- `CSLiftVal a b` means that `b = lift a`. This is used by `ring` to construct an expression `b`
from the input expression `a`, and then run the usual ring algorithm on `b`.  -/
Mathlib.Tactic.Ring.CSLiftVal : {α : Type u} → {β : outParam (Type u)} → [Mathlib.Tactic.Ring.CSLift α β] → α → outParam β → Prop
-- Mathlib.Data.List.Lattice
List.Nodup.bagInter_left : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₂.Nodup → (l₁.bagInter l₂).Nodup
-- Mathlib.Order.Heyting.Regular
Heyting.isRegular_of_boolean : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a : α), Heyting.IsRegular a
-- Mathlib.RingTheory.RingHom.Bijective
RingHom.Bijective.ofLocalizationSpan : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  (R : CategoryTheory.Presieve S), R ∈ J.toPrecoverage.coverings S ↔ CategoryTheory.Sieve.generate R ∈ J S
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Quote `e` using `「` and `」` if `e` is an arithmetic term that is being treated as a variable.  -/
Lean.Meta.Grind.Arith.quoteIfArithTerm : Lean.Expr → Lean.MessageData
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.mk.sizeOf_spec : ∀ (usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap) (modified : Bool),
  sizeOf { usedFVarsMap := usedFVarsMap, modified := modified } = 1 + sizeOf usedFVarsMap + sizeOf modified
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.termμ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaCurry_zero : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)], DFinsupp.sigmaCurry 0 = 0
-- Mathlib.Topology.CompactOpen
ContinuousMap.compRightContinuousMap_apply : ∀ {X : Type u_2} {Y : Type u_3} (Z : Type u_4) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)), (ContinuousMap.compRightContinuousMap Z f) g = g.comp f
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.le.injEq : ∀ (n n_1 : ℤ), (Mathlib.Tactic.IntervalCases.Bound.le n = Mathlib.Tactic.IntervalCases.Bound.le n_1) = (n = n_1)
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Ric.Sliceable.mkSlice xs *...=hi).stop = min (hi + 1) xs.size
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue : Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter)
  Lean.PrettyPrinter.Formatter.FormatterAliasValue
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- the isomorphism `F.obj ⊥ ≅ X`  -/
CategoryTheory.TransfiniteCompositionOfShape.isoBot : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (self : CategoryTheory.TransfiniteCompositionOfShape J f) → self.F.obj ⊥ ≅ X
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_spanning_iff : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : IsDomain A] {s : Set A},
  (AlgebraicIndependent.matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A
-- Mathlib.Analysis.CStarAlgebra.Unitization
/-- This is the key lemma used to establish the instance `Unitization.instCStarRing`
(i.e., proving that the norm on `Unitization 𝕜 E` satisfies the C⋆-property). We split this one
out so that declaring the `CStarRing` instance doesn't time out.  -/
Unitization.norm_splitMul_snd_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : DenselyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E] [inst_2 : StarRing E]
  [CStarRing E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E] [inst_6 : SMulCommClass 𝕜 E E]
  [inst_7 : StarRing 𝕜] [StarModule 𝕜 E] (x : Unitization 𝕜 E),
  ‖((Unitization.splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((Unitization.splitMul 𝕜 E) (star x * x)).2‖
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Ioo : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Ioo i j = Set.Ioo (Fin.castLE h i) (Fin.castLE h j)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- An `α`-coloring of a simple graph `G` is a homomorphism of `G` into the complete graph on `α`.
This is also known as a proper coloring.
 -/
SimpleGraph.Coloring : {V : Type u} → SimpleGraph V → Type v → Type (max u v)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Tagged prepartition with single box and prescribed tag.  -/
BoxIntegral.TaggedPrepartition.single : {ι : Type u_1} →
  (I J : BoxIntegral.Box ι) → J ≤ I → (x : ι → ℝ) → x ∈ BoxIntegral.Box.Icc I → BoxIntegral.TaggedPrepartition I
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- The exponential series as an `ofScalars` series.  -/
NormedSpace.expSeries_eq_ofScalars : ∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸],
  NormedSpace.expSeries 𝕂 𝔸 = FormalMultilinearSeries.ofScalars 𝔸 fun n => (↑n.factorial)⁻¹
-- Mathlib.RingTheory.PowerSeries.Order
/-- **Alias** of `PowerSeries.le_order_mul`.

---

The order of the product of two formal power series
is at least the sum of their orders.  -/
PowerSeries.order_mul_ge : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order + ψ.order ≤ (φ * ψ).order
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.hom = sq.f₃₄
-- Mathlib.Algebra.Order.Monoid.Units
/-- `val : αˣ → α` as an order embedding.  -/
Units.orderEmbeddingVal : {α : Type u_1} → [inst : Monoid α] → [inst_1 : LinearOrder α] → αˣ ↪o α
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (x : Fin n → K),
  Height.mulHeight (Matrix.vecCons 0 x) = Height.mulHeight x
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.ext_iff : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  {x y : e₀₁.CompStruct e₁₂ e₀₂}, x = y ↔ x.simplex = y.simplex
-- Mathlib.GroupTheory.Perm.List
List.formPerm_append_pair : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a b : α),
  (l ++ [a, b]).formPerm = (l ++ [a]).formPerm * Equiv.swap a b
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- The inclusion map from `F(S)` into `∫ᶜ F`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.ι : {𝒮 : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) →
      (S : 𝒮) → CategoryTheory.Functor (↑(F.obj { as := Opposite.op S })) F.CoGrothendieck
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiable_sinh : Differentiable ℝ Real.sinh
-- Mathlib.Algebra.Order.IsBotOne
le_one_iff_eq_one : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≤ 1 ↔ a = 1
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.toZModHom.eq_1 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (v : ℕ) (f : ℤ_[p] → ℕ) (f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v})
  (f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b),
  PadicInt.toZModHom v f f_spec f_congr =
    { toFun := fun x => ↑(f x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  ⇑U.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s = Subtype.val ⁻¹' X.zeroLocus s
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R), (γ.smul a).φH = a • γ.φH
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α}, (Std.DTreeMap.Raw.ofList l cmp).contains k = (List.map Sigma.fst l).contains k
-- Mathlib.Algebra.Lie.Weights.Killing
/-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
Killing form, the corresponding roots span the dual space of `H`.  -/
LieAlgebra.IsKilling.span_weight_eq_top : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L],
  Submodule.span K (Set.range (LieModule.Weight.toLinear K (↥H) L)) = ⊤
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counit_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f))
      (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) =
    CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Probability.Kernel.Deterministic
/-- The equation of a Positive Markov category: if the composition of two Markov kernels `η ∘ₖ κ` is
deterministic, the distribution over both `η ∘ₖ κ` and `κ` can be obtained by computing `η ∘ₖ κ`
and `κ` independently.  -/
ProbabilityTheory.Kernel.comp_parallelComp_comp_copy : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3}
  [inst : MeasurableSpace γ] {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ}
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η]
  [ProbabilityTheory.IsDeterministic (η.comp κ)],
  ((η.comp κ).parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) =
    ((η.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.copy β)).comp κ
-- Mathlib.LinearAlgebra.Dual.BaseChange
/-- The base change of an element of the dual.  -/
IsBaseChange.toDual : {R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommMonoid W] →
              [inst_4 : Module R W] →
                {A : Type u_4} →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Module A W] →
                        [inst_8 : IsScalarTower R A W] →
                          {j : V →ₗ[R] W} → IsBaseChange A j → Module.Dual R V →ₗ[R] Module.Dual A W
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A typeclass describing the property that forming all explicit pullbacks is stable under the
property `P`.
 -/
CompHausLike.HasExplicitPullbacks : (TopCat → Prop) → Prop
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atTop`.  -/
Filter.Tendsto.atBot_mul_neg : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  C < 0 →
    Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop