mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.sum_whiskerRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {Q R : C} {J : Type u_2}
  (s : Finset J) (g : J → (Q ⟶ R)) (P : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (∑ j ∈ s, g j) P =
    ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.whiskerRight (g j) P
-- Mathlib.Topology.Connected.LocallyPathConnected
IsOpen.isConnected_iff_isPathConnected : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsOpen U → (IsConnected U ↔ IsPathConnected U)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filterMap : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} [inst_1 : Monad n]
  [LawfulMonad n] [inst_3 : Std.Do.WPMonad n ps] [Std.Iterators.Finite α Id] [inst_5 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc =>
        match f out with
        | some c => g c acc
        | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterMap f it) init g ⦃Q⦄
-- Mathlib.Order.ULift
ULift.up_compare : ∀ {α : Type u} [inst : Ord α] (a b : α), compare { down := a } { down := b } = compare a b
-- Mathlib.LinearAlgebra.Span.Defs
/-- The span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.  -/
Submodule.span : (R : Type u_1) →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set M → Submodule R M
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMkSucc_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (β : F.δ₀ ⟶ G.δ₀)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
          (CategoryTheory.ComposableArrows.app' β 0 ⋯) =
        CategoryTheory.CategoryStruct.comp α (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯))
      _auto_220✝),
  (CategoryTheory.ComposableArrows.homMkSucc α β w).app 0 = α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Given a fixed family of limit data for every pair `X Y`, we obtain an associator.  -/
CategoryTheory.Limits.BinaryFan.associatorOfLimitCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (L : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) →
      (X Y Z : C) → (L (L X Y).cone.pt Z).cone.pt ≅ (L X (L Y Z).cone.pt).cone.pt
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a left homology data `h` of a short complex `S` is preserved by a functor `F`,
this is the induced left homology data `h.map F` for the short complex `S.map F`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              (h : S.LeftHomologyData) →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.PreservesZeroMorphisms] → [h.IsPreservedBy F] → (S.map F).LeftHomologyData
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.mk' : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.support.Nodup → p.IsPath
-- Mathlib.CategoryTheory.Shift.CommShift
/-- Given an isomorphism `e : F ⋙ G ≅ H` where `G` is fully faithful,
the functor `F` commutes with shifts by `A` if `G` and `H` do.  -/
CategoryTheory.Functor.CommShift.ofComp : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D E} →
                {H : CategoryTheory.Functor C E} →
                  (F.comp G ≅ H) →
                    [G.Full] →
                      [G.Faithful] →
                        (A : Type u_5) →
                          [inst_5 : AddMonoid A] →
                            [inst_6 : CategoryTheory.HasShift C A] →
                              [inst_7 : CategoryTheory.HasShift D A] →
                                [inst_8 : CategoryTheory.HasShift E A] →
                                  [G.CommShift A] → [H.CommShift A] → F.CommShift A
-- Lean.Meta.DiscrTree.Util
/-- Fold over the keys and values stored in a `DiscrTree`
 -/
Lean.Meta.DiscrTree.fold : {σ : Type u_1} → {α : Type} → (σ → Array Lean.Meta.DiscrTree.Key → α → σ) → σ → Lean.Meta.DiscrTree α → σ
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂ δ).app X₁).app X₂).app X₃ =
    (δ.app X₁).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.between.eq_1 : ∀ {V : Type u_1} (s t : Set V) (G : SimpleGraph V),
  SimpleGraph.between s t G =
    { Adj := fun v w => G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s), symm := ⋯, loopless := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b), CategoryTheory.CategoryStruct.comp self.f h.p₁ = g₁
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_pos : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), 0 < Nat.multinomial s f
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatFiberOfGeometricallyConnected : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyConnected f],
  ConnectedSpace ↥(AlgebraicGeometry.Scheme.Hom.fiber f s)
-- Mathlib.RingTheory.Artinian.Module
/-- This is the Fitting decomposition of the module `M` with respect to the endomorphism `f`.

See also `LinearMap.eventually_isCompl_ker_pow_range_pow` for an alternative spelling.  -/
LinearMap.isCompl_iSup_ker_pow_iInf_range_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M] (f : M →ₗ[R] M), IsCompl (⨆ n, (f ^ n).ker) (⨅ n, (f ^ n).range)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_le_iff' : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ↪r s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.op : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered α → CategoryTheory.NatTrans.Coequifibered (CategoryTheory.NatTrans.op α)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.mk.inj : ∀ {α σ : Type} {name : autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam} {addEntry : σ → α → σ}
  {initial : σ} {finalizeImport : σ → σ} {exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α)}
  {name_1 : autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam} {addEntry_1 : σ → α → σ}
  {initial_1 : σ} {finalizeImport_1 : σ → σ} {exportEntry?_1 : Lean.Environment → α → Lean.OLeanEntries (Option α)},
  { name := name, addEntry := addEntry, initial := initial, finalizeImport := finalizeImport,
        exportEntry? := exportEntry? } =
      { name := name_1, addEntry := addEntry_1, initial := initial_1, finalizeImport := finalizeImport_1,
        exportEntry? := exportEntry?_1 } →
    name = name_1 ∧
      addEntry = addEntry_1 ∧ initial = initial_1 ∧ finalizeImport = finalizeImport_1 ∧ exportEntry? = exportEntry?_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).getKey? k = if t₂.contains k = true then t₁.getKey? k else none
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.OplaxTrans.Hom η θ}, x.as = y.as → x = y
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.foldUntil.eq_def : ∀ {α : Type u_1} (it : String.Legacy.Iterator) (init : α) (f : α → Char → Option α),
  it.foldUntil init f =
    if it.atEnd = true then (init, it)
    else
      match f init it.curr with
      | some a => it.next.foldUntil a f
      | x => (init, it)
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_isMax : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α],
  Order.IsPredPrelimit a ↔ IsMax a
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.iff_of_associated : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} {r r' : R},
  Associated r r' → (IsLocalizedModule.Away r f ↔ IsLocalizedModule.Away r' f)
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.colimitLimitIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)),
  CategoryTheory.Limits.colimitLimitIso F = CategoryTheory.Limits.colimitLimitIso F
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instIntCastSubtypeMemAddSubgroup : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → IntCast ↥(selfAdjoint R)
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- The intervals `(0, k + 1)` have finite measure `MeasureTheory.Measure.volumeIoiPow _`
and cover the whole open ray `(0, +∞)`.  -/
MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio : (n : ℕ) → (MeasureTheory.Measure.volumeIoiPow n).FiniteSpanningSetsIn (Set.range Set.Iio)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.toMulEquiv_symm : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (f : A ≃⋆* B),
  f.symm.toMulEquiv = f.symm
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.tendstoUniformlyOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α),
  IsTopologicalGroup.rightUniformSpace G = u →
    (TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1)
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Typeclass asserting that the sets in `L.filter` are eventually contained in `L.support`. This
is a sufficient condition for `L`-summation to behave well on finitely-supported functions: every
finitely-supported `f` is `L`-summable with the sum `∑ᶠ x ∈ L.support, f x` (and similarly for
products).  -/
SummationFilter.HasSupport : {β : Type u_2} → SummationFilter β → Prop
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_le_iff_le_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  {f : BoundedLatticeHom α β} {M : BooleanSubalgebra β}, BooleanSubalgebra.map f L ≤ M ↔ L ≤ BooleanSubalgebra.comap f M
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A}
  (H : g.IsWeierstrassFactorization f h), f.degree = ↑(((PowerSeries.map (IsLocalRing.residue A)) g).order.lift ⋯)
-- Mathlib.Topology.MetricSpace.Defs
instMetricSpaceEmpty : MetricSpace Empty
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- The even terms of `expSeries` are real, and correspond to the series for $\cos ‖q‖$.  -/
Quaternion.expSeries_even_of_imaginary : ∀ {q : Quaternion ℝ},
  q.re = 0 →
    ∀ (n : ℕ),
      ((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n).factorial)
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] [Module.Flat ↑R ↑S],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (R.tensorProd S)
-- Lean.Environment
/-- Information from exported contexts.  -/
Lean.OLeanLevel.exported : Lean.OLeanLevel
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as an `AddMonoidHom`.  -/
Finset.singletonAddMonoidHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : AddZeroClass α] → α →+ Finset α
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instIsBotZeroClass : ∀ {ι : Type u_1} (α : ι → Type u_2) [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), IsBotZeroClass (α i)], IsBotZeroClass (Π₀ (i : ι), α i)
-- Mathlib.Data.FP.Basic
FP.ofPosRatDn : [C : FP.FloatCfg] → ℕ+ → ℕ+ → FP.Float × Bool
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The bijection between the additive free group on the empty type,
and a type with one element.  -/
FreeAddGroup.freeAddGroupEmptyEquivAddUnit : FreeAddGroup Empty ≃ Unit
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.sInter : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {S : Set (Set α)},
  S.Nonempty → (∀ s ∈ S, IsRelUpperSet s P) → IsRelUpperSet (⋂₀ S) P
-- Init.Meta.Defs
/-- Creates a globally unique `Name`, without any semantic interpretation.
The names are not intended to be user-visible.
With the default name generator, names use `_uniq` as a base and have a numeric suffix.

This is used for example by `Lean.mkFreshFVarId`, `Lean.mkFreshMVarId`, and `Lean.mkFreshLMVarId`.
To create fresh user-visible identifiers, use functions such as `Lean.Core.mkFreshUserName` instead.
 -/
Lean.mkFreshId : {m : Type → Type} → [Monad m] → [Lean.MonadNameGenerator m] → m Lean.Name
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.SplitEpi.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (section_ section__1 : Y ⟶ X)
  (e_section_ : section_ = section__1)
  (id : CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y),
  { section_ := section_, id := id } = { section_ := section__1, id := ⋯ }
-- Mathlib.Topology.Spectral.Hom
instCoeTCSpectralMapOfSpectralMapClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : FunLike F α β] → [SpectralMapClass F α β] → CoeTC F (SpectralMap α β)
-- Lean.Expr
Lean.instInhabitedLiteral.default : Lean.Literal
-- Mathlib.Algebra.Group.Equiv.Defs
MonoidHom.toMulEquiv_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (g : N →* M)
  (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N), ⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
-- Mathlib.Logic.Function.Basic
eq_rec_inj : ∀ {α : Sort u_1} {a a' : α} (h : a = a') {C : α → Type u_3} (x y : C a), h ▸ x = h ▸ y ↔ x = y
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_finite : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [Finite ι]
  {F : ι → X → α} {S : Set X} {x₀ : X}, EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.mk.sizeOf_spec : ∀ (value : Lean.Expr) (compile isPrivate : Bool),
  sizeOf { value := value, compile := compile, isPrivate := isPrivate } =
    1 + sizeOf value + sizeOf compile + sizeOf isPrivate
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.getLast_support : ∀ {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b), p.support.getLast ⋯ = b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Structure witnessing that a binary bicone is a limit cone and a limit cocone.  -/
CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {b : CategoryTheory.Limits.BinaryBicone P Q} → b.IsBilimit → CategoryTheory.Limits.IsColimit b.toCocone
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instFullSimplexCategory : CategoryTheory.Functor.Full SSet.stdSimplex
-- Init.Data.UInt.Lemmas
USize.lt_irrefl : ∀ (a : USize), ¬a < a
-- Std.Http.Protocol.H1.Parser
/-- Parses a single space (SP, 0x20).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.sp : Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) {F F' : CategoryTheory.Sheaf J (Type v)} (f : F ⟶ F')
  (x : F.obj.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (J.yonedaEquiv.symm x) f =
    J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`,
and for each `g i` let `n i` be a natural number.
Let `K` be an algebra over `R[X]` containing inverses `gi i` for each `g i`.
Then a fraction of the form `f * ∏ i ∈ s, gi i ^ n i` can be rewritten as
`q + ∑ i ∈ s, ∑ j : Fin (n i), r i j * gi i ^ (j + 1)`
in at most one way, where `degree (r i j) < degree (g i)`.
See `mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse` for the
existence of such a representation.  -/
Polynomial.quo_add_sum_rem_mul_pow_inverse_unique : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : CommRing K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] {ι : Type u_3} {s : Finset ι} {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {n : ι → ℕ} {gi : ι → K},
        (∀ i ∈ s, gi i * (algebraMap (Polynomial R) K) (g i) = 1) →
          ∀ {q₁ q₂ : Polynomial R} {r₁ r₂ : (i : ι) → Fin (n i) → Polynomial R},
            (∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree) →
              (∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree) →
                (algebraMap (Polynomial R) K) q₁ +
                      ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r₁ i j) * gi i ^ (↑j + 1) =
                    (algebraMap (Polynomial R) K) q₂ +
                      ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r₂ i j) * gi i ^ (↑j + 1) →
                  q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_sum_eq : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] (μ : ι → MeasureTheory.Measure α),
  MeasureTheory.ae (MeasureTheory.Measure.sum μ) = ⨆ i, MeasureTheory.ae (μ i)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.isContinuous_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Functor.id C).IsContinuous J J
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.eq_singletonSubgraph_iff_verts_eq : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) {v : V}, H = G.singletonSubgraph v ↔ H.verts = {v}
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The image of a totally bounded set under a uniformly continuous map is totally bounded.  -/
TotallyBounded.image : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : α → β} {s : Set α},
  TotallyBounded s → UniformContinuous f → TotallyBounded (f '' s)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_iUnion : ∀ {X : Type u_2} [inst : EMetricSpace X] {ι : Sort u_4} [Countable ι] (s : ι → Set X), dimH (⋃ i, s i) = ⨆ i, dimH (s i)
-- Mathlib.Data.UInt
UInt8.instNonUnitalCommRing : NonUnitalCommRing UInt8
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is right-regular if and only if `R` is trivial.  -/
IsRightRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRightRegular 0 → Subsingleton R
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
form a bilinear map `Q → Q' → P`.  -/
LinearMap.compl₁₂ : {R₁ : Type u_3} →
  {R₂ : Type u_4} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {Mₗ : Type u_6} →
          {N : Type u_7} →
            {Pₗ : Type u_9} →
              {Qₗ : Type u_10} →
                {Qₗ' : Type u_11} →
                  [inst_2 : AddCommMonoid Mₗ] →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : AddCommMonoid Pₗ] →
                        [inst_5 : AddCommMonoid Qₗ] →
                          [inst_6 : AddCommMonoid Qₗ'] →
                            [inst_7 : Module R₁ Mₗ] →
                              [inst_8 : Module R₂ N] →
                                [inst_9 : Module R₂ Pₗ] →
                                  [inst_10 : Module R₁ Pₗ] →
                                    [inst_11 : Module R₁ Qₗ] →
                                      [inst_12 : Module R₂ Qₗ'] →
                                        [inst_13 : SMulCommClass R₂ R₁ Pₗ] →
                                          (Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) →
                                            (Qₗ →ₗ[R₁] Mₗ) → (Qₗ' →ₗ[R₂] N) → Qₗ →ₗ[R₁] Qₗ' →ₗ[R₂] Pₗ
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.withProtectedMCtx.main : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadControlT Lean.MetaM m] →
        [MonadLiftT Lean.MetaM m] → Lean.Grind.Config → (Lean.MVarId → m α) → Lean.MVarId → m α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β} {he : (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.minKey he = k ↔
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true