mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- If the L-series of `f` converges at some point, then `f 1` is the limit of `LSeries f x`
as `x → ∞`.  -/
LSeries.tendsto_atTop : ∀ {f : ℕ → ℂ}, LSeries.abscissaOfAbsConv f < ⊤ → Filter.Tendsto (fun x => LSeries f ↑x) Filter.atTop (nhds (f 1))
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- In a space with the Besicovitch covering property, the ratio of the measure of balls converges
almost surely to the Radon-Nikodym derivative.  -/
Besicovitch.ae_tendsto_rnDeriv : ∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β]
  [HasBesicovitchCovering β] (ρ μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ]
  [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ∀ᵐ (x : β) ∂μ,
    Filter.Tendsto (fun r => ρ (Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds (ρ.rnDeriv μ x))
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.Collect : Type → Type
-- Lean.Parser.Term
Lean.Parser.Term.binop_lazy.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_adj : ∀ {n : ℕ} {u v : Fin (n + 2)}, (SimpleGraph.cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1
-- Init.Data.Int.Order
Int.pos_of_sign_eq_one : ∀ {a : ℤ}, a.sign = 1 → 0 < a
-- Mathlib.Topology.Homotopy.Contractible
homotopic_of_indiscrete : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [IndiscreteTopology Y]
  (f g : C(X, Y)), f.Homotopic g
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE'_apply : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientGroup.mk) (a : α ⧸ s),
  (Subgroup.quotientEquivProdOfLE' h_le f hf) a =
    (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] (M : A),
  CategoryTheory.Presheaf.IsSheaf J (Φ.skyscraperPresheaf M)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.h : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context : Type
-- Mathlib.Order.LiminfLimsup
/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below.  -/
Filter.HasBasis.liminf_eq_ite : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
  v.HasBasis p s →
    ∀ (f : ι → α),
      Filter.liminf f v =
        if ∃ j, s ↑j = ∅ then sSup Set.univ
        else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- Left whiskering of a strong natural transformation between pseudofunctors
and a modification.  -/
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.Pseudofunctor B C} →
          (η : F ⟶ G) →
            {θ ι : G ⟶ H} → (θ ⟶ ι) → (CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.Order.Defs.LinearOrder
min_def' : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b = if b ≤ a then b else a
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight.inj : ∀ {e : Lean.Expr} {f g : Mathlib.Tactic.BicategoryLike.Mor₁} {η : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {h : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr} {f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso} {h_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e_1 f_1 g_1 η_1 h_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1 ∧ h = h_1
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
/-- Restrict domain and codomain of an affine map to the given subspaces.  -/
AffineMap.restrict : {k : Type u_1} →
  {V₁ : Type u_2} →
    {P₁ : Type u_3} →
      {V₂ : Type u_4} →
        {P₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        (φ : P₁ →ᵃ[k] P₂) →
                          {E : AffineSubspace k P₁} →
                            {F : AffineSubspace k P₂} →
                              [inst_7 : Nonempty ↥E] → [inst_8 : Nonempty ↥F] → AffineSubspace.map φ E ≤ F → ↥E →ᵃ[k] ↥F
-- Mathlib.Algebra.MonoidAlgebra.Lift
/-- `liftNC` as a `RingHom`, for when `f` and `g` commute  -/
AddMonoidAlgebra.liftNCRingHom : {k : Type u₁} →
  {G : Type u₂} →
    {R : Type u_2} →
      [inst : Semiring k] →
        [inst_1 : AddMonoid G] →
          [inst_2 : Semiring R] →
            (f : k →+* R) →
              (g : Multiplicative G →* R) →
                (∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) → AddMonoidAlgebra k G →+* R
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : CategoryTheory.IsIso f.f],
  CategoryTheory.Center.isoMk f = CategoryTheory.Center.isoMk f_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_infiniteTheory_iff : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], M ⊨ L.infiniteTheory ↔ Infinite M
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.sup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {I J : Ideal A},
  Ideal.IsHomogeneous 𝒜 I → Ideal.IsHomogeneous 𝒜 J → Ideal.IsHomogeneous 𝒜 (I ⊔ J)
-- Mathlib.Data.Multiset.Fintype
Multiset.prod_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_3} [inst_1 : CommMonoid β] (m : Multiset α) (f : α → ℕ → β),
  ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f x.fst ↑x.snd
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- If `C` has finite colimits then it has finite coproducts.  -/
CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instFullMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommMon.forget₂Mon C).Full
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- An alternate version of **Beck's monadicity theorem**: if `G` reflects isomorphisms, preserves
coequalizers of `G`-split pairs and `C` has coequalizers of `G`-split pairs, then it is monadic.
 -/
CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (F ⊣ G) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] →
                  [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] → CategoryTheory.MonadicRightAdjoint G
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instOne : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → One (Module.End R M)
-- Lean.Elab.Tactic.Omega.Core
/-- The current constraints, indexed by their coefficients.  -/
Lean.Elab.Tactic.Omega.Problem.constraints : Lean.Elab.Tactic.Omega.Problem → Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_natCast : ∀ {r : ℝ} {n : ℕ}, r.toNNReal ≤ ↑n ↔ r ≤ ↑n
-- Mathlib.Data.Set.Prod
Set.subset_pi_eval_image : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (u : Set ((i : ι) → α i)), u ⊆ s.pi fun i => Function.eval i '' u
-- Mathlib.RingTheory.Grassmannian
_private.Mathlib.RingTheory.Grassmannian.0.Module.Grassmannian.baseChangeMkQ.eq_1 : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type w}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (B : Type w) [inst_5 : CommRing B] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)),
  Module.Grassmannian.baseChangeMkQ B N =
    LinearMap.baseChange B N.mkQ ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M).symm
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_add_right : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (d : ℝ),
  ∫ (x : ℝ) in a..b, f (x + d) = ∫ (x : ℝ) in a + d..b + d, f x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.prodEquiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : A →⋆ₐ[R] B × C),
  StarAlgHom.prodEquiv.symm f = ((StarAlgHom.fst R B C).comp f, (StarAlgHom.snd R B C).comp f)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The isomorphism between `HeightOneSpectrum`s of isomorphic rings.  -/
IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_4} →
      [inst_1 : CommRing S] → R ≃+* S → IsDedekindDomain.HeightOneSpectrum R ≃ IsDedekindDomain.HeightOneSpectrum S
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The algEquiv between an intermediate field and its lift.  -/
IntermediateField.liftAlgEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {E : IntermediateField K L} → (F : IntermediateField K ↥E) → ↥F ≃ₐ[K] ↥(IntermediateField.lift F)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.degree_map_lt : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  f p.leadingCoeff = 0 → p ≠ 0 → (Polynomial.map f p).degree < p.degree
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.coe_basis : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  ⇑(WeierstrassCurve.Affine.CoordinateRing.basis W') = ![1, (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X]
-- Lean.DocString.Add
/-- Adds a docstring to the environment.

Whether the docstring is processed as Verso or as Markdown is determined by the form of its syntax
tree. To explicitly control whether the docstring is in Verso format, use `addDocStringOf` instead.

Markdown docstrings have their documentation links validated.

For Verso docstrings, `binders` should be the syntax of the parameters to the constant that is being
documented, as a null node that contains a sequence of bracketed binders. It is used to allow
interactive features such as document highlights and “find references” to work for documented
parameters. If no parameter binders are available, pass `Syntax.missing` or an empty null node.
`binders` is not used for Markdown docstrings.
 -/
Lean.addDocString : Lean.Name → Lean.Syntax → Lean.TSyntax `Lean.Parser.Command.docComment → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊤.op = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.pOpcycles S.moduleCatOpcyclesIso.hom =
    ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.  -/
NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] {l : Filter ι} {ε : ι → 𝕜} {f : ι → E},
  Filter.Tendsto ε l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) → Filter.Tendsto (ε • f) l (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is a monoid object, then `Hom(-, M)` as a presheaf of monoids is represented by `M`.  -/
CategoryTheory.yonedaMonObjRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) →
        [inst_2 : CategoryTheory.MonObj M] →
          ((CategoryTheory.yonedaMonObj M).comp (CategoryTheory.forget MonCat)).RepresentableBy M
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {toProd toProd_1 : R × A},
  Unitization.mk toProd = Unitization.mk toProd_1 → toProd = toProd_1
-- Mathlib.Combinatorics.Enumerative.Composition
/-- A composition of `n` is a list of positive integers summing to `n`.  -/
Composition : ℕ → Type
-- Lean.Elab.Term.TermElabM
/-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`.  -/
Lean.Elab.Term.mkBodyInfo : Lean.Syntax → Option Lean.Expr → Lean.Elab.Info
-- Batteries.Lean.Expr
/-- Annotates a `binderIdent` with the binder information from an `fvar`.  -/
Lean.Expr.addLocalVarInfoForBinderIdent : Lean.Expr → Lean.TSyntax `Lean.binderIdent → Lean.MetaM Unit
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_coeff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ)
  (f : LaurentSeries V) (n : ℤ), ((LaurentSeries.hasseDeriv R k) f).coeff n = Ring.choose (n + ↑k) k • f.coeff (n + ↑k)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toEquiv_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B], Function.Injective CoalgEquiv.toEquiv
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrict_apply : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} {S : Type u_6} [inst_1 : MulOneClass N] [inst_2 : SetLike S M]
  [inst_3 : SubmonoidClass S M] (f : M →* N) (s : S) (x : ↥s), (f.domRestrict s) x = f ↑x
-- Init.Data.List.Nat.TakeDrop
List.length_zip : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, (l₁.zip l₂).length = min l₁.length l₂.length
-- Mathlib.Data.Nat.Factors
Nat.isChain_cons_primeFactorsList : ∀ {n a : ℕ}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → a ≤ p) → List.IsChain (fun x1 x2 => x1 ≤ x2) (a :: n.primeFactorsList)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version on a set, but with full pullback  -/
ContMDiffOn.mpullback_vectorField_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffOn I' I'.tangent m (fun x => ⟨x, V x⟩) t →
    ContMDiff I I' n f →
      (∀ x ∈ f ⁻¹' t, (mfderiv% f x).IsInvertible) →
        m + 1 ≤ n → ContMDiffOn I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) (f ⁻¹' t)
-- Std.Data.DTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.DTreeMap.foldlM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DTreeMap α β cmp → m δ
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.coindep_iff_forall_subset_not_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X ↔ (∀ K ⊆ X, ¬M.IsCocircuit K) ∧ X ⊆ M.E
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) =
    (Std.DTreeMap.Internal.Impl.contains k t || l.contains k)
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
/-- If the vector field `v` vanishes at `x₀`, then the constant curve at `x₀`
is a global integral curve of `v`.  -/
isMIntegralCurve_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  {v : (x : M) → TangentSpace I x} {x : M}, v x = 0 → IsMIntegralCurve (fun x_1 => x) v
-- Mathlib.SetTheory.Ordinal.Notation
/-- `opow o₁ o₂` calculates the ordinal notation for the ordinal exponential `o₁ ^ o₂`.  -/
ONote.opow : ONote → ONote → ONote
-- Mathlib.Algebra.Group.Commute.Hom
semiconjBy_map_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {a : M} [inst_2 : FunLike F M N]
  [MulHomClass F M N] {f : F}, Function.Injective ⇑f → ∀ {x y : M}, SemiconjBy (f a) (f x) (f y) ↔ SemiconjBy a x y
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.nsmul_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ℕ), x ∈ I → n • x ∈ I
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.isoCycles₁ A =
    CategoryTheory.ShortComplex.cyclesMapIso' (groupHomology.isoShortComplexH1 A)
      (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 1).leftHomologyData
      (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData
-- Mathlib.Algebra.FreeMonoid.Basic
/-- free monoids over isomorphic types are isomorphic  -/
FreeMonoid.freeMonoidCongr : {α : Type u_6} → {β : Type u_7} → α ≃ β → FreeMonoid α ≃* FreeMonoid β
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : β → α} {g : γ → β},
  MeasurableSpace.comap g (MeasurableSpace.comap f m) = MeasurableSpace.comap (f ∘ g) m
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorObj_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.ιFunctorObj f πX) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX)
      (CategoryTheory.SmallObject.ρFunctorObj f πX)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_congr_set : ∀ {𝕜 : 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'} {x : M} {s t : Set M},
  s =ᶠ[nhds x] t → (MDiffAt[s] f x ↔ MDiffAt[t] f x)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Algebra equivalences between `Algebra`s are the same as isomorphisms in `CommAlgCat`.  -/
CommAlgCat.isoEquivAlgEquiv : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : CommRing X] →
        [inst_2 : Algebra R X] →
          [inst_3 : CommRing Y] → [inst_4 : Algebra R Y] → (CommAlgCat.of R X ≅ CommAlgCat.of R Y) ≃ X ≃ₐ[R] Y
-- Mathlib.Probability.Process.Predictable
MeasureTheory.Predictable.stronglyAdapted : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {β : Type u_4} [inst : TopologicalSpace β] {f : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → β},
  (MeasureTheory.StronglyAdapted f fun n => u (n + 1)) →
    MeasureTheory.StronglyMeasurable (u 0) → MeasureTheory.StronglyAdapted f u
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIcoMod hp a b = toIcoDiv hp a b • p
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
MonotoneOn.sSup_image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {a b : α},
  b ≤ a → MonotoneOn f (Set.Icc b a) → sSup (f '' Set.Icc b a) = f a
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.tryTheoremCore : Lean.Expr →
  Array Lean.Expr →
    Array Lean.BinderInfo →
      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.SimpTheorem → ℕ → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Complete matches of norm rules.  -/
Aesop.ForwardRuleMatches.normMatches : Aesop.ForwardRuleMatches → Lean.PHashSet Aesop.ForwardRuleMatch
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (src tgt : C) (rel : CategoryTheory.Subobject (src ⨯ tgt)) (src_1 tgt_1 : C)
  (rel_1 : CategoryTheory.Subobject (src_1 ⨯ tgt_1)),
  ({ src := src, tgt := tgt, rel := rel } = { src := src_1, tgt := tgt_1, rel := rel_1 }) =
    (src = src_1 ∧ tgt = tgt_1 ∧ rel ≍ rel_1)
-- Mathlib.Data.W.Basic
WType.ofSigma_toSigma : ∀ {α : Type u_1} {β : α → Type u_2} (w : WType β), WType.ofSigma w.toSigma = w
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIoc.congr_simp : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], AddCircle.equivIoc p a = AddCircle.equivIoc p a