mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- `Subfield.extendScalars.orderIso` bundles `Subfield.extendScalars`
into an order isomorphism from
`{ E : Subfield L // F ≤ E }` to `IntermediateField F L`. Its inverse is
`IntermediateField.toSubfield`.  -/
Subfield.extendScalars.orderIso : {L : Type u_2} → [inst : Field L] → (F : Subfield L) → { E // F ≤ E } ≃o IntermediateField (↥F) L
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The isomorphism of corepresentable functors that defines the right unitor for
Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F : CategoryTheory.Functor C V) →
              ((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
                  (((CategoryTheory.Functor.whiskeringLeft (C × CategoryTheory.Discrete PUnit.{1}) (C × C) V).obj
                        ((CategoryTheory.Functor.id C).prod
                          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))).comp
                    (CategoryTheory.coyoneda.obj
                      (Opposite.op
                        (CategoryTheory.MonoidalCategory.externalProduct F
                          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)))))) ≅
                CategoryTheory.coyoneda.obj (Opposite.op F)
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- Monadic bind for ultrafilters, coming from the one on filters
defined in terms of map and join.  -/
Ultrafilter.bind : {α : Type u} → {β : Type v} → Ultrafilter α → (α → Ultrafilter β) → Ultrafilter β
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ici_succ_eq_Ioi_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → Set.Ici (Order.succ a) = Set.Ioi a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {s : CategoryTheory.Presieve X},
  (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.map F s)).arrows =
    CategoryTheory.Presieve.functorPushforward F s
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.mem_center_iff : ∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ Subsemigroup.center M ↔ ∀ (g : M), g * z = z * g
-- Mathlib.Data.Fin.Tuple.Basic
Fin.contractNth.eq_1 : ∀ {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
  j.contractNth op g k = if ↑k < ↑j then g k.castSucc else if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_rightAngleRotation_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.areaForm (o.rightAngleRotation x)) y = -inner ℝ x y
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The proposition that the function preserves 1  -/
MulRingSeminorm.map_one' : ∀ {R : Type u_2} [inst : NonAssocRing R] (self : MulRingSeminorm R), self.toFun 1 = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The canonical pairing of a vector space and its topological dual.  -/
topDualPairing : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : Module 𝕜 E] →
              [inst_5 : TopologicalSpace E] → [inst_6 : ContinuousConstSMul 𝕜 𝕜] → (E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instSemiring : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Semiring (TensorAlgebra R M)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Eliminates overlapping tokens by selecting a single “best” token for each interval between token
boundaries.

While LSP allows clients to state they they can handle overlapping tokens, widely used clients such
as VS Code cannot handle them. Thus, we need to make them non-overlapping (this strictly generalizes
removal of duplicates).

Given tokens A, B, C, D as in:
```
|-----A------|  |----D----|
    |------B----------|
        |----C----|
```
with priorities C > B, B > A, B > D, we want to emit the tokens:
```
|-A-|-B-|----C----|-B-|-D--|
```
In other words, `B` is split into two regions: before and after `C`.

If two overlapping tokens have the same priority, then ties are broken as follows:
 * If the tokens start at the same position, then the shorter one is used.
 * If they have the same start position and are the same length, then the one that occurs later in
   the original input array is used.
 * If a new token starts in the middle of an existing one, and they have the same priority, then the
   new token is used.

Callers should ensure that all tokens in `tokens` designate non-empty regions of the file. In other
words, it should be true that `∀ t ∈ tokens, t.pos < t.tailPos`.
 -/
Lean.Server.FileWorker.handleOverlappingSemanticTokens : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken → Array Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : AlgebraicGeometry.UniversallyOpen g],
  AlgebraicGeometry.UniversallyOpen (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Data.Matrix.Composition
Matrix.comp_transpose : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)),
  (Matrix.comp J I K L R) M.transpose = ((Matrix.comp I J L K R) (M.map fun x => x.transpose)).transpose
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.restrictionGEIso_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ),
  h.restrictionGEIso.hom.f i =
    (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the inclusion `(F.obj (op j)).obj j ⟶ chosenCoend F`
for any `j : J`.  -/
CategoryTheory.Limits.chosenCoend.ι : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} J] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
          [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] →
            (j : J) → (F.obj (Opposite.op j)).obj j ⟶ CategoryTheory.Limits.chosenCoend F
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of preserving effective epimorphic families.
 -/
CategoryTheory.Functor.PreservesEffectiveEpiFamilies : {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] → CategoryTheory.Functor C D → Prop
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.mk.injEq : ∀ (ref : Lean.Syntax) (structural : Bool) (vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]) (body : Lean.Term)
  (synthetic : Bool) (ref_1 : Lean.Syntax) (structural_1 : Bool)
  (vars_1 : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]) (body_1 : Lean.Term) (synthetic_1 : Bool),
  ({ ref := ref, structural := structural, vars := vars, body := body, synthetic := synthetic } =
      { ref := ref_1, structural := structural_1, vars := vars_1, body := body_1, synthetic := synthetic_1 }) =
    (ref = ref_1 ∧ structural = structural_1 ∧ vars = vars_1 ∧ body = body_1 ∧ synthetic = synthetic_1)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.asIdealOpposite.eq_1 : ∀ {R : Type u_1} [inst : Ring R],
  TwoSidedIdeal.asIdealOpposite =
    { toFun := fun I => TwoSidedIdeal.asIdeal { ringCon := I.ringCon.op }, monotone' := ⋯ }
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind : Type
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_getLast : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [Std.Refl R],
  List.Pairwise R l → ∀ (ha : a ∈ l), R a (l.getLast ⋯)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (K : Subgroup N),
  H.prod K = { toSubmonoid := H.prod K.toSubmonoid, inv_mem' := ⋯ }
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nnrat_rawCast : ∀ {n d : ℕ} {R : Type u_3} [inst : DivisionSemiring R], NNRat.rawCast n d = n.rawCast / d.rawCast
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The submonoid generated by an element.  -/
Submonoid.powers : {M : Type u_1} → [inst : Monoid M] → M → Submonoid M
-- Init.Data.Nat.Lemmas
Nat.add_succ_lt_add : ∀ {a b c d : ℕ}, a < b → c < d → a + c + 1 < b + d
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.isoMk_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.PullbackCone.isoMk t).inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.injectiveSeminorm_apply : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  (x : PiTensorProduct 𝕜 fun i => E i), PiTensorProduct.injectiveSeminorm x = ⨆ p, ↑p x
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_le : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.ae (μ.restrict s) ≤ MeasureTheory.ae μ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.Internal.List.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α),
  Std.Internal.List.getKeyD a l fallback = (Std.Internal.List.getKey? a l).getD fallback
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.sum_eq_iSup_of_mk_le_iSup : ∀ {ι : Type u} {f : ι → Cardinal.{u}},
  Cardinal.aleph0 ≤ Cardinal.mk ι → Cardinal.mk ι ≤ iSup f → Cardinal.sum f = ⨆ i, f i
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    {k : α} →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive x
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.toRightFun.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : AddSubgroup.IsComplement (↑H) T),
  hT.toRightFun = ⇑hT.rightQuotientEquiv ∘ Quotient.mk''
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.minpoly_eq : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (a : L),
  minpoly K a =
    Polynomial.X ^ ringExpChar K ^ IsPurelyInseparable.elemExponent K a -
      Polynomial.C (IsPurelyInseparable.elemReduct K a)
-- Mathlib.Data.EReal.Basic
EReal.instCanLiftENNRealToERealLeOfNat : CanLift EReal ENNReal ENNReal.toEReal fun x => 0 ≤ x
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) {x : E}, ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.mk.inj : ∀ {toSheafedSpace : AlgebraicGeometry.SheafedSpace CommRingCat}
  {isLocalRing : ∀ (x : ↑↑toSheafedSpace.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace.presheaf.stalk x)}
  {toSheafedSpace_1 : AlgebraicGeometry.SheafedSpace CommRingCat}
  {isLocalRing_1 : ∀ (x : ↑↑toSheafedSpace_1.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace_1.presheaf.stalk x)},
  { toSheafedSpace := toSheafedSpace, isLocalRing := isLocalRing } =
      { toSheafedSpace := toSheafedSpace_1, isLocalRing := isLocalRing_1 } →
    toSheafedSpace = toSheafedSpace_1
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.card_boundaries_eq_succ_length : ∀ {n : ℕ} (c : CompositionAsSet n), c.boundaries.card = c.length + 1
-- Std.Http.Data.Status
Std.Http.Status.rangeNotSatisfiable.sizeOf_spec : sizeOf Std.Http.Status.rangeNotSatisfiable = 1
-- Mathlib.Data.ENNReal.Operations
ENNReal.lt_top_of_mul_ne_top_right : ∀ {a b : ENNReal}, a * b ≠ ⊤ → a ≠ 0 → b < ⊤
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- Finitely presented groups are closed under isomorphism.  -/
Group.IsFinitelyPresented.equiv : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (iso : G ≃* H) [h : Group.IsFinitelyPresented G],
  Group.IsFinitelyPresented H
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- A property of objects satisfies `P.IsClosedUnderColimitsOfShape J` if it
is stable by colimits of shape `J`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → (J : Type u') → [CategoryTheory.Category.{v', u'} J] → Prop
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), Stream'.WSeq.map f = Stream'.Seq.map (Option.map f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The equivariant map from embeddings of `Fin n`
(aka arrangements) to combinations.  -/
Set.powersetCard.addActionHom_of_embedding : (G : Type u_1) →
  [inst : AddGroup G] →
    (α : Type u_2) →
      [inst_1 : AddAction G α] → (n : ℕ) → [inst_2 : DecidableEq α] → (Fin n ↪ α) →ₑ[id] ↑(Set.powersetCard α n)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given `0 → I → S[Y] → T → 0`, this is an auxiliary map from `S[Y]` to `T ⊗[S] Ω[S⁄R]` whose
restriction to `ker(I/I² → ⊕ S dyᵢ)` is the connecting homomorphism in the Jacobi-Zariski sequence.
 -/
Algebra.Generators.H1Cotangent.δAux : (R : Type u₁) →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {T : Type u₃} →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] →
                    {ι : Type w₁} → (Q : Algebra.Generators S T ι) → Q.Ring →ₗ[R] TensorProduct S T Ω[S⁄R]
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_empty : ∀ {α : Type u} {s : Set α} {l : Filter α}, s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
-- Mathlib.Geometry.Manifold.ChartedSpace
chartAt_comp : ∀ (H : Type u_5) [inst : TopologicalSpace H] (H' : Type u_6) [inst_1 : TopologicalSpace H'] {M : Type u_7}
  [inst_2 : TopologicalSpace M] [inst_3 : ChartedSpace H H'] [inst_4 : ChartedSpace H' M] (x : M),
  chartAt H x = (chartAt H' x).trans (chartAt H (↑(chartAt H' x) x))
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply : ∀ (n : Type u) {X : AlgebraicGeometry.Scheme} (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ
      (AlgebraicGeometry.Spec.map
        (CommRingCat.ofHom
          (MvPolynomial.eval₂Hom ((algebraMap ℤ ↑(X.presheaf.1 (Opposite.op ⊤))).comp ULift.ringEquiv.toRingHom) v)))
-- Mathlib.Probability.Moments.Basic
/-- **Chernoff bound** on the upper tail of a real random variable.  -/
ProbabilityTheory.measure_ge_le_exp_mul_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ),
  0 ≤ t →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      μ.real {ω | ε ≤ X ω} ≤ Real.exp (-t * ε) * ProbabilityTheory.mgf X μ t
-- Mathlib.Data.PNat.Factors
/-- `coePNat`, the coercion from a multiset of primes to a multiset of positive
naturals, regarded as an `AddMonoidHom`.  -/
PrimeMultiset.coePNatMonoidHom : PrimeMultiset →+ Multiset ℕ+
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd : ℤ → ℤ → ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {P : C} (p : (b : J) → f b ⟶ P) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.desc p) =
    p j
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.support_expand_subset : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R),
  Function.support ((PowerSeries.expand p hp) φ) ⊆ (fun x => p • x) '' Function.support φ
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.brecOn : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  {a a_1 : MonCat.Colimits.Prequotient F} (t : MonCat.Colimits.Relation F a a_1),
  (∀ (a a_2 : MonCat.Colimits.Prequotient F) (t : MonCat.Colimits.Relation F a a_2),
      MonCat.Colimits.Relation.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.posLT_offset : ∀ {s : String.Slice} {p : s.Pos} {h : 0 < p.offset}, s.posLT p.offset h = p.prev ⋯
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.candidates.eq_1 : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : MetricSpace Y],
  GromovHausdorff.candidates X Y =
    {f |
      (((((∀ (x y : X), f (Sum.inl x, Sum.inl y) = dist x y) ∧ ∀ (x y : Y), f (Sum.inr x, Sum.inr y) = dist x y) ∧
              ∀ (x y : X ⊕ Y), f (x, y) = f (y, x)) ∧
            ∀ (x y z : X ⊕ Y), f (x, z) ≤ f (x, y) + f (y, z)) ∧
          ∀ (x : X ⊕ Y), f (x, x) = 0) ∧
        ∀ (x y : X ⊕ Y), f (x, y) ≤ ↑(GromovHausdorff.maxVar✝ X Y)}
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_single_of_forall_add_ne : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m m' : M} [inst_1 : Add M] (r : R) (x : AddMonoidAlgebra R M),
  (∀ (d : M), d + m ≠ m') → (x * AddMonoidAlgebra.single m r).coeff m' = 0
-- Init.SizeOf
Option.none.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf none = 1
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_range : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LindelofSpace X] {f : X → Y},
  Continuous f → IsLindelof (Set.range f)
-- Init.Control.StateCps
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value, discarding the final state.
 -/
StateCpsT.run' : {α σ : Type u} → {m : Type u → Type v} → [Monad m] → StateCpsT σ m α → σ → m α
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad : ∀ {α : Type u_2} (r : α → α → Prop) (rk : α → ℕ) (s : Set α),
  (∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f) →
    ∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.ext : ∀ {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} {inst : Group W} {x y : CoxeterSystem M W},
  x.mulEquiv = y.mulEquiv → x = y
-- Mathlib.Order.Disjoint
disjoint_bot_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint ⊥ a
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_eq : ∀ {l w : ℕ} {x : BitVec (l * w)} {n : ℕ} {acc : BitVec w}, BitVec.addRecAux✝ x n acc = BitVec.addRecAux✝ x n 0#w + acc
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β) (f : Std.Sat.CNF α),
  Std.Sat.CNF.relabel r f = { clauses := Array.map (Std.Sat.CNF.Clause.relabel r) f.clauses }
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_eq_zero' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {m : M} (s : ↥S), IsLocalizedModule.mk' f m s = 0 ↔ ∃ s', s' • m = 0
-- Mathlib.Topology.UnitInterval
/-- The affine homeomorphism from a nontrivial interval `[a,b]` to `[0,1]`.
 -/
iccHomeoI : {𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [IsStrictOrderedRing 𝕜] →
        [inst_3 : TopologicalSpace 𝕜] → [IsTopologicalRing 𝕜] → (a b : 𝕜) → a < b → ↑(Set.Icc a b) ≃ₜ ↑(Set.Icc 0 1)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv : ∀ {G : Type u_1} [inst : Group G],
  CanLift (Set G) (Subgroup G) SetLike.coe fun s =>
    1 ∈ s ∧ (∀ {x y : G}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : G}, x ∈ s → x⁻¹ ∈ s
-- Mathlib.Topology.Sets.Compacts
/-- Reinterpret a compact as a closed set.  -/
TopologicalSpace.Compacts.toCloseds : {α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → TopologicalSpace.Compacts α → TopologicalSpace.Closeds α
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.liftFromUnder_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X_1 ⟶ Y) (x : CategoryTheory.WithInitial J),
  (CategoryTheory.WithInitial.liftFromUnder.map f).app x =
    match x with
    | CategoryTheory.WithInitial.of x => CategoryTheory.Under.Hom.right (f.app x)
    | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturalityₗ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n m' : M}
  (f : m ⟶ m') (X : C) [inst_3 : F.OplaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      ((F.obj n).map ((F.map f).app X)) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f n)).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F m' n).app X)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsSelfAdjoint.instIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : CStarAlgebra A], IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_sSup_of_mem : ∀ {R : Type u} [inst : Semiring R] {S : Set (Ideal R)} {s : Ideal R}, s ∈ S → ∀ {x : R}, x ∈ s → x ∈ sSup S
-- Mathlib.Analysis.Asymptotics.Lemmas
summable_of_isBigO_nat : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ},
  Summable g → f =O[Filter.atTop] g → Summable f
-- Mathlib.Order.Category.LinOrd
LinOrd.hasForgetToLat : CategoryTheory.HasForget₂ LinOrd Lat