mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.instCategoryTotal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                CategoryTheory.Category.{max v v_1, max u_2 u_1} (CategoryTheory.Limits.ColimitPresentation.Total P)
-- Init.Data.SInt.Bitwise
Int8.toInt64_or : ∀ (a b : Int8), (a ||| b).toInt64 = a.toInt64 ||| b.toInt64
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Let `x₀`, `x₁`, `x₂` be `0`-simplices of a simplicial set `X`,
`e₀₁` an edge from `x₀` to `x₁`, `e₁₂` an edge from `x₁` to `x₂`,
`e₀₂` an edge from `x₀` to `x₂`. This is the data of a `2`-simplex whose
faces are respectively `e₀₂`, `e₁₂` and `e₀₁`. Such structures shall provide
relations in the homotopy category of arbitrary simplicial sets
(and specialized constructions for quasicategories and Kan complexes.).  -/
SSet.Edge.CompStruct : {X : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} → SSet.Edge x₀ x₁ → SSet.Edge x₁ x₂ → SSet.Edge x₀ x₂ → Type u
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.totalDegree_sub_C_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) (r : R),
  (p - MvPolynomial.C r).totalDegree ≤ p.totalDegree
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α E), MeasureTheory.Integrable (⇑f) μ → μ (Function.support ⇑f) < ⊤
-- Aesop.Rule.Name
Aesop.instHashablePhaseName.hash : Aesop.PhaseName → UInt64
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  X.σ₀Iter 1 ⋯ = X.σ 0
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.rel_of_right₁ : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ it₂' : Std.IterM m β},
  InvImage Std.IterM.TerminationMeasures.Finite.Rel Std.IterM.finitelyManySteps it₂' it₂ →
    Std.Iterators.Types.Flatten.Rel✝ α β m { internalState := { it₁ := it₁, it₂ := some it₂' } }
      { internalState := { it₁ := it₁, it₂ := some it₂ } }
-- Mathlib.Analysis.Convex.Basic
Convex.smul_mem_of_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} [AddRightMono 𝕜],
  Convex 𝕜 s → ∀ {x : E}, 0 ∈ s → x ∈ s → ∀ {t : 𝕜}, t ∈ Set.Icc 0 1 → t • x ∈ s
-- Mathlib.Order.Filter.Basic
/-- The dual version does not hold! `Filter α` is not a `CompleteDistribLattice`.  -/
Filter.instCoframe : {α : Type u} → Order.Coframe (Filter α)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.mk.sizeOf_spec : ∀ (failure? : Option Lean.Meta.Grind.Goal) (issues : List Lean.MessageData) (config : Lean.Grind.Config)
  (counters : Lean.Meta.Grind.Counters) (simp : Lean.Meta.Simp.Stats)
  (splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo) (ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo),
  sizeOf
      { failure? := failure?, issues := issues, config := config, counters := counters, simp := simp,
        splitDiags := splitDiags, ematchDiags := ematchDiags } =
    1 + sizeOf failure? + sizeOf issues + sizeOf config + sizeOf counters + sizeOf simp + sizeOf splitDiags +
      sizeOf ematchDiags
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- **Alias** of `ContinuousLinearMap.IsPositive.orthogonalProjectionOnto_comp`. -/
ContinuousLinearMap.IsPositive.orthogonalProjection_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E},
  T.IsPositive →
    ∀ (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection],
      (U.orthogonalProjectionOnto ∘SL T ∘SL U.subtypeL).IsPositive
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →ₙ+* B)
  (h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)), ⇑{ toNonUnitalRingHom := f, map_star' := h } = ⇑f
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_prod_left : ∀ {𝕜 : 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'] {x₀ : M} {y₀ : M'},
  (mfderiv% fun x => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
-- Mathlib.GroupTheory.Nilpotent
/-- If the quotient by `center G` is nilpotent, then so is G.  -/
Group.of_quotient_center_nilpotent : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent (G ⧸ Subgroup.center G) → Group.IsNilpotent G
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.hasLimits : CategoryTheory.Limits.HasLimits CommGrpCat
-- Lean.Server.References
/-- Identifiers that are logically identical to this reference.  -/
Lean.Server.Reference.aliases : Lean.Server.Reference → Array Lean.Lsp.RefIdent
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.of_finiteType : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S], Algebra.EssFiniteType R S
-- Std.Http.Data.Status
Std.Http.CustomStatus.mk.injEq : ∀ (code : UInt16) (phrase : String)
  (validReasonPhrase :
    autoParam (Std.Http.IsValidReasonPhrase phrase) Std.Http.CustomStatus.validReasonPhrase._autoParam)
  (validCode : autoParam (100 ≤ code ∧ code ≤ 999) Std.Http.CustomStatus.validCode._autoParam)
  (validUnknown : autoParam (¬Std.Http.isKnownStatusCode code = true) Std.Http.CustomStatus.validUnknown._autoParam)
  (code_1 : UInt16) (phrase_1 : String)
  (validReasonPhrase_1 :
    autoParam (Std.Http.IsValidReasonPhrase phrase_1) Std.Http.CustomStatus.validReasonPhrase._autoParam)
  (validCode_1 : autoParam (100 ≤ code_1 ∧ code_1 ≤ 999) Std.Http.CustomStatus.validCode._autoParam)
  (validUnknown_1 :
    autoParam (¬Std.Http.isKnownStatusCode code_1 = true) Std.Http.CustomStatus.validUnknown._autoParam),
  ({ code := code, phrase := phrase, validReasonPhrase := validReasonPhrase, validCode := validCode,
        validUnknown := validUnknown } =
      { code := code_1, phrase := phrase_1, validReasonPhrase := validReasonPhrase_1, validCode := validCode_1,
        validUnknown := validUnknown_1 }) =
    (code = code_1 ∧ phrase = phrase_1)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_ofNat : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (x + OfNat.ofNat n) = f x + OfNat.ofNat n
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom_comp : ∀ {X Y Z : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] [inst_2 : CommGroup Z] (f : X →* Y) (g : Y →* Z),
  CommGrpCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommGrpCat.ofHom f) (CommGrpCat.ofHom g)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_natCast : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (n : ℕ), MvPolynomial.eval₂ f g ↑n = ↑n
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of comm rings satisfies `OfLocalizationMaximal`
if `P` holds for `R` whenever `P` holds for `Rₘ` for all maximal ideal `m`.  -/
OfLocalizationMaximal : ((R : Type u) → [CommRing R] → Prop) → Prop
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder β] [inst_4 : Lattice γ] [inst_5 : BoundedOrder γ] (g : BoundedLatticeHom βᵒᵈ γᵒᵈ)
  (f : BoundedLatticeHom αᵒᵈ βᵒᵈ),
  BoundedLatticeHom.dual.symm (g.comp f) = (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 →
            P 1 * Q 2 ≠ W.negY Q * P 2 →
              W.dblX P / W.dblZ P =
                W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                  (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Init.Data.List.Sublist
List.infix_concat_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.many1 : {α ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι α → Std.Internal.Parsec ι (Array α)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.openRcNhdsToOpenNhds_mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.Compacts α), Monotone K.openRcNhdsToOpenNhds
-- Init.Data.String.Search
/-- Splits a string at each subslice that matches the pattern `pat`. Unlike `split` the
matched subslices are included at the end of each subslice.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`

* `("coffee tea water".splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`

* `("coffee tea water".splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`

* `("baaab".splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
 -/
String.splitInclusive : {ρ : Type} →
  {σ : String.Slice → Type} →
    (s : String) → (pat : ρ) → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → Std.Iter String.Slice
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonPUnit : Lean.Meta.FastSubsingleton PUnit.{u_1}
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_single_add : ∀ {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [inst : CommSemiring R],
  (MvPolynomial.monomial ((fun₀ | n => e) + s)) a = MvPolynomial.X n ^ e * (MvPolynomial.monomial s) a
-- Std.Time.Date.Unit.Day
/-- Convert `Minute.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Day.Offset
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), |(|a|ₘ)|ₘ = |a|ₘ
-- Mathlib.Data.Finset.Basic
Finset.Nontrivial.erase_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, s.Nontrivial → (s.erase a).Nonempty
-- Mathlib.ModelTheory.Order
FirstOrder.Language.denselyOrdered_of_dlo : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : Preorder M]
  [L.OrderedStructure M] [M ⊨ L.dlo], DenselyOrdered M
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} (self : I.SymmStruct)
  (i j : ι), CategoryTheory.CategoryStruct.comp (self.iso i j).hom (I.fst (j, i)) = I.snd (i, j)
-- Mathlib.GroupTheory.PGroup
IsPGroup.comap_subtype : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
  IsPGroup p ↥H → ∀ {K : Subgroup G}, IsPGroup p ↥(Subgroup.comap K.subtype H)
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_pos`. -/
Ideal.ramificationIdx'_pos : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [q.IsPrime] [Module.Finite R S], 0 < q.ramificationIdx R
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_add : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i), ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsStableUnderRetractsAnodyneExtensions : SSet.anodyneExtensions.IsStableUnderRetracts
-- Mathlib.Order.Filter.Pointwise
Filter.le_mul_iff : ∀ {α : Type u_2} [inst : Mul α] {f g h : Filter α}, h ≤ f * g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s * t ∈ h
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `CompleteBooleanAlgebra` across an `Equiv`.  -/
Equiv.completeBooleanAlgebra : {α : Type u} → {β : Type v} → α ≃ β → [CompleteBooleanAlgebra β] → CompleteBooleanAlgebra α
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.self_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] (x : A), x ∈ NonUnitalAlgebra.elemental R x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a))
  (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGE?.go k (some ⟨ky, y⟩) l
      | Ordering.eq => some ⟨ky, y⟩
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryGE?.go k best r
-- Init.Data.BitVec.Lemmas
BitVec.msb_umod : ∀ {w : ℕ} {x y : BitVec w}, (x % y).msb = (x.msb && (decide (x < y) || y == 0#w))
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 →
    (∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) →
      ↑n.factorial ∈ nonZeroDivisors R → n < Polynomial.rootMultiplicity t p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.inv_nonneg : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : PartialOrder A]
  [inst_4 : Algebra NNReal A] [ContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x] (a : Aˣ), 0 ≤ ↑a⁻¹ ↔ 0 ≤ ↑a
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_cons_zero : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), (Stream'.Seq.cons a s).get? 0 = some a
-- Mathlib.Data.Fintype.Fin
Fin.Ioi_succ : ∀ {n : ℕ} (i : Fin n), Finset.Ioi i.succ = Finset.map (Fin.succEmb n) (Finset.Ioi i)
-- Mathlib.Algebra.Lie.Weights.Basic
/-- See also `LieModule.iInf_lowerCentralSeries_eq_posFittingComp`.  -/
LieModule.iSup_ucs_eq_genWeightSpace_zero : ∀ (R : 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 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M], ⨆ k, LieSubmodule.ucs k ⊥ = LieModule.genWeightSpace M 0
-- Mathlib.Computability.Partrec
Partrec.nat_casesOn_right : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → ℕ} {g : α → σ}
  {h : α → ℕ →. σ},
  Computable f → Computable g → Partrec₂ h → Partrec fun a => Nat.casesOn (f a) (Part.some (g a)) (h a)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.eq_mul_inverse_iff_mul_eq : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y z : M₀), IsUnit z → (x = y * Ring.inverse z ↔ x * z = y)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.mk.sizeOf_spec : ∀ (val : Lean.Expr) (synthOrder : Array ℕ),
  sizeOf { val := val, synthOrder := synthOrder } = 1 + sizeOf val + sizeOf synthOrder
-- Mathlib.CategoryTheory.Monoidal.Tor
/-- We define `Tor C n : C ⥤ C ⥤ C` by left-deriving in the second factor of `(X, Y) ↦ X ⊗ Y`.  -/
CategoryTheory.Tor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Abelian C] →
        [CategoryTheory.MonoidalPreadditive C] →
          [CategoryTheory.HasProjectiveResolutions C] → ℕ → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Lean.Util.SortExprs
Lean.Perm : Type
-- Mathlib.Topology.Separation.Basic
biInter_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {x : X},
  (nhds x).HasBasis p s → ⋂ i, ⋂ (_ : p i), s i = {x}
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.ciSup_le_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [Nonempty ι] {f : ι → α} {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → (iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- The element in `d.Extension val₀ (Order.succ j)` obtained by extending
an element in `d.Extension val₀ j` when `j` is not maximal.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension.succ : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} → {j : J} → d.Extension val₀ j → ¬IsMax j → d.Extension val₀ (Order.succ j)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_pow_sub_goldenRatio_pow : ∀ (n : ℕ), Real.goldenRatio ^ (n + 2) - Real.goldenRatio ^ (n + 1) = Real.goldenRatio ^ n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom : Inhabited Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Mathlib.Algebra.MvPolynomial.Supported
Subalgebra.equivOfEq.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A)
  (h : S = T), S.equivOfEq T h = S.equivOfEq T h
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapAlgHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (R : Type u_3)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Y] [inst_4 : Algebra R Y] [inst_5 : IsTopologicalSemiring Y]
  (f : LocallyConstant X Y), (LocallyConstant.toContinuousMapAlgHom R) f = ↑f
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.comp_c_app : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z.toTopCat)ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp f g).c.app U =
    CategoryTheory.CategoryStruct.comp (g.c.app U)
      (f.c.app (Opposite.op ((TopologicalSpace.Opens.map g.base).obj (Opposite.unop U))))
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsMultiplicativeCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.cofibrations C).IsMultiplicative
-- Mathlib.Algebra.Group.Hom.Basic
nsmulAddMonoidHom.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ),
  nsmulAddMonoidHom n = { toFun := fun x => n • x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.mulLeft.eq_1 : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : LinearOrder α] [inst_2 : MulLeftStrictMono α] (m : α),
  OrderEmbedding.mulLeft m = OrderEmbedding.ofStrictMono (fun n => m * n) ⋯
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousOn_aeval : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {s : Set A},
  ContinuousOn (fun x => (Polynomial.aeval x) p) s
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerLeft : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
        (CategoryTheory.Bicategory.associator f g h').inv)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterM_equiv_iterM_toList : ∀ {n : ℕ} {α : Type w} {xs : Vector α n} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m],
  (xs.iterM m).Equiv (xs.toList.iterM m)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.triangle : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X CategoryTheory.FreeMonoidalCategory.unit Y).comp
      (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X (CategoryTheory.FreeMonoidalCategory.Hom.l_hom Y)))
    ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X).whiskerRight Y)
-- Mathlib.Data.Seq.Computation
/-- `think c` is the computation that delays for one "tick" and then performs
computation `c`.  -/
Computation.think : {α : Type u} → Computation α → Computation α
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopEquivalence_counitIso : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.unopEquivalence V c).counitIso = HomologicalComplex.unopCounitIso V c
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_lineMap_right : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidHomLequivInt_apply : ∀ {A : Type u_9} {B : Type u_10} (R : Type u_11) [inst : Semiring R] [inst_1 : AddCommGroup A] [inst_2 : AddCommGroup B]
  [inst_3 : Module R B] (f : A →+ B), (addMonoidHomLequivInt R) f = f.toIntLinearMap
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedAdd.toAddLeftMono : ∀ {α : Type u} [inst : AddSemigroup α] [inst_1 : LE α] [CanonicallyOrderedAdd α], AddLeftMono α
-- Lean.Elab.App
/-- Store the metavariable used to represent the motive that will be computed at `finalize`.  -/
Lean.Elab.Term.ElabElim.State.motive? : Lean.Elab.Term.ElabElim.State → Option Lean.Expr
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α}
  {f : α → β},
  List.maxIdxOn f (x :: xs) ⋯ =
    if h : xs = [] then 0 else if f (List.maxOn f xs h) ≤ f x then 0 else List.maxIdxOn f xs h + 1