mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function with bounded range
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.

The assumption `BddAbove (range f)` can be omitted,
if the codomain of `f` is a conditionally complete linear order or a complete lattice, see below.
 -/
Monotone.ciSup_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → BddAbove (Set.range f) → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib.CategoryTheory.Comma.Arrow
/-- `isoMk'''` is the dual of `isoMk'`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Arrow.isoMk''' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {W X Y Z : T} →
      (f : X ⟶ W) →
        (g : Z ⟶ Y) →
          (e₁ : W ≅ Y) →
            (e₂ : X ≅ Z) →
              autoParam (CategoryTheory.CategoryStruct.comp g e₁.inv = CategoryTheory.CategoryStruct.comp e₂.inv f)
                  CategoryTheory.Arrow.isoMk'''._auto_1 →
                (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g)
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.instInhabitedImpl.default : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β
-- Init.Data.List.Lemmas
List.forall_mem_nil : ∀ {α : Type u_1} (p : α → Prop), ∀ x ∈ [], p x
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sumIsoExt_inv_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor (A ⊕ B) C}
  (e₁ : (CategoryTheory.Sum.inl_ A B).comp F ≅ (CategoryTheory.Sum.inl_ A B).comp G)
  (e₂ : (CategoryTheory.Sum.inr_ A B).comp F ≅ (CategoryTheory.Sum.inr_ A B).comp G) (a : A),
  (CategoryTheory.Functor.sumIsoExt e₁ e₂).inv.app (Sum.inl a) = e₁.inv.app a
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaIsoCoyoneda_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  CategoryTheory.shrinkCoyonedaIsoCoyoneda.hom.app X =
    (CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.toIocMod_arg : ∀ (z : ℂ), toIocMod Real.two_pi_pos (-Real.pi) z.arg = z.arg
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.all : Substring.Raw → (Char → Bool) → Bool
-- Mathlib.Topology.Order.Lattice
Continuous.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}, Continuous f → Continuous g → Continuous (f ⊔ g)
-- Mathlib.Data.Finset.Union
Finset.biUnion_biUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq γ] (s : Finset α)
  (f : α → Finset β) (g : β → Finset γ), (s.biUnion f).biUnion g = s.biUnion fun a => (f a).biUnion g
-- Mathlib.Probability.Kernel.Category.Stoch
instDeterministicSFinKerHomWideSubcategoryStochHomOfStoch : ∀ {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ], CategoryTheory.Deterministic κ.hom
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.step.match_5.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Γ] (motive : Turing.TM0.Cfg Γ Λ → Sort u_3) (q : Λ)
  (T : Turing.Tape Γ) (h_1 : (q : Λ) → (T : Turing.Tape Γ) → motive { q := q, Tape := T }),
  (match { q := q, Tape := T } with
    | { q := q, Tape := T } => h_1 q T) =
    h_1 q T
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.sum_apply_ne_zero_iff_eq_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [inst_1 : Finite α], ∑ ψ, ψ a ≠ 0 ↔ a = 0
-- Mathlib.Data.Set.Image
Set.preimage_compl_eq_image_compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (s : Set α), compl ⁻¹' s = compl '' s
-- Mathlib.Algebra.Group.Shrink
Shrink.instNeg.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Neg α], Shrink.instNeg = (equivShrink α).symm.Neg
-- Mathlib.CategoryTheory.Limits.Sifted
/-- If `C` is sifted, the `colim` functor `(C ⥤ Type) ⥤ Type` preserves finite products.  -/
CategoryTheory.IsSifted.colim_preservesFiniteProducts_of_isSifted : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C],
  CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Identity map as a diffeomorphism.  -/
Diffeomorph.refl : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_5} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_9) →
                  [inst_4 : TopologicalSpace M] → [inst_5 : ChartedSpace H M] → (n : WithTop ℕ∞) → Diffeomorph I I M M n
-- Init.Data.BitVec.Lemmas
BitVec.replicate.eq_1 : ∀ {w : ℕ} (x : BitVec w), BitVec.replicate 0 x = 0#0
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingDownNat_f : ∀ (n : ℕ), ComplexShape.embeddingDownNat.f n = -↑n
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.symm : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x y : X), S.toSetoid x y → S.toSetoid y x
-- Init.Data.List.Basic
List.zipIdx_nil : ∀ {α : Type u} {i : ℕ}, [].zipIdx i = []
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Conformal.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y]
  [inst_2 : NormedAddCommGroup Z] [inst_3 : NormedSpace ℝ X] [inst_4 : NormedSpace ℝ Y] [inst_5 : NormedSpace ℝ Z]
  {f : X → Y} {g : Y → Z}, Conformal f → Conformal g → Conformal (g ∘ f)
-- Batteries.Data.List.Basic
List.dropSliceTR.eq_2 : ∀ {α : Type u_1} (n : ℕ) (l : List α) (m_2 : ℕ), List.dropSliceTR n m_2.succ l = List.dropSliceTR.go l m_2 l n #[]
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.boundedSpace_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α], BoundedSpace α ↔ ∃ C, ∀ (a b : α), dist a b ≤ C
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
/-- **Alias** of `SimpleGraph.cycleGraph.cycle`.

---

The Eulerian cycle of `cycleGraph (n + 3)`  -/
SimpleGraph.cycleGraph_EulerianCircuit : (n : ℕ) → (SimpleGraph.cycleGraph (n + 3)).Walk 0 0
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The assumption that a localized category for
`(HomologicalComplex.quasiIso C (ComplexShape.up ℤ))` has been chosen, and that the morphisms
in this chosen category are in `Type w`.  -/
HasDerivedCategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → Type (max (max ((max u v) + 1) v) (w + 1))
-- Mathlib.Data.Prod.Basic
Prod.mk.injArrow : {α : Type u_1} →
  {β : Type u_2} →
    {x₁ : α} → {y₁ : β} → {x₂ : α} → {y₂ : β} → (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_5⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P
-- Init.Data.List.Sort.Lemmas
List.cons_merge_cons_neg : ∀ {α : Type u_1} {a b : α} (s : α → α → Bool) (l r : List α),
  ¬s a b = true → (a :: l).merge (b :: r) s = b :: (a :: l).merge r s
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.seminormedAddCommGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F],
  Prod.seminormedAddCommGroup =
    { toNorm := Prod.seminormedAddGroup.toNorm, toAddGroup := Prod.seminormedAddGroup.toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := Prod.seminormedAddGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq.eq_2 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω_2 : List B),
  cs.leftInvSeq (i :: ω_2) = cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω_2)
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- `Real.log` is strictly concave on `(0, +∞)`.  -/
strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Set.Ioi 0) Real.log
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.uniq_cone_morphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t)
  {f f' : s ⟶ t}, f = f'
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_Ioc : ∀ {f : ℝ → ℝ} {y z : ℝ}, ConvexOn ℝ (Set.Ioc y z) f → ContinuousWithinAt f (Set.Iic z) z → ContinuousOn f (Set.Ioc y z)
-- Mathlib.Data.Finmap
Finmap.erase_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {s : Finmap β},
  Finmap.erase a (Finmap.erase a' s) = Finmap.erase a' (Finmap.erase a s)
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The `totalDegree` of a multivariable polynomial `p` is at least `i` more than the `totalDegree` of
the `i`th coefficient of `finSuccEquiv` applied to `p`, if this is nonzero.
 -/
MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ),
  ((MvPolynomial.finSuccEquiv R n) f).coeff i ≠ 0 →
    (((MvPolynomial.finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
-- Mathlib.GroupTheory.OrderOfElement
SemiconjBy.orderOf_eq : ∀ {G : Type u_1} [inst : Group G] (a : G) {x y : G}, SemiconjBy a x y → orderOf x = orderOf y
-- Mathlib.Tactic.Sat.FromLRAT
/-- `v.implies p [a, b, c] 0` definitionally unfolds to `(v 0 ↔ a) → (v 1 ↔ b) → (v 2 ↔ c) → p`.
This is used to introduce assumptions about the first `n` values of `v` during reification.  -/
Sat.Valuation.implies : Sat.Valuation → Prop → List Prop → ℕ → Prop
-- Std.Http.Data.Body.Stream
/-- Checks whether the channel is closed.
 -/
Std.Http.Body.Stream.isClosed : Std.Http.Body.Stream → Std.Async.Async Bool
-- Std.Internal.UV.System
/-- Unsets an environment variable.
 -/
Std.Internal.UV.System.osUnsetenv : String → IO Unit
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerived_ext : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (γ₁ γ₂ : RF ⟶ G),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft γ₁) = CategoryTheory.CategoryStruct.comp α (L.whiskerLeft γ₂) →
    γ₁ = γ₂
-- Mathlib.Data.List.Nodup
/-- **Alias** of the reverse direction of `List.nodup_mergeSort`. -/
List.Nodup.mergeSort : ∀ {α : Type u} {l : List α} {le : α → α → Bool}, l.Nodup → (l.mergeSort le).Nodup
-- Mathlib.Algebra.Free
/-- The head of the element  -/
FreeAddSemigroup.head : {α : Type u} → FreeAddSemigroup α → α
-- Mathlib.Analysis.Calculus.Deriv.Support
support_deriv_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, Function.support (deriv f) ⊆ tsupport f
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.map_vadd : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁),
  e (v +ᵥ p) = e.linear v +ᵥ e p
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_eq_prevn_toSlice : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.prevn n = String.Pos.ofToSlice (p.toSlice.prevn n)
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Equivalence.mapHomologicalComplex_functor : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [inst_4 : e.functor.PreservesZeroMorphisms]
  (c : ComplexShape ι), (e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_center_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⁅H, Subgroup.center G⁆ = ⊥
-- Init.Data.SInt.Bitwise
USize.toISize_xor : ∀ (a b : USize), (a ^^^ b).toISize = a.toISize ^^^ b.toISize
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableWithinAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x →
    DifferentiableWithinAt ℂ g s x → f x ∈ Complex.slitPlane → DifferentiableWithinAt ℂ (fun x => f x ^ g x) s x
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkspaceEdit.toJson : Lean.Lsp.WorkspaceEdit → Lean.Json
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- Given a cofan of a functor to types, this is a canonical map
from the Sigma type to the point of the cofan.  -/
CategoryTheory.Limits.CofanTypes.fromSigma : {C : Type u} → (F : C → Type v) → (c : CategoryTheory.Limits.CofanTypes F) → (i : C) × F i → c.pt
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.coeLM_apply : ∀ (𝕜 : Type u_3) [inst : NormedField 𝕜] (E : Type u_7) (F : Type u_8) [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup F] [inst_4 : TopologicalSpace F]
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] [inst_8 : ContinuousConstSMul 𝕜 F]
  (self : E →L[𝕜] F), (PointwiseConvergenceCLM.coeLM 𝕜 E F) self = ↑self
-- Mathlib.Data.Set.Function
Set.exists_eq_graphOn : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)}, (∃ f t, s = Set.graphOn f t) ↔ Set.InjOn Prod.fst s
-- Init.Data.Array.Basic
/-- Constructs a single-element array that contains `v`.

Examples:
* `Array.singleton 5 = #[5]`
* `Array.singleton "one" = #["one"]`
 -/
Array.singleton : {α : Type u} → α → Array α
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylorEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (r : R), (Polynomial.taylorEquiv r).symm = Polynomial.taylorEquiv (-r)
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- The canonical ring map from `R` to the explicit equalizer of
`includeLeft : S ⟶ S ⊗[R] S` and `includeRight : S ⟶ S ⊗[R] S`.  -/
Algebra.codRestrictEqLocusPushoutCocone : (R S : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : Algebra R S] →
        R →+*
          ↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.offset_of_isLongestMatchAt : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat ≠ "" →
    String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ → pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_toBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E), ⇑b.toBasis = ⇑b
-- Lean.Meta.BinderNameHint
/-- Resolves occurrences of `binderNameHint` in `e`. See docstring of `binderNameHint` for more
information.
 -/
Lean.Expr.resolveBinderNameHint : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A kernel-preserving functor between preadditive categories preserves binary products.  -/
CategoryTheory.Functor.preservesBinaryProducts_of_preservesKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.cond : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E},
  MeasureTheory.pdf.IsUniform id s μ[|s] μ
-- Mathlib.GroupTheory.Congruence.Defs
/-- Extensionality rule for additive congruence relations.  -/
AddCon.ext : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, (∀ (x y : M), c x y ↔ d x y) → c = d
-- Init.Grind.Attr
/-- The `usr` modifier indicates that this theorem was applied using a
**user-defined instantiation pattern**. Such patterns are declared with
the `grind_pattern` command, which lets you specify how `grind` should
match and use particular theorems.

Example:
- `grind [usr myThm]` means `grind` is using `myThm`, but with
  the custom pattern you defined with `grind_pattern`.
 -/
Lean.Parser.Attr.grindUsr : Lean.ParserDescr
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.mul : Nat.Primrec' fun v => v.head * v.tail.head
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.mk.inj : ∀ {ι : Type u_1} {faces : Set (Finset ι)} {isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty}
  {faces_1 : Set (Finset ι)} {isRelLowerSet_faces_1 : IsRelLowerSet faces_1 Finset.Nonempty},
  { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces } =
      { faces := faces_1, isRelLowerSet_faces := isRelLowerSet_faces_1 } →
    faces = faces_1
-- Mathlib.Analysis.Convex.Gauge
Convex.lipschitz_gauge : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → s ∈ nhds 0 → ∃ K, LipschitzWith K (gauge s)
-- Mathlib.Topology.Order.OrderClosed
CovBy.nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a ⋖ b → nhdsWithin b (Set.Iio b) = ⊥
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- A split group extension is equivalent to the extension associated to a semidirect product.  -/
GroupExtension.Splitting.semidirectProductToGroupExtensionEquiv : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] →
        {E : Type u_3} →
          [inst_2 : Group E] →
            {S : GroupExtension N E G} → (s : S.Splitting) → (SemidirectProduct.toGroupExtension s.conjAct).Equiv S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase!_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ∀ {fallback : α},
          (compare ((Std.DTreeMap.Internal.Impl.erase! k t).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝 x₀`) on the spectrum of `a`,
and each `f x` is continuous on the spectrum of `a` and maps zero to itself, then
`fun x ↦ cfcₙ (f x) a` is continuous at `x₀`.  -/
continuousAt_cfcₙ_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : SMulCommClass R A A] [inst_11 : IsScalarTower R A A]
  [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] [inst_13 : TopologicalSpace X] {f : X → R → R} {a : A}
  {x₀ : X},
  TendstoUniformlyOn f (f x₀) (nhds x₀) (quasispectrum R a) →
    (∀ᶠ (x : X) in nhds x₀, ContinuousOn (f x) (quasispectrum R a)) →
      (∀ᶠ (x : X) in nhds x₀, f x 0 = 0) → ContinuousAt (fun x => cfcₙ (f x) a) x₀
-- Init.Data.List.Basic
/-- Counts the number of times an element occurs in a list.

Examples:
* `[1, 1, 2, 3, 5].count 1 = 2`
* `[1, 1, 2, 3, 5].count 5 = 1`
* `[1, 1, 2, 3, 5].count 4 = 0`
 -/
List.count : {α : Type u} → [BEq α] → α → List α → ℕ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [Nonempty α] → Top (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.subset_interior : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) ⦃m n : ℕ⦄, m < n → K m ⊆ interior (K n)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.Balanced) (x_2 : ℕ) (x_3 : x_2 < x.size)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
              (n : ℕ) →
                (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                  motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h)
  (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
  (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
  x = Std.DTreeMap.Internal.Impl.inner size k v l' r' →
    x_1 ≍ hl →
      x_2 = n →
        x_3 ≍ h →
          (match x, x_1, x_2, x_3 with
            | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h => h_1 size k v l' r' hl n h) ≍
            h_1 size k v l' r' hl n h
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.mk : Lean.Name →
  List Lean.Name →
    Lean.Expr →
      Lean.Expr →
        Array Lean.Name →
          Lean.Name →
            Lean.Elab.FixedParamPerms → Array Lean.Elab.PartialFixpointType → Lean.Elab.PartialFixpoint.EqnInfo
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_sup_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S T : Submodule R M} {x : M}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithTop.map` for `AddHom`s.  -/
AddHom.withTopMap : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → WithTop M →ₙ+ WithTop N
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : ↥(Unitization.unitsFstOne R A)),
  ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x) = PreQuasiregular.equiv (↑↑x).toProd.2
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
 -/
Padic : (p : ℕ) → [Fact (Nat.Prime p)] → Type
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_3.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Stream'.Seq1 α)) → Sort u_2) (a : α) (s : Stream'.Seq α)
  (S' : Stream'.Seq (Stream'.Seq1 α)) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (S' : Stream'.Seq (Stream'.Seq1 α)) → motive (some ((a, s), S'))),
  (match some ((a, s), S') with
    | none => h_1 ()
    | some ((a, s), S') => h_2 a s S') =
    h_2 a s S'
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.neg_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun a => max (-f a) 0) μ