mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_div : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  interior s / interior t ⊆ interior (s / t)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.insertManyIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l l_1 : ρ),
  l = l_1 → ∀ (h : t.Balanced), t.insertManyIfNew l h = t.insertManyIfNew l_1 h
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.lift₂Expand_of : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_3}
  [inst_2 : AddAction R X] {C : Sort u_2} {P : X → ↥S → X → ↥S → C}
  {hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩}
  (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S), AddOreLocalization.lift₂Expand P hP (r₁ -ₒ s₁) (r₂ -ₒ s₂) = P r₁ s₁ r₂ s₂
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- The canonical equivalence between `C⋆ᵐᵒᵈ(A, E)` and `E`. This should always be used to
convert back and forth between the representations.  -/
WithCStarModule.equiv : (A : Type u_3) → (E : Type u_4) → WithCStarModule A E ≃ E
-- Mathlib.Algebra.Order.Sum
Sum.one_le_elim_iff : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [inst : LE β] [inst_1 : One β] {v₁ : α₁ → β} {v₂ : α₂ → β},
  1 ≤ Sum.elim v₁ v₂ ↔ 1 ≤ v₁ ∧ 1 ≤ v₂
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.coe_path : ∀ (x y : Circle), ⇑(x.path y) = ⇑Circle.exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))
-- Mathlib.Data.List.Lemmas
List.mapAccumr_eq_foldr : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} (f : α → σ → σ × β) (as : List α) (s : σ),
  List.mapAccumr f as s =
    List.foldr
      (fun a s =>
        have r := f a s.1;
        (r.1, r.2 :: s.2))
      (s, []) as
-- Mathlib.Data.Fin.Basic
Fin.natCast_lt_natCast : ∀ {n a b : ℕ}, a ≤ n → b ≤ n → (↑a < ↑b ↔ a < b)
-- Mathlib.Analysis.Real.Pi.Irrational
irrational_pi : Irrational Real.pi
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp s.inl (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.smul_fin3 : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) (u : R), u • P = ![u * P 0, u * P 1, u * P 2]
-- Mathlib.Algebra.Order.Ring.Archimedean
/-- See `mk_map_of_archimedean'` for a version taking `M →+*o R`.  -/
ArchimedeanClass.mk_map_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+o R) {x : S},
  x ≠ 0 → ArchimedeanClass.mk (f x) = ArchimedeanClass.mk (f 1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (D.ι i)
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.eq_1 : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (g : ι → β)
  (s : Set ι), MonovaryOn f g s = ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f i ≤ f j
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearEquiv_symm : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearEquiv e).symm = DFinsupp.mapRange.linearEquiv fun i => (e i).symm
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.ofSign.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (s : ℤˣ), Equiv.Perm.ofSign s = {x | Equiv.Perm.sign x = s}
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityCounit_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C)
  (c : CategoryTheory.Limits.Cocone (K.comp F)), ((adj.functorialityCounit K).app c).hom = adj.counit.app c.pt
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The image of an affine subspace under an affine map as an affine subspace.  -/
AffineSubspace.map : {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 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : AddCommGroup V₂] →
                    [inst_5 : Module k V₂] →
                      [inst_6 : AddTorsor V₂ P₂] → (P₁ →ᵃ[k] P₂) → AffineSubspace k P₁ → AffineSubspace k P₂
-- Mathlib.Topology.Constructions.SumProd
/-- Postcomposing `f` with `Prod.fst` is continuous at `x`  -/
ContinuousAt.fst : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y × Z} {x : X}, ContinuousAt f x → ContinuousAt (fun x => (f x).1) x
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum is finite iff all terms are finite.  -/
WithBot.bot_lt_sum_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M} [inst_1 : LT M],
  ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalReplace : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Order
Subsingleton.discreteTopology : ∀ {α : Type u} [t : TopologicalSpace α] [Subsingleton α], DiscreteTopology α
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.coe_lTensor : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] (f : N →ₗ[R] Q),
  ⇑((TensorProduct.AlgebraTensorModule.lTensor A M) f) = ⇑(LinearMap.lTensor M f)
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_min : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : LinearOrder M] (f g : α → M),
  (Function.support fun x => min (f x) (g x)) ⊆ Function.support f ∪ Function.support g
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- The second resolvent identity: for `r` in the resolvent set of both
`a` and `b`,
`resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r`.  -/
spectrum.resolvent_sub_resolvent : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a b : A} {r : R},
  r ∈ resolventSet R a → r ∈ resolventSet R b → resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.CompatibleRing.mk : {R : Type u_2} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      [inst_2 : Neg R] →
        [inst_3 : One R] →
          [inst_4 : Zero R] →
            [toStructure : FirstOrder.Language.ring.Structure R] →
              (∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1) →
                (∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1) →
                  (∀ (x : Fin 1 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0) →
                    (∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0) →
                      (∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1) →
                        FirstOrder.Ring.CompatibleRing R
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
prime, then the norm of `zeta (p ^ (k + 1)) K L - 1` is `p`.  -/
IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two : ∀ {p : ℕ} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ}
  [inst_3 : Fact (Nat.Prime p)] [inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L],
  Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
    p ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = ↑p
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp (e.hom.app X.left) X.hom
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {g' : β → α}, HasProdUniformlyOn f g s → Set.EqOn g g' s → HasProdUniformlyOn f g' s
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication.  -/
MulAction.automorphize_smul_left : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [T2Space M]
  {R : Type u_12} [inst_3 : DivisionRing R] [inst_4 : Module R M] [ContinuousConstSMul R M] [inst_6 : Group α]
  [inst_7 : MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R),
  MulAction.automorphize (g ∘ Quotient.mk' • f) = g • MulAction.automorphize f
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.splitter : {β : Type u_3} →
  {γ : Type u_1} →
    {init : γ} →
      (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out init) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out init)) →
              ((c : γ) →
                  (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩) →
                ((c : γ) →
                    (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩) →
                  motive __do_lift
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_iff_mul_fg : ∀ {H : Type u_4} [inst : AddGroup H], AddGroup.FG H ↔ Group.FG (Multiplicative H)
-- Lean.DocString.Types
Lean.Doc.Inline.text.inj : ∀ {i : Type u} {string string_1 : String},
  Lean.Doc.Inline.text string = Lean.Doc.Inline.text string_1 → string = string_1
-- Init.Data.Float.Float
/-- Obtains the `Float` whose value is the same as the given `UInt32`.  -/
UInt32.toFloat : UInt32 → Float
-- Mathlib.Order.Types.Defs
OrderType.type_lt_type : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β] (h : α ↪o β),
  IsEmpty (β ↪o α) → OrderType.type α < OrderType.type β
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.normalizedChainComplexFunctorObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (R : C) (X : SSet),
  (SSet.normalizedChainComplexFunctorObj R).obj X = X.normalizedChainComplex R
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- A version of `WithTop.coe_sSup'` with a more convenient but less general statement.  -/
WithTop.coe_sSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
-- Mathlib.Order.BoundedOrder.Basic
ne_top_of_le_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, b ≠ ⊤ → a ≤ b → a ≠ ⊤
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.qcPrecoverage.eq_1 : AlgebraicGeometry.Scheme.qcPrecoverage = AlgebraicGeometry.Scheme.qcCoverFamily.precoverage
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.eqLocus_same : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  f.eqLocus f = ⊤
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.mem_gen : ∀ {α : Type u_1} {β : Type u_5} {f g : UniformFun α β} {V : Set (β × β)},
  (f, g) ∈ UniformFun.gen α β V ↔ ∀ (x : α), (UniformFun.toFun f x, UniformFun.toFun g x) ∈ V
-- Mathlib.Order.JordanHolder
CompositionSeries.head_le_of_mem : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x : X},
  x ∈ s → RelSeries.head s ≤ x
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_smul : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (t : R) (m : ↥N), ↑(t • m) = t • ↑m
-- Init.Data.String.Defs
String.endExclusive_toSlice : ∀ {s : String}, s.toSlice.endExclusive = s.endPos
-- Mathlib.Data.Finset.Sups
Finset.disjSups_union_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t₁ t₂ : Finset α}, s.disjSups (t₁ ∪ t₂) = s.disjSups t₁ ∪ s.disjSups t₂
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- An odd Dirichlet character is an odd function.  -/
DirichletCharacter.Odd.to_fun : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} {χ : DirichletCharacter S m}, χ.Odd → Function.Odd ⇑χ
-- Init.Data.Array.Extract
Array.extract_reverse : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, as.reverse.extract i j = (as.extract (as.size - j) (as.size - i)).reverse
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCancelMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddCancelMonoid Mᵃᵒᵖ], DomAddAct.instAddCancelMonoidOfAddOpposite = inst
-- Lean.Elab.InfoTree.Main
_private.Lean.Elab.InfoTree.Main.0.Lean.Elab.withSavedPartialInfoContext : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadInfoTree m] → {α : Type} → [MonadFinally m] → m α → m (Option Lean.Elab.PartialContextInfo) → m α
-- Lean.Expr
Lean.isPatternWithRef : Lean.Expr → Bool
-- Lean.Data.Position
Lean.FileMap.mk : String → Array String.Pos.Raw → Lean.FileMap
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.top_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (s : NonUnitalSubsemiring S), ⊤.prod s = NonUnitalSubsemiring.comap (NonUnitalRingHom.snd R S) s
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.eval_at_0 : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ), Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0
-- Mathlib.Topology.Order.Bornology
Bornology.IsCobounded.eq_1 : ∀ {α : Type u_2} [inst : Bornology α] (s : Set α), Bornology.IsCobounded s = (s ∈ Bornology.cobounded α)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
-- Mathlib.Data.Tree.Basic
BinaryTree.numLeaves.eq_1 : ∀ {α : Type u}, BinaryTree.nil.numLeaves = 1
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Lean.Parser.Basic
/-- Each parser category is implemented using a Pratt's parser.
The system comes equipped with the following categories: `level`, `term`, `tactic`, and `command`.
Users and plugins may define extra categories.

The method
```
categoryParser `term prec
```
executes the Pratt's parser for category `term` with precedence `prec`.
That is, only parsers with precedence at least `prec` are considered.
The method `termParser prec` is equivalent to the method above.
 -/
Lean.Parser.ParserCategory : Type
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.div : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedDivisionRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'}, MDiffAt p z → MDiffAt q z → q z ≠ 0 → MDiffAt (p / q) z
-- Mathlib.RingTheory.Conductor
/-- The canonical morphism of rings from `R<x> ⧸ (I*R<x>)` to `S ⧸ (I*S)` is an isomorphism
when `I` and `(conductor R x) ∩ R` are coprime.  -/
quotAdjoinEquivQuotMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {x : S} →
            {I : Ideal R} →
              Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                Function.Injective ⇑(algebraMap (↥R[x]) S) →
                  ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I ≃+* S ⧸ Ideal.map (algebraMap R S) I
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_denote_mem_prefix : ∀ {w : ℕ} {inv : Bool} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign.toAIGAssignment,
      { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Topology.Separation.Basic
nhds_le_nhdsSet_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X} {x : X}, nhds x ≤ nhdsSet s ↔ x ∈ s
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsConnected (Set.Ici a)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- A strong transformation between pseudofunctors `F` and `G` is a natural transformation
that is "natural up to 2-isomorphisms".
More precisely, it consists of the following:
* a 1-morphism `η.app a : F.obj a ⟶ G.obj a` for each object `a : B`.
* a 2-isomorphism `η.naturality f : F.map f ≫ app b ≅ app a ≫ G.map f` for each 1-morphism
  `f : a ⟶ b`.
* These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the
  compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Pseudofunctor.StrongTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.Pseudofunctor B C → CategoryTheory.Pseudofunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₂ = CategoryTheory.kernelCokernelCompSequence.π f g
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_compl : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), ↑s.compl = (↑s)ᶜ
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.coconeOfRepresentable_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
  (x : P.Elementsᵒᵖ),
  (CategoryTheory.Presheaf.coconeOfRepresentable P).ι.app x = CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.ArgReorder.toString.eq_def : ∀ (r : Mathlib.Tactic.Translate.ArgReorder),
  r.toString =
    have perm := List.map (fun x => " ".intercalate (List.map (fun x => toString (x + 1)) ↑x)) r.perm;
    have argReorders :=
      Array.map (fun x => toString (x.1 + 1) ++ toString " (" ++ toString x.2.toString ++ toString ")") r.argReorders;
    toString (", ".intercalate (perm ++ argReorders.toList))
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm1b : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_w : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.w✝ S
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instTopOfZero : {M : Type u_1} → [Zero M] → [inst : Monoid M] → Top (Associates M)
-- Mathlib.LinearAlgebra.LinearPMap
/-- The inverse of a `LinearPMap`.  -/
LinearPMap.inverse : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} → [inst_3 : AddCommGroup F] → [inst_4 : Module R F] → (E →ₗ.[R] F) → F →ₗ.[R] E
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Init.Notation
/-- The `run_elab doSeq` command executes code in `TermElabM Unit`.
This is the same as `#eval show TermElabM Unit from discard do doSeq`.
 -/
Lean.runElab : Lean.ParserDescr
-- Mathlib.Tactic.NormNum.BigOperators
/-- This represents the result of trying to determine whether the given expression
`s : Q(List $α)` is either empty or consists of an element inserted into a strict subset.  -/
Mathlib.Meta.List.ProveNilOrConsResult : {u : Lean.Level} → {α : Q(Type u)} → Q(List «$α») → Type
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- The map from the image of the `GoodProducts` in `LocallyConstant (π C (ord I · < o)) ℤ` to
`smaller C o`
 -/
Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        (o : Ordinal.{u}) →
          ↑(Profinite.NobelingProof.GoodProducts.range
                (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) →
            ↑(Profinite.NobelingProof.GoodProducts.smaller C o)