mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Two bases are equal if they assign the same coordinates.  -/
Module.Basis.eq_ofRepr_eq_repr : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b₁ b₂ : Module.Basis ι R M}, (∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i) → b₁ = b₂
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_of_hasColimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [CategoryTheory.Limits.HasColimit F.unop], CategoryTheory.Limits.HasLimit F
-- Mathlib.Order.UpperLower.Principal
UpperSet.le_Ici : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α}, s ≤ UpperSet.Ici a ↔ a ∈ s
-- Mathlib.Data.PNat.Factors
/-- We now have four different results that all encode the
idea that inequality of multisets corresponds to divisibility
of positive integers.  -/
PNat.factorMultiset_le_iff : ∀ {m n : ℕ+}, m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.subtype_val_preimage : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {C : SubAddAction G X},
  AddAction.IsBlock G B → AddAction.IsBlock G (Subtype.val ⁻¹' B)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append.inj : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {i j k l : ι} {_w₁ : Monoid.CoprodI.NeWord M i j}
  {_hne : j ≠ k} {_w₂ : Monoid.CoprodI.NeWord M k l} {j_1 k_1 : ι} {_w₁_1 : Monoid.CoprodI.NeWord M i j_1}
  {_hne_1 : j_1 ≠ k_1} {_w₂_1 : Monoid.CoprodI.NeWord M k_1 l},
  _w₁.append _hne _w₂ = _w₁_1.append _hne_1 _w₂_1 → j = j_1 ∧ k = k_1 ∧ _w₁ ≍ _w₁_1 ∧ _w₂ ≍ _w₂_1
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivAt f f' x → HasDerivAt (c • f) (c • f') x
-- Mathlib.Algebra.Order.Monovary
/-- Two functions monovary iff the rearrangement inequality holds.  -/
monovaryOn_iff_smul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.tooltip? : Lean.Lsp.InlayHint → Option Lean.Lsp.InlayHintTooltip
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous chains is isomorphic
to `(A ⊗[k] P)_G`, where `P` is the bar resolution of `k` as a trivial `G`-representation.  -/
groupHomology.inhomogeneousChainsIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        [DecidableEq G] →
          groupHomology.inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (Rep.barComplex k G)
-- Lean.Util.SCC
Lean.SCC.State.sccs : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SCC.State α → List (List α)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_const : ∀ {𝕜 : 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'] (c : M') (x : M),
  HasMFDerivAt% (fun x => c) x 0
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.vecMulVec_one : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : MulOneClass R] (x : n → R),
  Matrix.vecMulVec x 1 = Matrix.replicateCol m x
-- Mathlib.Data.Set.Lattice
Set.inter_biInter : ∀ {ι : Type u_12} {α : Type u_13} {s : Set ι},
  s.Nonempty → ∀ (f : ι → Set α) (t : Set α), ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a measurable space equipped with a finite measure is generated by an algebra of sets, then
this algebra of sets is measure-dense.  -/
MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite : ∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) {𝒜 : Set (Set X)}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.IsSetAlgebra 𝒜 → m = MeasurableSpace.generateFrom 𝒜 → μ.MeasureDense 𝒜
-- Mathlib.Algebra.CharP.Two
CharTwo.natCast_eq_mod : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharP R 2] (n : ℕ), ↑n = ↑(n % 2)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_const : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (m : M),
  (Convexity.iConvexComb s fun x => m) = m
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial
translate.  -/
MeasureTheory.fundamentalFrontier : (G : Type u_1) → {α : Type u_3} → [inst : Group G] → [MulAction G α] → Set α → Set α
-- Mathlib.Analysis.Convex.Body
ConvexBody.instInhabited : {V : Type u_1} →
  [inst : TopologicalSpace V] → [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → Inhabited (ConvexBody V)
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr_trans : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {α₃ : Sort u_3} {β₁ : Sort u_4} {β₂ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ ≃ α₂)
  (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃),
  (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- Injectivity of `algebraMap R S` implies injectivity of `codRestrictEqLocusPushoutCocone`.  -/
Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [FaithfulSMul R S],
  Function.Injective ⇑(Algebra.codRestrictEqLocusPushoutCocone R S)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinAt f p s x → DifferentiableWithinAt 𝕜 f (insert x s) x
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- If `P` is a colimit presentation over `J` of `X` and for every `j` we are given a colimit
presentation `Qⱼ` over `I j` of the `P.diag.obj j`, this is the refined colimit presentation of `X`
over `Total Q`.  -/
CategoryTheory.Limits.ColimitPresentation.bind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {I : J → Type w} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] →
            {X : C} →
              (P : CategoryTheory.Limits.ColimitPresentation J X) →
                (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) →
                  [∀ (j : J), CategoryTheory.IsFiltered (I j)] →
                    [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] →
                      CategoryTheory.Limits.ColimitPresentation (CategoryTheory.Limits.ColimitPresentation.Total Q) X
-- Mathlib.Order.Filter.Extr
IsMinOn.isExtr : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMinOn f s a → IsExtrOn f s a
-- Std.Sync.Channel
Std.CloseableChannel.instDecidableEqError : DecidableEq Std.CloseableChannel.Error
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.quotEquivOfEq_eq_factor : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I = J) (x : R ⧸ I),
  (Ideal.quotEquivOfEq h) x = (Ideal.Quotient.factor ⋯) x
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : NumberField.RingOfIntegers K),
  (NumberField.IsCMField.ringOfIntegersComplexConj K) x = x ↔
    x ∈
      Set.range
        ⇑(algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) (NumberField.RingOfIntegers K))
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- The `R`-algebra `A⟦ℕ⟧` is isomorphic to `PowerSeries A`.  -/
HahnSeries.toPowerSeriesAlg : (R : Type u_2) →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → HahnSeries ℕ A ≃ₐ[R] PowerSeries A
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiff.rpow_const_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} {m : ℕ},
  ContDiff ℝ (↑m) f → ↑m ≤ p → ContDiff ℝ ↑m fun x => f x ^ p
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisseLimit.isExtensionPair : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  {N : Type w} [inst_1 : L.Structure N] [inst_2 : Countable ((l : ℕ) × L.Functions l)] [inst_3 : Countable M]
  [inst_4 : Countable N],
  FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisseLimit K N → L.IsExtensionPair M N
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.instLineDerivSMul : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], LineDerivSMul 𝕜 E (SchwartzMap E F) (SchwartzMap E F)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAt_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat (startPos.cast hst) (endPos.cast hst) ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos
-- Mathlib.Data.Fin.Tuple.Basic
/-- Concatenating the first element of a tuple with its tail gives back the original tuple  -/
Fin.snoc_init_self : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i), Fin.snoc (Fin.init q) (q (Fin.last n)) = q
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : CategoryTheory.Limits.KernelFork f)
  {kf' : CategoryTheory.Limits.KernelFork f'} (hf' : CategoryTheory.Limits.IsLimit kf')
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (kf.mapOfIsLimit hf' φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left φ) h)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The canonical linear map `M →ₗ[R] TensorAlgebra R M`.
 -/
TensorAlgebra.ι : (R : Type u_3) →
  [inst : CommSemiring R] →
    {M : Type u_4} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] TensorAlgebra R M
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.instPreservesLimitsOfSizeOppositeFunctorTypeUliftCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)}
    CategoryTheory.uliftCoyoneda.{w', v, u}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow : ∀ {x y : NNReal} {z : ℝ}, x < y → 0 < z → x ^ z < y ^ z
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Corecursor for `Multiseries basis_hd basis_tl`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec : {β : Type u_1} →
  {basis_hd : ℝ → ℝ} →
    {basis_tl : Tactic.ComputeAsymptotics.Basis} →
      (β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × β)) →
        β → Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- Auxiliary definition for `liftExtend`.  -/
ComplexShape.Embedding.liftExtend.f : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {e : c.Embedding c'} →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  {K : HomologicalComplex C c'} →
                    {L : HomologicalComplex C c} →
                      [inst_3 : e.IsRelIff] → (K.restriction e ⟶ L) → (i' : ι') → K.X i' ⟶ (L.extend e).X i'
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.instIsInducedPlusQuasiIsoQuasiIsoR : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.Plus.isRightDerivabilityStructure.R✝ C).IsInduced
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_div : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Module K M] [inst_5 : Algebra R K] (D : Derivation R K M) (a b : K),
  D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) {i j : K} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit F).map f)
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).hom
      (CategoryTheory.Limits.colimMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_natCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (n : ℕ),
  ArchimedeanClass.stdPart ↑n = ↑n
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

The universe polymorphic version of `rank_mul_rank` below.  -/
lift_rank_mul_lift_rank : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A],
  Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) =
    Cardinal.lift.{v, w} (Module.rank F A)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore denominator of a fraction.  -/
OreLocalization.oreDenom : {R : Type u_1} → [inst : Monoid R] → {S : Submonoid R} → [OreLocalization.OreSet S] → R → ↥S → ↥S
-- Std.Sync.Channel
Std.CloseableChannel.Error.alreadyClosed.sizeOf_spec : sizeOf Std.CloseableChannel.Error.alreadyClosed = 1
-- Mathlib.Order.KrullDimension
/-- The elements of finite height `n` are the minimal elements among those of height `≥ n`.  -/
Order.height_eq_coe_iff_minimal_le_height : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ}, Order.height a = ↑n ↔ Minimal (fun y => ↑n ≤ Order.height y) a
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedCommSemiring : Inhabited Lean.Meta.Sym.Arith.CommSemiring
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pushout cocone `(𝟙 X, 𝟙 X)` for the pair `(f, f)` is a colimit if `f` is an epi. The converse is
shown in `epi_of_isColimit_mk_id_id`.
 -/
CategoryTheory.Limits.PushoutCocone.isColimitMkIdId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Epi f] →
          CategoryTheory.Limits.IsColimit
            (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y)
              (CategoryTheory.CategoryStruct.id Y) ⋯)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.ofFunction.congr_simp : ∀ {α : Type u_1} (m m_1 : Set α → ENNReal) (e_m : m = m_1) (m_empty : m ∅ = 0),
  MeasureTheory.OuterMeasure.ofFunction m m_empty = MeasureTheory.OuterMeasure.ofFunction m_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_lt_cos_of_nonneg_of_le_pi_div_two : ∀ {x y : ℝ}, 0 ≤ x → y ≤ Real.pi / 2 → x < y → Real.cos y < Real.cos x
-- Std.Internal.Do.PredTrans
Std.Internal.Do.PredTrans.mk.sizeOf_spec : ∀ {Pred : Type u} {EPred : Type v} {α : Type w} [inst : SizeOf Pred] [inst_1 : SizeOf EPred] [inst_2 : SizeOf α]
  (apply : (α → Pred) → EPred → Pred), sizeOf { apply := apply } = 1
-- Mathlib.CategoryTheory.Extensive
/-- A category is (finitary) pre-extensive if it has finite coproducts,
and binary coproducts are universal.  -/
CategoryTheory.FinitaryPreExtensive : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.DHashMap.Raw
/-- Monadically computes a value by folding the given function over the mappings in the hash
map in the reverse order used by `foldM`.
 -/
Std.DHashMap.Raw.foldRevM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} → {m : Type w → Type w'} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DHashMap.Raw α β → m δ
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.wikidataIdParser.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.dependencyBuildMode? : Lean.Lsp.LeanDidOpenTextDocumentParams → Option Lean.Lsp.DependencyBuildMode
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.eq_top_iff_eq_one : ∀ (p q : ENNReal) [p.HolderConjugate q], p = ⊤ ↔ q = 1
-- Init.Data.String.Slice
/-- Creates an iterator over all lines in `s` with the line ending characters `\r\n` or `\n` being
stripped.

Examples:

* `"foo\r\nbar\n\nbaz\n".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`

* `"foo\r\nbar\n\nbaz".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`

* `"foo\r\nbar\n\nbaz\r".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
 -/
String.Slice.lines : (s : String.Slice) → Std.Iter String.Slice
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR.eq_1 : ∀ {α : Type u_1} (l : List α) (i : ℕ) (f : α → α), l.modifyTR i f = List.modifyTR.go✝ f l i #[]
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `assoc_symm_comp_map` that only fires when `f₁ ≠ id`.  -/
CoassocSimps.assoc_symm_comp_map_simproc : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.default_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Subsingleton S] [inst_6 : Subsingleton T] (x : S),
  default x = 0
-- Mathlib.Tactic.NormNum.Result
/-- Helper function to synthesize a typed `Semiring α` expression.  -/
Mathlib.Meta.NormNum.inferSemiring : {u : Lean.Level} → (α : Q(Type u)) → Lean.MetaM Q(Semiring «$α»)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instTransOrdOrdinal : Std.TransOrd Std.Time.Month.Ordinal
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.ofInvolutive_toEquiv : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f),
  (MeasurableEquiv.ofInvolutive f hf hf').toEquiv = Function.Involutive.toPerm f hf
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.toFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (U : C), G.toFunctor.obj U = ↑(G.obj U)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k : C)
  {X Y : C} (f : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C).obj G).obj k).map f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X G k).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f G) k)
        (CategoryTheory.MonoidalCategoryStruct.associator Y G k).hom)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- The map `p ↦ v +ᵥ p` as an affine automorphism of an affine space.

Note that there is no need for an `AffineMap.constVAdd` as it is always an equivalence.
This is roughly to `DistribMulAction.toLinearEquiv` as `+ᵥ` is to `•`.  -/
AffineEquiv.constVAdd : (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → V₁ → P₁ ≃ᵃ[k] P₁
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {A B : CommAlgCat R} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit : ∀ {ι : Type u_3} {C : Type u_4} {inst : CategoryTheory.Category.{v_2, u_4} C}
  {inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C}
  [self : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι C] ⦃J : ι → Type w⦄
  [inst_2 : (i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)]
  ⦃F : (i : ι) → CategoryTheory.Functor (J i) C⦄ ⦃c : (i : ι) → CategoryTheory.Limits.Cocone (F i)⦄
  (a : (i : ι) → CategoryTheory.Limits.IsColimit (c i)),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))
-- Mathlib.SetTheory.Cardinal.Regular
/-- A singular cardinal is not regular, see `IsSingular.not_isRegular`.  -/
Cardinal.IsSingular.cof_ord_ne : ∀ {c : Cardinal.{u_1}}, c.IsSingular → c.ord.cof ≠ c
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.insert.injEq : ∀ {basis : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ) (ex : Tactic.ComputeAsymptotics.BasisExtension basis)
  (f_1 : ℝ → ℝ) (ex_1 : Tactic.ComputeAsymptotics.BasisExtension basis),
  (Tactic.ComputeAsymptotics.BasisExtension.insert f ex = Tactic.ComputeAsymptotics.BasisExtension.insert f_1 ex_1) =
    (f = f_1 ∧ ex = ex_1)
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.mk : {J : CategoryTheory.Limits.MulticospanShape} →
  {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} →
    (val : (i : J.L) → I.left i) →
      (∀ (r : J.R),
          (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val (J.fst r)) =
            (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val (J.snd r))) →
        I.sections