mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk_id : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], { toLinearMap := LinearMap.id, cont := ⋯ } = ContinuousLinearMap.id R₁ M₁
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.single_finsetSum`. -/
Finsupp.single_finset_sum : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α),
  (fun₀ | a => ∑ b ∈ s, f b) = ∑ b ∈ s, fun₀ | a => f b
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 - AkraBazziRecurrence.smoothingFn ↑n
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] {k fallback : α},
  m.contains k = true → m.getD k fallback = k
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgOption : {α : Type} → [Lean.Doc.FromDocArg α] → Lean.Doc.FromDocArg (Option α)
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.addRange : Lean.FileMap →
  Lean.Lsp.FoldingRangeKind →
    Option String.Pos.Raw → Option String.Pos.Raw → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM Unit
-- Mathlib.Control.Traversable.Instances
Sum.traverse_map : ∀ {σ : Type u} {G : Type u → Type u} [inst : Applicative G] {α β γ : Type u} (g : α → β) (f : β → G γ) (x : σ ⊕ α),
  Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
-- Mathlib.RingTheory.Smooth.NoetherianDescent
/-- (Implementation detail): If `S` is an `R`-algebra with presentation `P`
and section `σ` of the projection `R[Xᵢ] ⧸ I^2 → S`, then a
`DescentAux` structure contains the data necessary to reconstruct `σ`.  -/
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux : (A : Type u) → (B : Type u_2) → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → Type (max (max 1 u) u_2)
-- Mathlib.Data.Matrix.Basic
Matrix.transposeAlgEquiv_symm_apply : ∀ (m : Type u_2) (R : Type u_7) (α : Type u_11) [inst : CommSemiring R] [inst_1 : CommSemiring α] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Algebra R α] (a : (Matrix m m α)ᵐᵒᵖ),
  (Matrix.transposeAlgEquiv m R α).symm a = (MulOpposite.unop a).transpose
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero' : ∀ {w w' : ℕ} (n : BitVec w), n <<< 0#w' = n
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop`. -/
CategoryTheory.CardinalFilteredPoset.exists_mem_propSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (a : ↑J.withTop.obj), ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S
-- Std.Time.Format
/-- The leanDateTime24HourNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss` for
representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTime24HourNoNanos : Std.Time.GenericFormat (Std.Time.Awareness.only Std.Time.TimeZone.GMT)
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (C r : NNReal)
  (f : X → Y), HolderWith C r f = ∀ (x y : X), edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.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 :
    (sz : ℕ) →
      (k : α) →
        (v : β k) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k v l r => h_2 sz k v l r) =
    h_1 ()
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.maxD fallback = fallback
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instIsScalarTowerCircle_1 : IsScalarTower Circle Complex.UnitClosedDisc Complex.UnitClosedDisc
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.hasFiniteLimits : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasFiniteLimits A]
  [CategoryTheory.Limits.PreservesFiniteLimits G],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.StructuredArrow X G)
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_eq_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Set.kernImage f s = (f '' sᶜ)ᶜ
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- If `R` is a commutative ring and `A` is a commutative `R`-algebra with injective algebra map
and no zero-divisors, then the `R`-algebraic independent subsets of `A` form a matroid.  -/
AlgebraicIndependent.matroid : (R : Type u_1) →
  (A : Type w) →
    [inst : CommRing R] →
      [inst_1 : CommRing A] → [inst_2 : Algebra R A] → [FaithfulSMul R A] → [NoZeroDivisors A] → Matroid A
-- Mathlib.Algebra.Homology.Localization
/-- The class of quasi-isomorphisms in the homotopy category.  -/
HomotopyCategory.quasiIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Preadditive C] →
          [CategoryTheory.CategoryWithHomology C] → CategoryTheory.MorphismProperty (HomotopyCategory C c)
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_associator_inv_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).inv.unop2 =
    (CategoryTheory.Bicategory.associator h.unop g.unop f.unop).hom
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv_left₀`. -/
AntivaryOn.inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → AntivaryOn f g s → MonovaryOn f⁻¹ g s
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldDef : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.Cartan
Matrix.isSimplyLaced_iff_of_linearOrder : ∀ {ι : Type u_1} [inst : LinearOrder ι] (A : Matrix ι ι ℤ),
  A.IsSymm → (A.IsSimplyLaced ↔ ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1)
-- Mathlib.CategoryTheory.Sites.Canonical
/-- If `C` is a category with `[Category.{max w v} C]`, this is the isomorphism
`uliftYoneda.{w} (C := C) ≅ yoneda`.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{max w v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] → CategoryTheory.GrothendieckTopology.uliftYoneda.{w, max v w, u} J ≅ J.yoneda
-- Mathlib.Topology.Separation.CompletelyRegular
isDenseInducing_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X] [CompletelyRegularSpace X], IsDenseInducing stoneCechUnit
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.instLiesOverAsIdealComapAlgebraMap : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : PrimeSpectrum S), p.asIdeal.LiesOver (PrimeSpectrum.comap (algebraMap R S) p).asIdeal
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Inv.inv '' Set.Icc a b = Set.Icc b⁻¹ a⁻¹
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Int8
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- If we apply the free functor `Type u ⥤ ModuleCat.{u} k` to the universal cover of the
classifying space of `G` as a simplicial set, then take the alternating face map complex, the result
is isomorphic to the standard resolution of the trivial `G`-representation `k` as a complex of
`k`-modules.  -/
Rep.standardComplex.compForgetAugmentedIso : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      AlgebraicTopology.AlternatingFaceMapComplex.obj
          (CategoryTheory.SimplicialObject.Augmented.drop.obj
            (classifyingSpaceUniversalCover.compForgetAugmented.toModule k G)) ≅
        Rep.standardComplex.forget₂ToModuleCat k G
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Subobject F),
  (RelIso.symm (CategoryTheory.Subfunctor.orderIsoSubobject F)) X = CategoryTheory.Subfunctor.range X.arrow
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminal.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P : C}
  (f g : P ⟶ ⊤_ C), f = g
-- Lean.Elab.InfoTree.Main
Lean.Elab.withMacroExpansionInfo : {m : Type → Type} →
  {α : Type} →
    [MonadFinally m] →
      [Monad m] → [Lean.Elab.MonadInfoTree m] → [Lean.MonadLCtx m] → Lean.Syntax → Lean.Syntax → m α → m α
-- Mathlib.Data.DFinsupp.Defs
/-- A computable version of `comapDomain` when an explicit left inverse is provided.  -/
DFinsupp.comapDomain' : {ι : Type u} →
  {β : ι → Type v} →
    {κ : Type u_1} →
      [inst : (i : ι) → Zero (β i)] →
        (h : κ → ι) → {h' : ι → κ} → Function.LeftInverse h' h → (Π₀ (i : ι), β i) → Π₀ (k : κ), β (h k)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filter!_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).Equiv t ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f a (t.get a h) = true)
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The embedding of `R[X]` into `R[Xᵢ]` as an `R`-algebra homomorphism.  -/
Polynomial.toMvPolynomial : {R : Type u_1} → {σ : Type u_3} → [inst : CommSemiring R] → σ → Polynomial R →ₐ[R] MvPolynomial σ R
-- Batteries.CodeAction.Misc
/-- Hole code action used to fill in a structure's field when specifying an instance.

In the following:
```lean
instance : Monad Id := _
```

invoking the hole code action "Generate a (minimal) skeleton for the structure under construction."
produces:
```lean
instance : Monad Id where
  pure := _
  bind := _
```

and invoking "Generate a (maximal) skeleton for the structure under construction." produces:
```lean
instance : Monad Id where
  map := _
  mapConst := _
  pure := _
  seq := _
  seqLeft := _
  seqRight := _
  bind := _
```
 -/
Batteries.CodeAction.instanceStub : Lean.CodeAction.HoleCodeAction
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_def : ∀ (x : Turing.ToPartrec.Cont),
  x.then =
    match (motive := Turing.ToPartrec.Cont → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont) x with
    | Turing.ToPartrec.Cont.halt => fun k' => k'
    | Turing.ToPartrec.Cont.cons₁ fs as k => fun k' => Turing.ToPartrec.Cont.cons₁ fs as (k.then k')
    | Turing.ToPartrec.Cont.cons₂ ns k => fun k' => Turing.ToPartrec.Cont.cons₂ ns (k.then k')
    | Turing.ToPartrec.Cont.comp f k => fun k' => Turing.ToPartrec.Cont.comp f (k.then k')
    | Turing.ToPartrec.Cont.fix f k => fun k' => Turing.ToPartrec.Cont.fix f (k.then k')
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Variant of `get_map` that holds without `LawfulEqOrd`.  -/
Std.DTreeMap.Internal.Impl.Const.get_map' : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → γ} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.map f t) k h' =
    f (t.getKey k ⋯) (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous K J] (adj : F ⊣ G)
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S)
  (H₁ :
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.obj =
      CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom))
  (H₂ :
    CategoryTheory.CategoryStruct.comp φ.hom
        (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.obj)) =
      CategoryTheory.CategoryStruct.id S.obj)
  (M : SheafOfModules S) (U : Cᵒᵖ)
  (x : ↑((((SheafOfModules.pushforward ψ).comp (SheafOfModules.pushforward φ)).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom
        (((SheafOfModules.pushforwardPushforwardAdj adj φ ψ H₁ H₂).counit.app M).val.app U))
      x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (adj.unit.app (Opposite.unop U)).op)) x
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_sdiff_singleton_empty : ∀ {α : Type u_1} {s : Set α} {t : Set (Set α)}, s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty
-- Mathlib.Data.Rel
SetRel.preimage_subset_preimage_left : ∀ {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} {t : Set β}, R₁ ⊆ R₂ → R₁.preimage t ⊆ R₂.preimage t
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_zpow : ∀ (n : ℤ), Continuous fun x => x ^ n
-- Mathlib.Algebra.Lie.TraceForm
LieModule.range_traceForm_le_span_weight : ∀ (K : Type u_2) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M] [FiniteDimensional K M]
  [inst_8 : LieRing.IsNilpotent L] [inst_9 : LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M],
  LinearMap.range (LieModule.traceForm K L M) ≤ Submodule.span K (Set.range (LieModule.Weight.toLinear K L M))
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_mul : ∀ {α : Type u} {x y : FreeCommRing α} {s : Set α}, x.IsSupported s → y.IsSupported s → (x * y).IsSupported s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → k ∉ t₁ \ t₂
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.mem_cons_self : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ a :: l
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`.  -/
Orientation.oangle_add_right_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 → ∀ (r : ℝ), o.oangle x (x + r • (o.rotation ↑(Real.pi / 2)) x) = ↑(Real.arctan r)
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_right_eq_if : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} [inst : DecidablePred fun x => x ∈ s],
  Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅
-- Mathlib.Order.BooleanAlgebra.Set
Set.nonempty_compl_of_nontrivial : ∀ {α : Type u_1} [Nontrivial α] (x : α), {x}ᶜ.Nonempty
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.Array.eraseP_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match none with
    | some y => h_1 y
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
MonoidAlgebra.instNoZeroDivisorsOfUniqueProds : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [NoZeroDivisors R] [inst_2 : Mul A] [UniqueProds A],
  NoZeroDivisors (MonoidAlgebra R A)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.cnstrs : Lean.Meta.Grind.EMatchTheorem → List Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- An ind-object `X` is the colimit (in `Ind C`!) of the filtered diagram presenting it.  -/
CategoryTheory.Ind.colimitPresentationCompYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.Ind C) → CategoryTheory.Limits.colimit (X.presentation.F.comp CategoryTheory.Ind.yoneda) ≅ X
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.eq_zero_imp : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {c : ℝ} {f'' : α → E''} {g'' : α → F''} {l : Filter α},
  Asymptotics.IsBigOWith c l f'' g'' → ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The embedding from `up' a` to itself via (· + b).  -/
ComplexShape.embeddingUp'Add : {A : Type u_3} →
  [inst : AddCommSemigroup A] →
    [inst_1 : IsRightCancelAdd A] → (a : A) → A → (ComplexShape.up' a).Embedding (ComplexShape.up' a)
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.insertSurrounding.go : Lean.Server.FileWorker.AbsoluteLspSemanticToken →
  List Lean.Server.FileWorker.AbsoluteLspSemanticToken → List Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y y' : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F y y'),
  CommRingCat.Colimits.Relation.below x_1 → motive y y' x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The isometric equivalence from `C(ℤ_[p], E)` to the space of sequences in `E` tending to `0` given
by Mahler's theorem, for `E` a nonarchimedean `ℚ_[p]`-Banach space.
 -/
PadicInt.mahlerEquiv : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    (E : Type u_1) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : Module ℤ_[p] E] →
          [inst_2 : IsBoundedSMul ℤ_[p] E] →
            [IsUltrametricDist E] → [CompleteSpace E] → C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] ZeroAtInftyContinuousMap ℕ E
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The natural bijection between points of order `n` and natural numbers less than and coprime to
`n`. The inverse of the map sends `m ↦ (m/n * p : AddCircle p)` where `m` is coprime to `n` and
satisfies `0 ≤ m < n`.  -/
AddCircle.setAddOrderOfEquiv : {𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [hp : Fact (0 < p)] → {n : ℕ} → 0 < n → ↑{u | addOrderOf u = n} ≃ ↑{m | m < n ∧ m.gcd n = 1}
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCodetector.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∃ G, CategoryTheory.IsCodetector G) → CategoryTheory.HasCodetector C
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
forall_lt_add_iff_lt_left : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α]
  [AddLeftReflectLT α] [IsLeftCancelAdd α], (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- pushout commutes with composition (up to natural isomorphism).  -/
CategoryTheory.Under.pushoutComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] →
            [inst_2 : CategoryTheory.Limits.HasPushoutsAlong g] →
              CategoryTheory.Under.pushout (CategoryTheory.CategoryStruct.comp f g) ≅
                (CategoryTheory.Under.pushout f).comp (CategoryTheory.Under.pushout g)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_succ : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σₘ[A]` of a finset `A` in a group is `|A * A| / |A|`.  -/
Combinatorics.Additive.«termσₘ[_]» : Lean.ParserDescr
-- Std.Http.Data.Headers.Value
Std.Http.Header.Value.mk : (value : String) →
  autoParam (Std.Http.Header.IsValidHeaderValue value) Std.Http.Header.Value.isValidHeaderValue._autoParam →
    Std.Http.Header.Value
-- Mathlib.Data.Fintype.Card
Fintype.card_quotient_le : ∀ {α : Type u_1} [inst : Fintype α] (s : Setoid α) [inst_1 : DecidableRel fun x1 x2 => x1 ≈ x2],
  Fintype.card (Quotient s) ≤ Fintype.card α
-- Mathlib.Topology.LocalAtTarget
/-- **Alias** of `Set.restrictPreimage_isOpenEmbedding`. -/
Topology.IsOpenEmbedding.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding (s.restrictPreimage f)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- The rank `Matroid.eRank M` of `M` is the `ℕ∞`-valued cardinality of each base of `M`.
(See `Matroid.cRank` for a worse-behaved cardinal-valued version)  -/
Matroid.eRank : {α : Type u_1} → Matroid α → ℕ∞
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sInf_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C}
  (f : Y ⟶ X), (sInf Ss).arrows f ↔ ∀ S ∈ Ss, S.arrows f
-- Mathlib.RingTheory.PolynomialAlgebra
/-- (Implementation detail.)

The bare function `A[X] → A ⊗[R] R[X]`.
(We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)
 -/
PolyEquivTensor.invFun : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Polynomial A → TensorProduct R A (Polynomial R)
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.hausdorffMeasure.eq_1 : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d : ℝ),
  MeasureTheory.Measure.hausdorffMeasure d = MeasureTheory.Measure.mkMetric fun r => r ^ d
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instZero : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → [Zero β] → Zero (BoundedContinuousFunction α β)