mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.fderivWithin_apply : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x y : F} {s : Set F},
  HasGradientWithinAt f f' s x → UniqueDiffWithinAt 𝕜 s x → (fderivWithin 𝕜 f s x) y = inner 𝕜 f' y
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.groupname : Std.Internal.UV.System.GroupInfo → String
-- Mathlib.Algebra.Lie.Graded
GradedLieAlgebra.toDecomposition : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      {inst : DecidableEq ι} →
        {inst_1 : AddCommMonoid ι} →
          {inst_2 : CommRing R} →
            {inst_3 : LieRing L} →
              {inst_4 : LieAlgebra R L} →
                {ℒ : ι → Submodule R L} → [self : GradedLieAlgebra ℒ] → DirectSum.Decomposition ℒ
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.mk.sizeOf_spec : ∀ (pattern : Lean.Meta.Sym.Pattern) (unify zetaDelta : Bool),
  sizeOf { pattern := pattern, unify := unify, zetaDelta := zetaDelta } =
    1 + sizeOf pattern + sizeOf unify + sizeOf zetaDelta
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = true → Std.Internal.List.getKey? a l = some (Std.Internal.List.getKey! a l)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset.inj : ∀ {A B : GrpCat} {f : A ⟶ B} {a a_1 : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)},
  GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a = GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a_1 →
    a = a_1
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Iic_add_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∑ i ≤ a + 1, f i = ∑ i ≤ a, f i + f (a + 1)
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.reCLM_enorm : ‖Complex.reCLM‖ₑ = 1
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoDiv hp a (b - ↑m * p) = toIcoDiv hp a b - m
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom d)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom)
        h)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Additive equivalences between `AddCommGroup`s are
the same as (isomorphic to) isomorphisms in `AddCommGrpCat`.  -/
addEquivIsoAddCommGroupIso : {X Y : AddCommGrpCat} → ↑X ≃+ ↑Y ≅ X ≅ Y
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Forward direction of the counit.  -/
CategoryTheory.OverPresheafAux.counitForward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
        (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) →
          F.obj (Opposite.op s) →
            CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F)
              s.hom
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toFin = ⟨UInt16.size - 1, UInt16.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If a function defined on a topological additive group has compact support,
then either the function is trivial or the group is locally compact.  -/
HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] [inst_4 : Zero α] [T1Space α] {f : G → α},
  HasCompactSupport f → Continuous f → f = 0 ∨ LocallyCompactSpace G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.norm_measure_le_variation : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} {E : Set X},
  autoParam (μ.variation E ≠ ⊤) MeasureTheory.VectorMeasure.norm_measure_le_variation._auto_1 →
    ‖μ E‖ ≤ μ.variation.real E
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The categorical coproduct in `Type u` is the type-theoretic coproduct `Σ j, F j`.  -/
CategoryTheory.Limits.Types.coproductIso : {J : Type v} → (F : J → Type (max v u)) → ∐ F ≅ (j : J) × F j
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality.congr_simp : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms],
  CategoryTheory.Limits.Bicones.functoriality F G = CategoryTheory.Limits.Bicones.functoriality F G
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.forIn'_eq_if.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_eq_count_D : ∀ {p : DyckWord}, p.semilength = List.count DyckStep.D ↑p
-- Init.Data.Vector.Lemmas
Vector.getElem?_eq_some_iff : ∀ {α : Type u_1} {n i : ℕ} {b : α} {xs : Vector α n}, xs[i]? = some b ↔ ∃ (h : i < n), xs[i] = b
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 1]` which avoids `3`.  -/
SSet.horn₃₁.ι₃ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 1).toSSet
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso F A =
    CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso F A
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsRelationalOrder : FirstOrder.Language.order.IsRelational
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- The transvection matrix `transvection i j c` is equal to the identity plus `c` at position
`(i, j)`. Multiplying by it on the left (as in `transvection i j c * M`) corresponds to adding
`c` times the `j`-th row of `M` to its `i`-th row. Multiplying by it on the right corresponds
to adding `c` times the `i`-th column to the `j`-th column.  -/
Matrix.transvection : {n : Type u_1} → {R : Type u₂} → [DecidableEq n] → [CommRing R] → n → n → R → Matrix n n R
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Division `y ↦ y / x` as an `IsometryEquiv`.  -/
IsometryEquiv.divRight : {G : Type v} → [inst : Group G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricSMul Gᵐᵒᵖ G] → G → G ≃ᵢ G
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.groupIsoToMulEquiv.eq_1 : ∀ {X Y : GrpCat} (i : X ≅ Y), i.groupIsoToMulEquiv = (GrpCat.Hom.hom i.hom).toMulEquiv (GrpCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.le_op_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S₁ : Subalgebra R Aᵐᵒᵖ} {S₂ : Subalgebra R A}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMapOn_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (p : Polynomial R)
  (X : Set R) (x : ↑X), (p.toContinuousMapOn X) x = p.toContinuousMap ↑x
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_injective : ∀ (b : Ordinal.{u_1}), Function.Injective (Ordinal.CNF.coeff b)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
Order.IsNormal.isClub_fixedPoints : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {f : α → α},
  Order.cof α ≠ Cardinal.aleph0 → Order.IsNormal f → IsClub (Function.fixedPoints f)
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S x → slope f x y < f'
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toNormedRing : {A : Type u_1} → [self : CStarAlgebra A] → NormedRing A
-- Mathlib.Topology.Algebra.Group.Defs
Filter.Tendsto.div' : ∀ {G : Type u_1} {α : Type u_2} [inst : TopologicalSpace G] [inst_1 : Div G] [ContinuousDiv G] {f g : α → G}
  {l : Filter α} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x / g x) l (nhds (a / b))
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- A representative of a finite module in the same universe as the semiring.  -/
Module.Finite.reprₛ : (R : Type u) →
  (M : Type u_1) →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Module.Finite R M] → Type u
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.instWellFoundedRelationFinite : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] → WellFoundedRelation (Std.IterM.TerminationMeasures.Finite α m)
-- Init.Data.Nat.Basic
Nat.add_one_inj : ∀ {a b : ℕ}, a + 1 = b + 1 ↔ a = b
-- Mathlib.CategoryTheory.EssentialImage
/-- All the objects of the target category are in the essential image.  -/
CategoryTheory.Functor.EssSurj.mem_essImage : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  (F : CategoryTheory.Functor C D) [self : F.EssSurj] (Y : D), F.essImage Y
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremsArray.isDeclToUnfold : Lean.Meta.SimpTheoremsArray → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesFiniteProducts : ∀ (C : Type u) [inst : CategoryTheory.SmallCategory C]
  [h : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim], CategoryTheory.IsSiftedOrEmpty C
-- Init.Data.UInt.Lemmas
UInt64.toNat_inj : ∀ {a b : UInt64}, a.toNat = b.toNat ↔ a = b
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {D : Type u_3} [inst_7 : CategoryTheory.Category.{v_3, u_3} D] [inst_8 : CategoryTheory.Limits.HasZeroObject D]
  [inst_9 : CategoryTheory.HasShift D ℤ] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [inst_13 : F.CommShift ℤ]
  [inst_14 : F.IsTriangulated] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.mapTriangulatedFunctor F).δ f g =
    CategoryTheory.CategoryStruct.comp (F.map (X.δ f g))
      ((CategoryTheory.Functor.commShiftIso F 1).hom.app (X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)))
-- Mathlib.Topology.Separation.Regular
Filter.HasBasis.nhds_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {ι : Sort u_3} {x : X} {p : ι → Prop} {s : ι → Set X},
  (nhds x).HasBasis p s → (nhds x).HasBasis p fun i => closure (s i)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l f →
    Filter.Tendsto (fun x => f x * g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_comp_add : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (m y : M),
  fwdDiff h (fun r => f (r + m)) y = fwdDiff h f (y + m)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is `C^k` on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
contMDiffOn_localFrameCoeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  {k : WithTop ℕ∞} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  IsOpen t →
    t ⊆ e.baseSet →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) t →
        ∀ (i : ι),
          ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k
            ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) t
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_empty : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M], M ⊨ ∅
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingProd_eq_finsetProd : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] (L : List G), L.alternatingProd = ∏ i, L[i] ^ (-1) ^ ↑i
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_sInf : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}
-- Mathlib.Logic.Embedding.Basic
/-- Change the value of an embedding `f` at one point. If the prescribed image
is already occupied by some `f a'`, then swap the values at these two points.  -/
Function.Embedding.setValue : {α : Sort u_1} →
  {β : Sort u_2} →
    (f : α ↪ β) → (a : α) → (b : β) → [(a' : α) → Decidable (a' = a)] → [(a' : α) → Decidable (f a' = b)] → α ↪ β
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGED : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoLT_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (x : α), e.toRelIsoLT x = e x
-- Lean.Meta.Match.Match
/-- Solve pending alternative constraints and overlap assumptions.
If all constraints can be solved perform assignment `mvarId := alt.rhs`, else throw error.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.solveCnstrs : Lean.MVarId → Lean.Meta.Match.Alt → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Order.Atoms
IsCoatom.le_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → b ≠ ⊤ → (a ≤ b ↔ b = a)
-- Mathlib.Order.OrderIsoNat
/-- The **antitone chain** condition: an antitone sequence in a partially-ordered type with
well-founded `<` is eventually constant.

This is the dual of `WellFoundedGT.monotone_chain_condition`. It is provided for convenience,
since it unbundles the antitone property from the order homomorphism.  -/
WellFoundedLT.antitone_chain_condition : ∀ {α : Type u_1} [inst : PartialOrder α] [WellFoundedLT α] {f : ℕ → α}, Antitone f → ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.injective_type₂' : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) {s t : self.ι},
  { dim := self.dim s,
        simplex :=
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index s)))
            (self.simplex s) } =
      { dim := self.dim t,
        simplex :=
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index t)))
            (self.simplex t) } →
    s = t
-- Mathlib.Algebra.Order.Module.Pointwise
smul_upperBounds_subset_lowerBounds_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {s : Set β} {a : α},
  a ≤ 0 → a • upperBounds s ⊆ lowerBounds (a • s)
-- Mathlib.Combinatorics.Enumerative.Stirling
/-- `Nat.stirlingFirst n k` is the (unsigned) Stirling number of the first kind,
counting the number of permutations of `n` elements with exactly `k` disjoint cycles.
 -/
Nat.stirlingFirst : ℕ → ℕ → ℕ
-- Mathlib.Order.Category.HeytAlg
HeytAlg.instCategory : CategoryTheory.Category.{u, u + 1} HeytAlg
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- (Implementation) One way to express the flipped version of our functor. We choose this
association because the type of `Presheaf.tautologicalCocone` is
`Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)`, so this association will show up in the
proof.  -/
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
      {J : Type} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          (K : CategoryTheory.Functor J Cᵒᵖ) →
            (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A
                  K).flip ≅
              ((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp CategoryTheory.yoneda).comp
                ((CategoryTheory.Functor.whiskeringLeft J Cᵒᵖ (Type u)).obj K)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.instIsIsoFunctorOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.IsIso (CategoryTheory.NatTrans.op α)
-- Mathlib.RingTheory.Valuation.ValuationRing
Function.Surjective.preValuationRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Mul R] [PreValuationRing R] [inst_2 : Mul S] (f : R →ₙ* S),
  Function.Surjective ⇑f → PreValuationRing S
-- Mathlib.Algebra.Module.Torsion.Basic
/-- If an `R`-module `M` is annihilated by a two-sided ideal `I`, then the identity is a semilinear
map from the `R`-module `M` to the `R ⧸ I`-module `M`.  -/
Module.IsTorsionBySet.semilinearMap : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {I : Ideal R} →
            [inst_3 : I.IsTwoSided] →
              (hM : Module.IsTorsionBySet R M ↑I) →
                have x := hM.module;
                M →ₛₗ[Ideal.Quotient.mk I] M
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V : (x : M) → TangentSpace I x},
  UniqueMDiffAt[s] x → VectorField.mpullbackWithin I I id V s x = V x
-- Mathlib.Tactic.Sat.FromLRAT
/-- The reification of a singleton clause `¬⟦l⟧_v ≡ ¬⟦l⟧_v`.  -/
Sat.Clause.reify_one : ∀ {v : Sat.Valuation} {l : Sat.Literal} {a : Prop},
  Sat.Literal.reify v l a → Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.isAddCommMonoid : {R : Type u} → [inst : Semiring R] → (self : SemimoduleCat R) → AddCommMonoid ↑self
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.mkIdent : ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Std.Http.Data.URI.Basic
/-- The hierarchical path component.
 -/
Std.Http.URI.path : Std.Http.URI → Std.Http.URI.Path
-- Init.Omega.Coeffs
/-- Identity, turning `Coeffs` into `List Int`.  -/
Lean.Omega.Coeffs.toList : Lean.Omega.Coeffs → List ℤ
-- Lean.Language.Basic
/-- The empty set of diagnostics.  -/
Lean.Language.Snapshot.Diagnostics.empty : Lean.Language.Snapshot.Diagnostics
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ext_iff : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] {f g : A ≃⋆ₐ[R] B},
  f = g ↔ ∀ (a : A), f a = g a
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `Cᵒᵖ` to the triangle
`Z.unop ⟶ Y.unop ⟶ X.unop ⟶ Z.unop⟦1⟧` in `C` (without introducing signs).  -/
CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ