mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Elements
/-- Show that `Elements.initial A` is initial in the category of elements for the `yoneda` functor.
 -/
CategoryTheory.Functor.Elements.isInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : C) → CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initial A)
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.eq_fiber_image : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f), ↑a = f ⁻¹' {Function.Fiber.image f a}
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftAdjointMate_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.HasLeftDual X], (ᘁCategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ᘁX
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homEquiv_symm_π_app_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C}
  (f : (CategoryTheory.Functor.const J).obj W ⟶ F) (j : J) {Z : C} (h_1 : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.homEquiv.symm f) (CategoryTheory.CategoryStruct.comp (t.π.app j) h_1) =
    CategoryTheory.CategoryStruct.comp (f.app j) h_1
-- Init.Data.Vector.Lemmas
Vector.back_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} [inst : NeZero (n + m)],
  (xs ++ ys).back =
    if h' : m = 0 then
      have this := ⋯;
      xs.back
    else
      have this := ⋯;
      ys.back
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsTheta.rpow : ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
  0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → (fun x => f x ^ r) =Θ[l] fun x => g x ^ r
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.uniformSpace : UniformSpace CompareReals.Q
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.lift_leftSMul_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M)
  {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ModObj.leftSMul M X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (m • x) x) h
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom_assoc : ∀ {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] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E}
  (h : (CategoryTheory.Limits.colimit G).comp F ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F) h
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
MeasurableSpace.prod.eq_1 : ∀ {α : Type u_6} {β : Type u_7} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β),
  m₁.prod m₂ = MeasurableSpace.comap Prod.fst m₁ ⊔ MeasurableSpace.comap Prod.snd m₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addY_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → W'.addY P (W'.neg P) = -W'.dblZ P ^ 3
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instAddZeroClass : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Affine F} → [DecidableEq F] → AddZeroClass W.Point
-- Mathlib.Algebra.Group.Basic
sub_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a - b) = b
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_eq_bot : ∀ {G : Type u_2} [inst : Group G] {S : Subgroup Gᵐᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Init.Grind.Norm
Lean.Grind.iff_eq : ∀ (p q : Prop), (p ↔ q) = (p = q)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Only assumes right strict covariance  -/
Right.add_lt_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightStrictMono α] {a b c d : α},
  a < b → c < d → a + c < b + d
-- Mathlib.Topology.UniformSpace.Cauchy
/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
Designed to be relatively compact when `V n` tends to the diagonal.  -/
interUnionBalls : {α : Type u} → (ℕ → α) → (ℕ → ℕ) → (ℕ → SetRel α α) → Set α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.alpha : Lean.Lsp.Color → Float
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.sum_sum : ∀ {M : Type u_4} {ι : Type u_5} [inst : AddCommMonoid M] (f : ι → Multiset M) (s : Finset ι),
  (∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
/-- Eisenstein series are bounded at infinity.  -/
EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF : ∀ {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ},
  3 ≤ k →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ),
      UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A ⇑(EisensteinSeries.eisensteinSeriesSIF a k))
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] {g : G},
  ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
-- Mathlib.Analysis.Normed.Field.Approximation
/-- **Continuity of Roots.** Let `f` and `g` be two monic polynomials with `g` splits.
If the coefficients of two polynomials `f` and `g` are sufficiently close, then every root of `f`
has a corresponding root of `g` nearby.  -/
Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt : ∀ {K : Type u_1} [inst : NormedField K] {f g : Polynomial K} {ε : ℝ},
  0 < ε →
    ∀ {a : K},
      Polynomial.eval a f = 0 →
        f.Monic →
          g.Monic →
            g.natDegree = f.natDegree →
              (∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε) →
                g.Splits → ∃ b ∈ g.roots, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
-- Mathlib.Algebra.GCDMonoid.Basic
associated_normalize : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α), Associated x (normalize x)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.apply_smulCommClass : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M], SMulCommClass S (Module.End R M) M
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Evaluate a polynomial `p` given a ring hom `f` from the scalar ring
to the target and a value `x` for the variable in the target  -/
Polynomial.eval₂ : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → S → Polynomial R → S
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_map_finset_iff : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β},
  (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t
-- Init.Data.Array.Extract
Array.map_extract : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {as : Array α} {i j : ℕ},
  Array.map f (as.extract i j) = (Array.map f as).extract i j
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the `n + 1`th integer part `bₙ₊₁` of the stream is smaller or equal than the inverse of
the `n`th fractional part `frₙ` of the stream.
This result is straight-forward as `bₙ₊₁` is defined as the floor of `1 / frₙ`.
 -/
GenContFract.IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K]
  {ifp_n ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n →
    GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n → ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.of_succ : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' (n + 1) f s x → ContMDiffWithinAt I I' n f s x
-- Init.Data.UInt.Lemmas
UInt16.eq_of_toBitVec_eq : ∀ {a b : UInt16}, a.toBitVec = b.toBitVec → a = b
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.instRankOneAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) → [Module.Finite ℤ R] → [Module.Free ℤ R] → Valued.v.RankOne
-- Mathlib.Data.Fin.Basic
/-- Two elements of `Fin k` and `Fin l` are heq iff their values in `ℕ` coincide. This requires
`k = l`. For the left implication without this assumption, see `val_eq_val_of_heq`.  -/
Fin.heq_ext_iff : ∀ {k l : ℕ}, k = l → ∀ {i : Fin k} {j : Fin l}, i ≍ j ↔ ↑i = ↑j
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → Y.Opens),
  iSup U = ⊤ → (P f ↔ ∀ (i : ι), P (f ∣_ U i))
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.isAdjointPair_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F),
  (innerₛₗ 𝕜).flip.IsAdjointPair (innerₛₗ 𝕜).flip ⇑A ⇑(ContinuousLinearMap.adjoint A)
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iter_eq_toIter_iterM : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter = (xs.iterM Id).toIter
-- Mathlib.Order.Fin.Basic
Fin.monotone_pred_comp : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ 0),
  Monotone f → Monotone fun a => (f a).pred ⋯
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Ioo : ∀ (a b : ENNReal), ENat.toENNReal ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ₑ ⌈b⌉ₑ
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangent.dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsIntTangent s₂ → dist s₁.center s₂.center = s₂.radius - s₁.radius
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_zero`. -/
SimpleGraph.Walk.setOf_length_eq_zero : ∀ {V : Type u} (G : SimpleGraph V) (u : V), {p | p.length = 0} = {SimpleGraph.Walk.nil}
-- Init.Data.Slice.Notation
Std.Rii.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Rii β → γ) → Std.Rii.Sliceable α β γ
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
summable_norm_pow_mul_geometric_div_one_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → Summable fun n => ↑n ^ k * r ^ n / (1 - r ^ n)
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instExcept : {ε : Type u_1} → MonadSatisfying (Except ε)
-- Lean.Elab.Command
Lean.Elab.Command.State.mk.sizeOf_spec : ∀ (env : Lean.Environment) (messages : Lean.MessageLog) (scopes : List Lean.Elab.Command.Scope)
  (usedQuotCtxts : Lean.NameSet) (nextMacroScope maxRecDepth : ℕ) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (infoState : Lean.Elab.InfoState) (traceState : Lean.TraceState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf
      { env := env, messages := messages, scopes := scopes, usedQuotCtxts := usedQuotCtxts,
        nextMacroScope := nextMacroScope, maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
        infoState := infoState, traceState := traceState, snapshotTasks := snapshotTasks } =
    1 + sizeOf env + sizeOf messages + sizeOf scopes + sizeOf usedQuotCtxts + sizeOf nextMacroScope +
                sizeOf maxRecDepth +
              sizeOf ngen +
            sizeOf auxDeclNGen +
          sizeOf infoState +
        sizeOf traceState +
      sizeOf snapshotTasks
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.ConnectedComponent.odd_matches_node_outside : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [Finite V] {u : Set V},
  M.IsPerfectMatching → ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), ∃ w ∈ u, ∃ v, M.Adj (↑v) w ∧ v ∈ (↑c).supp
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_right_iff : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insertIfNew k v).size ≤ t.size + 1
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- If additive functors are related by an isomorphism `F ⋙ G ≅ H`, this is
the corresponding isomorphism for the induced functors on homotopy categories
of homological complexes.  -/
CategoryTheory.Functor.mapHomotopyCategoryCompIso : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_1, u_3} W] →
            [inst_3 : CategoryTheory.Preadditive W] →
              {W' : Type u_4} →
                [inst_4 : CategoryTheory.Category.{u_5, u_4} W'] →
                  [inst_5 : CategoryTheory.Preadditive W'] →
                    {F : CategoryTheory.Functor V W} →
                      {G : CategoryTheory.Functor W W'} →
                        {H : CategoryTheory.Functor V W'} →
                          (F.comp G ≅ H) →
                            [inst_6 : F.Additive] →
                              [inst_7 : G.Additive] →
                                [inst_8 : H.Additive] →
                                  (c : ComplexShape ι) →
                                    (F.mapHomotopyCategory c).comp (G.mapHomotopyCategory c) ≅ H.mapHomotopyCategory c
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onFormula_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L'), ⇑φ.onFormula = φ.toLHom.onFormula
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_le_comap_iff_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → ∀ {S T : AddSubsemigroup N}, AddSubsemigroup.comap f S ≤ AddSubsemigroup.comap f T ↔ S ≤ T
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.eLpNorm_one_le_of_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {r : NNReal},
  MeasureTheory.Integrable f μ →
    0 ≤ ∫ (x : α), f x ∂μ → (∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r) → MeasureTheory.eLpNorm f 1 μ ≤ 2 * μ Set.univ * ↑r
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperHemicontinuousOn_iff_frequently`. -/
UpperHemicontinuousOn.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  (∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) →
    UpperHemicontinuousOn f s
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α), (CategoryTheory.Limits.CompleteLattice.colimitCocone F).cocone.pt = iSup F.obj
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.text? : Lean.Linter.DeprecationEntry → Option String
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_eq_eraseIdx.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : Unit → motive none) (h_2 : (i : ℕ) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftCycles.congr_simp : ∀ {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 j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ n₁_1 : ℤ)
  (e_n₁ : n₁ = n₁_1) (hn₁ : n₀ + 1 = n₁) {A : C} (x x_1 : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g))
  (e_x : x = x_1) (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0),
  X.liftCycles f g n₀ n₁ hn₁ x hx = X.liftCycles f g n₀ n₁_1 ⋯ x_1 ⋯
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a multiplication-invariant distance.  -/
NormedGroup.ofMulDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : Group E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)) → NormedGroup E
-- Mathlib.Analysis.Complex.CauchyIntegral
Differentiable.deriv : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  Differentiable ℂ f → Differentiable ℂ (deriv f)
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instCommRing : (k : Type u) → [inst : Field k] → CommRing (AlgebraicClosure k)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_subset_Icc_union_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Icc a c ⊆ Set.Icc a b ∪ Set.Ioc b c
-- Mathlib.Order.SuccPred.Tree
instCoeSortRootedTreeType : CoeSort RootedTree (Type u_2)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If `E` is finite, then any collection of subsets of `E` satisfying
the usual independence axioms determines a matroid  -/
IndepMatroid.ofFinite : {α : Type u_1} →
  {E : Set α} →
    E.Finite →
      (Indep : Set α → Prop) →
        Indep ∅ →
          (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
            (∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
              (∀ ⦃I : Set α⦄, Indep I → I ⊆ E) → IndepMatroid α
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.instAddCommGroupHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → AddCommGroup (S₁ ⟶ S₂)
-- Mathlib.Data.Int.Basic
/-- If two integers are congruent to a sufficiently large modulus, they are equal.  -/
Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs : ∀ {a b c : ℤ}, a % b = c → (a - c).natAbs < b.natAbs → a = c
-- Init.Data.Range.Polymorphic.IntLemmas
Std.PRange.Int.succ?_eq : ∀ {n : ℤ}, Std.PRange.succ? n = some (n + 1)
-- Mathlib.Data.List.Dedup
List.dedup_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.dedup = l ↔ l.Nodup
-- Mathlib.ModelTheory.Syntax
/-- The negation of a formula.  -/
FirstOrder.Language.Formula.not : {L : FirstOrder.Language} → {α : Type u'} → L.Formula α → L.Formula α
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation `t.eTruncLT.obj i ⟶ 𝟭 C` for all `i : EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTruncLTι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (i : EInt) → t.eTruncLT.obj i ⟶ CategoryTheory.Functor.id C
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkHom_comp : ∀ {M N O : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  [inst_2 : SeminormedAddCommGroup O] (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O) (hf : f.NormNoninc)
  (hg : g.NormNoninc) (hgf : (g.comp f).NormNoninc),
  SemiNormedGrp₁.mkHom (g.comp f) hgf =
    CategoryTheory.CategoryStruct.comp (SemiNormedGrp₁.mkHom f hf) (SemiNormedGrp₁.mkHom g hg)
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeEquivSubtypePerm_apply_coe : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p] (f : Equiv.Perm (Subtype p)),
  ↑((Equiv.Perm.subtypeEquivSubtypePerm p) f) = Equiv.Perm.ofSubtype f
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr
      (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.Data.Fintype.Powerset
Fintype.card_finset_len : ∀ {α : Type u_1} [inst : Fintype α] (k : ℕ), Fintype.card { s // s.card = k } = (Fintype.card α).choose k
-- Mathlib.Tactic.FunProp.Theorems
/-- Constant theorem e.g. `Continuous fun x ↦ y`  -/
Mathlib.Meta.FunProp.LambdaTheoremType.const : Mathlib.Meta.FunProp.LambdaTheoremType
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentEdit.toJson : Lean.Lsp.TextDocumentEdit → Lean.Json
-- Lean.Parser.Term
Lean.Parser.Term.have.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Data.NameTrie
Lean.NameTrie.insert : {β : Type u_1} → Lean.NameTrie β → Lean.Name → β → Lean.NameTrie β
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.nontrivial : ∀ {α : Type u} {s : Set α}, s.Infinite → s.Nontrivial
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.sin (x + ↑n * Real.pi) = (-1) ^ n * Real.sin x
-- Mathlib.Order.Heyting.Hom
HeytingHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (toLatticeHom : LatticeHom α β)
  (map_bot' : toLatticeHom.toFun ⊥ = ⊥)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b)
  (toLatticeHom_1 : LatticeHom α β) (map_bot'_1 : toLatticeHom_1.toFun ⊥ = ⊥)
  (map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b),
  ({ toLatticeHom := toLatticeHom, map_bot' := map_bot', map_himp' := map_himp' } =
      { toLatticeHom := toLatticeHom_1, map_bot' := map_bot'_1, map_himp' := map_himp'_1 }) =
    (toLatticeHom = toLatticeHom_1)