mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.sup_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Max L]
  [ContinuousSup L],
  Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun i => f i ⊔ g i) l (nhds (x ⊔ y))
-- Batteries.Data.Fin.Coding
Fin.encodeSum.eq_2 : ∀ {n m : ℕ} (x_1 : Fin m), Fin.encodeSum (Sum.inr x_1) = Fin.natAdd n x_1
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.instCategoryStructSigma : {I : Type w₁} →
  {C : I → Type u₁} →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      CategoryTheory.CategoryStruct.{max (max u₁ w₁) v₁, max u₁ w₁} ((i : I) × C i)
-- Mathlib.Data.Set.Card
Set.ncard_exchange : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∉ s → b ∈ s → (insert a (s \ {b})).ncard = s.ncard
-- Init.Data.Nat.Basic
Nat.not_le : ∀ {a b : ℕ}, ¬a ≤ b ↔ b < a
-- Mathlib.Order.BoundedOrder.Basic
/-- `⊤` is the greatest element  -/
OrderTop.le_top : ∀ {α : Type u} {inst : LE α} [self : OrderTop α] (a : α), a ≤ ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) S.cokernelToAbelianCoimage =
    CategoryTheory.Abelian.coimage.π S.g
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNormedCommRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : NormedCommRing R] → NormedCommRing (BoundedContinuousFunction α R)
-- Mathlib.Probability.Kernel.Composition.Prod
/-- Product of two kernels. This is meaningful only when the kernels are s-finite.  -/
ProbabilityTheory.Kernel.prod : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α (β × γ)
-- Init.Data.String.Lemmas.Iterate
String.Model.mem_positionsFrom_startPos : ∀ {s : String} {q : { q // q ≠ s.endPos }}, q ∈ String.Model.positionsFrom s.startPos
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order.0.CFC.cfc_rpow_sub_one_eqOn : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : ℝ},
  Set.EqOn (fun a => if a ∈ {b | IsStrictlyPositive b} then cfc (fun x => p⁻¹ * (x ^ p - 1)) a else 0)
    (fun a => p⁻¹ • (a ^ p - 1)) {a | IsStrictlyPositive a}
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoPrefixPatternModel.eq_empty : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.NoPrefixPatternModel pat] (s t : String),
  String.Slice.Pattern.Model.PatternModel.Matches pat s →
    String.Slice.Pattern.Model.PatternModel.Matches pat (s ++ t) → t = ""
-- Mathlib.Order.Hom.Basic
/-- An order embedding is an embedding `f : α ↪ β` such that `a ≤ b ↔ (f a) ≤ (f b)`.
This definition is an abbreviation of `RelEmbedding (≤) (≤)`.  -/
OrderEmbedding : (α : Type u_6) → (β : Type u_7) → [LE α] → [LE β] → Type (max u_6 u_7)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.instWithGeneratedByTopology`. -/
deltaGeneratedSpace_deltaGenerated : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Topology.IsGeneratedBy X (Topology.WithGeneratedByTopology X Y)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ)
  (ll rr : List ((a : α) × β a))
  (hm_2 :
    Std.DTreeMap.Internal.Impl.contains' k l = true →
      Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = true),
  Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll Std.DTreeMap.Internal.Impl.leaf hm_2 rr =
    f ll Std.DTreeMap.Internal.Cell.empty ⋯ rr
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_counitIso : ∀ (X : Type u) [inst : Preorder X],
  (CategoryTheory.orderDualEquivalence X).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun x => OrderDual.toDual (Opposite.unop x), map := fun {X_1 Y} f => CategoryTheory.homOfLE ⋯,
            map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun x => Opposite.op (OrderDual.ofDual x), map := fun {X_1 Y} f => (CategoryTheory.homOfLE ⋯).op,
          map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Algebra.Group.Center
Set.decidableMemAddCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : Add M] [inst_1 : (a : M) → Decidable (∀ b ∈ S, b + a = a + b)] (x : M),
  Set.decidableMemAddCentralizer x = decidable_of_iff' (∀ m ∈ S, m + x = x + m) ⋯
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Sort u_3)
  (it : Std.DTreeMap.Internal.Zipper α β)
  (h_1 : (it : Std.DTreeMap.Internal.Zipper α β) → motive Std.DTreeMap.Internal.Impl.leaf it)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (it : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it),
  (match Std.DTreeMap.Internal.Impl.leaf, it with
    | Std.DTreeMap.Internal.Impl.leaf, it => h_1 it
    | Std.DTreeMap.Internal.Impl.inner size k v l r, it => h_2 size k v l r it) =
    h_1 it
-- Lean.Elab.MutualDef
Lean.Elab.Term.AsyncBodyInfo.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIso_midπ_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ),
  autoParam (i ≤ n₀ + ↑q) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIso_midπ_f._auto_1✝ →
    CategoryTheory.IsIso ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q).f i)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.mk.sizeOf_spec : ∀ (toBddDistLat : BddDistLat) [isFintype : Fintype ↑toBddDistLat.toDistLat],
  sizeOf { toBddDistLat := toBddDistLat, isFintype := isFintype } = 1 + sizeOf toBddDistLat + sizeOf isFintype
-- Mathlib.FieldTheory.RatFunc.Degree
/-- `intDegree x` is the degree of the rational function `x`, defined as the difference between
the `natDegree` of its numerator and the `natDegree` of its denominator. In particular,
`intDegree 0 = 0`.  -/
RatFunc.intDegree : {K : Type u} → [inst : Field K] → RatFunc K → ℤ
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_top : ∀ {α : Type u_2} [inst : TopologicalSpace α] (x : α), x ∈ ⊤
-- Mathlib.Analysis.Normed.Group.Uniform
norm_map : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity between the iterated `SubMulAction`
of the `fixingSubgroup` and the `SubMulAction` of the `fixingSubgroup`
of the union, as an equivariant map.  -/
SubMulAction.map_ofFixingSubgroupUnion : (M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (s t : Set α) →
          have ψ := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩;
          ↥(SubMulAction.ofFixingSubgroup M (s ∪ t)) →ₑ[ψ]
            ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t))
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.union.sizeOf_spec : ∀ (leanTypeName : Lean.Name) (types : Array Lean.IR.IRType),
  sizeOf (Lean.IR.IRType.union leanTypeName types) = 1 + sizeOf leanTypeName + sizeOf types
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.instHasLeftKanLiftComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  CategoryTheory.Bicategory.HasLeftKanLift f (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.RingTheory.FreeCommRing
/-- The free ring on the empty type is isomorphic to `ℤ`.  -/
freeRingPEmptyEquivInt : FreeRing PEmpty.{u + 1} ≃+* ℤ
-- Mathlib.Topology.IsLocalHomeomorph
/-- **Alias** of `Homeomorph.isLocalHomeomorph`.

---

A homeomorphism is a local homeomorphism.  -/
IsLocalHomeomorph.Homeomorph.isLocalHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ₜ Y),
  IsLocalHomeomorph ⇑f
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn_congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  f =ᶠ[nhdsSet s] g → (CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_eq_zero_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ), Dynamics.netMaxcard T F U n = 0 ↔ F = ∅
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
eventuallyMeasurableSet_of_mem_filter : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [inst : CountableInterFilter l],
  s ∈ l → EventuallyMeasurableSet m l s
-- Lean.Compiler.Options
Lean.Compiler.compiler.inLeanIR : Lean.Option Bool
-- Init.Data.String.Modify
String.Pos.Raw.isValid_add_char_set : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos}, String.Pos.Raw.IsValid (p.set c hp) (p.offset + c)
-- Mathlib.Topology.CantorBendixson
CantorBendixson.isClosed_iteratedDerivedSet : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsClosed s → ∀ (a : Ordinal.{u}), IsClosed (CantorBendixson.iteratedDerivedSet s a)
-- Std.Http.Data.Response
Std.Http.Response.instEncodeV11Head : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Response.Head
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles : Type
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instDecidableAnyOfDecidablePred : {α : Type u_1} → {p : α → Prop} → {t : RBTree.RBNode α} → [DecidablePred p] → Decidable (RBTree.RBNode.Any p t)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minKey? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.div`

---

`f x / g x` is analytic away from `g x = 0`  -/
AnalyticAt.fun_div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {x : E}, AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → g x ≠ 0 → AnalyticAt 𝕜 (fun i => f i / g i) x
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rank'_lt_rankMax : ∀ (self : Batteries.UnionFind) (i : ℕ) (h : i < self.arr.size), self.arr[i].rank < self.rankMax
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCore_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (c' : F.CoconeTypes) (a : c.pt), hc.isColimitCore.desc c' a = hc.desc c' a
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Arity of the "output" of the fractional operation.  -/
FractionalOperation.size : {D : Type u_1} → {m : ℕ} → FractionalOperation D m → ℕ
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instStar : {n : Type u_2} → {A : Type u_5} → [Star A] → Star (CStarMatrix n n A)
-- Lean.Data.SMap
/-- Staged map for implementing the Environment. The idea is to store
imported entries into a hashtable and local entries into a persistent hashtable.

Hypotheses:
- The number of entries (i.e., declarations) coming from imported files is much bigger than
  the number of entries in the current file.
- HashMap is faster than PersistentHashMap.
- When we are reading imported files, we have exclusive access to the map, and efficient
  destructive updates are performed.

Remarks:
- We never remove declarations from the Environment. In principle, we could support
  deletion by using `(PHashMap α (Option β))` where the value `none` would indicate
  that an entry was "removed" from the hashtable.
- We do not need additional bookkeeping for extracting the local entries.
 -/
Lean.SMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Init.Internal.Order.Basic
Lean.Order.prod_csup : {α : Sort u} →
  {β : Sort v} →
    [inst : Lean.Order.CCPO α] → [inst_1 : Lean.Order.CCPO β] → (c : α ×' β → Prop) → Lean.Order.chain c → α ×' β
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instSMul : (p : ENNReal) → (K : Type u_1) → (V : Type u_4) → [SMul K V] → SMul K (WithLp p V)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V], (CategoryTheory.Cat.FreeRefl.quotientFunctor V).Full
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.gaussNorm_eq : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  PowerSeries.gaussNorm v c f = ⨆ i, v ((PowerSeries.coeff i) f) * c ^ i
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f.toPshHom = X
-- Std.Time.Format.Modifier
Std.Time.Modifier.M.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.M presentation) = 1 + sizeOf presentation
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey? k = t.getKey? k
-- Mathlib.Control.Traversable.Equiv
/-- The function `Equiv.map` transfers the functoriality of `t` to
`t'` using the equivalences `eqv`.  -/
Equiv.functor : {t t' : Type u → Type u} → ((α : Type u) → t α ≃ t' α) → [Functor t] → Functor t'
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- A countable limit ordinal has cofinality `ℵ₀`.  -/
Ordinal.cof_eq_aleph0_of_isSuccLimit : ∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → o < Ordinal.omega 1 → o.cof = Cardinal.aleph0
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.sub_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Sub Y] (f g : LocallyConstant X Y) (x : X),
  (f - g) x = f x - g x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.constructor : Lean.Lsp.SymbolKind
-- Mathlib.CategoryTheory.Preadditive.Transfer
/-- If `D` is a preadditive category, any fully faithful functor `F : C ⥤ D` induces a preadditive
structure on `C`.  -/
CategoryTheory.Preadditive.ofFullyFaithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Preadditive D] →
          {F : CategoryTheory.Functor C D} → F.FullyFaithful → CategoryTheory.Preadditive C
-- Mathlib.Data.DFinsupp.BigOperators
/-- While we didn't need decidable instances to define it, we do to reduce it to a sum  -/
DFinsupp.sumAddHom_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ)
  (f : Π₀ (i : ι), β i), (DFinsupp.sumAddHom φ) f = f.sum fun x => ⇑(φ x)
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.iff_eq_top_or_exists : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.IsSubnormal ↔ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_filter_exists : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α → β) [inst_1 : Fintype β]
  [inst_2 : DecidablePred fun y => ∃ x, f x = y] [inst_3 : DecidableEq β],
  {y | ∃ x, f x = y} = Finset.image f Finset.univ
-- Init.Data.Ord.Vector
Vector.instReflCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {n : ℕ}, Std.ReflCmp (Vector.compareLex cmp)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- Given an almost everywhere measurable function `f`, associate to it a measurable function
that coincides with it almost everywhere. `f` is explicit in the definition to make sure that
it shows in pretty-printing.  -/
AEMeasurable.mk : {α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      [inst : MeasurableSpace β] → {μ : MeasureTheory.Measure α} → (f : α → β) → AEMeasurable f μ → α → β
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mk : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            (toMonoidHom : A →* B) →
              autoParam (Continuous (↑toMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam → A →ₜ* B
-- Mathlib.Analysis.RCLike.Basic
RCLike.real_smul_eq_coe_mul : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), r • z = ↑r * z
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Unweighted mean inequality, version for two elements of `ℝ≥0∞` and real exponents.  -/
ENNReal.rpow_add_le_mul_rpow_add_rpow : ∀ (z₁ z₂ : ENNReal) {p : ℝ}, 1 ≤ p → (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_neg : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x : V), WithLp.toLp p (-x) = -WithLp.toLp p x
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablyGenerated.sup : ∀ {β : Type u_2} {m₁ m₂ : MeasurableSpace β},
  MeasurableSpace.CountablyGenerated β → MeasurableSpace.CountablyGenerated β → MeasurableSpace.CountablyGenerated β
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_pos : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ → 0 < ProbabilityTheory.mgf X μ t
-- Mathlib.Order.WithBot
WithBot.ofDual_le_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot αᵒᵈ}, WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.map.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} (g g_1 : (i : ι) → G i →ₗ[R] G' i)
  (e_g : g = g_1) (hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i),
  Module.DirectLimit.map g hg = Module.DirectLimit.map g_1 ⋯
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_inf : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (s t : Subfield K) (f : K →+* L),
  Subfield.map f (s ⊓ t) = Subfield.map f s ⊓ Subfield.map f t
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_comp_inr : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0],
  (MonoidWithZeroHom.snd G₀ H₀).comp (MonoidWithZeroHom.inr G₀ H₀) = MonoidWithZeroHom.id H₀
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ContainsUnit.prop_unit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P : CategoryTheory.ObjectProperty C} [self : P.ContainsUnit], P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β),
  f.comp (SupBotHom.id α) = f
-- Mathlib.Order.Filter.IsBounded
Filter.IsCoboundedUnder.of_frequently_ge : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder α] {f : Filter ι} {u : ι → α} {a : α},
  (∃ᶠ (x : ι) in f, a ≤ u x) → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_ite : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (P : Prop) [inst_1 : Decidable P] (m n : ℕ),
  ↑(if P then m else n) = if P then ↑m else ↑n
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.instPreservesMonomorphismsFree : AddCommGrpCat.free.PreservesMonomorphisms
-- Mathlib.Combinatorics.HalesJewett
/-- The underlying line of an almost monochromatic line, where the coordinate dimension `α` is
extended by an additional symbol `none`, thought to be marking the endpoint of the line.  -/
Combinatorics.Line.AlmostMono.line : {α : Type u_5} →
  {ι : Type u_6} →
    {κ : Type u_7} → {C : (ι → Option α) → κ} → Combinatorics.Line.AlmostMono C → Combinatorics.Line (Option α) ι
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.presieve.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C} {X : C}
  (E : CategoryTheory.PreZeroHypercover X), P.property E → P.presieve E.presieve₀
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.isEquivalent_sin : Asymptotics.IsEquivalent (nhds 0) Complex.sin id
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, (Std.ExtDHashMap.Const.ofList l).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Data.Complex.Basic
Complex.div_natCast : ∀ (z : ℂ) (n : ℕ), z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
-- Mathlib.GroupTheory.PushoutI
/-- The chosen element of the base group itself is the identity  -/
Monoid.PushoutI.NormalWord.Transversal.one_mem : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι), 1 ∈ self.set i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_add_one_sinh : ∀ (n : ℕ), iteratedDeriv (n + 1) Real.sinh = iteratedDeriv n Real.cosh
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.is_presheafedSpace_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp a (b - ↑m * p) = toIcoMod hp a b
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated submonoid of a monoid with a single unit has finitely many irreducible
elements.  -/
Submonoid.FG.finite_irreducible_mem_submonoidClosure : ∀ {M : Type u_1} [inst : CommMonoid M] [Subsingleton Mˣ] {S : Submonoid M}, S.FG → {p | p ∈ S ∧ Irreducible p}.Finite