mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Basic
add_neg_eq_add_neg_iff_add_eq_add : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c d : G}, a + -b = c + -d ↔ a + d = c + b
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vsub_left_image : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, ⋃ a ∈ s, (fun x => a -ᵥ x) '' t = s -ᵥ t
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_one : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S), Polynomial.eval₂ f x 1 = 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rio_eq_self : ∀ {n i fallback : ℕ}, i < n → (*...n).toList.getD i fallback = i
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The set of points in a sphere is cospherical.  -/
EuclideanGeometry.Sphere.cospherical : ∀ {P : Type u_2} [inst : MetricSpace P] (s : EuclideanGeometry.Sphere P),
  EuclideanGeometry.Cospherical (Metric.sphere s.center s.radius)
-- Mathlib.Logic.Function.Basic
/-- A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`.  -/
Std.Symm.forall_existsUnique_iff : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r],
  (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion_self : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A}, NonUnitalSubalgebra.inclusion ⋯ = NonUnitalAlgHom.id R ↥S
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.φ₁ S.L₂.f = S.φ₂
-- Mathlib.Data.Real.Basic
Real.ofCauchy_div : ∀ (f g : CauSeq.Completion.Cauchy abs), { cauchy := f / g } = { cauchy := f } / { cauchy := g }
-- Init.Data.UInt.Lemmas
UInt16.ofNat_add : ∀ (a b : ℕ), UInt16.ofNat (a + b) = UInt16.ofNat a + UInt16.ofNat b
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The canonical pairing of a vector space and its algebraic dual.  -/
Module.dualPairing : (R : Type u_4) →
  (M : Type u_5) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Dual R M →ₗ[R] M →ₗ[R] R
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_singleton_natCast : ∀ {R : Type u} [inst : NonAssocSemiring R] (n : ℕ), Subsemiring.closure {↑n} = ⊥
-- Mathlib.FieldTheory.SeparableDegree
/-- `Field.Emb F E` is the type of `F`-algebra homomorphisms from `E` to the algebraic closure
of `E`.  -/
Field.Emb : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → Type v
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_of_injective : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι → κ),
  Function.Injective e →
    ∀ (f : ι → M) (g : κ → M), (∀ i ∉ Set.range e, g i = 0) → (∀ (i : ι), f i = g (e i)) → ∑ i, f i = ∑ j, g j
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The identity map as a continuous linear equivalence.  -/
ContinuousLinearEquiv.refl : (R₁ : Type u_1) →
  [inst : Semiring R₁] →
    (M₁ : Type u_4) →
      [inst_1 : TopologicalSpace M₁] → [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → M₁ ≃L[R₁] M₁
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.fstKernelFork_ι : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.biprod.fstKernelFork X Y) = CategoryTheory.Limits.biprod.inr
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_characteristic : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) [S.Characteristic] (n : ℕ), (S.lowerCentralSeries n).Characteristic
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I D : Set α}, (M.delete D).Indep I ↔ M.Indep I ∧ Disjoint I D
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.add : ∀ {M : Type u_1} {E : Type u_2} [inst : Bornology M] {s₁ s₂ t₁ t₂ : Set E} [inst_1 : AddZeroClass E]
  [inst_2 : DistribSMul M E], Absorbs M s₁ t₁ → Absorbs M s₂ t₂ → Absorbs M (s₁ + s₂) (t₁ + t₂)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} {f g : M ⟶ N}, f.hom = g.hom → f = g
-- Std.Sync.RecursiveMutex
/-- Recursive (or reentrant) mutual exclusion primitive (lock) guarding shared state of type `α`.

The type `RecursiveMutex α` is similar to `IO.Ref α`, except that concurrent accesses are guarded
by a mutex instead of atomic pointer operations and busy-waiting. Additionally locking a
`RecursiveMutex` multiple times from the same thread does not block, unlike `Mutex`.
 -/
Std.RecursiveMutex : Type → Type
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedBuiltinSimprocs : Inhabited Lean.Meta.Simp.BuiltinSimprocs
-- Mathlib.Data.Nat.Fib.Zeckendorf
_private.Mathlib.Data.Nat.Fib.Zeckendorf.0.Nat.zeckendorf_aux : ∀ {m : ℕ}, 0 < m → m - Nat.fib m.greatestFib < m
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : List ((_ : α) × β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (fst : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨fst, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨fst, v⟩ :: l => h_2 fst v l) =
    h_1 ()
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The counit cofork is a colimit provided `G` reflects it.  -/
CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer : {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} →
            (adj : F ⊣ G) →
              (B : D) →
                [CategoryTheory.Limits.ReflectsColimit
                      (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B)))
                        (adj.counit.app (F.obj (G.obj B))))
                      G] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The type of *double centralizers*, also known as the *multiplier algebra* and denoted by
`𝓜(𝕜, A)`, of a non-unital normed algebra.

If `x : 𝓜(𝕜, A)`, then `x.fst` and `x.snd` are what is usually referred to as $L$ and $R$.  -/
MultiplierAlgebra.«term𝓜(_,_)» : Lean.ParserDescr
-- Mathlib.Data.Finset.Grade
Multiset.instGradeMinOrder : {α : Type u_1} → GradeMinOrder ℕ (Multiset α)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (x : ↥P.ker),
  (Algebra.Extension.Cotangent.map f) (Algebra.Extension.Cotangent.mk x) =
    Algebra.Extension.Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limitCone_pt : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Mon.limitCone F c hc).pt = CategoryTheory.Mon.limit F c hc
-- Mathlib.Tactic.Spread
/-- Mathlib extension to preserve old behavior of structure instances.
We need to be able to `let` some implementation details that are still local instances.
Normally implementation detail fvars are not local instances,
but we need them to be implementation details so that `simp` will see them as "reducible" fvars.
 -/
letImplDetailStx : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.inf'_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeInf β]
  [inst_3 : ContinuousInf β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) (a : α),
  (s.inf' H f) a = s.inf' H fun i => (f i) a
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Iio x) x = sSup (slope f x '' {y | y ∈ S ∧ y < x})
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.hoFunctor.preservesTerminal' : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) SSet.hoFunctor
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l) =
      some ((Std.Internal.List.maxKey? l).elim k fun k' => if compare k' k = Ordering.lt then k else k')
-- Aesop.Rule
Aesop.instInhabitedRegularRule : Inhabited Aesop.RegularRule
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.nextParamIdx : Lean.Meta.AbstractMVars.State → ℕ
-- Mathlib.Analysis.Calculus.LocalExtr.Polynomial
/-- The number of real roots of a polynomial is at most the number of roots of its derivative plus
one.  -/
Polynomial.card_rootSet_le_derivative : ∀ {F : Type u_1} [inst : CommRing F] [inst_1 : Algebra F ℝ] (p : Polynomial F),
  Fintype.card ↑(p.rootSet ℝ) ≤ Fintype.card ↑((Polynomial.derivative p).rootSet ℝ) + 1
-- Lean.Compiler.ExternAttr
Lean.ExternAttrData.entries : Lean.ExternAttrData → List Lean.ExternEntry
-- Mathlib.SetTheory.ZFC.Class
Class.mem_sInter : ∀ {x y : Class.{u}}, Set.Nonempty x → (y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z)
-- Mathlib.Order.Category.HeytAlg
HeytAlg.instInhabited : Inhabited HeytAlg
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasStrictDerivAt.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasStrictDerivAt c c' x →
    HasStrictDerivAt d d' x → d x ≠ 0 → HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓRes_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G) (U : Cᵒᵖ),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.Γ J A).map f) (G.ΓRes U) =
    CategoryTheory.CategoryStruct.comp (F.ΓRes U) (f.hom.app U)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_XIsoBiprod_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv =
    HomologicalComplex.homotopyCofiber.inrX φ j
-- Mathlib.Topology.Algebra.GroupWithZero
continuousOn_inv₀ : ∀ {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀],
  ContinuousOn Inv.inv {0}ᶜ
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.span_coroot'_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsRootSystem],
  Submodule.span R (Set.range P.coroot') = ⊤
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens}
  (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map f))
      (CategoryTheory.CategoryStruct.comp hU.fromSpec h) =
    CategoryTheory.CategoryStruct.comp hV.fromSpec h
-- Init.Data.Fin.Lemmas
Fin.exists_fin_succ : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∃ i, P i) ↔ P 0 ∨ ∃ i, P i.succ
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- If the inverse of a Freiman homomorphism is itself a Freiman homomorphism, then it is a Freiman
isomorphism.
 -/
IsMulFreimanHom.to_isMulFreimanIso : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ} {g : β → α}, Set.InvOn g f A B → IsMulFreimanHom n A B f → IsMulFreimanHom n B A g → IsMulFreimanIso n A B f
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_ExceptT_eq.match_1_11.eq_2 : ∀ {α ρ : Type u_1} {p : α → Prop} (motive : { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a } → Sort u_2) (e : ρ)
  (property : ∀ (a : α), Except.error e = Except.ok a → p a)
  (h_1 : (a : α) → (h : ∀ (a_1 : α), Except.ok a = Except.ok a_1 → p a_1) → motive ⟨Except.ok a, h⟩)
  (h_2 : (e : ρ) → (property : ∀ (a : α), Except.error e = Except.ok a → p a) → motive ⟨Except.error e, property⟩),
  (match ⟨Except.error e, property⟩ with
    | ⟨Except.ok a, h⟩ => h_1 a h
    | ⟨Except.error e, property⟩ => h_2 e property) =
    h_2 e property
-- Mathlib.Data.Num.Lemmas
PosNum.cast_lt : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {m n : PosNum}, ↑m < ↑n ↔ m < n
-- Mathlib.Data.Set.Operations
/-- The Cartesian product `Set.prod s t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.  -/
Set.prod : {α : Type u} → {β : Type v} → Set α → Set β → Set (α × β)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ENat_card_ofStabilizer_add_zero_eq : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (a : α),
  ENat.card ↥(SubAddAction.ofStabilizer G a) + 1 = ENat.card α
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyClosed f],
  AlgebraicGeometry.UniversallyClosed (CategoryTheory.Limits.pullback.snd f g)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_1 ()
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mapCostly : {α : Type u_1} → {β : Type u_2} → (α → β) → Lean.Server.ServerTask α → Lean.Server.ServerTask β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`.  -/
Polynomial.Chebyshev.S_two_mul_complex_cos : ∀ (θ : ℂ) (n : ℤ),
  Polynomial.eval (2 * Complex.cos θ) (Polynomial.Chebyshev.S ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.cartan_eq : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [Fintype ι] [IsDomain R] [CharZero R]
  [Module.IsTorsionFree R L], H.toLieSubmodule = LieAlgebra.rootSpace H 0
-- Mathlib.Util.Notation3
/-- `notation3` declares notation using Lean-3-style syntax.

Examples:
```
notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => r
notation3 "MyList[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x
```
By default notation is unable to mention any variables defined using `variable`, but
`local notation3` is able to use such local variables.

Use `notation3 (prettyPrint := false)` to keep the command from generating a pretty printer
for the notation.

This command can be used in mathlib4 but it has an uncertain future and was created primarily
for backward compatibility.
 -/
Mathlib.Notation3.notation3 : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_pos : ∀ (e : ONote) (n : ℕ+) (a : ONote), 0 < e.oadd n a
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_dvd_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime y z → x ∣ y → IsRelPrime x z
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology : AlgebraicGeometry.Scheme.jointlySurjectiveTopology =
  AlgebraicGeometry.Scheme.jointlySurjectivePretopology.toGrothendieck
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_pair_subset : ∀ {α : Type u} {s : Set α} {x y : α}, x ≠ y → {x, y} ⊆ s → s.Nontrivial
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_eq_constantCoeff_apply : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), (PowerSeries.coeff 0) φ = PowerSeries.constantCoeff φ
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.pushout f g) Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.hom Q) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q) h
-- Mathlib.RingTheory.PowerBasis
PowerBasis.map_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {S' : Type u_7}
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S'),
  (pb.map e).basis = pb.basis.map ↑e
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new empty map.  -/
RBTree.RBMap.empty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.canLiftCardinalNat : CanLift Cardinal.{u_1} ℕ Nat.cast fun x => x < Cardinal.aleph0
-- Mathlib.Algebra.GroupWithZero.Action.Basic
smul_zpow₀' : ∀ {G : Type u_1} {G₀ : Type u_2} [inst : Group G] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G G₀]
  (g : G) (x : G₀) (n : ℤ), g • x ^ n = (g • x) ^ n
-- Mathlib.Order.Defs.Unbundled
/-- `Iff` is an equivalence relation.  -/
iff_isEquiv : IsEquiv Prop Iff
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
smul_finprod' : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : CommMonoid N] [inst_2 : MulDistribMulAction M N]
  {ι : Sort u_4} [Finite ι] {f : ι → N} (r : M), r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.coeMulHom_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  (self : { x // x ∈ Set.Ioo 0 1 }), Set.Ioo.coeMulHom self = ↑self
-- Mathlib.CategoryTheory.Monoidal.End
/-- Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
 -/
CategoryTheory.MonoidalCategory.instMonoidalFunctorTensoringRight : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.MonoidalCategory.tensoringRight C).Monoidal
-- Mathlib.Analysis.Normed.Module.MStructure
IsMprojection.mk : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsIdempotentElem P → (∀ (x : X), ‖x‖ = max ‖P • x‖ ‖(1 - P) • x‖) → IsMprojection X P
-- Mathlib.Data.Multiset.AddSub
/-- **Alias** of the reverse direction of `Multiset.add_le_add_iff_right`. -/
Multiset.add_le_add_right : ∀ {α : Type u_1} {s t u : Multiset α}, s ≤ t → s + u ≤ t + u
-- Std.Http.Protocol.H1
/-- Reader-side handling for `.readBody`.

When upper layers are not pulling body chunks, the machine drains body bytes
internally to keep parsing/connection progress moving.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processReadBodyState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Reader.BodyState → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Topology.Defs.Filter
/-- The *neighborhoods kernel* of a set is the intersection of all its neighborhoods. In an
Alexandrov-discrete space, this is the smallest neighborhood of the set.  -/
nhdsKer : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
Algebra.isSeparable_residueField_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  {q : Ideal B} [inst_3 : q.LiesOver p] [inst_4 : p.IsMaximal] [inst_5 : q.IsMaximal]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q],
  Algebra.IsSeparable p.ResidueField q.ResidueField ↔ Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_inv_τ₃ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₃ = (K.restrictionXIso e hk').inv
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs
`⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂` (given by `IsFiltered.max`)
and multiply them there.
 -/
MonCat.FilteredColimits.colimitMulAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) →
      [CategoryTheory.IsFiltered J] → (j : J) × ↑(F.obj j) → (j : J) × ↑(F.obj j) → MonCat.FilteredColimits.M F
-- Lean.Elab.Command
Lean.Elab.Command.modifyScope : (Lean.Elab.Command.Scope → Lean.Elab.Command.Scope) → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.instCoalgebra : {R : Type u} → [inst : CommRing R] → (self : CoalgCat R) → Coalgebra R ↑self.toModuleCat