mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- pushout (𝟙 X) : Under X ⥤ Under X is the identity functor.  -/
CategoryTheory.Under.pushoutId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      CategoryTheory.Under.pushout (CategoryTheory.CategoryStruct.id X) ≅
        CategoryTheory.Functor.id (CategoryTheory.Under X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.pair_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C),
  (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } = X
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toPreimages_finite : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) [∀ (j : J), Finite (F.obj j)] (j : J), Finite ((F.toPreimages s).obj j)
-- Init.System.ST
ST.Ref.mk.sizeOf_spec : ∀ {σ α : Type} [inst : SizeOf σ] [inst_1 : SizeOf α] (ref : ST.RefPointed.type) (h : Nonempty α),
  sizeOf { ref := ref, h := h } = 1 + sizeOf ref + sizeOf h
-- Batteries.Data.Char.AsciiCasing
Char.isAlpha.eq_1 : ∀ (c : Char), c.isAlpha = (c.isUpper || c.isLower)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight_map_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B)
  (R : CategoryTheory.Functor B T) {Y X : CategoryTheory.Comma L (F.comp R)} (f : Y ⟶ X),
  ((CategoryTheory.Comma.preRight L F R).map f).right = F.map f.right
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.mem_find_carrier_iff : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)} {i : ι} (ne : c.Nonempty),
  i ∈ (ShrinkingLemma.PartialRefinement.find c ne i).carrier ↔ i ∈ ShrinkingLemma.PartialRefinement.chainSupCarrier c
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne'_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (y : R) (m : ↥M), M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instModuleSubtypePreLpMemAddSubgroup : {𝕜 : Type u_1} →
  {α : Type u_3} →
    {E : α → Type u_4} →
      {p : ENNReal} →
        [inst : (i : α) → NormedAddCommGroup (E i)] →
          [inst_1 : NormedRing 𝕜] →
            [inst_2 : (i : α) → Module 𝕜 (E i)] → [∀ (i : α), IsBoundedSMul 𝕜 (E i)] → Module 𝕜 ↥(lp E p)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_sqrt : ∀ {x y : ℝ}, x ≤ y → √x ≤ √y
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_distrib_left`.  -/
Option.map₂_map_left_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5}
  {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' a b)) → Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' a b)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f g : R} [inst_2 : Algebra R S]
  [IsLocalization.Away f S], PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ IsUnit ((algebraMap R S) g)
-- Mathlib.Topology.Algebra.Group.Defs
/-- If a function converges to a value in a multiplicative topological group, then its inverse
converges to the inverse of this value.
For the version in topological groups with zero (including topological fields)
assuming additionally that the limit is nonzero, use `Filter.Tendsto.inv₀`.  -/
Filter.Tendsto.inv : ∀ {G : Type u_1} {α : Type u_2} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {f : α → G}
  {l : Filter α} {y : G}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => (f x)⁻¹) l (nhds y⁻¹)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.differentiableOn_mul_log : DifferentiableOn ℝ (fun x => x * Real.log x) {0}ᶜ
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
MonoidHom.map_cyclic : ∀ {G : Type u_2} [inst : Group G] [h : IsCyclic G] (σ : G →* G), ∃ m, ∀ (g : G), σ g = g ^ m
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_6} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → ∀ (c : 𝕜'), ContDiff 𝕜 n fun x => f x / c
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_rotateR : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  Ordnode.All P (l.rotateR x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Restrict an `OpenPartialHomeomorph` to a pair of corresponding open sets.  -/
OpenPartialHomeomorph.IsImage.restr : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {e : OpenPartialHomeomorph X Y} →
          {s : Set X} → {t : Set Y} → e.IsImage s t → IsOpen (e.source ∩ s) → OpenPartialHomeomorph X Y
-- Mathlib.Control.Fold
Monoid.foldlM.mk.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α : Type u} (f : α → m α), Monoid.foldlM.mk f = MulOpposite.op f
-- Mathlib.Data.List.Sublists
List.mem_sublists' : ∀ {α : Type u} {s t : List α}, s ∈ t.sublists' ↔ s.Sublist t
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNegOfContinuousNeg.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Neg β]
  [inst_3 : ContinuousNeg β],
  ContinuousMap.instNegOfContinuousNeg = { neg := fun f => { toFun := -⇑f, continuous_toFun := ⋯ } }
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply : ∀ {ι : Type u_1} [inst : Finite ι] (X : ι → FintypeCat) (x : (i : ι) → (X i).obj) (i : ι),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π X i))
      ((CategoryTheory.Limits.FintypeCat.productEquiv X).symm x) =
    x i
-- Lean.Parser.Basic
/-- Succeeds if `c.prec <= prec`  -/
Lean.Parser.checkPrecFn : ℕ → Lean.Parser.ParserFn
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.maximalIdeal_mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
  (NumberField.FinitePlace.mk v).maximalIdeal = v
-- Mathlib.Data.Rel
/-- A relation homomorphism with respect to a given pair of relations `R` and `S` s is a function
`f : α → β` such that `a ~[R] b → f a ~[s] f b`.  -/
SetRel.Hom : {α : Type u_1} → {β : Type u_2} → SetRel α α → SetRel β β → Type (max u_1 u_2)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  φ.pt ∈ φ.toOpenPartialHomeomorph.source
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_coe_iff : ∀ {α : Type u_4} {l : Filter α} {x : NNReal} {f : ENNReal → α},
  Filter.Tendsto f (nhds ↑x) l ↔ Filter.Tendsto (f ∘ ENNReal.ofNNReal) (nhds x) l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_eq_neg_sum_Ioc_of_ne : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] {a b : α},
  a ≠ b → (IncidenceAlgebra.mu 𝕜) a b = -∑ x ∈ Finset.Ioc a b, (IncidenceAlgebra.mu 𝕜) x b
-- Mathlib.Topology.UrysohnsLemma
/-- The outer set in the inductive construction towards Urysohn's lemma  -/
Urysohns.CU.U : {X : Type u_2} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Set X
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.separatingLeft_iff_det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], M.SeparatingLeft ↔ M.det ≠ 0
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsComplete.mem_iff : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, H.IsComplete → (e ∈ H.edgeSet ↔ e ⊆ H.vertexSet)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.intCast_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (z : ℤ) (m : α), ↑z m = z • m
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.Ioo i j = Set.Ioo (i.addNat m) (j.addNat m)
-- Init.Data.SInt.Lemmas
Int32.lt_asymm : ∀ {a b : Int32}, a < b → ¬b < a
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_app_comm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
      ((CategoryTheory.shiftFunctor D a).map (τ.app X)) =
    CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
      ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X)
-- Mathlib.Tactic.Tauto
/-- The current goal.  -/
Mathlib.Tactic.Tauto.DistribNotState.currentGoal : Mathlib.Tactic.Tauto.DistribNotState → Lean.MVarId
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
PresheafOfModules.instAbelian : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) → CategoryTheory.Abelian (PresheafOfModules R)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)
-- Mathlib.Analysis.Calculus.DSlope
ContinuousLinearMap.dslope_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F)
  (g : 𝕜 → E) (a b : 𝕜), (a = b → DifferentiableAt 𝕜 g a) → dslope (⇑f ∘ g) a b = f (dslope g a b)
-- Batteries.Data.Fin.Coding
Fin.decodePi.eq_2 : ∀ (n_2 : ℕ) (f_2 : Fin (n_2 + 1) → ℕ) (x_2 : ℕ) (hx : x_2 < Fin.prod f_2),
  Fin.decodePi f_2 ⟨x_2, hx⟩ = fun x =>
    match x with
    | ⟨0, isLt⟩ => ⟨x_2 % f_2 0, ⋯⟩
    | ⟨i.succ, hi⟩ => Fin.decodePi (fun x => f_2 x.succ) ⟨x_2 / f_2 0, ⋯⟩ ⟨i, ⋯⟩
-- Init.Data.Int.Order
Int.eq_natAbs_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → a = ↑a.natAbs
-- Mathlib.Topology.Path
/-- Concatenation of two paths from `x` to `y` and from `y` to `z`, putting the first
path on `[0, 1/2]` and the second one on `[1/2, 1]`.  -/
Path.trans : {X : Type u_1} → [inst : TopologicalSpace X] → {x y z : X} → Path x y → Path y z → Path x z
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.ext : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  (s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)), ↑s = ↑t → s = t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrpObjObjEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y : Cᵒᵖ},
  CategoryTheory.shrinkYonedaGrpObjObjEquiv = Shrink.mulEquiv
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.keepAliveTimeout : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option Std.Time.Millisecond.Offset
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.copyEnvModifications : Lean.Environment → Lean.Environment → Lean.CoreM Unit
-- Lean.Meta.Tactic.SolveByElim
/-- Attempt typeclass inference on each goal, before applying lemmas.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.synthInstance : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → Lean.Meta.SolveByElim.SolveByElimConfig
-- Init.Data.Int.Compare
Int.compare_eq_eq : ∀ {a b : ℤ}, compare a b = Ordering.eq ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.inv z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.hom z) h) =
    h
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_units_left : ∀ {R : Type u_1} [inst : CommSemiring R] {u v : R},
  IsUnit u → IsUnit v → ∀ (y z : R), IsCoprime (u * y) (v * z) ↔ IsCoprime y z
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_mul_X : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), (p * Polynomial.X).reverse = p.reverse
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.inr_biprodXIso_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : (K ⊞ L).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) h
-- Init.Data.List.Lemmas
List.foldl_append : ∀ {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l l' : List α},
  List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'
-- Init.Data.SInt.Lemmas
Int16.neg_mul_neg : ∀ (a b : Int16), -a * -b = a * b
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight.fst_mul_snd_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformRight e x).1 * (Finset.mulETransformRight e x).2 ⊆ x.1 * x.2
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_union : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s t : Set ι} {f : ι → α},
  (s ∪ t).PairwiseDisjoint f ↔
    s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.precomposeComp`.

---

Precomposing a cocone by the composite natural transformation `α ≫ β` is the same as
precomposing by `β` and then by `α`.  -/
CategoryTheory.Limits.Cocones.postcomposeComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G H : CategoryTheory.Functor J C} →
          (β : H ⟶ G) →
            (α : G ⟶ F) →
              CategoryTheory.Limits.Cocone.precompose (CategoryTheory.CategoryStruct.comp β α) ≅
                (CategoryTheory.Limits.Cocone.precompose α).comp (CategoryTheory.Limits.Cocone.precompose β)
-- Mathlib.Algebra.Free
FreeAddSemigroup.instTraversable.eq_1 : FreeAddSemigroup.instTraversable =
  { toFunctor := FreeAddSemigroup.instMonad.toFunctor, traverse := @FreeAddSemigroup.traverse }
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.newCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)),
  (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).pt = c.pt
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (v : β k), (t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.evaluation_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesColimit F (PresheafOfModules.evaluation R X)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGELTHSubIntOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ),
  t.IsLE ((t.truncGELT a b).obj X) (b - 1)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The second leg of a pushout cocone is a regular epimorphism if the right component is too.

See also `Pushout.sndOfEpi` for the basic epimorphism version, and
`regularOfIsPushoutFstOfRegular` for the flipped version.
 -/
CategoryTheory.regularOfIsPushoutSndOfRegular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q R S : C} →
      {f : P ⟶ Q} →
        {g : P ⟶ R} →
          {h : Q ⟶ S} →
            {k : R ⟶ S} →
              CategoryTheory.RegularEpi g →
                (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm) →
                    CategoryTheory.RegularEpi h
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_2) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 a a_1 f
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measurable_toRatCDF : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α], Measurable f → Measurable (ProbabilityTheory.toRatCDF f)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`.  -/
Ideal.spanNorm_mul : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [IsDedekindDomain R] [IsDedekindDomain S] (I J : Ideal S),
  Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.of_lt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α},
  t.Bounded o₁ o₂ → Ordnode.nil.Bounded o₁ ↑x → Ordnode.All (fun x_1 => x_1 < x) t → t.Bounded o₁ ↑x
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound_succ : ∀ (k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.numBound k D (n + 1) =
    ChevalleyThm.MvPolynomialC.numBound k D n * ChevalleyThm.MvPolynomialC.degBound k D n * D n
-- Mathlib.Logic.Relation
Relation.ReflGen.to_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.ReflGen r a b → Relation.ReflTransGen r a b