mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A measurable subspace of a standard Borel space is standard Borel.  -/
MeasurableSet.standardBorel : ∀ {α : Type u_4} [inst : MeasurableSpace α] [StandardBorelSpace α] {s : Set α}, MeasurableSet s → StandardBorelSpace ↑s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_univ_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, 0 < μ Set.univ ↔ μ ≠ 0
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
  Measurable f → μ.withDensity (r • f) = r • μ.withDensity f
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddSemigroup : {α : Type u_1} → [AddSemigroup α] → AddSemigroup αᵃᵒᵖ
-- Lean.Meta.AppBuilder
/-- Returns `@Classical.ofNonempty α _`  -/
Lean.Meta.mkOfNonempty : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ◫ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalHorizontalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ →
      Mathlib.Tactic.BicategoryLike.Mor₂ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            (page : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r)) →
              ((r r' : ℤ) →
                  (pq : κ) →
                    (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
                      (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
                        (page r ⋯).homology pq ≅ (page r' ⋯).X pq) →
                CategoryTheory.SpectralSequence C c r₀
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_surjective : ∀ {α : Type u}, Function.Surjective FreeAddGroup.negRev
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.hasFDerivAt : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (f : E [⋀^ι]→L[𝕜] F) (x : ι → E), HasFDerivAt (⇑f) (f.linearDeriv x) x
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.foldl.match_1.eq_2 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (a : α) (b : β) (l : List β)
  (h_1 : (a : α) → motive a []) (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)),
  (match a, b :: l with
    | a, [] => h_1 a
    | a, b :: l => h_2 a b l) =
    h_2 a b l
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as a list in ascending order.
 -/
Std.Rcc.toList : {α : Type u} →
  [inst : LE α] →
    [DecidableLE α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Rcc α → List α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b) {Z : C} (h_1 : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp h.p₁ h_1) =
    CategoryTheory.CategoryStruct.comp g₁ h_1
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instCreatesColimitLocallyRingedSpaceWalkingMultispanProdJMultispanDiagramForgetToLocallyRingedSpace : (D : AlgebraicGeometry.Scheme.GlueData) →
  CategoryTheory.CreatesColimit D.diagram.multispan AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.applyS.tacticBuilder : Lean.MVarId → Lean.Expr → Option Lean.Term → Lean.Meta.TransparencyMode → Array Lean.MVarId → Aesop.Script.TacticBuilder
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.ext : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D}, F.toFunctor = G.toFunctor → F = G
-- Mathlib.Data.ULift
ULift.up_surjective : ∀ {α : Type u}, Function.Surjective ULift.up
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
measure_Ico_lt_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α}, μ (Set.Ico a b) < ⊤
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_injective : ∀ {α : Sort u_1} {β : Sort u_2}, Function.Injective fun f => ⇑f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.withAssertPurity : {α : Sort u_1} → [Inhabited α] → (is should : Lean.Compiler.LCNF.Purity) → (is = should → α) → α
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α} {init : β}
  {motive : ℕ → β → Prop} {f : β → α → m β},
  motive 0 init →
    (∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])) →
      SatisfiesM (motive as.size) (Array.foldlM f init as)
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.finiteDimensional_pi' : ∀ (K : Type u) [inst : DivisionRing K] {ι : Type u_1} [Finite ι] (M : ι → Type u_2)
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module K (M i)] [∀ (i : ι), FiniteDimensional K (M i)],
  FiniteDimensional K ((i : ι) → M i)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instAlternative : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Alternative (Std.Internal.Parsec ι)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The identity functor on `C`, viewed as a functor from the
monoidal opposite of `C` to `C`, upgraded to a braided functor.  -/
CategoryTheory.MonoidalOpposite.instBraidedUnmopFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.unmopFunctor C).Braided
-- Init.Data.UInt.Lemmas
instAssociativeUInt8HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.cardinalMk_le : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S],
  Cardinal.mk (OreLocalization S R) ≤ Cardinal.mk R
-- Lean.Meta.Structure
/-- Adds projection functions to the environment for the one-constructor inductive type named `n`.
- The `projName`s in each `StructProjDecl` are used for the names of the declarations added to the environment.
- If `instImplicit` is true, then generates projections with `self` being instance implicit.

Notes:
- This function supports everything that `Expr.proj` supports (see `lean::type_checker::infer_proj`).
  This means we can generate projections for inductive types with one-constructor,
  even if it is an indexed family (which is not supported by the `structure` command).
- We throw errors in the cases that `Expr.proj` is not type-correct.
 -/
Lean.Meta.mkProjections : Lean.Name → Array Lean.Meta.StructProjDecl → Bool → Lean.MetaM Unit
-- Std.Data.ExtDTreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtDTreeMap.Const.alter : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] →
        Std.ExtDTreeMap α (fun x => β) cmp → α → (Option β → Option β) → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsRingFiltration.toIsFiltration : ∀ {ι : Type u_1} (R : Type u_2) {σ : Type u_3} {inst : AddMonoid ι} {inst_1 : PartialOrder ι} {inst_2 : Preorder σ}
  {inst_3 : Semiring R} {inst_4 : SetLike σ R} {F : ι → σ} {F_lt : outParam (ι → σ)} [self : IsRingFiltration F F_lt],
  IsFiltration F F_lt
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzEvenFEPair_zero_symm : (HurwitzZeta.hurwitzEvenFEPair 0).symm = HurwitzZeta.hurwitzEvenFEPair 0
-- Mathlib.Topology.Connected.Basic
IsPreconnected.connectedComponentIn : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, IsPreconnected F → x ∈ F → connectedComponentIn F x = F
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.eq_snd_of_adj_start : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic → ∀ {u v w : V} {p : G.Walk u v}, p.IsPath → G.Adj u w → w ∈ p.support → w = p.snd
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The top `Submonoid` is isomorphic to the `Monoid`.  -/
Submonoid.topEquiv : {M : Type u_5} → [inst : MulOneClass M] → ↥⊤ ≃* M
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkHom_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor),
  CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom α) (CategoryTheory.Equivalence.mkHom β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Init.Data.Array.Attach
Array.pmap_append' : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs ys : Array α} (h₁ : ∀ a ∈ xs, p a)
  (h₂ : ∀ a ∈ ys, p a), Array.pmap f (xs ++ ys) ⋯ = Array.pmap f xs h₁ ++ Array.pmap f ys h₂
-- Mathlib.RingTheory.Kaehler.Basic
/-- The `S`-linear maps from `Ω[S⁄R]` to `M` are (`S`-linearly) equivalent to `R`-derivations
from `S` to `M`.  -/
KaehlerDifferential.linearMapEquivDerivation : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {M : Type u_1} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] → [inst_6 : IsScalarTower R S M] → (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Derivation R S M
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul : ∀ {R : Type u} [inst : CommRing R] (A : AlgCat R), CategoryTheory.MonObj.mul = ModuleCat.ofHom (LinearMap.mul' R ↑A)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimit.preservesLimit_eCoyoneda : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {V : outParam (Type u')}
  {inst_1 : CategoryTheory.Category.{v', u'} V} {inst_2 : CategoryTheory.MonoidalCategory V} {C : Type u}
  {inst_3 : CategoryTheory.Category.{v, u} C} {inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C}
  {F : CategoryTheory.Functor J C} [self : CategoryTheory.Enriched.HasConicalLimit V F] (X : C),
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.eCoyoneda V X)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.fvar.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId),
  sizeOf (Lean.Compiler.LCNF.Arg.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.obj'.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M : ModuleCat R),
  ModuleCat.ExtendScalars.obj' f M =
    ModuleCat.of S (TensorProduct R ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) ↑M)
-- Std.Async.System
Std.Async.System.instDecidableEqCPUInfo.decEq : (x x_1 : Std.Async.System.CPUInfo) → Decidable (x = x_1)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.clAddPrehaar.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ : Set G) (V : TopologicalSpace.OpenNhdsOf 0),
  MeasureTheory.Measure.haar.clAddPrehaar K₀ V =
    closure (MeasureTheory.Measure.haar.addPrehaar K₀ '' {U | U ⊆ ↑V.toOpens ∧ IsOpen U ∧ 0 ∈ U})
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal.congr_simp : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv =
    NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Smooth.finitePresentation : ∀ {R : Type u_4} {inst : CommRing R} {A : Type u} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.Smooth R A], Algebra.FinitePresentation R A
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_forall_one_lt_lt_mul' : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α]
  {a b : α} [MulLeftStrictMono α], a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_5.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : List Lean.Elab.InfoTree) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_6 t ×' Lean.Elab.InfoTree.below_5 t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiable_cosh : Differentiable ℂ Complex.cosh
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.Monic 1
-- Mathlib.GroupTheory.Perm.Support
/-- A permutation c is the extension of a restriction of g to s
iff its support is contained in s and its restriction is that of g  -/
Equiv.Perm.ofSubtype_eq_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α} {s : Finset α}
  (hg : ∀ (x : α), g x ∈ s ↔ x ∈ s),
  Equiv.Perm.ofSubtype (g.subtypePerm hg) = c ↔
    c.support ⊆ s ∧ ∀ (hc' : ∀ (x : α), c x ∈ s ↔ x ∈ s), c.subtypePerm hc' = g.subtypePerm hg
-- Mathlib.Data.UInt
UInt16.toBitVec_zsmul : ∀ (z : ℤ) (a : UInt16), (z • a).toBitVec = z • a.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.components_matrix : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : ⨁ f ⟶ ⨁ g),
  (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.Limits.biproduct.components m j k) = m
-- Batteries.Util.ProofWanted
/-- This construction would be a welcome contribution to the library!

The syntax mirrors `theorem_wanted` but admits any `Sort` (not just `Prop`). It accepts the same
`❰…❱` bracket syntax for cross-referencing earlier `theorem_wanted` or `def_wanted` declarations,
including parametrised ones — `❰foo❱ x y` applies `foo`'s parameters. A body without any `❰…❱`
reference is rejected with an actionable "Try this:" suggesting `def`.

A **bodyless** `def_wanted` records an opaque placeholder of type `... → DefWanted type` (a hole). A
`def_wanted` **with a body** is instead emitted as a genuine `@[reducible]` definition of type
`... → DerivedWanted type` (carrying the body), so `❰foo❱` inlines it and is definitionally equal to
its body — letting you derive honest accessors and data on top of opaque holes. The `DerivedWanted`
wrapper keeps it from being used directly as a value of `type`; only `❰…❱` accesses it. Either
way no `axiom`/`sorry` is introduced (see the module docstring).

Modifiers (such as `@[simp]`) are accepted for syntactic compatibility with `def` but are
currently ignored.

Typical usage:
```
def_wanted decision_procedure (n : Nat) : Decidable (Nat.Prime n)

def_wanted prime_dec_3 : Decidable (Nat.Prime 3) := ❰decision_procedure❱ 3
```
 -/
def_wanted : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.ofOption.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k),
  Std.DTreeMap.Internal.Cell.ofOption k (some v) = Std.DTreeMap.Internal.Cell.of k v
-- Lean.Parser.Do
/-- `termBeforeDo` is defined as `withForbidden("do", term)`, which will parse a term but
disallows `do` outside of a bracketing construct. This is used for parsers like `for _ in t do ...`
or `unless t do ...`, where we do not want `t do ...` to be parsed as an application of `t` to a
`do` block, which would otherwise be allowed.  -/
Lean.Parser.Term.termBeforeDo : Lean.Parser.Parser
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.self_mem_adjoin_singleton : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (x : A), x ∈ NonUnitalStarAlgebra.adjoin R {x}
-- Std.Http.Data.Status
/-- 100 Continue
 -/
Std.Http.Status.continue : Std.Http.Status
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filterM : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_14 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_16 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (ULift.{w, 0} Bool)} {init : γ}
  {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filterM f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.toIsQuotientMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → Topology.IsQuotientMap f
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.fromHex? : Char → Option ℕ
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match 0 with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.IsPositive 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon_obj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.NumberTheory.Multiplicity
not_dvd_geom_sum₂ : ∀ {R : Type u_1} {n : ℕ} [inst : CommRing R] {x y p : R},
  Prime p → p ∣ x - y → ¬p ∣ x → ¬p ∣ ↑n → ¬p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.mk.sizeOf_spec : ∀ {X : TopCat} {x y : ↑X} (hom : TopCat.I ⟶ X)
  (hom₀ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 0 = x) TopCat.Path.hom₀._autoParam)
  (hom₁ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 1 = y) TopCat.Path.hom₁._autoParam),
  sizeOf { hom := hom, hom₀ := hom₀, hom₁ := hom₁ } = 1 + sizeOf hom + sizeOf hom₀ + sizeOf hom₁
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.reachable_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β},
  (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates applications of "matchers" such as
```
List.map.match_1 : {α : Type _} →
  (motive : List α → Sort _) →
    (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
```
 -/
Lean.PrettyPrinter.Delaborator.delabAppMatch : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mk.injEq : ∀ {V : Type u} {G : SimpleGraph V} (verts : Set V) (Adj : V → V → Prop) (adj_sub : ∀ {v w : V}, Adj v w → G.Adj v w)
  (edge_vert : ∀ {v w : V}, Adj v w → v ∈ verts) (symm : autoParam (Std.Symm Adj) SimpleGraph.Subgraph.symm._autoParam)
  (verts_1 : Set V) (Adj_1 : V → V → Prop) (adj_sub_1 : ∀ {v w : V}, Adj_1 v w → G.Adj v w)
  (edge_vert_1 : ∀ {v w : V}, Adj_1 v w → v ∈ verts_1)
  (symm_1 : autoParam (Std.Symm Adj_1) SimpleGraph.Subgraph.symm._autoParam),
  ({ verts := verts, Adj := Adj, adj_sub := adj_sub, edge_vert := edge_vert, symm := symm } =
      { verts := verts_1, Adj := Adj_1, adj_sub := adj_sub_1, edge_vert := edge_vert_1, symm := symm_1 }) =
    (verts = verts_1 ∧ Adj = Adj_1)
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.head?_dropWhile_not.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive x
-- Lean.DocString.DeferredCheck
/-- The docstring or moduledoc in which the reference appears.  -/
Lean.Doc.DeferredCheck.site : Lean.Doc.DeferredCheck → Lean.Doc.DeferredCheckSite
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R x y = midpoint R y x
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.matchesAt_iff_matchesAt_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt c pos ↔ String.Slice.Pattern.Model.MatchesAt (fun x => x == c) pos
-- Mathlib.Data.Setoid.Basic
Setoid.symm' : ∀ {α : Type u_1} (r : Setoid α) {x y : α}, r x y → r y x
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformAddGroup.uniformity_eq : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : AddGroup G} [self : IsLeftUniformAddGroup G],
  uniformity G = Filter.comap (fun x => -x.1 + x.2) (nhds 0)