mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mk.injEq : ∀ (toElabInfo : Lean.Elab.ElabInfo) (mctxBefore : Lean.MetavarContext) (goalsBefore : List Lean.MVarId)
  (mctxAfter : Lean.MetavarContext) (goalsAfter : List Lean.MVarId) (toElabInfo_1 : Lean.Elab.ElabInfo)
  (mctxBefore_1 : Lean.MetavarContext) (goalsBefore_1 : List Lean.MVarId) (mctxAfter_1 : Lean.MetavarContext)
  (goalsAfter_1 : List Lean.MVarId),
  ({ toElabInfo := toElabInfo, mctxBefore := mctxBefore, goalsBefore := goalsBefore, mctxAfter := mctxAfter,
        goalsAfter := goalsAfter } =
      { toElabInfo := toElabInfo_1, mctxBefore := mctxBefore_1, goalsBefore := goalsBefore_1, mctxAfter := mctxAfter_1,
        goalsAfter := goalsAfter_1 }) =
    (toElabInfo = toElabInfo_1 ∧
      mctxBefore = mctxBefore_1 ∧ goalsBefore = goalsBefore_1 ∧ mctxAfter = mctxAfter_1 ∧ goalsAfter = goalsAfter_1)
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
Std.Http.Response.Builder.new : Std.Http.Response.Builder
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol is multiplicative in its second argument.  -/
jacobiSym.mul_right : ∀ (a : ℤ) (b₁ b₂ : ℕ) [NeZero b₁] [NeZero b₂], jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.isoClosure_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C),
  (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure
-- Mathlib.GroupTheory.ArchimedeanDensely
Int.not_denselyOrdered : ¬DenselyOrdered ℤ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsCentralScalar : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X]
  [inst_3 : SMul Mᵐᵒᵖ X] [inst_4 : IsCentralScalar M X], IsCentralScalar M (SeparationQuotient X)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.left_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g), h.left.r = h.r.left
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁),
  g.comp f =
    { weightMap := g.weightMap ∘ₗ f.weightMap, coweightMap := f.coweightMap ∘ₗ g.coweightMap,
      indexEquiv := f.indexEquiv.trans g.indexEquiv, weight_coweight_transpose := ⋯, root_weightMap := ⋯,
      coroot_coweightMap := ⋯ }
-- Mathlib.Data.Set.Lattice.Image
Set.surjective_iff_surjective_of_iUnion_eq_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β},
  Set.iUnion U = Set.univ → (Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f))
-- Aesop.Rule.Name
Aesop.instToJsonScopeName : Lean.ToJson Aesop.ScopeName
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorem.mk.inj : ∀ {funPropName thmName : Lean.Name}
  {keys : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)} {priority : ℕ}
  {funPropName_1 thmName_1 : Lean.Name}
  {keys_1 : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)} {priority_1 : ℕ},
  { funPropName := funPropName, thmName := thmName, keys := keys, priority := priority } =
      { funPropName := funPropName_1, thmName := thmName_1, keys := keys_1, priority := priority_1 } →
    funPropName = funPropName_1 ∧ thmName = thmName_1 ∧ keys = keys_1 ∧ priority = priority_1
-- Mathlib.Topology.FiberBundle.Trivialization
/-- A fiberwise inverse to `e`. This is the function `F → E b` that induces a local inverse
`B × F → TotalSpace F E` of `e` on `e.baseSet`. Outside of `e.baseSet` it takes on arbitrarily
chosen junk values.  -/
Bundle.Pretrivialization.symm : {B : Type u_1} →
  {F : Type u_2} →
    {E : B → Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [∀ (x : B), Nonempty (E x)] → Bundle.Pretrivialization F Bundle.TotalSpace.proj → (b : B) → F → E b
-- Lean.Data.KVMap
Lean.KVMap.getBool : Lean.KVMap → Lean.Name → optParam Bool false → Bool
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.exClosure.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {inst : DecidableEq α} [inst_1 : DecidableEq α] (φ φ_1 : L.Formula α),
  φ = φ_1 → φ.exClosure = φ_1.exClosure
-- Mathlib.Data.FunLike.IsApply
/-- `IsZeroApply F α β` states for all `x : α`, `(0 : F) x = 0`.  -/
IsZeroApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Zero β] → [Zero F] → Prop
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an isomorphism in the category `AddCommGrpCat` from an `AddEquiv`
between `AddCommGroup`s.  -/
AddEquiv.toAddCommGrpIso : {X Y : AddCommGrpCat} → ↑X ≃+ ↑Y → (X ≅ Y)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects finite limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteLimits F],
  CategoryTheory.Limits.ReflectsFiniteColimits F.op
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inl_comp_pushoutObjIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inl f g).app d)
      (CategoryTheory.Limits.pushoutObjIso f g d).hom =
    CategoryTheory.Limits.pushout.inl (f.app d) (g.app d)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.zero_notMem_range_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [NeZero 2],
  0 ∉ Set.range ⇑P.coroot
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.id_app : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.id X) U =
    CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))
-- Mathlib.Algebra.Algebra.Unitization
MulActionHom.mk.congr_simp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  (toFun toFun_1 : X → Y) (e_toFun : toFun = toFun_1) (map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x),
  { toFun := toFun, map_smul' := map_smul' } = { toFun := toFun_1, map_smul' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchesAt_iff_exists_isLongestRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
    ∃ startPos, ∃ (h : startPos ≤ pos), String.Slice.Pattern.Model.IsLongestRevMatch pat (pos.sliceTo startPos h)
-- Lean.Elab.Do.Basic
/-- The least upper bound of two code livenesses.  -/
Lean.Elab.Do.CodeLiveness.lub : Lean.Elab.Do.CodeLiveness → Lean.Elab.Do.CodeLiveness → Lean.Elab.Do.CodeLiveness
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_simple_submodule : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Nontrivial M], ∃ m, IsSimpleModule R ↥m
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.singleton_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, {a} ∩ s = if a ∈ s then {a} else ∅
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative additive groups is full.  -/
AddCommGrpCat.instFullUliftFunctor : AddCommGrpCat.uliftFunctor.Full
-- Init.Core
/-- Strict subset relation: `a ⊂ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊂` in identifiers is `ssubset`. -/
HasSSubset.SSubset : {α : Type u} → [self : HasSSubset α] → α → α → Prop
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isSeparating_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C),
  P.op.IsSeparating ↔ P.IsCoseparating
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
/-- If a gcf terminated at position `n`, it also terminated at `m ≥ n`.  -/
GenContFract.terminated_stable : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ}, n ≤ m → g.TerminatedAt n → g.TerminatedAt m
-- Init.Internal.Order.Basic
/-- Park induction principle for least fixpoint.
In general, this construction does not require monotonicity of `f`.
Monotonicity is required to show that `lfp f` is indeed a fixpoint of `f`.
 -/
Lean.Order.lfp_le_of_le : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {x : α} {f : α → α},
  Lean.Order.PartialOrder.rel (f x) x → Lean.Order.PartialOrder.rel (Lean.Order.lfp f) x
-- Mathlib.Data.Fin.Tuple.Basic
/-- Adding an element at the end of an `n`-tuple, to get an `n+1`-tuple. The name `snoc` comes from
`cons` (i.e., adding an element to the left of a tuple) read in reverse order.  -/
Fin.snoc : {n : ℕ} → {α : Fin (n + 1) → Sort u_1} → ((i : Fin n) → α i.castSucc) → α (Fin.last n) → (i : Fin (n + 1)) → α i
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_mul_complEDS₂ : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The transformation formula for `η` under `S : z ↦ -1 / z`: we have
`η(-1 / z) = (√I)⁻¹ · √z · η(z)` on the upper half-plane.  -/
ModularForm.eta_comp_eq_csqrt_I_inv : Set.EqOn (ModularForm.eta ∘ fun x => -1 / x) (Complex.I.sqrt⁻¹ • (Complex.sqrt * ModularForm.eta))
  UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ENat.LEInfty.mk : ∀ {m : WithTop ℕ∞}, m ≤ ↑⊤ → ENat.LEInfty m
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.processAnchor : Lean.Meta.Grind.Params → Lean.TSyntax `hexnum → Lean.CoreM Lean.Meta.Grind.Params
-- Std.Sync.Broadcast
/-- Queue of producers blocked waiting for buffer space to become available.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.producers : {α : Type} → Std.Bounded.State✝ α → Std.Queue (IO.Promise Bool)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.minimal_not_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → Minimal (fun x => ¬M.Indep x) C
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ)
  (s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)),
  (CategoryTheory.Coyoneda.colimitCoconeIsColimit X).desc s =
    TypeCat.ofHom fun x =>
      (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.unop X)))
        (CategoryTheory.CategoryStruct.id (Opposite.unop X))
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.isReduced_iff : ∀ (u : PNat.XgcdType), u.IsReduced ↔ u.IsReduced'
-- Std.Async.Signal
/-- `Signal.Waiter` can be used to handle a specific signal once.
 -/
Std.Async.Signal.Waiter : Type
-- Batteries.Tactic.PrintPrefix
/-- Include declarations in imported environment.  -/
Batteries.Tactic.PrintPrefixConfig.imported : Batteries.Tactic.PrintPrefixConfig → Bool
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializedParams.mk : Lean.Lsp.InitializedParams
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃Obj_map : ∀ {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  {X Y : CategoryTheory.Functor C₂ D₂} (τ₂ : X ⟶ Y),
  (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).map τ₂ =
    CategoryTheory.Functor.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (x l : ℕ) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.rel R ts).listEncode =
    [Sum.inr (Sum.inl ⟨l, R⟩), Sum.inr (Sum.inr x)] ++ List.map (fun i => Sum.inl ⟨x, ts i⟩) (List.finRange l)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- If `a.card = b.card + 1`, then the hypergeometric series has convergence radius `1`, unless it
is a polynomial.  -/
Complex.radius_regularizedHGFunSeries_eq_one : ∀ {a b : Multiset ℂ},
  a.card = b.card + 1 → (∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k) → (Complex.regularizedHGFunSeries a b).radius = 1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- Returns `true` if the current ring satisfies the property
```
∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
```
 -/
Lean.Meta.Grind.Arith.CommRing.noZeroDivisors : Lean.Meta.Grind.Arith.CommRing.RingM Bool
-- Mathlib.Algebra.Group.Commutator
addCommutatorElement_def : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G), ⁅g₁, g₂⁆ = g₁ + g₂ + -g₁ + -g₂
-- Init.Data.Option.Lemmas
Option.guard_congr : ∀ {α : Type u_1} {f g : α → Bool}, (∀ (a : α), f a = g a) → Option.guard f = Option.guard g
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.inv_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (γ : CategoryTheory.PresheafOfGroups.OneCochain G U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j),
  γ⁻¹.ev i j a b = (γ.ev i j a b)⁻¹
-- Mathlib.Algebra.Group.Idempotent
isIdempotentElem_iff : ∀ {M : Type u_1} [inst : Mul M] {a : M}, IsIdempotentElem a ↔ a * a = a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.instMin : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → Min (L.BoundedFormula α n)
-- Mathlib.CategoryTheory.Groupoid
/-- A category with a unique morphism between any two objects is a groupoid  -/
CategoryTheory.Groupoid.ofHomUnique : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → ({X Y : C} → Unique (X ⟶ Y)) → CategoryTheory.Groupoid C
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instInsert : {α : Type u_1} → Insert α (Multiset α)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_symm_add : ∀ {a b : ℕ}, (a + b).choose a = (a + b).choose b
-- Mathlib.Tactic.CategoryTheory.CancelIso
/-- `cancelIso` simplifies the composition of a morphism and its inverse,
given an expression of the form `f ≫ g`.

Assuming `f` is not a composition (as `Category.assoc` is tagged `@[simp]`),
if `g` is not a composition itself, it checks whether `f` is inverse to `g`
by checking if `f` has an `IsIso` instance and then by running `push inv` on `inv f` and on `g`.
If the check succeeds, then `f ≫ g` is rewritten to `𝟙 _`.

If `g` is of the form `h ≫ k`, the procedure instead checks if `f` and `h` are inverses to each
other, and the procedure rewrites `f ≫ h ≫ k` to `k` if that is the case.
This special case is useful as `f ≫ (h ≫ k)` is in simp-normal form and does not
contain `f ≫ g` directly as a subterm.

For instance, the simproc will successfully rewrite expressions such as
`F.map (G.map (inv (H.map (e.hom)))) ≫ F.map (G.map (H.map (e.inv)))` to `𝟙 _`
because `CategoryTheory.Functor.map_inv` is a `@[push ←]` lemma, and
`CategoryTheory.IsIso.Iso.inv_hom` is a `@[push]` lemma.

This procedure is mostly intended as a post-procedure: it will work better if `f` and `g`
have already been traversed beforehand.  -/
Mathlib.Tactic.CategoryTheory.CancelIso.cancelIsoSimproc : Lean.Meta.Simp.Simproc
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_eq_zero : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {a : α →₀ M} {f : M → N},
  Function.Injective f → ∀ (h : f 0 = 0), Finsupp.mapRange f h a = 0 ↔ a = 0
-- Std.Do.WP.SimpLemmas
Std.Do.WP.read_MonadReader : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ : Type u} {Q : Std.Do.PostCond ρ ps} [inst : MonadReaderOf ρ m]
  [inst_1 : Std.Do.WP m ps], (Std.Do.wp read).apply Q = (Std.Do.wp MonadReaderOf.read).apply Q
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.exists_of_sep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  (∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))),
      (∀ (I : S.Arrow),
          (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x =
            (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) →
        x = y) →
    ∀ (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S), ∃ t, CategoryTheory.Meq.mk S t = s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.injective_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N), Function.Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsAddRegular x
-- Std.Http.Server.Connection
/-- Runs the main request/response processing loop for a single connection.
Drives the HTTP/1.1 state machine through four phases each iteration:
send buffered output, process H1 events, dispatch pending requests, poll for I/O.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.handle : {α σ : Type} →
  [Std.Http.Transport α] →
    [h : Std.Http.Server.Handler σ] →
      Std.Http.Server.Connection α → Std.Http.Config → Std.CancellationContext → σ → Std.Async.Async Unit
-- Mathlib.GroupTheory.Index
/-- If `H` and `K` are subgroups of an additive group `G`, then `relIndex H K : ℕ`
is the index of `H ∩ K` in `K`. The function returns `0` if the index is infinite.  -/
AddSubgroup.relIndex : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_mul : ∀ {n : ℕ} (x y : ℕ), BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkipWhile_le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.revSkipWhile pat ≤ pos
-- Mathlib.RingTheory.HahnSeries.Valuation
HahnSeries.addVal_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : AddCancelCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Ring R] [inst_4 : IsDomain R] {x : HahnSeries Γ R},
  (HahnSeries.addVal Γ R) x = x.orderTop
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheorem.default : Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X) [U.IsRefl] [U.IsSymm],
  Dynamics.coverEntropyInfEntourage T F (U.comp U) ≤ Dynamics.netEntropyInfEntourage T F U
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_right_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (x + z * y) y ↔ IsRelPrime x y
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α], AddUnits.instPreorder = Preorder.lift AddUnits.val
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodProdProdComm_symm : ∀ (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'],
  (RingEquiv.prodProdProdComm R R' S S').symm = RingEquiv.prodProdProdComm R S R' S'
-- Mathlib.Topology.Compactness.Compact
Set.Infinite.exists_accPt_cofinite_inf_principal : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [CompactSpace X],
  s.Infinite → ∃ x, AccPt x (Filter.cofinite ⊓ Filter.principal s)
-- Mathlib.Algebra.Order.Star.Basic
/-- A star projection is non-negative in a star-ordered ring.  -/
IsStarProjection.nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {p : R}, IsStarProjection p → 0 ≤ p
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsDivApply.div_apply`. -/
div_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Div β}
  {inst_2 : Div F} [self : IsDivApply F α β] (f g : F) (x : α), (f / g) x = f x / g x
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_zero_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} (s : Set α), MeasureTheory.Measure.real 0 s = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : Finite X] [inst_2 : AddGroup Y] [inst_3 : Finite Y] (f : X →+ Y),
  FiniteAddGrp.ofHom f = CategoryTheory.InducedCategory.homMk (AddGrpCat.ofHom f)
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness : Type
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.hom₂ (CategoryTheory.CategoryStruct.comp e.hom.hom₂ h) = h
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.toList_copy_takeEnd : ∀ {s : String.Slice} {n : ℕ}, (s.takeEnd n).copy.toList = List.drop (s.copy.toList.length - n) s.copy.toList
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommRingOfMulOpposite : {M : Type u_1} → [CommRing Mᵐᵒᵖ] → CommRing Mᵈᵐᵃ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_one : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_248✝ → cfc 1 a = 1
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.sInf_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, sInf I.minimalPrimes = I.radical