mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.tower_bot : ∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T), Function.Injective ⇑g → (g.comp f).IsIntegral → f.IsIntegral
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Typeclass stating that the constant sheaf functor has a right adjoint. This right adjoint will
then be called the global sections functor and written `Sheaf.Γ`.  -/
CategoryTheory.HasGlobalSectionsFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} A] → [CategoryTheory.HasWeakSheafify J A] → Prop
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (f : ℱ ⟶ ℱ'.obj)
  {𝒢' : CategoryTheory.Sheaf K A} (g : ℱ' ⟶ 𝒢') {Z : CategoryTheory.Functor Cᵒᵖ A} (h : G.op.comp 𝒢'.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm (CategoryTheory.CategoryStruct.comp f g.hom)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm f)
      (CategoryTheory.CategoryStruct.comp (G.op.whiskerLeft g.hom) h)
-- Mathlib.Data.Fin.SuccPred
/-- A version of the right-to-left implication of `castPred_le_castPred_iff`
that deduces `i ≠ last n` from `i ≤ j` and `j ≠ last n`.  -/
Fin.castPred_le_castPred : ∀ {n : ℕ} {i j : Fin (n + 1)} (h : i ≤ j) (hj : j ≠ Fin.last n), i.castPred ⋯ ≤ j.castPred hj
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp},
  Array.map Prod.fst t.toArray = t.keysArray
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- An upper estimate (in terms of `Asymptotics.IsLittleO`)
on the difference between two compositions of Taylor series.

Let `p₁`, `p₂`, `q₁`, `q₂` be four families of formal multilinear series
depending on a parameter `a`.
Suppose that the norms of `(p₁ · k)`, `(q₁ · k)`, and `(q₂ · k)` are bounded along a filter `l`
for all `k ≤ n`.
Also, suppose that $p₁(a, k) - p₂(a, k) = o(f(a))$, $q₁(a, k) - q₂(a, k) = o(f(a))$
along `l` for all `k ≤ n`.
Then the difference between `n`th terms of `(p₁ a).taylorComp (q₁ a)` and `(p₂ a).taylorComp (q₂ a)`
is `o(f(a))` too.
 -/
FormalMultilinearSeries.taylorComp_sub_taylorComp_isLittleO : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {α : Type u_5} {H : Type u_6}
  [inst_7 : NormedAddCommGroup H] {l : Filter α} {p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G}
  {q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F} {f : α → H} {n : ℕ},
  (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖p₁ x k‖) →
    (∀ k ≤ n, (fun a => p₁ a k - p₂ a k) =o[l] f) →
      (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₁ x k‖) →
        (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₂ x k‖) →
          (∀ k ≤ n, (fun a => q₁ a k - q₂ a k) =o[l] f) →
            (fun a => (p₁ a).taylorComp (q₁ a) n - (p₂ a).taylorComp (q₂ a) n) =o[l] f
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.ExtTreeMap.getEntryGT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α × β
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.IsoLift.mk.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂Iso} {eq : Lean.Expr} {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {eq_1 : Lean.Expr}, { e := e, eq := eq } = { e := e_1, eq := eq_1 } → e = e_1 ∧ eq = eq_1
-- Mathlib.Algebra.Homology.Monoidal
/-- The tensor product of two homological complexes.  -/
HomologicalComplex.tensorObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
          [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
            {I : Type u_2} →
              [inst_5 : AddMonoid I] →
                {c : ComplexShape I} →
                  [inst_6 : c.TensorSigns] →
                    [DecidableEq I] → (K₁ K₂ : HomologicalComplex C c) → [K₁.HasTensor K₂] → HomologicalComplex C c
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
is_bot_adic_iff : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : TopologicalSpace A] [IsTopologicalRing A], IsAdic ⊥ ↔ DiscreteTopology A
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.run_bind' : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β},
  (x >>= f).run = do
    let x ← x.run
    (f x).run
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), Set.uIoo a b = Set.Ioo (min a b) (max a b)
-- Std.Http.Protocol.H1
/-- The HTTP/1.1 protocol state machine.
 -/
Std.Http.Protocol.H1.Machine : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The underlying vertex.  -/
Quiver.SchreierGraph.toVertex : {V : Type u_1} → {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → {_ι : S → M} → Quiver.SchreierGraph V _ι → V
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instSMulIntHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → SMul ℤ (M ⟶ N)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, t.WF → (Std.DTreeMap.Raw.filter f t).size ≤ t.size
-- Mathlib.Data.Set.List
Set.range_list_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.range (List.map f) = {l | ∀ x ∈ l, x ∈ Set.range f}
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom.injEq : ∀ (α α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom),
  (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α_1) =
    (α = α_1)
-- Lean.Level
Lean.mkLevelMVarEx : Lean.LMVarId → Lean.Level
-- Mathlib.Topology.Order.LiminfLimsup
OrderTop.to_BoundedLENhdsClass : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [OrderTop α], BoundedLENhdsClass α
-- Mathlib.GroupTheory.OrderOfElement
mem_zmultiples_zsmul_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {k : ℤ}, g ∈ AddSubgroup.zmultiples (k • g) ↔ k.gcd ↑(addOrderOf g) = 1
-- Mathlib.Data.Set.Restrict
Set.domRestrict_dite_compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
  (g : (a : α) → a ∉ s → β), (sᶜ.domRestrict fun a => if h : a ∈ s then f a h else g a h) = fun a => g ↑a ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct'_comp_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c c' : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hc' : CategoryTheory.Limits.IsColimit c')
  (hf : CategoryTheory.Limits.IsLimit f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom
      (CategoryTheory.Limits.opCoproductIsoProduct' hc' hf).inv =
    (hc.coconePointUniqueUpToIso hc').op.inv
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.send : {α : Type} → Std.CloseableChannel.Zero✝ α → α → BaseIO (Task (Except Std.CloseableChannel.Error Unit))
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) (h0 : 0 ∈ s) [CompactSpace ↑s],
  ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    closure ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.le_iff_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] {x : A} {s : StarSubalgebra R A},
  IsClosed ↑s → (StarAlgebra.elemental R x ≤ s ↔ x ∈ s)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.const.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremType.const = 1
-- Mathlib.CategoryTheory.Dialectica.Monoidal
_private.Mathlib.CategoryTheory.Dialectica.Monoidal.0.CategoryTheory.Dial.termπ₁ : Lean.ParserDescr
-- Mathlib.Data.UInt
UInt32.instNonUnitalCommRing : NonUnitalCommRing UInt32
-- Mathlib.Topology.Order
nhds_false : nhds False = ⊤
-- Init.WF
WellFounded.recursion : {α : Sort u} →
  {r : α → α → Prop} → WellFounded r → {C : α → Sort v} → (a : α) → ((x : α) → ((y : α) → r y x → C y) → C x) → C a
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- A typeclass carrying a choice of lift of a morphism from `C` to `FreeMonoidalCategory C`.
It must be the case that `projectMap id _ _ (LiftHom.lift f) = f` by defeq.  -/
Mathlib.Tactic.Coherence.LiftHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → [Mathlib.Tactic.Coherence.LiftObj X] → [Mathlib.Tactic.Coherence.LiftObj Y] → (X ⟶ Y) → Type u
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.toMultiplicativeBialgEquiv_single : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M] (m : M) (a : A),
  (AddMonoidAlgebra.toMultiplicativeBialgEquiv R A M) (AddMonoidAlgebra.single m a) =
    MonoidAlgebra.single (Multiplicative.ofAdd m) a
-- Mathlib.Data.Nat.Nth
Nat.filter_range_nth_eq_insert_of_finite : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (hf : (Set.ofPred p).Finite) {k : ℕ},
  k + 1 < hf.toFinset.card →
    {n ∈ Finset.range (Nat.nth p (k + 1)) | p n} = insert (Nat.nth p k) ({n ∈ Finset.range (Nat.nth p k) | p n})
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.objEquiv_apply_fst : ∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  (i : Fin (n + 1)), ((SSet.prodStdSimplex.objEquiv x) i).1 = x.1 i
-- Lean.Attributes
Lean.AttributeImplCore.descr : Lean.AttributeImplCore → String
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.constant : Lean.Lsp.SymbolKind
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- The reduction of a Weierstrass curve over `K` given by a minimal Weierstrass equation,
which is a Weierstrass curve over the residue field of `R`.  -/
WeierstrassCurve.reduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [inst_2 : IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] →
            [inst_4 : Algebra R K] →
              [inst_5 : IsFractionRing R K] →
                (W : WeierstrassCurve K) →
                  [WeierstrassCurve.IsMinimal R W] → WeierstrassCurve (IsLocalRing.ResidueField R)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The pullback commutes with the Lie bracket of vector fields on manifolds.  -/
VectorField.mpullback_mlieBracketWithin : ∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M]
  [inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'}
  {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'},
  MDiffAt[t] (T% V) (f x₀) →
    MDiffAt[t] (T% W) (f x₀) →
      UniqueMDiff[s] →
        ContMDiffAt I I' n f x₀ →
          x₀ ∈ s →
            minSmoothness 𝕜 2 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                VectorField.mpullback I I' f (VectorField.mlieBracketWithin I' V W t) x₀ =
                  VectorField.mlieBracketWithin I (VectorField.mpullback I I' f V) (VectorField.mpullback I I' f W) s x₀
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen {K | (↑K ∩ U).Nonempty}
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- The product of `X` with an initial object in a category with strict initial objects is itself
initial.
This is the generalisation of the fact that `Empty × X ≃ Empty` for types (or `0 * n = 0`).
 -/
CategoryTheory.Limits.initialMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        (X : C) → [inst_3 : CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] → (⊥_ C) ⨯ X ≅ ⊥_ C
-- Mathlib.Data.List.Rotate
List.IsRotated.nodup_iff : ∀ {α : Type u} {l l' : List α}, l ~r l' → (l.Nodup ↔ l'.Nodup)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq : ∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              Set.MapsTo f s t →
                f x₀ = y₀ →
                  ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) s x₀
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulLeft.congr_simp : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x x_1 : X),
  x = x_1 → ContinuousMap.mulLeft x = ContinuousMap.mulLeft x_1
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'.eq_1 : ∀ (acc : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  (Lean.Grind.AC.Seq.var x).sort' acc = Lean.Grind.AC.Seq.insert x acc
-- Init.Data.SInt.Basic
/-- Strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
 -/
Int16.lt : Int16 → Int16 → Prop
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.countP` as a bundled multiplicative monoid homomorphism.  -/
FreeMonoid.countP : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → FreeMonoid α →* Multiplicative ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine.eq_1 : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Jacobian F) (P : Fin 3 → F),
  WeierstrassCurve.Jacobian.Point.toAffine W P =
    if hP : W.Nonsingular P ∧ P 2 ≠ 0 then WeierstrassCurve.Affine.Point.some (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) ⋯ else 0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
GroupWithZero.eq_zero_or_unit : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a = 0 ∨ ∃ u, a = ↑u
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- any cocone descends (in a unique way) as a map  -/
CategoryTheory.Functor.CoconeTypes.IsColimitCore.desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      {c : F.CoconeTypes} → c.IsColimitCore → (c' : F.CoconeTypes) → c.pt → c'.pt
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingEquiv.ofLeftInverseS_symm_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {g : S → R} {f : R →+* S}
  (h : Function.LeftInverse g ⇑f) (x : ↥f.rangeS), (RingEquiv.ofLeftInverseS h).symm x = g ↑x
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.fst : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} [MeasureTheory.SFinite P]
  {Y : Ω → 𝓨 × 𝓩} {κ : ProbabilityTheory.Kernel 𝓧 (𝓨 × 𝓩)} [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P → ProbabilityTheory.HasCondDistrib (fun ω => (Y ω).1) X κ.fst P
-- Mathlib.Algebra.Category.Grp.EpiMono
/-- Define `h : B ⟶ S(X')` to be `τ g τ⁻¹`
 -/
GrpCat.SurjectiveOfEpiAuxs.h : {A B : GrpCat} → (f : A ⟶ B) → ↑B →* Equiv.Perm (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBotCoeff.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α α_1 : L → R),
  α = α_1 → ∀ (β β_1 : LieModule.Weight R L M), β = β_1 → LieModule.chainBotCoeff α β = LieModule.chainBotCoeff α_1 β_1
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_toArray_rcc : ∀ {m n : ℤ}, (m...=n).toArray.toList = (m...=n).toList
-- Lean.Server.ServerTask
Lean.Server.instCoeTaskServerTask : {α : Type u_1} → Coe (Task α) (Lean.Server.ServerTask α)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), (Lean.Meta.Origin.fvar fvarId = Lean.Meta.Origin.fvar fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Data.Set.Order
MonotoneOn.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x ∩ g x) s
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.mem_span_support_coeff`.

---

An element of `k[G]` is in the subalgebra generated by its support.  -/
MonoidAlgebra.mem_span_support : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : MulOneClass G] (f : MonoidAlgebra k G),
  f ∈ Submodule.span k (⇑(MonoidAlgebra.of k G) '' ↑f.coeff.support)
-- Mathlib.Data.Set.Pointwise.Support
/-- Note: to_additive also automatically translates `SMul` to `VAdd`, so we give the additive
version manually.  -/
support_comp_inv_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Zero γ] (c : α)
  (f : β → γ), (Function.support fun x => f (c⁻¹ • x)) = c • Function.support f
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse : ∀ {X X' : SSet.Truncated 2} (Y : SSet.Truncated 2) (f : X ⟶ X'),
  ((SSet.Truncated.mapHomotopyCategory f).prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X' Y) =
    (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingSum.eq_def : ∀ {G : Type u_4} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (x : List G),
  x.alternatingSum =
    match x with
    | [] => 0
    | [g] => g
    | g :: h :: t => g + -h + t.alternatingSum
-- Init.Core
iff_of_true : ∀ {a b : Prop}, a → b → (a ↔ b)
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.hom_apply : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), (legendreSym.hom p) a = legendreSym p a
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {M : Type u_4} [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : CategoryTheory.HasShift D M]
  [inst_6 : CategoryTheory.HasShift E M] {X Y : C} {a : M} (f : CategoryTheory.ShiftedHom X Y a)
  (F : CategoryTheory.Functor C D) [inst_7 : F.CommShift M] (G : CategoryTheory.Functor D E) [inst_8 : G.CommShift M],
  f.map (F.comp G) = (f.map F).map G
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a`  -/
AddAction.IsBlock.stabilizer_le : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B → ∀ {a : X}, a ∈ B → AddAction.stabilizer G a ≤ AddAction.stabilizer G B
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.object : Lean.IR.IRType
-- Mathlib.MeasureTheory.Integral.Prod
/-- **Fubini's Theorem** for set integrals.  -/
MeasureTheory.setIntegral_prod : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α × β → E) {s : Set α} {t : Set β},
  MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.prod ν) →
    ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.Algebra.Homology.Augment
ChainComplex.chainComplex_d_succ_succ_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i : ℕ), C.d (i + 2) 0 = 0
-- Lean.Parser.Extension
Lean.Parser.getParserAliasInfo : Lean.Name → IO Lean.Parser.ParserAliasInfo