mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Basic
rec_heq_of_heq : ∀ {α : Sort u_2} {β : Sort u_1} {a b : α} {C : α → Sort u_1} {x : C a} {y : β} (e : a = b), x ≍ y → e ▸ x ≍ y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key : Type
-- Mathlib.Data.PNat.Basic
instAddRightCancelSemigroupPNat : AddRightCancelSemigroup ℕ+
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_fst_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom)
        (CategoryTheory.Limits.pullback.snd R.hom S.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.Limits.pullback.fst S.hom T.hom)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The set of all maximal common external tangent spaces to the spheres `s₁` and `s₂`: tangent
spaces not containing a point strictly between the centers of the spheres. (In the degenerate case
where the two spheres are the same sphere with radius 0, the space is considered both an internal
and an external common tangent.)  -/
EuclideanGeometry.Sphere.commonExtTangents : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → Set (AffineSubspace ℝ P)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k₁ k₂ fallback : α}, (k₁ == k₂) = true → m.getKeyD k₁ fallback = m.getKeyD k₂ fallback
-- Std.Time.Format.Modifier
Std.Time.Modifier.A.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.A presentation) = 1 + sizeOf presentation
-- Aesop.BuiltinRules.Ext
Aesop.BuiltinRules.extCore : Lean.MVarId → Aesop.ScriptM (Option (Array Lean.MVarId))
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_top : ⊥ * ⊤ = ⊥
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.leftCancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : LeftCancelMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.leftCancelMonoid f hf one mul npow =
    { toMonoid := Function.Injective.monoid f hf one mul npow, toIsLeftCancelMul := ⋯ }
-- Mathlib.Order.SymmDiff
Disjoint.symmDiff_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b c : α},
  Disjoint a c → Disjoint b c → Disjoint (symmDiff a b) c
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M),
  ↑R (j.endHom f) ∘ₗ α = α ∘ₗ f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instMul : {α : Type u} → Mul (FreeGroup α)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)), (G'.deleteEdges s).verts = G'.verts
-- Mathlib.Data.Setoid.Partition
Setoid.mem_classes : ∀ {α : Type u_1} (r : Setoid α) (y : α), {x | r x y} ∈ r.classes
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefixWhile_eq_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startsWith pat = false → s.skipPrefixWhile pat = s.startPos
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.subtype_comp_restrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q),
  q.subtype ∘ₛₗ f.restrict hf = f.domRestrict p
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.instInhabitedPrequotient : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Inhabited (CommRingCat.Colimits.Prequotient F)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The structure for rewrite lemmas stored in the `RefinedDiscrTree`.  -/
Mathlib.Tactic.ClickSuggestions.GrwLemma : Type
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The natural injection from `DoubleCentralizer.toProd` except the second coordinate inherits
`MulOpposite.op`. The ring structure on `𝓜(𝕜, A)` is the pullback under this map.  -/
DoubleCentralizer.toProdMulOpposite : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] → DoubleCentralizer 𝕜 A → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toCommMonoidWithZero : {G₀ : Type u_2} → [self : CommGroupWithZero G₀] → CommMonoidWithZero G₀
-- Std.Http.Data.Headers
Std.Http.Headers.instEmptyCollection : EmptyCollection Std.Http.Headers
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.brecOn : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {a : ℕ →. ℕ} (t : Nat.RecursiveIn O a),
  (∀ (a : ℕ →. ℕ) (t : Nat.RecursiveIn O a), Nat.RecursiveIn.below t → motive a t) → motive a t
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.one_lt_goodτ : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  1 < Besicovitch.goodτ E
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- For `X : C`, the short complex `Φ.r.obj X ⟶ X ⟶ Φ.quotient.obj X` obtained by evaluating
`Φ.shortComplex` at `X`.  -/
CategoryTheory.Abelian.Preradical.shortComplexObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian.Preradical C → C → CategoryTheory.ShortComplex C
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_iff_div_lt : ∀ {a b c : Ordinal.{u_4}}, a ≠ 0 → (c < a * b ↔ c / a < b)
-- Mathlib.Condensed.Discrete.Colimit
/-- The presheaf on `LightProfinite` of locally constant functions to `X`.  -/
LightCondensed.locallyConstantPresheaf : Type u → CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerLeft.eq_1 : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C) {Y Y' : C}
  (g : Y ⟶ Y'),
  CategoryTheory.eHomWhiskerLeft V X g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) ((CategoryTheory.eHomEquiv V) g))
        (CategoryTheory.eComp V X Y Y'))
-- Init.Data.Range.Polymorphic.UInt
UInt16.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt16
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_lt_re : ∀ (a : ℝ), frontier {z | a < z.re} = {z | z.re = a}
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_union_of_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_4 : HAdd Std.Time.Hour.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.leftHomologyData.homologyIso = S.leftHomologyIso.symm
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Arithmetic shift right by a constant value.

This operation has a dedicated constant representation as shiftRight can take `Nat` as a shift amount.
We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a
constant `Nat` value.
 -/
Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst : ℕ → Std.Tactic.BVDecide.BVUnOp
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, k ∈ Std.ExtTreeMap.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') t[k] = true
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_val : ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.uliftYonedaAdjunction.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [inst_3 : L.IsLeftKanExtension α],
  CategoryTheory.Presheaf.uliftYonedaAdjunction L α =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv L α, homEquiv_naturality_left_symm := ⋯,
        homEquiv_naturality_right := ⋯ }
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- **Alias** of `ContinuousLinearMap.WOTofCLM`.

---

The inclusion map from `E →[𝕜] F` to `E →WOT[𝕜] F`, bundled as a continuous linear map.  -/
ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] →
                              [ContinuousSMul 𝕜₁ E] → (E →SL[σ] F) →L[𝕜₂] E →SWOT[σ] F
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
LinearMap.shortExact_shortComplexKer : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type v}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N}, Function.Surjective ⇑f → f.shortComplexKer.ShortExact
-- Mathlib.Data.Finset.Insert
Finset.ssubset_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), s ⊂ Finset.cons a s h
-- Std.Data.HashMap.Basic
/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.HashMap.all : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → (α → β → Bool) → Bool
-- Lean.Setup
/-- Constructs a plugin from just a shared library's `path`,
inferring the name of the initialization function from the library's name.
 -/
Lean.Plugin.ofFilePath : System.FilePath → Lean.Plugin
-- Mathlib.CategoryTheory.Functor.Category
/-- The monoid of natural transformations of the identity is commutative.  -/
CategoryTheory.NatTrans.id_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  (α β : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.id C),
  CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.comp β α
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
CategoryTheory.IsCofiltered.infTo.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X : C} (m : X ∈ O),
  CategoryTheory.IsCofiltered.infTo O H m = CategoryTheory.IsCofiltered.infTo O H m
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A type synonym for `C`, which should come equipped with a `V`-enriched category structure.
In a moment we will equip this with the (honest) category structure
so that `X ⟶ Y` is `(𝟙_ W) ⟶ (X ⟶[W] Y)`.

We obtain this category by
transporting the enrichment in `V` along the lax monoidal functor `coyonedaTensorUnit`,
then using the equivalence of `Type`-enriched categories with honest categories.

This is sometimes called the "underlying" category of an enriched category,
although some care is needed as the functor `coyonedaTensorUnit`,
which always exists, does not necessarily coincide with
"the forgetful functor" from `V` to `Type`, if such exists.
When `V` is any of `Type`, `Top`, `AddCommGroup`, or `Module R`,
`coyonedaTensorUnit` is just the usual forgetful functor, however.
For `V = Algebra R`, the usual forgetful functor is coyoneda of `R[X]`, not of `R`.
(Perhaps we should have a typeclass for this situation: `ConcreteMonoidal`?)
 -/
CategoryTheory.ForgetEnrichment : (W : Type v) →
  [inst : CategoryTheory.Category.{w, v} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] → (C : Type u₁) → [CategoryTheory.EnrichedCategory W C] → Type u₁
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_eq_iInf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α),
  μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an isomorphism in the category `GrpCat` from a `MulEquiv` between `Group`s.  -/
MulEquiv.toGrpIso : {X Y : GrpCat} → ↑X ≃* ↑Y → (X ≅ Y)
-- Init.Data.Nat.Compare
Nat.compare_ne_gt : ∀ {a b : ℕ}, compare a b ≠ Ordering.gt ↔ a ≤ b
-- Mathlib.Order.Filter.IsBounded
isBoundedUnder_le_finset_sup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] [inst_1 : OrderBot β] {f : Filter α}
  {F : ι → α → β} {s : Finset ι},
  (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup fun i => F i a
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The language of a subshift `Y` on a finite shape `U`.  -/
SymbolicDynamics.FullShift.MulSubshift.languageOn : {A : Type u_3} →
  {G : Type u_4} →
    [inst : TopologicalSpace A] →
      [inst_1 : Inhabited A] →
        [inst_2 : Monoid G] →
          SymbolicDynamics.FullShift.MulSubshift A G → Finset G → Set (SymbolicDynamics.FullShift.Pattern A G)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.closedEBall_ofReal`.

---

Closed balls defined using the distance or the edistance coincide  -/
Metric.emetric_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ},
  0 ≤ ε → Metric.closedEBall x (ENNReal.ofReal ε) = Metric.closedBall x ε
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.takeWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.takeWhile pat = s.sliceTo (s.skipPrefixWhile pat)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The restriction of a partial map to a smaller domain.  -/
AlgebraicGeometry.Scheme.PartialMap.restrict : {X Y : AlgebraicGeometry.Scheme} → (f : X.PartialMap Y) → (U : X.Opens) → Dense ↑U → U ≤ f.domain → X.PartialMap Y
-- Mathlib.GroupTheory.OrderOfElement
smul_eq_of_le_smul : ∀ {G : Type u_6} [inst : Group G] [Finite G] {α : Type u_7} [inst_2 : PartialOrder α] {g : G} {a : α}
  [inst_3 : MulAction G α] [CovariantClass G α HSMul.hSMul LE.le], a ≤ g • a → g • a = a
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Prove that the lifted cocone is colimiting.  -/
CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              (t : CategoryTheory.Limits.IsColimit c) →
                [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] →
                  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  S.L₀' =
    { X₁ := S.L₁.X₁, X₂ := S.P, X₃ := S.L₀.X₃, f := CategoryTheory.Limits.pullback.lift S.L₁.f 0 ⋯,
      g := CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃, zero := ⋯ }
-- Lean.Util.HasConstCache
Lean.HasConstCache.mk.inj : ∀ {declNames : Array Lean.Name} {cache cache_1 : Std.HashMap.Raw Lean.Expr Bool},
  { cache := cache } = { cache := cache_1 } → cache = cache_1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp.eq_1 : ∀ (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp c k = Turing.PartrecToTM2.codeSupp' c k ∪ Turing.PartrecToTM2.contSupp k
-- Mathlib.Order.InitialSeg
/-- An initial segment embedding is either an isomorphism, or a principal segment embedding.

See also `InitialSeg.ltOrEq`.  -/
InitialSeg.eq_or_principal : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s),
  Function.Surjective ⇑f ∨ ∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.apply_union_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {s₁ s₂ : Set Ω},
  μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.infLELeft : {X : TopCat} → (U V : TopologicalSpace.Opens ↑X) → U ⊓ V ⟶ U
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instAddMonoid : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddMonoid R] → AddMonoid (HahnSeries Γ R)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderivWithin`.  -/
fderivWithin_continuousMultilinear_apply_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} {M : ι → Type u_6}
  [inst_3 : (i : ι) → NormedAddCommGroup (M i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      ∀ (u : (i : ι) → M i) (m : E), (fderivWithin 𝕜 (fun y => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The map obtained by quotienting by the kernel of `logEmbedding`.  -/
NumberField.Units.logEmbeddingQuot : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K) →+
        NumberField.Units.dirichletUnitTheorem.logSpace K
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.kerEquivRange.eq_1 : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) [inst_7 : LieAlgebra.IsExtension i p],
  LieAlgebra.IsExtension.kerEquivRange i p =
    LinearEquiv.ofEq (LieIdeal.toLieSubalgebra R L p.ker).toSubmodule i.range.toSubmodule ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.logDeriv_cosh : logDeriv Real.cosh = Real.tanh
-- Mathlib.Data.Nat.Choose.Multinomial
/-- Alternative multinomial definition based on a finsupp, using the support
for the big operations
 -/
Finsupp.multinomial : {α : Type u_1} → (α →₀ ℕ) → ℕ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.exsphere signs =
    { center := (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs),
      radius := |(∑ i, s.excenterWeightsUnnorm signs i)⁻¹| }
-- Mathlib.CategoryTheory.Limits.Final
/-- We provide an induction principle for reasoning about `lift` and `homToLift`.
We want to perform some construction (usually just a proof) about
the particular choices `lift F d` and `homToLift F d`,
it suffices to perform that construction for some other pair of choices
(denoted `X₀ : C` and `k₀ : d ⟶ F.obj X₀` below),
and to show how to transport such a construction
*both* directions along a morphism between such choices.
 -/
CategoryTheory.Functor.Final.induction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Final] →
            {d : D} →
              (Z : (X : C) → (d ⟶ F.obj X) → Sort u_1) →
                ((X₁ X₂ : C) →
                    (k₁ : d ⟶ F.obj X₁) →
                      (k₂ : d ⟶ F.obj X₂) →
                        (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂ → Z X₁ k₁ → Z X₂ k₂) →
                  ((X₁ X₂ : C) →
                      (k₁ : d ⟶ F.obj X₁) →
                        (k₂ : d ⟶ F.obj X₂) →
                          (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂ → Z X₂ k₂ → Z X₁ k₁) →
                    {X₀ : C} →
                      {k₀ : d ⟶ F.obj X₀} →
                        Z X₀ k₀ → Z (CategoryTheory.Functor.Final.lift F d) (CategoryTheory.Functor.Final.homToLift F d)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of `SimpleGraph.Colorable.chromaticNumber_pos`. -/
SimpleGraph.chromaticNumber_pos : ∀ {V : Type u} {G : SimpleGraph V} [Nonempty V] {n : ℕ}, G.Colorable n → 0 < G.chromaticNumber
-- Mathlib.Algebra.Order.Archimedean.Class
/-- `MulArchimedeanClass M` is the quotient of the group `M` by multiplicative archimedean
equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b|ₘ ≤ |a|ₘ ^ m) ∧ (∃ n : ℕ, |a|ₘ ≤ |b|ₘ ^ n)`.  -/
MulArchimedeanClass : (M : Type u_1) → [inst : CommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedMonoid M] → Type u_1
-- Mathlib.Topology.UniformSpace.Defs
/-- Notation for the uniformity filter with respect to a non-standard `UniformSpace` instance.  -/
Uniformity.«term𝓤[_]» : Lean.ParserDescr
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrdered.prod : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsPreorder α r],
  WellQuasiOrdered r → WellQuasiOrdered s → WellQuasiOrdered fun a b => r a.1 b.1 ∧ s a.2 b.2