mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_def : ∀ {F : Type u_1} [inst : Field F] {a : F} (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha = Matrix.SpecialLinearGroup.diag2n ⋯ a ha
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_le_of_le_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥F ≤ Module.finrank K ↥E
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.diff_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with
the boundary of the cell.  -/
Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n ≤ ↑m →
    ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.closedCell m j =
      ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.cellFrontier m j
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions.  -/
MeasureTheory.tendsto_measure_iUnion_accumulate : ∀ {α : Type u_8} {ι : Type u_9} [inst : Preorder ι] [Filter.atTop.IsCountablyGenerated] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : ι → Set α},
  Filter.Tendsto (fun i => μ (Set.accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_le_of_le_right : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, K ≤ L → H.relIndex L ≠ 0 → H.relIndex K ≤ H.relIndex L
-- Mathlib.RingTheory.Polynomial.Quotient
MvPolynomial.eval₂_C_mk_eq_zero : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] {I : Ideal R} {a : MvPolynomial σ R},
  a ∈ Ideal.map MvPolynomial.C I →
    (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0
-- Mathlib.Order.Bounded
Set.Bounded.mono : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Set.Bounded r t → Set.Bounded r s
-- Lean.Expr
Lean.Expr.lam.inj : ∀ {binderName : Lean.Name} {binderType body : Lean.Expr} {binderInfo : Lean.BinderInfo} {binderName_1 : Lean.Name}
  {binderType_1 body_1 : Lean.Expr} {binderInfo_1 : Lean.BinderInfo},
  Lean.Expr.lam binderName binderType body binderInfo = Lean.Expr.lam binderName_1 binderType_1 body_1 binderInfo_1 →
    binderName = binderName_1 ∧ binderType = binderType_1 ∧ body = body_1 ∧ binderInfo = binderInfo_1
-- Mathlib.Control.Bifunctor
Prod.bifunctor : Bifunctor Prod
-- Std.Http.Data.Request
/-- Builds and returns the final HTTP Request with the specified body.
 -/
Std.Http.Request.Builder.body : {t : Type} → Std.Http.Request.Builder → t → Std.Http.Request t
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.congr' : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {f' : Ω → β} {g' : Ω → β'},
  ProbabilityTheory.Kernel.IndepFun f g κ μ →
    (∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f') → (∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g') → ProbabilityTheory.Kernel.IndepFun f' g' κ μ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.nrRealPlaces_eq_zero : ∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K] [h : NumberField.IsTotallyComplex K],
  NumberField.InfinitePlace.nrRealPlaces K = 0
-- Mathlib.Computability.Partrec
Computable.list_cons : ∀ {α : Type u_1} [inst : Primcodable α], Computable₂ List.cons
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.setLIntegral_comp_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ ν →
    MeasurableEmbedding g → ∀ (f : β → ENNReal) (s : Set α), ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.mk : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.Rii α → Std.DTreeMap.Internal.RiiSliceData α β
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_const : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ}
  {b : β}, b ∈ B → IsAddFreimanHom n A B fun x => b
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- A set of linearly independent vectors in a module `M` over a semiring `K` is also linearly
independent over a subring `R` of `K`.

See also `LinearIndependent.restrict_scalars'` for a version with more convenient typeclass
assumptions.

TODO : `LinearIndepOn` version.  -/
LinearIndependent.restrict_scalars : ∀ {ι : Type u'} {R : Type u_2} {K : Type u_3} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring K] [inst_4 : SMulWithZero R K] [inst_5 : Module K M] [IsScalarTower R K M],
  (Function.Injective fun r => r • 1) → LinearIndependent K v → LinearIndependent R v
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C D}, W.IsInvertedBy L → W.op.IsInvertedBy L.op
-- Lean.Server.References
Lean.Server.instInhabitedReferences : Inhabited Lean.Server.References
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.id_comp : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) × C i}
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
-- Init.Tactics
/-- Syntax for including all local hypotheses in `solve_by_elim`.  -/
Lean.Parser.Tactic.SolveByElim.star : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] →
        [LawfulBEq α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Option (β a) × Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproductBiproductIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)]
  [inst_3 : CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i],
  (CategoryTheory.Limits.biproductBiproductIso f g).hom =
    CategoryTheory.Limits.biproduct.lift fun x =>
      match x with
      | ⟨i, x⟩ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun i => ⨁ g i) i)
          (CategoryTheory.Limits.biproduct.π (g i) x)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseAtLeastNum : ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Init.Data.Array.Lemmas
Array.or_all_distrib_right : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {q : Bool}, (xs.all p || q) = xs.all fun a => p a || q
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toList_eq_match_rci : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.least? with
    | none => []
    | some init => init...*.toList
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.gradient : ∀ {𝕜 : 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 : F}, HasGradientAt f f' x → gradient f x = f'
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termSₚ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toMonad_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R), h.toMonad.toFunctor = L.comp R
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.PreservesFiniteColimits L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (Std.DHashMap.Const.ofList l).contains k = (List.map Prod.fst l).contains k
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_le_add : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R} {g : Γ₀}, g ≤ v x → g ≤ v y → g ≤ v (x + y)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RooSliceData α β → Std.Roo α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.H1Iso A =
    (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 1).leftHomologyIso.symm ≪≫
      CategoryTheory.ShortComplex.leftHomologyMapIso' (groupCohomology.isoShortComplexH1 A)
        (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 1).leftHomologyData
        (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
ContinuousLinearMap.isUniformEmbedding_of_bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal}, (∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) → IsUniformEmbedding ⇑f
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between two vectors is at most π.  -/
InnerProductGeometry.angle_le_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x y ≤ Real.pi
-- Mathlib.Topology.Order
continuous_le_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
  t₂ ≤ t₁ → Continuous f → Continuous f
-- Mathlib.Algebra.Category.ModuleCat.Simple
simple_iff_isSimpleModule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  CategoryTheory.Simple (ModuleCat.of R M) ↔ IsSimpleModule R M
-- Mathlib.Algebra.Ring.Parity
range_two_mul_add_one : ∀ (α : Type u_4) [inst : Semiring α], (Set.range fun x => 2 * x + 1) = {a | Odd a}
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceTextDocumentItem : Lean.Lsp.FileSource Lean.Lsp.TextDocumentItem
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.toSubmonoid_strictMono : ∀ {R : Type u} [inst : NonAssocSemiring R], StrictMono Subsemiring.toSubmonoid
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The inclusion of each summand in the coproduct decomposition of simplices
in split simplicial objects is a natural transformation of functors
`SimplicialObject.Split C ⥤ C`  -/
CategoryTheory.SimplicialObject.Split.natTransCofanInj : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Δ : SimplexCategoryᵒᵖ} →
      (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) →
        CategoryTheory.SimplicialObject.Split.evalN C (Opposite.unop A.fst).len ⟶
          (CategoryTheory.SimplicialObject.Split.forget C).comp ((CategoryTheory.evaluation SimplexCategoryᵒᵖ C).obj Δ)
-- Mathlib.Lean.Expr.Basic
/-- Returns `true` if the provided `Expr` is exactly of the form `sorryAx _ _`.
This is the form produced by the `sorry` term/tactic.

Contrast with `Lean.Expr.isSorry`, which additionally returns `true` for any function application of
`sorry`/`sorryAx` (including e.g. `sorryAx α true x y z`).  -/
Lean.Expr.isSorryAx : Lean.Expr → Bool
-- Init.Data.Array.MapIdx
/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
Array.mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {x : α × ℕ} {xs : Array α}, x ∈ xs.zipIdx ↔ xs[x.2]? = some x.1
-- Mathlib.Analysis.Convex.Gauge
gauge.eq_1 : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : Set E) (x : E),
  gauge s x = sInf {r | 0 < r ∧ x ∈ r • s}
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_mul_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f g : Equiv.Perm α),
  (f * g).support ⊆ f.support ⊔ g.support
-- Init.Data.SInt.Lemmas
Int64.add_assoc : ∀ (a b c : Int64), a + b + c = a + (b + c)
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Specialized destructor on `WPath`  -/
MvPFunctor.wPathCasesOn : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {a : P.A} →
        {f : P.last.B a → P.last.W} →
          (P.drop.B a).Arrow α →
            ((j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α) → TypeVec.Arrow (P.WPath (WType.mk a f)) α
-- Mathlib.Algebra.Group.Defs
CommSemigroup.toSemigroup : {G : Type u} → [self : CommSemigroup G] → Semigroup G
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.ext_mk : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : F (α ::: MvQPF.Cofix F α)),
  MvQPF.Cofix.mk x = MvQPF.Cofix.mk y → x = y
-- Mathlib.LinearAlgebra.Matrix.WithConv
/-- `WithConv (Matrix m n α)` is ⋆-algebraically equivalent to `WithConv ((n → α) →ₗ m → α)`.

In particular, the convolutive product on linear maps corresponds to the Hadamard product
on matrices and the intrinsic star on linear maps corresponds to taking the star of each element in
the matrix.  -/
WithConv.matrixToLin'StarAlgEquiv : (m : Type u_1) →
  (n : Type u_2) →
    (α : Type u_3) →
      [inst : CommSemiring α] →
        [inst_1 : StarRing α] →
          [inst_2 : Fintype n] →
            [inst_3 : DecidableEq n] → WithConv (Matrix m n α) ≃⋆ₐ[α] WithConv ((n → α) →ₗ[α] m → α)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_toSubgroup_apply : ∀ {A : Type u_2} [inst : AddGroup A] (S : AddSubgroup A), ↑(AddSubgroup.toSubgroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
-- Init.Data.Vector.Find
Vector.find?_replicate_eq_some_iff : ∀ {α : Type} {n : ℕ} {a b : α} {p : α → Bool},
  Vector.find? p (Vector.replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
/-- The set of fixed points under a group action, as a subring.  -/
FixedPoints.subsemiring : (B' : Type u_3) →
  [inst : Semiring B'] → (G : Type u_4) → [inst_1 : Monoid G] → [MulSemiringAction G B'] → Subsemiring B'
-- Mathlib.FieldTheory.Galois.Basic
/-- See `InfiniteGalois.fixedField_bot` for the infinite case,
i.e. without the `[FiniteDimensional F E]` assumption.  -/
IsGalois.fixedField_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E]
  [FiniteDimensional F E], IntermediateField.fixedField ⊤ = ⊥
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterM.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := true })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := true }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_2 hf
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
instPreservesFilteredColimitsAlgCatForgetAlgHomCarrier : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget (AlgCat R))
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_map_iff_mem_range : ∀ {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(Set.powersetCard α n)) (b : β),
  b ∈ Set.powersetCard.map n f s ↔ b ∈ ⇑f '' ↑s
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantTo i₀ →
    ∀ [CategoryTheory.IsCofiltered J] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
      CategoryTheory.IsIso (c.π.app i₀)
-- Mathlib.Computability.EpsilonNFA
εNFA.start_zero : ∀ {α : Type u} {σ : Type v}, εNFA.start 0 = ∅
-- Mathlib.Algebra.Order.SuccPred
Order.Iic_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] [NeZero 1],
  Set.Iic 1 = {0, 1}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsInner.ne_last : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} [self : h.IsInner] (s : h.ι), h.index s ≠ Fin.last (h.dim s + 1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- The underlying topological space of a colimit of presheafed spaces is
the colimit of the underlying topological spaces.
 -/
AlgebraicGeometry.PresheafedSpace.forget_preservesColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.PreservesColimits (AlgebraicGeometry.PresheafedSpace.forget C)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.σ_injective : ∀ {n : ℕ}, Function.Injective SimplexCategory.σ
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.neg_ofNat_sub : ∀ {α : Type u} [inst : Lean.Grind.Ring α] {x y : ℕ}, y ≤ x → -OfNat.ofNat (x - y) = OfNat.ofNat y - OfNat.ofNat x
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- Converting a monoid object in `Type` to a bundled monoid.
 -/
MonTypeEquivalenceMon.functor : CategoryTheory.Functor (CategoryTheory.Mon (Type u)) MonCat
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSub_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 0 → ∀ (p : ι → P) (v : V), (s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_mul_prod_filter_not : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p]
  [inst_2 : (x : ι) → Decidable ¬p x] (f : ι → M), (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {f : (a : α) → β a → Bool},
  (Std.DHashMap.filterMap (fun k => Option.guard fun v => f k v) m).Equiv (Std.DHashMap.filter f m)
-- Init.Data.List.Control
List.findSome?.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → Option β) (a : α) (as : List α),
  List.findSome? f (a :: as) =
    match f a with
    | some b => some b
    | none => List.findSome? f as
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.  -/
CategoryTheory.Functor.PreservesEpimorphisms.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  CategoryTheory.Epi (F.map f)
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_symm : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), e.symm.symm = e
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (x : List α), List.splitOnPPrepend p [] x = [x.reverse]
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `smul_apply`. -/
SchwartzMap.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
/-- The pseudofunctor from `LocallyDiscrete CommRingCat` to `Cat` which sends
a commutative ring `R` to its category of modules. The functoriality is given by
the extension of scalars.  -/
CommRingCat.moduleCatExtendScalarsPseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat) CategoryTheory.Cat
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.val_smul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ S] [inst_5 : Module R₀ P.Cotangent]
  [inst_6 : IsScalarTower R₀ S P.Cotangent] (r : R₀) (x : P.H1Cotangent), ↑(r • x) = r • ↑x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprExpr.repr : Lean.Grind.CommRing.Expr → ℕ → Std.Format
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_one`. -/
Ordinal.principal_add_one : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) 1
-- Mathlib.Algebra.Group.Basic
sub_right_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b - c = a - c - b
-- Mathlib.CategoryTheory.Yoneda
/-- A chosen term in `F.RepresentableBy (reprX F)` when `F.IsRepresentable` holds.  -/
CategoryTheory.Functor.representableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) → [hF : F.IsRepresentable] → F.RepresentableBy F.reprX
-- Init.Data.Int.Lemmas
_private.Init.Data.Int.Lemmas.0.Int.add_assoc.aux1 : ∀ (m n : ℕ) (c : ℤ), ↑m + ↑n + c = ↑m + (↑n + c)
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.coeff_ofSubring : ∀ {R : Type u_1} [inst : Ring R] (T : Subring R) (p : Polynomial ↥T) (n : ℕ),
  (Polynomial.ofSubring T p).coeff n = ↑(p.coeff n)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_set' : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ}
  {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f μ a b → Set.uIoc c d ⊆ Set.uIoc a b → IntervalIntegrable f μ c d
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.Functor.id C).Monoidal
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.onTheory.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (g : L →ᴸ L') (T : L.Theory), g.onTheory T = g.onSentence '' T