mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) =
    CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderColimitsOfShape J ↔ P.colimitsOfShape J ≤ P
-- Mathlib.Order.Sublattice
/-- The inclusion homomorphism from a sublattice `L` to a bigger sublattice `M`.  -/
Sublattice.inclusion : {α : Type u_2} → [inst : Lattice α] → {L M : Sublattice α} → L ≤ M → LatticeHom ↥L ↥M
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_one_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.degree 1 ≤ 0
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_same : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), lcm a a = normalize a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.biSup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α},
  s.Countable → (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_pow_card : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] [MulLeftMono N] (s : Finset ι) (f : ι → N)
  (n : N), (∀ x ∈ s, f x ≤ n) → s.prod f ≤ n ^ s.card
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Config.mk.inj : ∀ {run run_1 : Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit},
  { run := run } = { run := run_1 } → run = run_1
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.iteration_map_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  (κ : Cardinal.{w}) [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [inst_7 : Fact κ.IsRegular] (j : κ.ord.ToType),
  (CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.OrthogonalReflection.toSucc W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j))
      (CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j).inv
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limit_ext : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u})
  (x y : ↑(ProfiniteGrp.limit F).toProfinite.toTop), (∀ (j : J), ↑x j = ↑y j) → x = y
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `IsLocalization S T`, then `A[S⁻¹]` is a `T`-algebra.
This should eventually be replaced with `IsLocalizedModule f N` and `Algebra T N`.  -/
LocalizedModule.algebraOfIsLocalization : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      (T : Type u_1) →
        [inst_1 : CommSemiring T] →
          [inst_2 : Algebra R T] →
            [IsLocalization S T] →
              {A : Type u_3} → [inst_4 : Semiring A] → [inst_5 : Algebra R A] → Algebra T (LocalizedModule S A)
-- Mathlib.Algebra.GroupWithZero.Hom
/-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
MonoidWithZeroHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → (f : α →*₀ β) → (f' : α → β) → f' = ⇑f → α →* β
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `LinearMap.toMatrix'` is a particular case of `LinearMap.toMatrix`, for the standard basis
`Pi.basisFun R n`.  -/
LinearMap.toMatrix_eq_toMatrix' : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'
-- Mathlib.Data.Seq.Computation
/-- Map a function on the result of a computation.  -/
Computation.map : {α : Type u} → {β : Type v} → (α → β) → Computation α → Computation β
-- Mathlib.Logic.Equiv.Prod
Equiv.sumArrowEquivProdArrow_apply_fst : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α ⊕ β → γ) (a : α),
  ((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)
-- Init.Data.Option.Basic
Option.le : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → Option α → Option β → Prop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_mul : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (f g : α →ᵈ α), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.measure_self_or_compl_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  PreErgodic f μ → MeasurableSet s → f ⁻¹' s = s → μ s = 0 ∨ μ sᶜ = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.ofRepresentableBy_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X),
  CategoryTheory.AddMonObj.add =
    α.homEquiv'.symm
      (α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) +
        α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.snd X X))
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.coproducts.{w, v, u}
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.mk'.inj : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1}
  {inner inner_1 : Quotient (Std.DTreeMap.isSetoid α β cmp)},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Algebra.Central.Defs
/-- For a commutative ring `K` and a `K`-algebra `D`, we say that `D` is a central algebra over `K` if
the center of `D` is the image of `K` in `D`.
 -/
Algebra.IsCentral : (K : Type u) → [inst : CommSemiring K] → (D : Type v) → [inst_1 : Semiring D] → [Algebra K D] → Prop
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instCompleteSemilatticeInf.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instCompleteSemilatticeInf M =
    { toPartialOrder := SaturatedAddSubmonoid.instPartialOrder, toInfSet := SaturatedAddSubmonoid.instInfSet M,
      isGLB_sInf := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₃ : ∀ (l : ℕ) (r : ℤ) (pq : ℤ × Fin l) (hr : 2 ≤ r),
  (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l).i₃ r pq hr = Fin.clamp (↑↑pq.2 + (r - 1)).toNat l
-- Mathlib.Topology.Instances.Real.Lemmas
Real.exists_seq_rat_strictMono_tendsto : ∀ (x : ℝ), ∃ u, StrictMono u ∧ (∀ (n : ℕ), ↑(u n) < x) ∧ Filter.Tendsto (fun x => ↑(u x)) Filter.atTop (nhds x)
-- Mathlib.Algebra.BigOperators.Pi
Fintype.prod_apply : ∀ {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [inst : Fintype ι] [inst_1 : (a : α) → CommMonoid (M a)] (a : α)
  (g : ι → (a : α) → M a), (∏ c, g c) a = ∏ c, g c a
-- Init.Data.List.MapIdx
List.mapFinIdx_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : (i : ℕ) → α → i < 1 → β},
  [a].mapFinIdx f = [f 0 a List.mapFinIdx_singleton._proof_1]
-- Init.Data.Fin.OverflowAware
/-- Overflow-aware addition of a natural number to an element of `Fin n`.

Examples:

* `(2 : Fin 3).addNat? 1 = (none : Option (Fin 3))`

* `(2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))`
 -/
Fin.addNat? : {n : ℕ} → Fin n → ℕ → Option (Fin n)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
CochainComplex.Plus.modelCategoryQuillen.cm5a : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] (n : ℤ) [K.IsStrictlyGE (n + 1)]
  [L.IsStrictlyGE n],
  ∃ K',
    ∃ (_ : K'.IsStrictlyGE n),
      ∃ ι π,
        CategoryTheory.Mono ι ∧
          QuasiIso ι ∧ CochainComplex.degreewiseEpiWithInjectiveKernel π ∧ CategoryTheory.CategoryStruct.comp ι π = f
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.π_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J),
  (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₁ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₁) j
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalOneₐ_comp_algebraMap_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  (AdicCompletion.evalOneₐ I).comp (algebraMap R (AdicCompletion I R)) = Ideal.Quotient.mk I
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
/-- If `Φ` is a localizer morphism from `W₁ : MorphismProperty C₁` to
`W₂ : MorphismProperty C₂`, if `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` are
localization functors for `W₁` and `W₂`, if `F : C₂ ⥤ H` is a functor,
if `F₁ : D₁ ⥤ H` is a right derived functor of `Φ.functor ⋙ F`,
and if `F₂ : D₂ ⥤ H` is a functor equipped with a
natural transformation `α₂ : F ⟶ L₂ ⋙ F₂`, this is the canonical
morphism `F₁ ⟶ Φ.localizedFunctor L₁ L₂ ⋙ F₂`.  -/
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {D₁ : Type u₄} →
              {D₂ : Type u₅} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂] →
                    {W₁ : CategoryTheory.MorphismProperty C₁} →
                      {W₂ : CategoryTheory.MorphismProperty C₂} →
                        (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                          (L₁ : CategoryTheory.Functor C₁ D₁) →
                            (L₂ : CategoryTheory.Functor C₂ D₂) →
                              [inst_5 : L₁.IsLocalization W₁] →
                                [inst_6 : L₂.IsLocalization W₂] →
                                  (F : CategoryTheory.Functor C₂ H) →
                                    (F₁ : CategoryTheory.Functor D₁ H) →
                                      (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) →
                                        (F₂ : CategoryTheory.Functor D₂ H) →
                                          (F ⟶ L₂.comp F₂) →
                                            [F₁.IsRightDerivedFunctor α₁ W₁] → F₁ ⟶ (Φ.localizedFunctor L₁ L₂).comp F₂
-- Mathlib.Data.Set.Operations
Set.rangeFactorization_surjective : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α}, Function.Surjective (Set.rangeFactorization f)
-- Mathlib.Analysis.LocallyConvex.Basic
Absorbent.eq_univ_of_smulMemClass : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {S : Type u_7} [inst_3 : SetLike S E] [SMulMemClass S 𝕜 E] {V : S}, Absorbent 𝕜 ↑V → ↑V = Set.univ
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.mk.sizeOf_spec : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : SizeOf J]
  (toDiagram : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (top : J)
  (isTerminal : toDiagram.IsTerminal top) (uniq_terminal : ∀ (j : J) (hj : toDiagram.IsTerminal j), j = top),
  sizeOf { toDiagram := toDiagram, top := top, isTerminal := isTerminal, uniq_terminal := uniq_terminal } =
    1 + sizeOf toDiagram + sizeOf top + sizeOf isTerminal
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `|r| < 1`, then `n * r ^ n` tends to zero.  -/
tendsto_self_mul_const_pow_of_abs_lt_one : ∀ {r : ℝ}, |r| < 1 → Filter.Tendsto (fun n => ↑n * r ^ n) Filter.atTop (nhds 0)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.Raw.ofList l).getD k' fallback = v
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_div_add : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a < b * (a / b) + b
-- Mathlib.Algebra.Order.Group.Equiv
coe_toLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], ⇑(toLexMulEquiv α) = ⇑toLex
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- The sum of two Stieltjes functions is a Stieltjes function.  -/
StieltjesFunction.add : {R : Type u_1} →
  [inst : LinearOrder R] →
    [inst_1 : TopologicalSpace R] → StieltjesFunction R → StieltjesFunction R → StieltjesFunction R
-- Mathlib.Algebra.Ring.Defs
/-- A typeclass stating that multiplication is left and right distributive
over addition.  -/
Distrib : Type u_1 → Type u_1
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.iff_local_bezout_domain : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
-- Std.Time.DateTime.Timestamp
Std.Time.instLETimestamp : LE Std.Time.Timestamp
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_iff_zero_le : ∀ {d : ℕ} {a : ℤ√↑d}, a.Nonneg ↔ 0 ≤ a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.antitoneOn_ringInverse : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  AntitoneOn Ring.inverse {a | IsStrictlyPositive a}
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_sdiff_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a \ Set.Iio b = Set.Ico b a
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.instIsIsoPost_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F], CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post F G)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.flip_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, f.flip = g.flip → f = g
-- Mathlib.Order.Filter.Cofinite
Filter.le_cofinite_iff_eventually_ne : ∀ {α : Type u_2} {l : Filter α}, l ≤ Filter.cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.norm_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = (p == (lhs.sub rhs).norm)
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence.  -/
exists_linearIndependent_cons_of_lt_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M},
  LinearIndependent R v → ↑n < Module.rank R M → ∃ x, LinearIndependent R (Fin.cons x v)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `F` preserves colimits of shape `J`, it maps colimit presentations of `X` to
colimit presentations of `F(X)`.  -/
CategoryTheory.Limits.ColimitPresentation.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.ColimitPresentation J X →
            {D : Type u_1} →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
                (F : CategoryTheory.Functor C D) →
                  [CategoryTheory.Limits.PreservesColimitsOfShape J F] →
                    CategoryTheory.Limits.ColimitPresentation J (F.obj X)
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_le_iff_le : ∀ {M : Type u_1} [inst : AddZeroClass M] {a : AddSubmonoid M} {b : SaturatedAddSubmonoid M},
  a.saturation ≤ b ↔ a ≤ b.toAddSubmonoid
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- Equivalence of the nth roots of unity of the Circle with nth roots of unity of the complex
numbers  -/
rootsOfUnityCircleEquiv : (n : ℕ) → [NeZero n] → ↥(rootsOfUnity n Circle) ≃* ↥(rootsOfUnity n ℂ)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- A vector in `Kᗮ` is orthogonal to one in `K`.  -/
Submodule.inner_left_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {u v : E}, u ∈ K → v ∈ Kᗮ → inner 𝕜 v u = 0
-- Mathlib.Data.Finset.Card
/-- Given a surjective map `f` defined on a finite set `s` to another finite set `t`, if `s` is no
larger than `t`, then `f` is injective when restricted to `s`.
See `Finset.injOn_of_surjOn_of_card_le` for the version where `f` is a non-dependent function.
 -/
Finset.inj_on_of_surj_on_of_card_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b) →
      s.card ≤ t.card → ∀ ⦃a₁ : α⦄ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
-- Lean.LocalContext
/-- Creates the expression `(x₁:α₁) → .. → (xₙ:αₙ) → b` for free variables `xs = #[x₁, .., xₙ]`,
suitably abstracting `b` and the types for each of the `xᵢ`, `αᵢ`.  -/
Lean.LocalContext.mkForall : Lean.LocalContext → Array Lean.Expr → Lean.Expr → optParam Bool true → optParam Bool false → Lean.Expr
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.finite_of_compl : ∀ {α : Type u} {s : Set α}, s.Finite → sᶜ.Finite → Finite α
-- Mathlib.Data.Quot
/-- Unwrap the VM representation of a quotient to obtain an element of the equivalence class.
Computable but unsound.  -/
Quot.unquot : {α : Sort u_1} → {r : α → α → Prop} → Quot r → α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.tensorObj.instTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} [inst_3 : CategoryTheory.AddGrpObj G]
  [inst_4 : CategoryTheory.AddGrpObj H],
  CategoryTheory.AddGrpObj.tensorObj.instTensorObj =
    { toAddMonObj := CategoryTheory.AddMon.instAddMonObjTensorObj,
      neg := CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg,
      left_neg := ⋯, right_neg := ⋯ }
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Iic' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atTop → Set.Ici (f a) ⊆ f '' Set.Iic a
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tmul_mk' : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid R) [inst_5 : IsLocalization M A] (s : S) (x : R)
  (y : ↥M),
  s ⊗ₜ[R] IsLocalization.mk' A x y =
    IsLocalization.mk' (TensorProduct R S A) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Data.Bool.Basic
Bool.ne_not : ∀ {a b : Bool}, a ≠ !b ↔ a = b
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.of_cancel_eq : ∀ (ctx : Nat.Internal.Linear.Context) (a b c d : Nat.Internal.Linear.Expr),
  a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly) →
    (Nat.Internal.Linear.Expr.denote ctx a = Nat.Internal.Linear.Expr.denote ctx b) =
      (Nat.Internal.Linear.Expr.denote ctx c = Nat.Internal.Linear.Expr.denote ctx d)
-- Mathlib.GroupTheory.SemidirectProduct
instDecidableEqSemidirectProduct.decEq : {N : Type u_4} →
  {G : Type u_5} →
    {inst : Group N} →
      {inst_1 : Group G} →
        {φ : G →* MulAut N} → [DecidableEq N] → [DecidableEq G] → (x x_1 : N ⋊[φ] G) → Decidable (x = x_1)
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), Quaternion.normSq (-a) = Quaternion.normSq a
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_of_dvd_ediv : ∀ {a b c : ℤ}, c ∣ b → a ∣ b / c → c * a ∣ b
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.mk : {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] →
        {E : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {L : CategoryTheory.Functor C D} →
              {W : CategoryTheory.MorphismProperty C} →
                {F : CategoryTheory.Functor C E} →
                  {F' : CategoryTheory.Functor D E} → (L.comp F' ≅ F) → CategoryTheory.Localization.Lifting L W F F'
-- Mathlib.Algebra.Group.Basic
leftInverse_neg : ∀ (G : Type u_3) [inst : InvolutiveNeg G], Function.LeftInverse (fun a => -a) fun a => -a
-- Mathlib.Logic.Equiv.Set
Equiv.Set.univPi_symm_apply_coe : ∀ {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : (a : α) → ↑(s a)) (a : α),
  ↑((Equiv.Set.univPi s).symm f) a = ↑(f a)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instMul : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Mul (WithVal v)