mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Diagnostics
Lean.Meta.subCounters : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashMap α ℕ → Lean.PHashMap α ℕ → Lean.PHashMap α ℕ
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.setLIntegral_kernel_prod_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : β → α → ENNReal},
  Measurable (Function.uncurry f) → ∀ {s : Set β}, MeasurableSet s → Measurable fun b => ∫⁻ (a : β) in s, f a b ∂κ b
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- View an element of `HomogeneousLocalization 𝒜 x` as an element of `Aₓ` by forgetting that the
numerator and denominator are of the same grading.
 -/
HomogeneousLocalization.val : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization 𝒜 x → Localization x
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_fg_of_artinian' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinianRing R]
  [Module.Finite R M], IsArtinian R M
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes,
this is the homotopy equivalence `mappingConeCompHomotopyEquiv f g`
between `mappingCone g` and the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`.  -/
CochainComplex.mappingConeCompHomotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (f : X₁ ⟶ X₂) →
            (g : X₂ ⟶ X₃) →
              HomotopyEquiv (CochainComplex.mappingCone g)
                (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁)
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.mul_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x * a)) (c * a⁻¹)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
/-- The compatibility isomorphism relating `N₂ ⋙ Γ₂` and `N₁ ⋙ Γ₂`.  -/
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).comp
            (AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂) ≅
          AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.forIn_eq_forIn_toList : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn f init t =
    forIn (Std.DTreeMap.Internal.Impl.Const.toList t) init fun a b => f a.1 a.2 b
-- Mathlib.Data.List.ToFinsupp
List.coe_toFinsupp : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0],
  ⇑l.toFinsupp = fun x => l.getD x 0
-- Std.Http.Transport
Std.Http.Internal.instTransportServer : Std.Http.Transport Std.Http.Internal.Mock.Server
-- Mathlib.Order.Heyting.Basic
sup_himp_self_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ a = b ⇨ a
-- Mathlib.Order.Interval.Set.Image
Antitone.mapsTo_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  Antitone f → Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Construct a `NormalizationMonoid` from a right inverse of `Associates.mk`.  -/
NormalizationMonoid.ofRightInverse : {α : Type u_2} →
  [inst : MonoidWithZero α] →
    [IsLeftCancelMulZero α] →
      (out : Associates α → α) → (∀ (a : Associates α), Associates.mk (out a) = a) → out 1 = 1 → NormalizationMonoid α
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isTree_iff_existsUnique_path : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath
-- Init.Data.ToString.Name
/-- Converts a name to a string.

- If `escape` is `true`, then escapes name components using `«` and `»` to ensure that
those names that can appear in source files round trip.
Names with number components, anonymous names, and names containing `»` might not round trip.
Furthermore, "pseudo-syntax" produced by the delaborator, such as `_`, `#0` or `?u`, is not escaped.
 -/
Lean.Name.toString : Lean.Name → optParam Bool true → String
-- Mathlib.Data.Nat.Cast.WithTop
Nat.cast_withTop : ∀ (n : ℕ), ↑n = ↑n
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- If `S` is a subset of `R`, and `S` is covering, then `R` is covering as well.

See also discussion after [MM92] Chapter III, Section 2, Definition 1.  -/
CategoryTheory.GrothendieckTopology.superset_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C), S ≤ R → S ∈ J X → R ∈ J X
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.inner_orthogonalProjectionOnto_eq_of_mem_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : ↥K) (v : E),
  inner 𝕜 (K.orthogonalProjectionOnto v) u = inner 𝕜 v ↑u
-- Mathlib.RingTheory.Nilpotent.Defs
isRadical_iff_pow_one_lt : ∀ {R : Type u_1} {y : R} [inst : Monoid R] (k : ℕ), 1 < k → (IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x)
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X], StableUnderSpecialization Set.univ
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : MeasurableSpace M] [inst_2 : MeasurableSpace α]
  [toMeasurableConstVAdd : MeasurableConstVAdd M α], (∀ (x : α), Measurable fun x_1 => x_1 +ᵥ x) → MeasurableVAdd M α
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_empty_ne_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i j : Fin (n + 1)), s.touchpoint ∅ i ≠ s.points j
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_le_iSup_add_one : ∀ {β : Type u_2} (f : β → Ordinal.{u_3}), ⨆ i, f i ≤ ⨆ i, f i + 1
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcher : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ioc_bot_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ioc ⊥ ↑a = Finset.map Function.Embedding.some (Finset.Iic a)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffOn_iff_localFrameCoeff`.

---

A section `s` of `V` is `C^k` on `t ⊆ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffOn_iff_localFrame_coeff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  {k : WithTop ℕ∞} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  IsOpen t →
    t ⊆ e.baseSet →
      (ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) t ↔
        ∀ (i : ι),
          ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k
            ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) t)
-- Lean.Meta.Tactic.Grind.Action
/-- If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]` or its variant using `·`
returns `.close [t₁, ... tₙ]`
 -/
Lean.Meta.Grind.Action.ungroup : Lean.Meta.Grind.Action
-- Lean.Elab.MacroArgUtil
/-- Convert `macro` arg into a `syntax` command item and a pattern element  -/
Lean.Elab.Command.expandMacroArg : Lean.TSyntax `Lean.Parser.Command.macroArg → Lean.Elab.Command.CommandElabM (Lean.TSyntax `stx × Lean.Term)
-- Mathlib.Topology.ContinuousMap.Star
/-- Post-composition with a continuous star algebra homomorphism is a star algebra homomorphism
between spaces of continuous maps.  -/
ContinuousMap.compStarAlgHom : (X : Type u_1) →
  {𝕜 : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : TopologicalSpace X] →
          [inst_1 : CommSemiring 𝕜] →
            [inst_2 : TopologicalSpace A] →
              [inst_3 : Semiring A] →
                [inst_4 : IsTopologicalSemiring A] →
                  [inst_5 : Star A] →
                    [inst_6 : ContinuousStar A] →
                      [inst_7 : Algebra 𝕜 A] →
                        [inst_8 : TopologicalSpace B] →
                          [inst_9 : Semiring B] →
                            [inst_10 : IsTopologicalSemiring B] →
                              [inst_11 : Star B] →
                                [inst_12 : ContinuousStar B] →
                                  [inst_13 : Algebra 𝕜 B] → (φ : A →⋆ₐ[𝕜] B) → Continuous ⇑φ → C(X, A) →⋆ₐ[𝕜] C(X, B)
-- Std.Http.Protocol.H1
/-- Events that happened during reading and writing.
 -/
Std.Http.Protocol.H1.Machine.events : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Array (Std.Http.Protocol.H1.Event dir)
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_findIdxNth_of_ge_countP_ge_countP : ∀ {α : Type u_1} {p : α → Bool} {n m : ℕ} {xs : List α},
  List.countP p xs ≤ n → List.countP p xs ≤ m → List.findIdxNth p xs n = List.findIdxNth p xs m
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.coe_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v x : V} {h : f v = 0}, (LinearEquiv.transvection h) x = (LinearMap.transvection f v) x
-- Mathlib.Topology.Order.Lattice
ContinuousOn.sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f ⊔ g) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getValueCast? a (Std.Internal.List.insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then some (cast ⋯ v)
    else Std.Internal.List.getValueCast? a l
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_finsuppProd : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : CommMonoid M] [inst_2 : Zero β] (c : RingCon M)
  (h : ι → β → M) (f : ι →₀ β), ↑(f.prod h) = f.prod fun i b => ↑(h i b)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- A category has all finite limits if every functor `J ⥤ C` with a `FinCategory J`
instance and `J : Type` has a limit.

This is often called 'finitely complete'.
 -/
CategoryTheory.Limits.HasFiniteLimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskering.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J),
  CategoryTheory.Limits.Cocone.whiskering E =
    { obj := fun c => CategoryTheory.Limits.Cocone.whisker E c, map := fun {Y X} f => { hom := f.hom, w := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keysArray_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → Bool},
  (Std.TreeMap.filter (fun k x => f k) t).keysArray = Array.filter f t.keysArray
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_neg : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜}, ↑(-x) = -↑x
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), ↑(e.restr s).symm = ↑e.symm
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.isRefl : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → B.IsRefl
-- Mathlib.Data.Fintype.Card
/-- **Alias** of the forward direction of `Finite.surjective_iff_bijective`. -/
Function.Surjective.bijective_of_finite : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Surjective f → Function.Bijective f
-- Mathlib.Data.Finsupp.Basic
Finsupp.restrictSupportEquiv_apply : ∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M] (f : { f // ↑f.support ⊆ s }),
  (Finsupp.restrictSupportEquiv s M) f = Finsupp.subtypeDomain (fun x => x ∈ s) ↑f
-- Init.Conv
/-- `intro` traverses into binders. Synonym for `ext`.  -/
Lean.Parser.Tactic.Conv.convIntro___ : Lean.ParserDescr
-- Mathlib.Data.ENat.Lattice
ENat.natCast_iInf : ∀ {ι : Sort u_1} {f : ι → ℕ} [Nonempty ι], ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- **Alias** of `MeasurableEquiv.setOfPred_symm_apply`. -/
MeasurableEquiv.setOf_symm_apply : ∀ {α : Type u_8} (s : Set α) (a : α), MeasurableEquiv.setOfPred.symm s a = (a ∈ s)
-- Mathlib.Topology.UniformSpace.Matrix
Matrix.uniformity : ∀ (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [inst : UniformSpace 𝕜],
  uniformity (Matrix m n 𝕜) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (uniformity 𝕜)
-- Init.Prelude
Nat.ctorIdx_succ : ∀ {n : ℕ}, n.succ.ctorIdx = 1
-- Mathlib.Logic.Nontrivial.Defs
/-- A type is either a subsingleton or nontrivial.  -/
subsingleton_or_nontrivial : ∀ (α : Type u_3), Subsingleton α ∨ Nontrivial α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_congr_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  (∀ y ∈ s, f₁ y = f y) → x ∈ s → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Init.Data.Array.BinSearch
Array.binSearchAux : {α : Type u} →
  {β : Type v} →
    (α → α → Bool) → (Option α → β) → (as : Array α) → α → (lo : Fin (as.size + 1)) → (hi : Fin as.size) → ↑lo ≤ ↑hi → β
-- Init.Data.Nat.Basic
Nat.eq_iff_le_and_ge : ∀ {a b : ℕ}, a = b ↔ a ≤ b ∧ b ≤ a
-- Init.Data.Array.Lemmas
Array.toList_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (Array.filter p xs).toList = List.filter p xs.toList
-- Mathlib.RingTheory.PowerBasis
PowerBasis.gen : {R : Type u_7} → {S : Type u_8} → [inst : CommRing R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → PowerBasis R S → S
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instZero : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] → [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → Zero (E₁ →ₚ[R] E₂)
-- Mathlib.Topology.EMetricSpace.Defs
instPseudoEMetricSpaceAdditive : {X : Type u_1} → [PseudoEMetricSpace X] → PseudoEMetricSpace (Additive X)
-- Lean.Message
/-- Structured success/failure result set by `withTraceNode`/`withTraceNodeBefore`.
`none` for trace nodes not created by these functions (e.g. `addTrace`, diagnostic nodes).  -/
Lean.TraceData.result? : Lean.TraceData → Option Lean.TraceResult
-- Mathlib.Topology.MetricSpace.IsometricSMul
Pi.isIsometricVAdd' : ∀ {ι : Type u_4} {M : ι → Type u_2} {X : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → VAdd (M i) (X i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricVAdd (M i) (X i)],
  IsIsometricVAdd ((i : ι) → M i) ((i : ι) → X i)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.map_right : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R),
  (d.map F).right i = F.obj (d.right i)
-- Mathlib.Analysis.Normed.Group.Bounded
Continuous.bounded_above_of_compact_support : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  Continuous f → HasCompactSupport f → ∃ C, ∀ (x : α), ‖f x‖ ≤ C
-- Mathlib.RingTheory.Localization.Free
/-- If `M` is a finitely presented `R`-module
such that `Mₛ` is free over `Rₛ` for some `S : Submonoid R`,
then `Mᵣ` is already free over `Rᵣ` for some `r ∈ S`.
 -/
Module.FinitePresentation.exists_free_localizedModule_powers : ∀ {R : Type u_4} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  {M' : Type u_1} [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  (Rₛ : Type u_3) [inst_6 : CommRing Rₛ] [inst_7 : Algebra R Rₛ] [inst_8 : Module Rₛ M'] [IsScalarTower R Rₛ M']
  [Nontrivial Rₛ] [IsLocalization S Rₛ] [Module.FinitePresentation R M] [Module.Free Rₛ M'],
  ∃ r ∈ S,
    Module.Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      Module.finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = Module.finrank Rₛ M'
-- Mathlib.Algebra.Free
FreeSemigroup.instDecidableEq.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (x x_1 : FreeSemigroup α),
  x.instDecidableEq x_1 = decidable_of_iff' (x.head = x_1.head ∧ x.tail = x_1.tail) ⋯
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i]
  [CategoryTheory.IsNoetherianObject Y], CategoryTheory.IsNoetherianObject X
-- Mathlib.Tactic.Positivity.Core
/-- A definition of type `PositivityExt` tagged `@[positivity t]` extends the `positivity` tactic.
The term (with underscores) `t` indicates which expressions this extension accepts.
An extension will be given an expression `e : α`, together with hypotheses
`[Zero α] [PartialOrder α]` and attempts to prove `e > 0`, `e ≥ 0`, or `e ≠ 0`.

When `Positivity.core` calls this extension on an expression `e`, it does not guarantee that `e`
matches `t` perfectly: validate the form of the expression (using e.g.
`match_expr (← withReducible (whnf e))`) before building a proof. See also the
`let .app ... ← withReducible (whnf e) | throwError ...` lines in the example below.

An extension can call `Mathlib.Meta.Positivity.core` to recursively solve subgoals.

Example:
```lean
@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα e := do
  let .app (.app (.app (.app f (p : Q(Prop))) (_ : Q(Decidable $p))) (a : Q($α))) (b : Q($α))
    ← withReducible (whnf e) | throwError "not ite"
  haveI' : $e =Q ite $p $a $b := ⟨⟩
  guard <| ← withDefault <| withNewMCtxDepth <| isDefEq f q(ite (α := $α))
  let ra ← core zα pα a; let rb ← core zα pα b
  ...
```
 -/
positivity : Lean.ParserDescr
-- Mathlib.GroupTheory.Coset.Basic
rightCoset_assoc : ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α),
  MulOpposite.op b • MulOpposite.op a • s = MulOpposite.op (a * b) • s
-- Mathlib.GroupTheory.Perm.List
List.support_formPerm_le' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), {x | l.formPerm x ≠ x} ⊆ ↑l.toFinset
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) (x : E),
  f.normed μ x = ↑f x / ∫ (x : E), ↑f x ∂μ
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The map `pr₁*` of the Stacks entry.  -/
CategoryTheory.Presheaf.secondMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {U : C} →
          (R : CategoryTheory.Presieve U) →
            (P : CategoryTheory.Functor Cᵒᵖ A) →
              [inst_2 : CategoryTheory.Limits.HasProducts A] →
                [inst_3 : CategoryTheory.Limits.HasPullbacks C] →
                  CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.of_comp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
      Q (g.comp f) → Q g) →
    ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (CategoryTheory.CategoryStruct.comp f g) → P f
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity.coe_mkOfPowEq : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {n : ℕ} [inst_1 : NeZero n] (h : ζ ^ n = 1),
  ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ
-- Mathlib.Data.Fintype.Sets
Set.toFinset_compl : ∀ {α : Type u_1} (s : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype α] [inst_3 : Fintype ↑sᶜ],
  sᶜ.toFinset = s.toFinsetᶜ
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.card_eq_of_mem_parts_equitabilise : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {m a b : ℕ} {P : Finpartition s}
  {h : a * m + b * (m + 1) = s.card}, t ∈ (Finpartition.equitabilise h).parts → t.card = m ∨ t.card = m + 1
-- Init.WF
WellFounded.Nat.fix.go_congr : ∀ {α : Sort u} {motive : α → Sort v} (h : α → ℕ)
  (F : (x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) (x : α) (fuel₁ fuel₂ : ℕ)
  (h₁ : h x < fuel₁) (h₂ : h x < fuel₂), WellFounded.Nat.fix.go h F fuel₁ x h₁ = WellFounded.Nat.fix.go h F fuel₂ x h₂
-- Mathlib.Algebra.Order.Module.Defs
smul_neg_iff_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β],
  0 < a → (a • b < 0 ↔ b < 0)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_neg : ∀ {h : ℝ} {f : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    Function.Periodic.cuspFunction h (-f) = -Function.Periodic.cuspFunction h f
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The neighbor finset of `v ∈ s` in `G.between s sᶜ` excludes the vertices in `s` adjacent to `v`
in `G`.  -/
SimpleGraph.neighborFinset_subset_between_union : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] {s : Finset V}
  [inst_2 : DecidableRel G.Adj], v ∈ s → G.neighborFinset v ⊆ (SimpleGraph.between (↑s) (↑s)ᶜ G).neighborFinset v ∪ s