mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum`. -/
ProbabilityTheory.Kernel.IsSFiniteKernel.finset_sum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κs : ι → ProbabilityTheory.Kernel α β} (I : Finset ι),
  (∀ i ∈ I, ProbabilityTheory.IsSFiniteKernel (κs i)) → ProbabilityTheory.IsSFiniteKernel (∑ i ∈ I, κs i)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.nsmul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {x : M} {g : M → G},
  ContMDiffAt I' I n g x → ∀ (m : ℕ), ContMDiffAt I' I n (fun x => m • g x) x
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.bicategory : Mathlib.Tactic.Widget.StringDiagram.Kind
-- Mathlib.Analysis.MellinTransform
/-- Suppose `f` is locally integrable on `(0, ∞)`, is `O(x ^ (-a))` as `x → ∞`, and is
`O(x ^ (-b))` as `x → 0`. Then its Mellin transform is differentiable on the domain `b < re s < a`,
with derivative equal to the Mellin transform of `log • f`.  -/
mellin_hasDerivAt_of_isBigO_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    (f =O[Filter.atTop] fun x => x ^ (-a)) →
      s.re < a →
        (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
          b < s.re →
            MellinConvergent (fun t => Real.log t • f t) s ∧
              HasDerivAt (mellin f) (mellin (fun t => Real.log t • f t) s) s
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.CommMonCat.Hom.mk.injEq : ∀ {A B : CommMonCat} (hom' hom'_1 : ↑A →* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Time.Format.DateFormat
Std.Time.DayPeriodSymbols.mk.inj : ∀ {am pm noon midnight am_1 pm_1 noon_1 midnight_1 : String},
  { am := am, pm := pm, noon := noon, midnight := midnight } =
      { am := am_1, pm := pm_1, noon := noon_1, midnight := midnight_1 } →
    am = am_1 ∧ pm = pm_1 ∧ noon = noon_1 ∧ midnight = midnight_1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_smul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X]
  (c : M) (x : X), SeparationQuotient.mk (c • x) = c • SeparationQuotient.mk x
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.filter.eq_1 : ∀ {α : Type u_1} (B : FilterBasis α),
  B.filter = { sets := {s | ∃ t ∈ B, t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ChooseArg.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (name : Lean.Name) (expectedType? : Option Lean.Term),
  sizeOf { ref := ref, name := name, expectedType? := expectedType? } =
    1 + sizeOf ref + sizeOf name + sizeOf expectedType?
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instIsOrderedAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid αᵃᵒᵖ
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {firstRejected : s.Pos},
  String.Slice.Pattern.Model.split pat firstRejected s.endPos ⋯ = [s.subslice firstRejected s.endPos ⋯]
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.bot_mem : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α}, ⊥ ∈ L
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a `π / 2` rotation of a vector and a multiple of that vector is
zero.  -/
Orientation.inner_rotation_pi_div_two_left_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ), inner ℝ ((o.rotation ↑(Real.pi / 2)) x) (r • x) = 0
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.cond : ∀ {R : Type u₀} [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B], IsMoritaEquivalent R A B → Nonempty (MoritaEquivalence R A B)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- `ContinuousLinearMap.toSpanSingleton` as a continuous linear equivalence.  -/
ContinuousLinearMap.toSpanSingletonCLE : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            [inst_4 : IsTopologicalAddGroup E] → [inst_5 : ContinuousSMul 𝕜 E] → E ≃L[𝕜] 𝕜 →L[𝕜] E
-- Mathlib.Logic.Encodable.Basic
/-- The `encode` function, viewed as an embedding.  -/
Encodable.encode' : (α : Type u_1) → [Encodable α] → α ↪ ℕ
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.prevRoot? : Lean.Elab.ConfigEval.ConfigItem → Option Lean.Syntax
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallMetaTelescopeReducingAux.process : Bool →
  Option ℕ →
    Lean.MetavarKind →
      Array Lean.Expr →
        Array Lean.BinderInfo → ℕ → Lean.Expr → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsMonHom.monoidHom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N)
  [inst_4 : CategoryTheory.IsMonHom f] (X : C),
  CategoryTheory.IsMonHom.monoidHom f X =
    { toFun := fun x => CategoryTheory.CategoryStruct.comp x f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.ArchimedeanDensely
WithZero.mulArchimedean_iff : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α], MulArchimedean (WithZero α) ↔ MulArchimedean α
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_iSup : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocSemiring R] (S : ι → Subsemiring Rᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Lean.LibrarySuggestions.Basic
/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs.  -/
Lean.Expr.relevantConstantsAsSet : Lean.Expr → Lean.MetaM Lean.NameSet
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being open.

The type of the resulting slices is `γ`.
 -/
Std.Roo.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.GroupTheory.Coprod.Basic
/-- The minimal congruence relation `c` on `FreeMonoid (M ⊕ N)`
such that `FreeMonoid.of ∘ Sum.inl` and `FreeMonoid.of ∘ Sum.inr` are monoid homomorphisms
to the quotient by `c`.  -/
Monoid.coprodCon : (M : Type u_1) → (N : Type u_2) → [MulOneClass M] → [MulOneClass N] → Con (FreeMonoid (M ⊕ N))
-- Batteries.Data.ByteArray
ByteArray.get_push_eq : ∀ (a : ByteArray) (x : UInt8), (a.push x)[a.size] = x
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.arrow_mk_eqToHom_comp : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X' X Y : T} (f : X ⟶ Y) (h : X' = X),
  CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) = CategoryTheory.Arrow.mk f
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonPublishDiagnosticsParams : Lean.FromJson Lean.Lsp.PublishDiagnosticsParams
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instLawfulOrderLeftLeaningMaxOfOrd : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α], Std.LawfulOrderLeftLeaningMax α
-- Init.Data.UInt.Lemmas
UInt64.le_zero_iff : ∀ {a : UInt64}, a ≤ 0 ↔ a = 0
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.inf : ∀ {α : Type u} {β : Type v} [inst : Min β] {l : Filter α} {f f' g g' : α → β},
  f =ᶠ[l] f' → g =ᶠ[l] g' → f ⊓ g =ᶠ[l] f' ⊓ g'
-- Init.Data.Stream
Std.instStreamSubarray : {α : Type u_1} → Std.Stream (Subarray α) α
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_localTriv_target : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι)
  (p : B × F), p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
/-- If a functor `G : J ⥤ C` to a concrete category has a limit and that `forget C`
is corepresentable, then `(G ⋙ forget C).sections` is small.  -/
CategoryTheory.Limits.Concrete.small_sections_of_hasLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type v)}
  [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).IsCorepresentable] {J : Type w} [inst_4 : CategoryTheory.Category.{t, w} J]
  (G : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit G],
  Small.{v, max v w} ↑(G.comp (CategoryTheory.forget C)).sections
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α], Colex.instCommMonoid = { toMonoid := Colex.instMonoid, mul_comm := ⋯ }
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minEntry.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false),
  x.minEntry x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_1 => l.minEntry ⋯
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_add_left : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s + t) → t.Nonempty → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.IsIdempotentComplete (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.fun_sum : ∀ {𝕜 : 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] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x) → HasFDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
/-- Enumerate the elements of a cofinal subset of `α` by `α` itself. This is a generalization of
`Nat.nth`.  -/
Order.enum : {α : Type u_1} →
  [inst : LinearOrder α] → [inst_1 : WellFoundedLT α] → [IsRegularCardinalOrder α] → (s : Set α) → IsCofinal s → α ≃o ↑s
-- Mathlib.Geometry.Manifold.Notation
/-- Information on the underlying normed space,
if this model is the trivial model with corners on a normed space.  -/
Manifold.Elab.FindModelResult.normedSpaceInfo? : Manifold.Elab.FindModelResult → Option Manifold.Elab.NormedSpaceInfo
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.pairwise_sub_notMem_range : ∀ {ι : Type u_1} {G : Type u_3} [inst : AddCommGroup G] [inst_1 : InvolutiveNeg ι] (v : ι → G),
  (∀ (i : ι), v i ≠ 0) →
    (∀ (i : ι), v (-i) = -v i) →
      ∀ (s t : Set ι),
        s ⊆ {i | IsAddIndecomposable v t i} →
          (∀ (i : ι), i ∈ t ∨ -i ∈ t) → s.Pairwise fun i j => v i - v j ∉ Set.range v
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYoneda.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical],
  CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J =
    J.yoneda.comp (CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{w, v})
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_left_cancel : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x y : R} {c : ↥M},
  (algebraMap R S) (x * ↑c) = (algebraMap R S) (y * ↑c) → (algebraMap R S) x = (algebraMap R S) y
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.subRight.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  MeasurableEquiv.subRight g = { toEquiv := Equiv.subRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The retract of a binary bicone `c` given by `c.inl` and `c.fst`.  -/
CategoryTheory.Limits.BinaryBicone.retract_left : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (c : CategoryTheory.Limits.BinaryBicone P Q) → CategoryTheory.Retract P c.pt
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      W'.addX P Q * (P 2 * Q 2) ^ 2 =
        (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2 +
                W'.a₁ * (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * P 2 * Q 2 * WeierstrassCurve.Jacobian.addZ P Q -
              W'.a₂ * P 2 ^ 2 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 -
            P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 -
          Q 0 * P 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2
-- Mathlib.Order.Category.DistLat
DistLat.hom_inv_apply : ∀ {X Y : DistLat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousWithinAt.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {s : Set Z}
  {z : Z}, ContinuousWithinAt f s z → ContinuousWithinAt (fun z => ⇑(f z)) s z
-- Lean.Meta.Instances
/-- Compute the order the arguments of `inst` should be synthesized.

The synthesization order makes sure that all mvars in non-out-params of the
subgoals are assigned before we try to synthesize it.  Otherwise it goes left
to right.

For example:
  - `[Add α] [Zero α] : Foo α` returns `[0, 1]`
  - `[Mul A] [Mul B] [MulHomClass F A B] : FunLike F A B` returns `[2, 0, 1]`
    (because A B are out-params and are only filled in once we synthesize 2)

(The type of `inst` must not contain mvars.)

Remark: `projInfo?` is `some` if the instance is a projection.
We need this information because of the heuristic we use to annotate binder
information in projections. See PR #5376 and issue #5333. Before PR
#5376, given a class `C` at
```
class A (n : Nat) where

instance [A n] : A n.succ where

class B [A 20050] where

class C [A 20000] extends B where
```
we would get the following instance
```
C.toB [inst : A 20000] [self : @C inst] : @B ...
```
After the PR, we have
```
C.toB {inst : A 20000} [self : @C inst] : @B ...
```
Note the attribute `inst` is now just a regular implicit argument.
To ensure `computeSynthOrder` works as expected, we should take
this change into account while processing field `self`.
This field is the one at position `projInfo?.numParams`.
 -/
_private.Lean.Meta.Instances.0.Lean.Meta.computeSynthOrder : Lean.Expr → Option Lean.ProjectionFunctionInfo → Lean.MetaM (Array ℕ)
-- Batteries.Tactic.Unreachable
/-- This tactic causes a panic when run (at compile time).
(This is distinct from `exact unreachable!`, which inserts code which will panic at run time.)

It is intended for tests to assert that a tactic will never be executed, which is otherwise an
unusual thing to do (and the `unreachableTactic` linter will give a warning if you do).

The `unreachableTactic` linter has a special exception for uses of `unreachable!`.
```
example : True := by trivial <;> unreachable!
```
 -/
Batteries.Tactic.unreachableConv : Lean.ParserDescr
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
/-- A (mostly trivial) primitivity criterion for stabilizers.  -/
MulAction.isPreprimitive_stabilizer_subgroup : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α}
  [MulAction.IsPreprimitive ↥(MulAction.stabilizer M s) ↑s] {G : Subgroup M},
  MulAction.stabilizer M s ≤ G → MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥G) s) ↑s
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.bijective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit → Function.Bijective (F.descColimitType c)
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderBinaryCoproducts] {X Y : C} {B : CategoryTheory.Limits.BinaryCofan X Y}
  (hB : CategoryTheory.Limits.IsColimit B), P X → P Y → P B.pt
-- Lean.Data.Options
/-- Similar to `set`, but update `opts` only if it doesn't already contains an setting for `opt.name`  -/
Lean.Option.setIfNotSet : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Option α → α → Lean.Options
-- Std.Data.HashMap.Lemmas
Std.HashMap.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.containsThenInsert k v).1 = m.contains k
-- Init.Data.Array.Range
Array.erase_range' : ∀ {s n i : ℕ},
  (Array.range' s n).erase i =
    Array.range' s (min n (i - s)) ++ Array.range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).getKey? k = some k
-- Qq.Macro
Qq.Impl.floatExprAntiquot : {m : Type → Type} →
  [Monad m] → [Lean.MonadQuotation m] → ℕ → Lean.Term → StateT (Array (Lean.Ident × Lean.Term × Lean.Term)) m Lean.Term
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.containsThenInsert.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.containsThenInsert a = t_1.containsThenInsert a_1
-- Std.Http.Data.Headers.Basic
/-- Serializes a `Connection` header back to a comma-separated value.
 -/
Std.Http.Header.Connection.serialize : Std.Http.Header.Connection → Std.Http.Header.Name × Std.Http.Header.Value
-- Init.Grind.Ring.Basic
_private.Init.Grind.Ring.Basic.0.Lean.Grind.IsCharP.mk'_aux : ∀ {x y : ℕ} (p : ℕ), y ≤ x → ((x - y) % p = 0 ↔ ∃ k₁ k₂, x + k₁ * p = y + k₂ * p)
-- Init.Data.String.OrderInstances
String.Pos.instLawfulOrderBEq : ∀ {s : String}, Std.LawfulOrderBEq s.Pos
-- Mathlib.MeasureTheory.Group.Measure
/-- A Haar measure on a σ-compact space is σ-finite.

See Note [lower instance priority]  -/
MeasureTheory.Measure.IsHaarMeasure.sigmaFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [SigmaCompactSpace G], MeasureTheory.SigmaFinite μ
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.left_distrib : ∀ {q : ℕ} (x y z : LucasLehmer.X q), x * (y + z) = x * y + x * z
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X : C),
  CategoryTheory.MonObj.one.app X = CategoryTheory.MonObj.one
-- Lean.Parser.Command
Lean.Parser.Command.protected.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The map of a kernel fork is a limit iff
the kernel fork consisting of the mapped morphisms is a limit.
This essentially lets us commute `KernelFork.ofι` with `Functor.mapCone`.

This is a variant of `isLimitMapConeForkEquiv` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
 -/
CategoryTheory.Limits.isLimitMapConeForkEquiv' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  {f : X ⟶ Y} →
                    {h : Z ⟶ X} →
                      (w : CategoryTheory.CategoryStruct.comp h f = 0) →
                        CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.KernelFork.ofι h w)) ≃
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (G.map h) ⋯)
-- Init.Grind.Interactive
/-- `ring` (commutative) rings and fields.  -/
Lean.Parser.Tactic.Grind.ring : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Each member of the class has compact support.  -/
CompactlySupportedContinuousMapClass.hasCompactSupport : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : TopologicalSpace α} {inst_1 : Zero β}
  {inst_2 : TopologicalSpace β} {inst_3 : FunLike F α β} [self : CompactlySupportedContinuousMapClass F α β] (f : F),
  HasCompactSupport ⇑f
-- Mathlib.Data.Analysis.Filter
/-- A `CFilter α σ` is a realization of a filter (base) on `α`,
represented by a type `σ` together with operations for the top element and
the binary `inf` operation.  -/
CFilter : (α : Type u_1) → Type u_2 → [PartialOrder α] → Type (max u_1 u_2)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is right distributive over addition  -/
NonUnitalNonAssocRing.right_distrib : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a b c : α), (a + b) * c = a * c + b * c
-- Mathlib.RingTheory.Support
Module.mem_support_iff_of_span_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R} {s : Set M},
  Submodule.span R s = ⊤ → (p ∈ Module.support R M ↔ ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap' : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiable_add_const_iff : ∀ {𝕜 : 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}
  (c : F), (Differentiable 𝕜 fun y => f y + c) ↔ Differentiable 𝕜 f
-- Std.Time.Format.DateFormat
/-- Narrow era names (2 elements: index 0 = B, index 1 = C).
 -/
Std.Time.DateFormatSymbols.eraNarrow : Std.Time.DateFormatSymbols → Vector String 2