mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- The "remainder term" of `WittVector.wittPolyProd`. See `mul_polyOfInterest_aux2`.  -/
WittVector.wittPolyProdRemainder : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_of_eventually_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (C : ℝ),
  (∀ᶠ (n : ℕ) in Filter.atTop, ‖p n‖ * ↑r ^ n ≤ C) → ↑r ≤ p.radius
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.div.go.match_1.eq_1 : ∀ (x : ℕ) (motive : (fuel : ℕ) → x < fuel → Sort u_1) (fuel : ℕ) (hfuel : x < fuel.succ)
  (h_1 : (fuel : ℕ) → (hfuel : x < fuel.succ) → motive fuel.succ hfuel),
  (match fuel.succ, hfuel with
    | fuel.succ, hfuel => h_1 fuel hfuel) =
    h_1 fuel hfuel
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolTag.noConfusionType : Sort v✝ → Lean.Lsp.SymbolTag → Lean.Lsp.SymbolTag → Sort v✝
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- A non-unital subsemiring of a non-unital semiring `R` is a subset `s` that is both an additive
submonoid and a semigroup.  -/
NonUnitalSubsemiring : (R : Type u) → [NonUnitalNonAssocSemiring R] → Type u
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa?_ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.toStrongDual_inj : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x' y' : WeakDual 𝕜 E), WeakDual.toStrongDual x' = WeakDual.toStrongDual y' ↔ x' = y'
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- Construct a comonad as an object in `ComonadBicat B`.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} → (t : a ⟶ a) → [CategoryTheory.Bicategory.Comonad t] → CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B
-- Mathlib.Control.Monad.Cont
ContT.instLawfulMonadCont : ∀ {r : Type u} {m : Type u → Type v}, LawfulMonadCont (ContT r m)
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.mk.inj : ∀ {mctx : Lean.MetavarContext} {newParamNames : Array Lean.Name} {nextParamIdx : ℕ} {expr : Lean.Expr}
  {mctx_1 : Lean.MetavarContext} {newParamNames_1 : Array Lean.Name} {nextParamIdx_1 : ℕ} {expr_1 : Lean.Expr},
  { mctx := mctx, newParamNames := newParamNames, nextParamIdx := nextParamIdx, expr := expr } =
      { mctx := mctx_1, newParamNames := newParamNames_1, nextParamIdx := nextParamIdx_1, expr := expr_1 } →
    mctx = mctx_1 ∧ newParamNames = newParamNames_1 ∧ nextParamIdx = nextParamIdx_1 ∧ expr = expr_1
-- Mathlib.Data.List.AList
AList.union_assoc : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ s₃ : AList β},
  (s₁ ∪ s₂ ∪ s₃).entries.Perm (s₁ ∪ (s₂ ∪ s₃)).entries
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymm_one : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ],
  MvPolynomial.hsymm σ R 1 = ∑ i, MvPolynomial.X i
-- Lean.Parser.Term
Lean.Parser.Term.hygienicLParen.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The default value for the parameter, if the parameter has a default value.  -/
Lean.PrettyPrinter.Delaborator.ParamKind.defVal : Lean.PrettyPrinter.Delaborator.ParamKind → Option Lean.Expr
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.instEffectiveEpiFamilyComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B B' : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) (i : B ⟶ B') [CategoryTheory.EffectiveEpiFamily X π] [CategoryTheory.IsIso i],
  CategoryTheory.EffectiveEpiFamily X fun a => CategoryTheory.CategoryStruct.comp (π a) i
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_le_of_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_6} {E' : Type u_7}
  {F' : Type u_8} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜' E']
  [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜' F'] {p : FormalMultilinearSeries 𝕜 E F}
  {q : FormalMultilinearSeries 𝕜' E' F'}, (∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖) → q.radius ≤ p.radius
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_eq' : ∀ {α : Type u} (r : α → α → Prop) [H : IsWellOrder α r],
  Order.IsSuccLimit (Ordinal.type r) → ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = (Ordinal.type r).cof
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.ι₁_h_assoc : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁) {Z : TopCat} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁ (CategoryTheory.CategoryStruct.comp F.h h) =
    CategoryTheory.CategoryStruct.comp f₁ h
-- Std.Time.Time.Unit.Second
Std.Time.Second.instTransOrdOrdinal : ∀ {leap : Bool}, Std.TransOrd (Std.Time.Second.Ordinal leap)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.supportsStmt_write : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {S : Finset (Turing.TM1to1.Λ' Γ Λ σ)} {l : List Bool}
  {q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ},
  Turing.TM1.SupportsStmt S (Turing.TM1to1.write l q) = Turing.TM1.SupportsStmt S q
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.fst.inj : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} {a : Std.IterM m β} {a_1 : Std.IterM m β} {a_2 : Std.IterM m β}
  {a_3 : Std.IterM m β},
  Std.Iterators.Types.Append.fst a a_1 = Std.Iterators.Types.Append.fst a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- If `f` and `g` admit continuous left inverses, so does `f × g`.  -/
ContinuousLinearMap.HasLeftInverse.prodMap : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace E']
  [inst_5 : AddCommMonoid E'] [inst_6 : Module R E'] [inst_7 : TopologicalSpace F] [inst_8 : AddCommMonoid F]
  [inst_9 : Module R F] [inst_10 : TopologicalSpace F'] [inst_11 : AddCommMonoid F'] [inst_12 : Module R F']
  {f : E →L[R] F} {g : E' →L[R] F'}, f.HasLeftInverse → g.HasLeftInverse → (f.prodMap g).HasLeftInverse
-- Mathlib.Analysis.Calculus.FDeriv.Norm
fderiv_norm_smul_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E} {t : ℝ},
  0 < t → fderiv ℝ (fun x => ‖x‖) (t • x) = fderiv ℝ (fun x => ‖x‖) x
-- Mathlib.Algebra.Group.Defs
/-- A mixin for left cancellative addition.  -/
IsLeftCancelAdd : (G : Type u) → [Add G] → Prop
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_top : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β),
  BooleanSubalgebra.comap f ⊤ = ⊤
-- Init.Data.String.Basic
String.startInclusive_slice : ∀ {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive},
  (s.slice startInclusive endExclusive h).startInclusive = startInclusive
-- Mathlib.Data.List.Basic
/-- **Alias** of `List.filter_subset_self`. -/
List.filter_subset' : ∀ {α : Type u} {p : α → Bool} (l : List α), List.filter p l ⊆ l
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.nonUnitalAlgHom_comp_convMul_distrib : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : Coalgebra R C] [inst_8 : NonUnitalNonAssocSemiring B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] (h : A →ₙₐ[R] B) (f g : WithConv (C →ₗ[R] A)),
  ↑h ∘ₗ (f * g).ofConv = (WithConv.toConv (↑h ∘ₗ f.ofConv) * WithConv.toConv (↑h ∘ₗ g.ofConv)).ofConv
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The coercion of an algebra into its multiplier algebra as a non-unital star algebra
homomorphism.  -/
DoubleCentralizer.coeHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              [inst_5 : StarRing 𝕜] →
                [inst_6 : StarRing A] →
                  [inst_7 : StarModule 𝕜 A] → [inst_8 : NormedStarGroup A] → A →⋆ₙₐ[𝕜] DoubleCentralizer 𝕜 A
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.inv_cobounded : ∀ {E : Type u_2} [inst : SeminormedGroup E], (Bornology.cobounded E)⁻¹ = Bornology.cobounded E
-- Mathlib.Analysis.Calculus.LagrangeMultipliers
/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
at `x₀`, both `f : E → F` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is
a complete space, then the linear map `x ↦ (f' x, φ' x)` is not surjective.  -/
IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {φ : E → ℝ} {x₀ : E}
  {f' : E →L[ℝ] F} {φ' : StrongDual ℝ E},
  IsLocalExtrOn φ {x | f x = f x₀} x₀ →
    HasStrictFDerivAt f f' x₀ → HasStrictFDerivAt φ φ' x₀ → (↑(f'.prod φ')).range ≠ ⊤
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Generalization of `IsIntegral.of_mem_closure` bootstrapped up from that lemma  -/
IsIntegral.of_mem_closure' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (G : Set A),
  (∀ x ∈ G, IsIntegral R x) → ∀ x ∈ Subring.closure G, IsIntegral R x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.instIsAddHaarMeasureRealVolume : ∀ (T : ℝ) [hT : Fact (0 < T)], MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso_truncGT_map_truncGTπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ),
  b ≤ a → ∀ (X : C), CategoryTheory.IsIso ((t.truncGT a).map ((t.truncGTπ b).app X))
-- Mathlib.Data.Finsupp.Defs
Finsupp.unique_ext_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Unique α] {f g : α →₀ M}, f = g ↔ f default = g default
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyOutgoingCall : Inhabited Lean.Lsp.CallHierarchyOutgoingCall
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresenter.mk.injEq : ∀ (userName : String) (layoutKind : ProofWidgets.LayoutKind) (present : Lean.Expr → Lean.MetaM ProofWidgets.Html)
  (userName_1 : String) (layoutKind_1 : ProofWidgets.LayoutKind) (present_1 : Lean.Expr → Lean.MetaM ProofWidgets.Html),
  ({ userName := userName, layoutKind := layoutKind, present := present } =
      { userName := userName_1, layoutKind := layoutKind_1, present := present_1 }) =
    (userName = userName_1 ∧ layoutKind = layoutKind_1 ∧ present = present_1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.localRingHom_comp_stalkIso : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (p : ProjectiveSpectrum ℬ),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Proj.stalkIso 𝒜 ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p)).hom
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (HomogeneousLocalization.localRingHom f
            ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal
            p.asHomogeneousIdeal.toIdeal ⋯))
        (AlgebraicGeometry.Proj.stalkIso ℬ p).inv) =
    AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom p
-- Init.Data.List.Basic
/-- Inserts an element into a list without duplication.

If the element is present in the list, the list is returned unmodified. Otherwise, the new element
is inserted at the head of the list.

Examples:
 * `[1, 2, 3].insert 0 = [0, 1, 2, 3]`
 * `[1, 2, 3].insert 4 = [4, 1, 2, 3]`
 * `[1, 2, 3].insert 2 = [1, 2, 3]`
 -/
List.insert : {α : Type u} → [BEq α] → α → List α → List α
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toLinearMap_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective AlgHom.toLinearMap
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.isGE_triangleFunctor_obj_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (A : C),
  t.IsGE ((CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).obj A).obj₃ n
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.kind.sizeOf_spec : ∀ (val : Lean.SyntaxNodeKind), sizeOf (Lean.Parser.ParserExtension.OLeanEntry.kind val) = 1 + sizeOf val
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_toSubring : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ↑s.toSubring = ↑s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {C : ↑(groupHomology.H0 A) → Prop}
  (x : ↑(groupHomology.H0 A)), (∀ (x : ↑A), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) x)) → C x
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is an `AddZeroClass` under pointwise operations if `α` is.  -/
Filter.addZeroClass : {α : Type u_2} → [AddZeroClass α] → AddZeroClass (Filter α)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_def' : ∀ {b : ℕ}, 1 < b → ∀ {n : ℕ}, 0 < n → b.digits n = n % b :: b.digits (n / b)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.ker_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Matrix.ProjGenLinGroup.mk.ker = Subgroup.center (GL n R)
-- Mathlib.Probability.Kernel.Invariance
/-- A reversible Markov kernel leaves the measure `π` invariant.  -/
ProbabilityTheory.Kernel.IsReversible.invariant : ∀ {α : Type u_1} {mα : MeasurableSpace α} {κ : ProbabilityTheory.Kernel α α} [ProbabilityTheory.IsMarkovKernel κ]
  {π : MeasureTheory.Measure α}, κ.IsReversible π → κ.Invariant π
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Cᵒᵖ A) (U : Nᵒᵖ),
  (CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone p hp P).ι.app U =
    CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp (Opposite.unop U) P
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_sub : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : ℚ),
  Lean.Grind.Field.NormNum.ofRat (a - b) = Lean.Grind.Field.NormNum.ofRat a - Lean.Grind.Field.NormNum.ofRat b
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The full set is a fixed block.  -/
MulAction.IsFixedBlock.univ : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X], MulAction.IsFixedBlock G Set.univ
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constAddMonoidHom.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : AddZeroClass β],
  Pi.constAddMonoidHom α β = { toFun := Function.const α, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] (toOrderHom : α →o β) (continuous_toFun : Continuous toOrderHom.toFun)
  (toOrderHom_1 : α →o β) (continuous_toFun_1 : Continuous toOrderHom_1.toFun),
  ({ toOrderHom := toOrderHom, continuous_toFun := continuous_toFun } =
      { toOrderHom := toOrderHom_1, continuous_toFun := continuous_toFun_1 }) =
    (toOrderHom = toOrderHom_1)
-- Init.Data.Ord.UInt
UInt8.instLawfulEqOrd : Std.LawfulEqOrd UInt8
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
MulOpposite.opUniformEquivLeft.eq_1 : ∀ (G : Type u_2) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  MulOpposite.opUniformEquivLeft G =
    { toEquiv := MulOpposite.opEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Init.Data.Float.Model.Float32
/-- Converts an `Int8` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofInt8 : Int8 → Float32.Model
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.mk.injEq : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}
  (onFunction : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam)
  (onRelation : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam)
  (onFunction_1 : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam)
  (onRelation_1 : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam),
  ({ onFunction := onFunction, onRelation := onRelation } =
      { onFunction := onFunction_1, onRelation := onRelation_1 }) =
    (onFunction = onFunction_1 ∧ onRelation = onRelation_1)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], ↑1 = 1
-- Lean.Parser.Level
Lean.Parser.Level.max.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.conjTranspose_mul_mul_same : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype m] {A : Matrix n n R} {B : Matrix n m R},
  A.PosDef → Function.Injective B.mulVec → (B.conjTranspose * A * B).PosDef
-- Mathlib.Util.Qq
/-- Returns the natural number literal `n` as used in the frontend. It is a `OfNat.ofNat`
application. Recall that all theorems and definitions containing numeric literals are encoded using
`OfNat.ofNat` applications in the frontend.

This is a Qq version of `Lean.mkNatLit`.  -/
Qq.mkNatLitQ : ℕ → Q(ℕ)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.deriv_cosh : deriv Real.cosh = Real.sinh
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.ShortComplex.SnakeInput C)
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite partial order is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⋖ b`.  -/
monotone_iff_forall_covBy : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.uncurry : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β → γ} {Kα Kβ : NNReal},
  (∀ (b : β), LipschitzWith Kα fun a => f a b) →
    (∀ (a : α), LipschitzWith Kβ (f a)) → LipschitzWith (Kα + Kβ) (Function.uncurry f)
-- Init.Data.UInt.Bitwise
UInt16.zero_xor : ∀ {a : UInt16}, 0 ^^^ a = a
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumradius_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).circumradius = s.circumradius
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_C : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S} (r : S),
  MvPowerSeries.subst a (MvPowerSeries.C r) = MvPowerSeries.C r
-- Init.Grind.Lemmas
Lean.Grind.eqRecOn_heq : ∀ {α : Sort u_2} {a : α} {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a ⋯), Eq.recOn h v ≍ v
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.BinaryRefVec len → aig.RefVec len
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.of_isIdempotent : ∀ {M : Type u_1} [inst : Mul M] [Std.IdempotentOp fun x1 x2 => x1 * x2] (a : M), IsIdempotentElem a
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.mono : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U₁ U₂ : Submodule R M}
  {x y : M}, U₁ ≤ U₂ → x ≡ y [SMOD U₁] → x ≡ y [SMOD U₂]
-- Mathlib.Logic.ExistsUnique
ExistsUnique.intro₂ : ∀ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (w : α) (hp : p w),
  q w hp → (∀ (y : α) (hy : p y), q y hy → y = w) → ∃! x, ∃! hx, q x hx
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceAdd : Lean.Meta.Simp.DSimproc