mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftToInitial_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.liftToInitial F hZ).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => F.obj x
    | CategoryTheory.WithInitial.star => Z
-- Mathlib.CategoryTheory.Yoneda
/-- The representing element for the representable functor `F`, sometimes called the universal
element of the functor.
 -/
CategoryTheory.Functor.reprx : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) → [hF : F.IsRepresentable] → F.obj (Opposite.op F.reprX)
-- Init.Omega.IntList
Lean.Omega.IntList.instAdd : Add Lean.Omega.IntList
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_append_eq_left : ∀ {w w' : ℕ} {a : BitVec w} {b : BitVec w'}, BitVec.extractLsb' w' w (a ++ b) = a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List α} {k : α}, k ∈ m → (m.insertMany l).get! k = m.get! k
-- Mathlib.Lean.Expr.Basic
Lean.Expr.modifyAppArgM : {M : Type → Type u} → [Functor M] → [Pure M] → (Lean.Expr → M Lean.Expr) → Lean.Expr → M Lean.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).isEmpty = true ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = none)
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.instSliceableListSliceNat.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (stop : ℕ) (h_1 : Unit → motive none) (h_2 : (stop : ℕ) → motive (some stop)),
  (match some stop with
    | none => h_1 ()
    | some stop => h_2 stop) =
    h_2 stop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_empty : ∀ {α : Type u_2} [inst : Inv α], ∅⁻¹ = ∅
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.eta_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.eta.hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.M : Type → Type
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation.eq_1 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle),
  o.rotation θ =
    LinearIsometryEquiv.ofLinearIsometry (o.rotationAux θ)
      (θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv) ⋯ ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.prod_toLinearEquiv : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R N₁] [inst_9 : Module R N₂]
  [inst_10 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P}
  {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂'),
  (e₁.prod e₂).toLinearEquiv = e₁.prodCongr e₂.toLinearEquiv
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
_private.Mathlib.Algebra.ContinuedFractions.TerminatedStable.0.GenContFract.contsAux.match_1.eq_2 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (gp : GenContFract.Pair K)
  (h_1 : Unit → motive none) (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match some gp with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_2 gp
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.coe_of : ∀ {X : Type u_3} (toTwoPointing : TwoPointing X), (TwoP.of toTwoPointing).X = X
-- Mathlib.Algebra.Order.Floor.Extended
/-- `⌈r⌉ₑ` is the least extended natural `n` such that `r ≤ n`  -/
ENat.«term⌈_⌉ₑ» : Lean.ParserDescr
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_replicateRow : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateRow ι v‖ = ‖v‖
-- Lean.DocString.Extension
Lean.VersoModuleDocs.instInhabitedSnippet.default : Lean.VersoModuleDocs.Snippet
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_lt_add_one : ∀ {r : ENNReal}, r ≠ ⊤ → ↑⌈r⌉ₑ < r + 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.id_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (x : M₁), (ContinuousLinearMap.id R₁ M₁) x = x
-- Init.System.IO
EIO.throw : {ε α : Type} → ε → EIO ε α
-- Init.While
/-- `repeatM f a` iterates `f` at `a`, recursing on `.inl` and terminating on `.inr`.

Its unfolding lemma is `repeatM_eq_of_monadTail`.
 -/
repeatM : {α : Type u} → {m : Type u → Type v} → [Monad m] → {β : Type u} → [Nonempty β] → (α → m (α ⊕ β)) → α → m β
-- Init.Data.Vector.Lemmas
Vector.all_toList : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.toList.all p = xs.all p
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOneClass N] → Inhabited (M →* N)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instZero : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Zero β] → Zero (MeasureTheory.SimpleFunc α β)
-- Lean.Elab.Declaration
/-- Return `true` if `stx` is an `instance` declaration command  -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.isInstanceDecl : Lean.Syntax → Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_diag : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (f : ι × ι → M),
  ∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k₁ k₂ : α} [Std.TransCmp cmp] (t : RBTree.RBMap α β cmp),
  cmp k₁ k₂ = Ordering.eq → t.find? k₁ = t.find? k₂
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.mk : {X : Type u_3} → X → FundamentalGroupoid X
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.stratum_ne_bot : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M)
  {c : FiniteArchimedeanClass M}, u.stratum c ≠ ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A cotrident on `f : J → (X ⟶ Y)` is determined by the morphism `π : Y ⟶ P` satisfying
`∀ j₁ j₂, f j₁ ≫ π = f j₂ ≫ π`.
 -/
CategoryTheory.Limits.Cotrident.ofπ : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {P : C} →
              (π : Y ⟶ P) →
                (∀ (j₁ j₂ : J),
                    CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) →
                  CategoryTheory.Limits.Cotrident f
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprGroupInfo : Repr Std.Internal.UV.System.GroupInfo
-- Mathlib.Geometry.Manifold.Instances.Real
interior_euclideanQuadrant : ∀ (n : ℕ) (p : ENNReal) (a : ℝ), interior {y | ∀ (i : Fin n), a ≤ y.ofLp i} = {y | ∀ (i : Fin n), a < y.ofLp i}
-- Mathlib.Control.EquivFunctor
/-- The action of `f` on isomorphisms.  -/
EquivFunctor.map : {f : Type u₀ → Type u₁} → [self : EquivFunctor f] → {α β : Type u₀} → α ≃ β → f α → f β
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- the top morphism of the pushout square `isPushout i d`.  -/
SSet.relativeCellComplexOfMono.t : {X Y : SSet} →
  (i : X ⟶ Y) → (d : ℕ) → SSet.relativeCellComplexOfMono.sigmaBoundary i d ⟶ ((SSet.skeletonOfMono i) d).toSSet
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_mkOfNNDistEq : ∀ {α : Type u_5} {β : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f : α → β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y), ⇑(Dilation.mkOfNNDistEq f h) = f
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The map `ι' → Option ι` which sends `e.f i` to `some i` and the other elements to `none`.  -/
ComplexShape.Embedding.r : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → ι' → Option ι
-- Init.Data.List.TakeDrop
List.dropWhile_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  List.dropWhile p (List.replicate n a) = if p a = true then [] else List.replicate n a
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [AddLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ y ∉ t, 0 ≤ ∑ x ∈ s with g x = y, f x) → ∑ y ∈ t, ∑ x ∈ s with g x = y, f x ≤ ∑ x ∈ s, f x
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
measurableSet_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {a : α}, MeasurableSet {x | x = a}
-- Mathlib.RepresentationTheory.Intertwining
/-- The intertwining map induced from `f : σ → τ` to `ρ.tprod σ → ρ.tprod τ`.  -/
Representation.IntertwiningMap.lTensor : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          (ρ : Representation A G V) →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} → σ.IntertwiningMap τ → (ρ.tprod σ).IntertwiningMap (ρ.tprod τ)
-- Mathlib.Algebra.Group.Basic
mul_inv_eq_iff_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * b⁻¹ = c ↔ a = c * b
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_associated : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsRadical a → a ≠ 0 → Associated (UniqueFactorizationMonoid.radical a) a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Icc_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ ≤ b₂ → Finset.Icc a b₁ ⊆ Finset.Icc a b₂
-- Lean.Environment
_private.Lean.Environment.0.Lean.instInhabitedVisibilityMap : {a : Type} → [Inhabited a] → Inhabited (Lean.VisibilityMap✝ a)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.localizationAway.congr_simp : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r r_1 : R) (e_r : r = r_1)
  [inst_3 : IsLocalization.Away r S],
  Algebra.PreSubmersivePresentation.localizationAway S r = Algebra.PreSubmersivePresentation.localizationAway S r_1
-- Mathlib.Algebra.Group.Center
Set.subset_addCenter_add_units : ∀ {M : Type u_1} [inst : AddMonoid M], AddUnits.val ⁻¹' Set.addCenter M ⊆ Set.addCenter (AddUnits M)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [inst_4 : NeZero i] (hi : Even i)
  (x : ↥(LinearMap.ker A.ρ.norm)),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x = 0 ↔
    ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
Rep.Hom.Simps.hom : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → (A B : Rep.{w, u, v} k G) → A.Hom B → A.ρ.IntertwiningMap B.ρ
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.equiv_toAlgHom : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f),
  ↑h.equiv = SymmetricAlgebra.lift f
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.infSet : {V : Type u} → InfSet (SimpleGraph V)
-- Mathlib.Order.BooleanAlgebra.Basic
compl_compl : ∀ {α : Type u} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.readLspMessageAsString : IO.FS.Stream → IO String
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A B : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (hB : B.IsHermitian), hA.eigenvalues = hB.eigenvalues ↔ A.charpoly = B.charpoly
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Add M] [inst_3 : Add N]
  [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N],
  ContinuousAddEquiv.instUnique = { default := ContinuousAddEquiv.ofUnique, uniq := ⋯ }
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_le_psi : ∀ (x : ℝ), Chebyshev.theta x ≤ Chebyshev.psi x
-- Mathlib.LinearAlgebra.StdBasis
Pi.linearIndependent_single : ∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : DecidableEq η]
  (v : (j : η) → ιs j → Ms j),
  (∀ (i : η), LinearIndependent R (v i)) → LinearIndependent R fun ji => Pi.single ji.fst (v ji.fst ji.snd)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.coe_hasEvalIdeal : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S], ↑PowerSeries.hasEvalIdeal = {a | PowerSeries.HasEval a}
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.refl_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Retract.refl X).i = CategoryTheory.CategoryStruct.id X
-- Init.Notation
/-- The attribute `@[univ_out_params ..]` on a class specifies the universe output parameters.

* `@[univ_out_params]` means the class has no universe output parameters.
* `@[univ_out_params u v]` means the universes `u` and `v` are output parameters.

If this attribute is not present, Lean assumes that any universe parameter which does not
occur in any input parameter type is an output parameter.

### Effect on typeclass resolution

When typeclass resolution begins, output universe parameters are replaced with fresh universe
metavariables, similar to what is done for regular output parameters. This means the search
proceeds without being constrained by the specific output universes in the query, and the
actual output universes are determined by the instance that is found.

As a consequence, output universe parameters are erased from typeclass resolution cache keys.
Two queries that differ only in output universe parameters will share a cache entry,
and the first result found will be reused for subsequent queries.

### When to use this attribute

The default heuristic is wrong when the universe is
part of the *question* being asked, rather than something determined by the answer.

For example, in `class Foo.{u} (C : Type v)` where `u` specifies "how large" some auxiliary
data is, different values of `u` give genuinely different conditions on `C`. By default `u`
would be treated as output since it does not appear in `C : Type v`, and the cache would
conflate `Foo.{0} C` with `Foo.{1} C`, returning the wrong instance.
Use `@[univ_out_params]` to mark that no universe parameter is output.
 -/
Lean.univ_out_params : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_sum : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_3}
  (m : ι → MeasureTheory.Measure α) (f : α → MeasureTheory.Measure β),
  AEMeasurable f (MeasureTheory.Measure.sum fun i => m i) →
    (MeasureTheory.Measure.sum fun i => m i).bind f = MeasureTheory.Measure.sum fun i => (m i).bind f
-- Batteries.Data.Bool
/-- Boolean '>' is well founded  -/
Bool.gt_wfRel : WellFoundedRelation Bool
-- Mathlib.Topology.CompactOpen
/-- The curried form of a continuous map `α × β → γ` as a continuous map `α → C(β, γ)`.
If `a × β` is locally compact, this is continuous. If `α` and `β` are both locally
compact, then this is a homeomorphism, see `Homeomorph.curry`.  -/
ContinuousMap.curry : {X : Type u_2} →
  {Y : Type u_3} →
    {Z : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → C(X × Y, Z) → C(X, C(Y, Z))
-- Init.Prelude
instLTNat : LT ℕ
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The preimage of a subring along a ring homomorphism is a subring.  -/
Subring.comap : {R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (R →+* S) → Subring S → Subring R
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
deriv_riemannZeta₁_one : deriv riemannZeta₁ 1 = ↑Real.eulerMascheroniConstant
-- Mathlib.Algebra.GroupWithZero.Basic
_private.Mathlib.Algebra.GroupWithZero.Basic.0.inv_eq_of_mul : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b : G₀}, a * b = 1 → a⁻¹ = b
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.nodup_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v), (↑p).support.Nodup
-- Batteries.Data.Char.Basic
Char.exists_eq_true_of_any_eq_true : ∀ {p : Char → Bool}, Char.any p = true → ∃ c, p c = true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.mk : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred →
  ℕ → Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof → Lean.Meta.Grind.Arith.Cutsat.CooperSplit
-- Mathlib.Order.Defs.PartialOrder
lt_iff_gt_iff_le_iff_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (a < b ↔ b < a) ↔ (a ≤ b ↔ b ≤ a)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.mk.sizeOf_spec : ∀ {α : Type u₁} [inst : SizeOf α] (as : α), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Order.ModularLattice
/-- `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers both `a` and `b`  -/
IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup : ∀ {α : Type u_2} {inst : Lattice α} [self : IsWeakLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
-- Mathlib.Topology.Order.Basic
pi_Iio_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι],
  (∀ (i : ι), x i < a i) → Set.Iio a ∈ nhds x
-- Std.Time.DateTime
/-- Changes the `ZoneRules` to a new one.
 -/
Std.Time.DateTime.convertZoneRules : Std.Time.DateTime → Std.Time.TimeZone.ZoneRules → Std.Time.DateTime
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.load : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → (Γ → σ → σ) → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Γ Λ σ
-- Mathlib.Algebra.Group.Fin.Basic
/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too.  -/
Fin.instAddLeftCancelSemigroup : (n : ℕ) → AddLeftCancelSemigroup (Fin n)
-- Mathlib.Topology.Sober
isGenericPoint_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α}, IsGenericPoint x (closure {x})
-- Mathlib.Combinatorics.Graph.Simple
Graph.Simple.eq_of_isLink : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [self : G.Simple] ⦃e f : β⦄ ⦃x y : α⦄,
  G.IsLink e x y → G.IsLink f x y → e = f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.isEqBwdPattern : Lean.Expr → Bool
-- Batteries.Data.Fin.Basic
/-- Heterogeneous monadic fold over `Fin n` from left to right:
```
Fin.foldlM n f x₀ = do
  let x₁ : α 1 ← f 0 x₀
  let x₂ : α 2 ← f 1 x₁
  ...
  let xₙ : α n ← f (n-1) xₙ₋₁
  pure xₙ
```
This is the dependent version of `Fin.foldlM`.  -/
Fin.dfoldlM : {m : Type u_1 → Type u_2} →
  [Monad m] →
    (n : ℕ) → (α : Fin (n + 1) → Type u_1) → ((i : Fin n) → α i.castSucc → m (α i.succ)) → α 0 → m (α (Fin.last n))
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctorMonoidal.eq_1 : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N),
  CategoryTheory.Discrete.monoidalFunctorMonoidal F =
    { εIso := CategoryTheory.Discrete.eqToIso ⋯, μIso := fun m₁ m₂ => CategoryTheory.Discrete.eqToIso ⋯,
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheorem : Lean.ConstructorVal → Lean.MetaM Unit
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.get_eq_getₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (h : m.contains a = true), m.get a h = m.getₘ a h
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMkSucc_app_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (β : F.δ₀ ⟶ G.δ₀)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
          (CategoryTheory.ComposableArrows.app' β 0 ⋯) =
        CategoryTheory.CategoryStruct.comp α (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯))
      _auto_223✝)
  (i : ℕ) (hi : i + 1 < n + 1 + 1),
  (CategoryTheory.ComposableArrows.homMkSucc α β w).app ⟨i + 1, hi⟩ = CategoryTheory.ComposableArrows.app' β i ⋯
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.declModifiersPubNoDoc : Lean.Syntax → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.GroupTheory.Coset.Basic
leftAddCoset_assoc : ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), a +ᵥ b +ᵥ s = (a + b) +ᵥ s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instTypeNameCoeExpansionTrace : TypeName Lean.Elab.Term.CoeExpansionTrace
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is associative  -/
Semigroup.mul_assoc : ∀ {G : Type u} [self : Semigroup G] (a b c : G), a * b * c = a * (b * c)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCompletion.AdicCauchySequence I R),
  (AdicCompletion.evalₐ I n) ((AdicCompletion.mk I R) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)
-- Mathlib.Probability.Process.Predictable
/-- A predictable process is progressively measurable.  -/
MeasureTheory.IsStronglyPredictable.isStronglyProgressive : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E]
  [inst_1 : LinearOrder ι] [inst_2 : OrderBot ι] [inst_3 : MeasurableSpace ι] [inst_4 : TopologicalSpace ι]
  [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : MeasureTheory.Filtration ι m} {u : ι → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u → MeasureTheory.IsStronglyProgressive 𝓕 u