mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The isotropy subgroupoid of `S`  -/
CategoryTheory.Subgroupoid.disconnect : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → CategoryTheory.Subgroupoid C
-- Lean.Parser.Do
Lean.Parser.Term.termBeforeDo.formatter : Lean.PrettyPrinter.Formatter
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn.eq : ∀ {i : Type u} {motive_1 : Lean.Doc.Inline i → Sort u_1} {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1}
  {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} (t : Lean.Doc.Inline i)
  (F_1 : (t : Lean.Doc.Inline i) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Doc.Inline.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The (unique) morphism from `⊥ : MonoOver X` to any other `f : MonoOver X`.  -/
CategoryTheory.MonoOver.botLE : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] →
      [inst_2 : CategoryTheory.Limits.InitialMonoClass C] → {X : C} → (f : CategoryTheory.MonoOver X) → ⊥ ⟶ f
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_sum_filter : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s : Set α) [inst_1 : DecidablePred fun x => x ∈ s]
  (hf : Function.HasFiniteSupport f), ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ Set.Finite.toFinset hf with i ∈ s, f i
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.nonrec.sizeOf_spec : sizeOf Lean.Elab.RecKind.nonrec = 1
-- Init.Data.String.Defs
String.Pos.isAtEnd_iff : ∀ {s : String} {pos : s.Pos}, pos.IsAtEnd ↔ pos = s.endPos
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are field extensions of `F`, there exists a field extension `E` of `F` that
`A` and `B` embed into with linearly disjoint images, then `A ⊗[F] B` is a domain.  -/
IntermediateField.LinearDisjoint.isDomain' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : Type u_1} {B : Type u_2}
  [inst_3 : Field A] [inst_4 : Algebra F A] [inst_5 : Field B] [inst_6 : Algebra F B] {fa : A →ₐ[F] E} {fb : B →ₐ[F] E},
  fa.fieldRange.LinearDisjoint ↥fb.fieldRange → IsDomain (TensorProduct F A B)
-- Lean.Setup
Lean.instReprModuleSetup.repr : Lean.ModuleSetup → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.exactFunctor_le_leftExactFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  CategoryTheory.exactFunctor C D ≤ CategoryTheory.leftExactFunctor C D
-- Mathlib.Algebra.Group.Action.End
/-- The additive monoid hom representing an additive monoid action.

When `M` is a group, see `AddAction.toPermHom`.  -/
AddAction.toEndHom : {M : Type u_2} → {α : Type u_5} → [inst : AddMonoid M] → [AddAction M α] → M →+ Additive (Function.End α)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
/-- If an irreducible has a prime factorization,
then it is an associate of one of its prime factors.  -/
prime_factors_irreducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a : α} {f : Multiset α},
  Irreducible a → (∀ b ∈ f, Prime b) ∧ Associated f.prod a → ∃ p, Associated a p ∧ f = {p}
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_eq : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral f = MeasureTheory.L1.integralCLM f
-- Mathlib.Analysis.Normed.Module.Basic
SeminormedSpace.Core.norm_smul : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Norm E]
  [inst_3 : Module 𝕜 E], SeminormedSpace.Core 𝕜 E → ∀ (c : 𝕜) (x : E), ‖c • x‖ = ‖c‖ * ‖x‖
-- Lean.Compiler.ModPkgExt
Lean.registerModuleEnvExtension : {σ : Type} →
  [Inhabited σ] → IO σ → autoParam Lean.Name Lean.registerModuleEnvExtension._auto_1 → IO (Lean.ModuleEnvExtension σ)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkLocalInstanceLetDecls : Lean.Elab.Deriving.Context →
  Lean.Name → Array Lean.Name → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.letDecl))
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (t : CategoryTheory.Limits.Cocone G) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom
      (CategoryTheory.Limits.colimit.desc G t) =
    CategoryTheory.Limits.colimit.desc F ((CategoryTheory.Limits.Cocone.precompose w.hom).obj t)
-- Init.Data.Int.Order
Int.le.dest_sub : ∀ {a b : ℤ}, a ≤ b → ∃ n, b - a = ↑n
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYoneda_inv_app_hom_apply : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCatᵒᵖ)
  (a :
    (CategoryTheory.Limits.Types.productLimitCone fun x =>
          F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone.pt),
  (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).inv.app X)) a =
    (CategoryTheory.CategoryStruct.id
          (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt))).hom'
      ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv
                    (CategoryTheory.Discrete.natIso fun j =>
                      CategoryTheory.Iso.refl (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
                    (F.mapCone
                      (CategoryTheory.Limits.Fan.mk
                        (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt)
                        fun a =>
                        ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj a).op))).symm
                (CategoryTheory.Limits.isLimitOfPreserves F
                  (CategoryTheory.Limits.Cofan.IsColimit.op
                    (LightCondensed.fintypeCatAsCofanIsColimit (LightProfinite.of (Opposite.unop X).obj))))).lift
            (CategoryTheory.Limits.Types.productLimitCone fun x =>
                F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone).hom'
        a)
-- Mathlib.Analysis.Convex.Basic
convex_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E}, (∀ (i : ι), Convex 𝕜 (s i)) → Convex 𝕜 (⋂ i, s i)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `k`-linear `G`-representation `A`, there is a `k`-linear isomorphism between
representation morphisms `Hom(k[G], A)` and `A`.  -/
Rep.leftRegularHomEquiv : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] → [inst_1 : Monoid G] → (A : Rep.{max u v, u, v} k G) → (Rep.leftRegular k G ⟶ A) ≃ₗ[k] ↑A
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofBitVec : ∀ (b : BitVec 32), { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }
-- Mathlib.Topology.Order.IsLUB
IsLUB.mem_upperBounds_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  MonotoneOn f s → IsLUB s a → Filter.Tendsto f (nhdsWithin a s) (nhds b) → b ∈ upperBounds (f '' s)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.subtype_comp_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  (p : L.Substructure N) (h : ∀ (b : M), f b ∈ p), p.subtype.toHom.comp (FirstOrder.Language.Hom.codRestrict p f h) = f
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inr_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.snd X Y) =
    CategoryTheory.CategoryStruct.id Y
-- Std.Internal.UV.System
/-- Sets the scheduling priority of a process.
 -/
Std.Internal.UV.System.osSetPriority : UInt64 → Int64 → IO Unit
-- Mathlib.Data.Stream.Init
Stream'.tails_eq_iterate : ∀ {α : Type u} (s : Stream' α), s.tails = Stream'.iterate Stream'.tail s.tail
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, m.contains a = true → m[a]? = some (m.getD a fallback)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.logDeriv_cos : logDeriv Complex.cos = -Complex.tan
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprSyntax_mathlib : Lean.ToExpr Lean.Syntax
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_1 x
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongrEquiv_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) (f : P₁ →ᵃ[k] P₃)
  (x : P₂), ((e₁.arrowCongrEquiv e₂) f) x = e₂ (f (e₁.symm x))
-- Mathlib.Algebra.Order.Field.Basic
one_le_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → a ≤ 1 → 1 ≤ 1 / a
-- Mathlib.Order.Sublocale
Sublocale.infClosed : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X}, InfClosed ↑S
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- **Alias** of `SheafOfModules.Presentation.ofIsIso`.

---

Mapping a presentation under an isomorphism.  -/
SheafOfModules.Presentation.of_isIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M N : SheafOfModules R} → (f : M ⟶ N) → [CategoryTheory.IsIso f] → M.Presentation → N.Presentation
-- Init.Data.Array.Lemmas
Array.getElem_push_lt : ∀ {α : Type u_1} {xs : Array α} {x : α} {i : ℕ} (h : i < xs.size),
  have this := ⋯;
  (xs.push x)[i] = xs[i]
-- Mathlib.Topology.Separation.GDelta
Set.Subsingleton.isGδ_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [T1Space X], s.Subsingleton → IsGδ sᶜ
-- Mathlib.Data.List.Rotate
List.rotate_nil : ∀ {α : Type u} (n : ℕ), [].rotate n = []
-- Init.Data.ToString.Basic
instToStringUSize : ToString USize
-- Mathlib.FieldTheory.Normal.Closure
IsNormalClosure.splits : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} {inst : Field F} {inst_1 : Field K} {inst_2 : Field L}
  {inst_3 : Algebra F K} {inst_4 : Algebra F L} [self : IsNormalClosure F K L] (x : K),
  (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
-- Mathlib.Logic.Equiv.Basic
/-- Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the
LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. For that reason,
we have to explicitly substitute along `e.symm (e a) = a` in the statement of this lemma.  -/
Equiv.piCongrLeft'_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (f : (b : β) → P (e.symm b)) (x : α),
  (Equiv.piCongrLeft' P e).symm f x = ⋯ ▸ f (e x)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  ModuleCat.Hom.hom S.moduleCatLeftHomologyData.π = S.moduleCatToCycles.range.mkQ
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.«termΓ(_,_)_1» : Lean.ParserDescr
-- Mathlib.Topology.Covering.Basic
/-- If `f : E → X` is a continuous map between Hausdorff spaces with `E` compact,
and `f` restricts to a homeomorphism on a neighborhood of every point of a fiber `f ⁻¹' {x}`,
then `x` admits an evenly covered neighborhood.  -/
IsEvenlyCovered.of_openPartialHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} [T2Space E]
  [T2Space X] [CompactSpace E] {x : X},
  Continuous f → (∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f) → IsEvenlyCovered f x ↑(f ⁻¹' {x})
-- Mathlib.RingTheory.PowerSeries.Exp
/-- Shows that $e^{x} * e^{-x} = 1$  -/
PowerSeries.exp_mul_exp_neg_eq_one : ∀ {A : Type u_4} [inst : CommRing A] [inst_1 : Algebra ℚ A],
  PowerSeries.exp A * PowerSeries.evalNegHom (PowerSeries.exp A) = 1
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_symm_tmul : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (a : A) (b : B),
  (Algebra.TensorProduct.comm R A B).symm (b ⊗ₜ[R] a) = a ⊗ₜ[R] b
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.omega0_pos : 0 < Ordinal.omega0
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α)
  (a_1 a_2 : Std.DHashMap.Internal.AssocList α β),
  a_1 = a_2 → Std.DHashMap.Internal.AssocList.getCast? a a_1 = Std.DHashMap.Internal.AssocList.getCast? a a_2
-- Mathlib.Combinatorics.SetFamily.FourFunctions
sum_collapse : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {𝒜 : Finset (Finset α)} {a : α}
  {f : Finset α → β} {u : Finset α},
  𝒜 ⊆ (insert a u).powerset → a ∉ u → ∑ s ∈ u.powerset, collapse✝ 𝒜 a f s = ∑ s ∈ 𝒜, f s
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.inv_pos' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < r⁻¹
-- Mathlib.NumberTheory.ZetaValues
integral_bernoulliFun : ∀ (k : ℕ), ∫ (x : ℝ) in 0..1, bernoulliFun k x = if k = 0 then 1 else 0
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_eq_rootMultiplicity : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.rootMultiplicity t p = Polynomial.rootMultiplicity 0 (p.comp (Polynomial.X + Polynomial.C t))
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.apply_iUnion_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {f : ℕ → Set Ω},
  (Summable fun n => μ (f n)) → μ (⋃ n, f n) ≤ ∑' (n : ℕ), μ (f n)
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodAssoc.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P],
  MulEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_mul' := ⋯ }
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The homology data of `(K.extend e).sc' i' j' k'` that is deduced
from a homology data of `K.sc' i j k`.  -/
HomologicalComplex.extend.homologyData : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        e.f j = j' →
                          c.prev j = i →
                            c'.prev j' = i' →
                              c.next j = k →
                                c'.next j' = k' → (K.sc' i j k).HomologyData → ((K.extend e).sc' i' j' k').HomologyData
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
inv_mabs_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] (a : α), |a|ₘ⁻¹ ≤ a
-- Init.Data.SInt.Bitwise
Int8.zero_xor : ∀ {a : Int8}, 0 ^^^ a = a
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} [inst_1 : SizeOf C] [inst_2 : SizeOf I]
  (ev : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T)))
  (ev_precomp :
    autoParam
      (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
        (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev i j a b) =
          ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
      CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam),
  sizeOf { ev := ev, ev_precomp := ev_precomp } = 1
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_neg' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : α → E),
  MeasureTheory.setToFun μ (-T) ⋯ f = -MeasureTheory.setToFun μ T hT f
-- Mathlib.GroupTheory.GroupAction.Basic
/-- `smul` by a `k : M` over a group is injective, if `k` is not a zero divisor.
The general theory of such `k` is elaborated by `IsSMulRegular`.
The typeclass that restricts all terms of `M` to have this property is `Module.IsTorsionFree`.  -/
smul_cancel_of_non_zero_divisor : ∀ {M : Type u_1} {G : Type u_2} [inst : Monoid M] [inst_1 : AddGroup G] [inst_2 : DistribMulAction M G] (k : M),
  (∀ (x : G), k • x = 0 → x = 0) → ∀ {a b : G}, k • a = k • b → a = b
-- Aesop.Forward.SlotIndex
Aesop.instInhabitedSlotIndex.default : Aesop.SlotIndex
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.corootSubmodule_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] (I : LieIdeal K L)
  {α : LieModule.Weight K (↥H) L},
  LieAlgebra.rootSpace H ⇑α ≤ LieSubmodule.restr I H → LieAlgebra.IsKilling.corootSubmodule α ≤ LieSubmodule.restr I H
-- Init.Data.SInt.Lemmas
Int16.sub_neg : ∀ {a b : Int16}, a - -b = a + b
-- Mathlib.Topology.ContinuousOn
/-- See also `continuousWithinAt_sdiff_singleton` for the case of `s \ {y}`, but
requiring `T1Space α`.  -/
continuousWithinAt_sdiff_self : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_obj_right_obj : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : D), ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj X).right.obj X_1 = G.obj (X.right.obj X_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.open_source : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : OpenPartialHomeomorph X Y), IsOpen self.source
-- Mathlib.Data.Int.CharZero
Function.support_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne β] [CharZero β] {n : ℤ}, n ≠ 0 → Function.support ↑n = Set.univ
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Evaluation of functions into an indexed collection of additive
monoids at a point is an additive monoid homomorphism. This is `Function.eval i` as an
`AddMonoidHom`.  -/
Pi.evalAddMonoidHom : {I : Type u} → (f : I → Type v) → [inst : (i : I) → AddZeroClass (f i)] → (i : I) → ((i : I) → f i) →+ f i
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_ite_eq`.  -/
Fintype.prod_ite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι) (f : ι → M),
  (∏ j, if i = j then f j else 1) = f i
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Taking the pointwise norm of a bounded continuous function with values in a
`SeminormedAddCommGroup` yields a bounded continuous function with values in ℝ.  -/
BoundedContinuousFunction.normComp : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] → BoundedContinuousFunction α β → BoundedContinuousFunction α ℝ
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_one : ∀ {α : Type u_2} [inst : One α] {p : α → Prop}, (∀ᶠ (x : α) in 1, p x) ↔ p 1
-- Mathlib.RingTheory.Bialgebra.Basic
/-- A bialgebra over a nontrivial ring is nontrivial.  -/
Bialgebra.nontrivial : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [Bialgebra R A] [Nontrivial R],
  Nontrivial A
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- A type synonym for endowing a given type with a `CStarModule` structure. This has the scoped
notation `C⋆ᵐᵒᵈ`.  -/
WithCStarModule : Type u_1 → Type u_2 → Type u_2
-- Mathlib.Data.List.Sigma
List.kerase_cons_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)},
  a = s.fst → List.kerase a (s :: l) = l
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.oset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.Compiler.LCNF.Arg pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.oset fvarId i y h) = 1 + sizeOf fvarId + sizeOf i + sizeOf y + sizeOf h
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Delaborator for `mvfderivWithin`.  -/
Manifold.delabMVFDerivWithin : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isSome = !t.isEmpty
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.multipliable_powerSeriesMk_card_countRestricted : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] (m : ℕ),
  Multipliable fun i => ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of `Asymptotics.IsEquivalent.summable_iff`. -/
IsEquivalent.summable_iff : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f g : ι → E}, Asymptotics.IsEquivalent Filter.cofinite f g → (Summable f ↔ Summable g)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHomOfLE.congr_simp : ∀ {V : Type u_1} (G : SimpleGraph V) {s s' : Set V} (h : s ⊆ s'), G.induceHomOfLE h = G.induceHomOfLE h