mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.mk : Lean.Name → Bool → Bool → Lean.Parser.LeadingIdentBehavior → Lean.Elab.Term.ToParserDescrContext
-- Mathlib.Data.Finsupp.MonomialOrder
/-- **Alias** of `MonomialOrder.linearOrderSyn`.

---

`syn` is linearly ordered  -/
MonomialOrder.lo : {σ : Type u_1} → (self : MonomialOrder σ) → LinearOrder self.syn
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of binary join on function lattices.  -/
Lean.Order.join_apply : ∀ {σ : Type v} {β : Type w} [inst : Lean.Order.CompleteLattice β] (a b : σ → β) (s : σ),
  Lean.Order.join a b s = Lean.Order.join (a s) (b s)
-- Mathlib.Topology.Algebra.UniformConvergence
instDivUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Div β], instDivUniformFun = { div := instDivUniformFun._aux_1 }
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedLift.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : L.comp LF ⟶ F) (e_α : α = α_1) (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  [inst_3 : L.IsLocalization W] [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H)
  (β β_1 : L.comp G ⟶ F), β = β_1 → LF.leftDerivedLift α W G β = LF.leftDerivedLift α_1 W_1 G β_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldr_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  [inst : Std.TransCmp cmp] {f : α → δ → δ} {init : δ},
  Std.ExtDTreeMap.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableLeOrdinal : {leap : Bool} → {x y : Std.Time.Second.Ordinal leap} → Decidable (x ≤ y)
-- Init.Control.Lawful.MonadLift.Basic
/-- Lifting preserves `bind`  -/
LawfulMonadLift.monadLift_bind : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n}
  {inst_2 : MonadLift m n} [self : LawfulMonadLift m n] {α β : Type u} (ma : m α) (f : α → m β),
  MonadLift.monadLift (ma >>= f) = do
    let x ← MonadLift.monadLift ma
    MonadLift.monadLift (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.hom_ext_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  {arrows : (j : J) → objs j ⟶ B} [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C}
  {g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows},
  g1 = g2 ↔
    (∀ (j : J),
        CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.π arrows j) =
          CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.π arrows j)) ∧
      CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.base arrows) =
        CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.base arrows)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G),
  (CategoryTheory.StructuredArrow.preEquivalence F f).inverse = CategoryTheory.StructuredArrow.preEquivalenceInverse F f
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).hom
      (CategoryTheory.CategoryStruct.comp (E.p₁ k) h) =
    CategoryTheory.CategoryStruct.comp (E.p₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.getKey? t.minKey! = some t.minKey!
-- Init.Data.UInt.Bitwise
UInt16.not_and_self : ∀ {a : UInt16}, ~~~a &&& a = 0
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
/-- For a fixed bounded function `g`, `mulExpNegMulSq ε ∘ g` is bounded by `norm g`,
uniformly in `ε ≥ 0`.  -/
Real.abs_mulExpNegMulSq_comp_le_norm : ∀ {ε : ℝ} {E : Type u_1} [inst : TopologicalSpace E] {x : E} (g : BoundedContinuousFunction E ℝ),
  0 ≤ ε → |(ε.mulExpNegMulSq ∘ ⇑g) x| ≤ ‖g‖
-- Init.Data.Float.Model.Unpacked.Operations.Status
/-- Returns `true` if the float represents a real number, i.e., it is neither infinite nor `NaN`.
 -/
Float.Model.UnpackedFloat.isFinite : Float.Model.UnpackedFloat → Bool
-- Mathlib.Data.Set.Monotone
StrictMonoOn.strictMono : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictMonoOn f s → StrictMono (f ∘ Subtype.val)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.equivSubgroupOrbits.eq_1 : ∀ {G : Type u} (X : Type v) [inst : Group G] [inst_1 : MulAction G X] (H : Subgroup G),
  MulAction.equivSubgroupOrbits X H =
    (Setoid.sigmaQuotientEquivOfLe ⋯).symm.trans
      (Equiv.sigmaCongrRight fun ω => (MulAction.equivSubgroupOrbitsSetoidComap H ω).symm)
-- Lean.Parser.Term
Lean.Parser.Term.macroDollarArg : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fppfPrecoverage_eq_inf : AlgebraicGeometry.Scheme.fppfPrecoverage =
  AlgebraicGeometry.Scheme.precoverage @AlgebraicGeometry.Flat ⊓
    AlgebraicGeometry.Scheme.precoverage @AlgebraicGeometry.LocallyOfFinitePresentation
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_seminormedAddCommGroupToPi : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] (x : (i : ι) → α i), ‖x‖₊ = ‖WithLp.toLp p x‖₊
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomSurjective.instToRingHomRingEquiv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ : R₁ ≃+* R₂), RingHomSurjective ↑σ
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ico_eq_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → nhdsWithin b (Set.Ico a b) = nhdsWithin b (Set.Iio b)
-- Init.Control.Lawful.MonadAttach.Instances
instLawfulMonadAttachEStateM : ∀ {ε σ : Type u}, LawfulMonadAttach (EStateM ε σ)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A variant of `Matrix.det_units_conj`.  -/
Matrix.det_conj : ∀ {m : Type u} {α : Type v} [inst : CommRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m α},
  IsUnit M → ∀ (N : Matrix m m α), (M * N * M⁻¹).det = N.det
-- Mathlib.Analysis.Analytic.Linear
LinearIsometryEquiv.analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F)
  (x : E), AnalyticAt 𝕜 (⇑f) x
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_neg_of_neg_of_pos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, a < 0 → 0 < b → a * b < 0
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup.eq_1 : ∀ (x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var x).eraseDup = Lean.Grind.AC.Seq.var x
-- Mathlib.Dynamics.Minimal
IsOpen.iUnion_vadd : ∀ (G : Type u_2) {α : Type u_3} [inst : AddGroup G] [inst_1 : TopologicalSpace α] [inst_2 : AddAction G α]
  [AddAction.IsMinimal G α] {U : Set α}, IsOpen U → U.Nonempty → ⋃ g, g +ᵥ U = Set.univ
-- Mathlib.AlgebraicGeometry.Scheme
/-- The global sections as a functor. For the global section themselves, use `Γ(X, ⊤)` instead.  -/
AlgebraicGeometry.Scheme.Γ : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ CommRingCat
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_sub : ∀ (a b : UInt8), (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 256
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coeFn_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], ⇑0 = 0
-- Mathlib.Analysis.Analytic.Basic
/-- Taylor formula for an analytic function within a set, `IsBigO` version.  -/
HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x →
    ∀ (n : ℕ),
      (fun y => f (x + y) - p.partialSum n y) =O[nhdsWithin 0 ((fun x_1 => x + x_1) ⁻¹' insert x s)] fun y => ‖y‖ ^ n
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.add_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ₁ φ₂ φ₃ : MvPowerSeries σ R), (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative elements on
the left, namely `a₁ • b < a₂ • b → a₁ < a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
SMulPosReflectLT : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero β] → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  ¬compare k k' = Ordering.eq →
    Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl =
      Std.DTreeMap.Internal.Impl.contains k' t
-- ProofWidgets.Component.MakeEditLink
/-- The edit to perform on the file.  -/
ProofWidgets.MakeEditLinkProps.edit : ProofWidgets.MakeEditLinkProps → Lean.Lsp.TextDocumentEdit
-- Lean.Elab.RecAppSyntax
/-- Return `true` if `getRecAppSyntax? e` is a `some`.
 -/
Lean.hasRecAppSyntax : Lean.Expr → Bool
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
/-- An auxiliary neighborhood that will be used in the proof of
`OrderTopology.CompletelyNormalSpace`.  -/
Set.ordT5Nhd : {α : Type u_1} → [LinearOrder α] → Set α → Set α → Set α
-- Init.Control.Lawful.Instances
OptionT.run_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : α), (pure x).run = pure (some x)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.tsub_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] (f g : Π₀ (i : ι), α i) (i : ι), (f - g) i = f i - g i
-- Mathlib.Analysis.Complex.Arg
Complex.sameRay_iff : ∀ {x y : ℂ}, SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer"
products of the block matrices.  -/
Matrix.fromCols_mul_fromRows : ∀ {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R] [inst_1 : Fintype n₁]
  [inst_2 : Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R),
  A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.away_of_isIdempotentElem : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {e : R},
  IsIdempotentElem e →
    RingHom.ker (algebraMap R S) = Ideal.span {1 - e} → Function.Surjective ⇑(algebraMap R S) → IsLocalization.Away e S
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), (CategoryTheory.Functor.mapArrowEquivalence e).functor = e.functor.mapArrow
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Cache : Type
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.LFunction_ne_zero_of_not_quadratic_or_ne_one : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {t : ℝ},
  χ ^ 2 ≠ 1 ∨ t ≠ 0 → DirichletCharacter.LFunction χ (1 + Complex.I * ↑t) ≠ 0
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- Given a linear map `f : M → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `TensorAlgebra R M → A`.
 -/
TensorAlgebra.lift : (R : Type u_1) →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_3} → [inst_3 : Semiring A] → [inst_4 : Algebra R A] → (M →ₗ[R] A) ≃ (TensorAlgebra R M →ₐ[R] A)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanPrepareModuleHierarchyParams.textDocument : Lean.Lsp.LeanPrepareModuleHierarchyParams → Lean.Lsp.TextDocumentIdentifier
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ap.injEq : ∀ (x : Lean.IR.VarId) (ys : Array Lean.IR.Arg) (x_1 : Lean.IR.VarId) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.Expr.ap x ys = Lean.IR.Expr.ap x_1 ys_1) = (x = x_1 ∧ ys = ys_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- The map `v ↦ v +ᵥ b` as an affine equivalence between a module `V` and an affine space `P` with
tangent space `V`.  -/
AffineEquiv.vaddConst : (k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → P₁ → V₁ ≃ᵃ[k] P₁
-- Mathlib.Data.Multiset.AddSub
Multiset.add_comm : ∀ {α : Type u_1} (s t : Multiset α), s + t = t + s
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.regularMono : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y}
  [self : CategoryTheory.IsRegularMono f], Nonempty (CategoryTheory.RegularMono f)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- Find a representative of a `Lp.simpleFunc`.  -/
MeasureTheory.Lp.simpleFunc.toSimpleFunc : {α : Type u_1} →
  {E : Type u_4} →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} → ↥(MeasureTheory.Lp.simpleFunc E p μ) → MeasureTheory.SimpleFunc α E
-- Mathlib.Data.Int.Lemmas
Int.injOn_natAbs_Ici : Set.InjOn Int.natAbs (Set.Ici 0)
-- Init.Data.List.Basic
/-- Drops the first element of a nonempty list, returning the tail. Returns `none` when the argument is
empty.

Alternatives include `List.tail`, which returns the empty list on failure, `List.tailD`, which
returns an explicit fallback value, and `List.tail!`, which panics on the empty list.

Examples:
 * `["apple", "banana", "grape"].tail? = some ["banana", "grape"]`
 * `["apple"].tail? = some []`
 * `([] : List String).tail = none`
 -/
List.tail? : {α : Type u} → List α → Option (List α)
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
Submonoid.divPairs.eq_1 : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] (f : ⊤.LocalizationMap G)
  (s : Submonoid G), Submonoid.divPairs f s = Submonoid.comap (divMonoidHom.comp ((↑f).prodMap ↑f)) s
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃),
  (f.comp g).hom₃ = CategoryTheory.CategoryStruct.comp f.hom₃ g.hom₃
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (self : PresheafOfModules R) (X : Cᵒᵖ),
  self.map (CategoryTheory.CategoryStruct.id X) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app (self.obj X)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictPseudofunctorCore B C → CategoryTheory.StrictPseudofunctorPreCore B C
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- If the empty sieve is a cover of `X`, then `F(X)` is terminal.  -/
CategoryTheory.Sheaf.isTerminalOfBotCover : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          (F : CategoryTheory.Sheaf J A) →
            (X : C) → ⊥ ∈ J X → CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op X))
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- The Cauchy formula for the derivative of a holomorphic function.  -/
Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ},
  IsOpen U →
    ∀ {c w₀ : ℂ} {R : ℝ} {f : ℂ → E},
      Metric.closedBall c R ⊆ U →
        DifferentiableOn ℂ f U →
          w₀ ∈ Metric.ball c R →
            (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z = deriv f w₀
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- Shortcut instance to help typeclass inference out.  -/
NormedAddTorsor.toAddTorsor' : {V : Type u_1} →
  {P : Type u_2} → [inst : NormedAddCommGroup V] → [inst_1 : MetricSpace P] → [NormedAddTorsor V P] → AddTorsor V P
-- Mathlib.LinearAlgebra.Contraction
contractLeft_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.Dual R M) (m : M), (contractLeft R M) (f ⊗ₜ[R] m) = f m
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  t ∈ nhdsWithin x s →
    UniqueMDiffAt[s] x →
      MDiffAt[t] (T% V) x →
        MDiffAt[t] (T% W) x → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracketWithin I V W t x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E I : Set α},
  (N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ Set.InjOn f I ∧ I ⊆ E
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  {X Y : CategoryTheory.MonoOver (⊤_ C)} (f : X ⟶ Y),
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.map f = CategoryTheory.ObjectProperty.homMk f.hom.left
-- Mathlib.SetTheory.ZFC.Class
Class.instCompleteLattice : CompleteLattice Class.{u_1}
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_map_le_apply_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
  (m : Multiset α) (f : α → β), 0 ≤ f 1 → (∀ (a b : α), f a + f b ≤ f (a * b)) → (Multiset.map f m).sum ≤ f m.prod
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT25Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T25Space M], T25Space Mᵈᵃᵃ
-- Init.Data.String.Substring
/-- Retains only the specified number of characters (Unicode code points) at the end of a substring, by
moving its start position towards its end position.

If the substring's end position is reached, the start position is not advanced past it.
 -/
Substring.Raw.takeRight : Substring.Raw → ℕ → Substring.Raw
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_periodic : Function.Periodic Complex.cos (2 * ↑Real.pi)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andRight.sizeOf_spec : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.andRight ak p) = 1 + sizeOf ak + sizeOf p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.neg_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂), (-z₁).comp z₂ h = -z₁.comp z₂ h
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_of : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : M →* A) (m : M), ((MonoidAlgebra.lift R A M) F) ((MonoidAlgebra.of R M) m) = F m
-- Mathlib.Topology.MetricSpace.Infsep
Finset.coe_infsep : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (s : Finset α),
  (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (Function.uncurry dist) else 0
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_eq : ∀ {α : Type u_1} {xs : ListSlice α},
  Std.Slice.toList xs =
    match xs.internalRepresentation.stop with
    | some stop => List.take stop xs.internalRepresentation.list
    | none => xs.internalRepresentation.list
-- Lean.Meta.Sym.Canon
/-- Canonicalize a proposition that is also a term instance.
Given a term `e` of the form `@Grind.nestedProof prop h`, where `g` is the constant `Grind.nestedProof`,
we canonicalize it as follows:
1- We recursively canonicalize the proposition `prop`.
2- Try to resynthesize the instance, but keep the original one in case of failure since users often
provide them using `haveI`.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInstProp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Submodule.cardQuot_top : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], ⊤.cardQuot = 1
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.evalSimpMatch : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Nat.Cast.Defs
/-- `AddMonoidWithOne` implementation using binary recursion.  -/
AddMonoidWithOne.binary : {R : Type u_1} → [AddMonoid R] → [One R] → AddMonoidWithOne R
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.Props.mk.sizeOf_spec : ∀ (state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef)
  (cancelTk : Lean.Server.WithRpcRef IO.CancelToken),
  sizeOf { state := state, cancelTk := cancelTk } = 1 + sizeOf state + sizeOf cancelTk
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.instInhabitedQuotientCoeSubgroup : {G : Type u_1} → [inst : Group G] → (H K : Subgroup G) → Inhabited (DoubleCoset.Quotient ↑H ↑K)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionHom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {c c' d d' : C} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f g