mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `S` a module-finite free `R`-algebra, then the `R`-rank of a nonzero `R`-free
ideal `I` of `S` is the same as the rank of `S`.  -/
Ideal.rank_eq : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [StrongRankCondition R] [inst_2 : Ring S] [IsDomain S]
  [inst_4 : Algebra R S] {n : Type u_4} {m : Type u_5} [inst_5 : Fintype n] [inst_6 : Fintype m]
  (b : Module.Basis n R S) {I : Ideal S}, I ≠ ⊥ → ∀ (c : Module.Basis m R ↥I), Fintype.card m = Fintype.card n
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.riiIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.riiIterator t =
    { internalState := Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done }
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instIsLeftCancelMulZero : IsLeftCancelMulZero Ordinal.{u_4}
-- Lean.Syntax
Lean.Syntax.getAntiquotSpliceContents : Lean.Syntax → Array Lean.Syntax
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} [inst_4 : Inhabited β] {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k =
        (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomSnd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  [inst_4 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsAddMonHom (CategoryTheory.SemiCartesianMonoidalCategory.snd M N)
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- Given a pseudofunctor `F` from  `LocallyDiscrete Cᵒᵖ` to `Cat`, objects `M₁` and `M₂`
of `F` over `X₁` and `X₂`, morphisms `f₁ : Y ⟶ X₁` and `f₂ : Y ⟶ X₂`, this is a version
of the pullback map `(f₁^* M₁ ⟶ f₂^* M₂) → (g^* (f₁^* M₁) ⟶ g^* (f₂^* M₂))` by a
morphism `g : Y' ⟶ Y`, where we actually replace `g^* (f₁^* M₁)` by `gf₁^* M₁`
where `gf₁ : Y' ⟶ X₁` is a morphism such that `g ≫ f₁ = gf₁` (and similarly for `M₂`).  -/
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      ⦃X₁ X₂ : C⦄ →
        ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ →
          ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ →
            ⦃Y : C⦄ →
              ⦃f₁ : Y ⟶ X₁⦄ →
                ⦃f₂ : Y ⟶ X₂⦄ →
                  ((F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) →
                    ⦃Y' : C⦄ →
                      (g : Y' ⟶ Y) →
                        (gf₁ : Y' ⟶ X₁) →
                          (gf₂ : Y' ⟶ X₂) →
                            autoParam (CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
                                CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom._auto_1 →
                              autoParam (CategoryTheory.CategoryStruct.comp g f₂ = gf₂)
                                  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom._auto_3 →
                                ((F.map gf₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map gf₂.op.toLoc).toFunctor.obj M₂)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The counit isomorphism of the equivalence `equivalence₁` between `A` and `B'`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso : {A : Type u_1} →
  {A' : Type u_2} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eA : A ≌ A'} →
              {e' : A' ≌ B'} →
                {F : CategoryTheory.Functor A B'} →
                  (eA.functor.comp e'.functor ≅ F) →
                    ((e'.inverse.comp eA.inverse).comp F ≅ CategoryTheory.Functor.id B')
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `LinearMap.mul'` as an `AlgHom` over the base ring.  -/
Algebra.TensorProduct.lmul' : (R : Type uR) →
  {S : Type uS} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → TensorProduct R S S →ₐ[R] S
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryLeftEquiv_symm_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G)
  (v : (i : Fin n.succ) → Ei i), ((continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm f) v = (f (v 0)) (Fin.tail v)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.uniq_symm_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation)
  (g : relations.G), (h.uniq h').symm (solution'.var g) = solution.var g
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given a map `f : R →+* S` and an element `r : R`, such that `f r` is invertible,
we may construct a map `Rᵣ →+* S`.  -/
Localization.awayLift : {R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} → [inst_1 : CommSemiring P] → (f : R →+* P) → (r : R) → IsUnit (f r) → Localization.Away r →+* P
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- A category with equalizers has weak equalizers.  -/
CategoryTheory.Limits.HasWeakEqualizersOfHasEqualizers : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Limits.HasWeakEqualizers C
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap.congr_simp : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 → ∀ (s s_1 : NonUnitalSubring S), s = s_1 → NonUnitalSubring.comap f s = NonUnitalSubring.comap f_1 s_1
-- Lean.Server.Requests
Lean.Server.RequestError.internalError : String → Lean.Server.RequestError
-- Lean.Elab.Tactic.Doc
/-- Displays all available tactic tags, with documentation.
 -/
Lean.Elab.Tactic.Doc.elabPrintTacTags : Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithTerminal C)ᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).unitIso.inv.app X =
    (match Opposite.unop X with
      | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithTerminal.of x))
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithTerminal.star)).inv
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_eq_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (a : σ → R) (f : MvPowerSeries σ R),
  (MvPowerSeries.rescale a) f = MvPowerSeries.subst (a • MvPowerSeries.X) f
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` has characteristic zero.  -/
PadicComplex.charZero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], CharZero ℂ_[p]
-- Mathlib.Order.CompleteLattice.Basic
sInf_le_sInf_of_subset_insert_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, s ⊆ insert ⊤ t → sInf t ≤ sInf s
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Ideal.isLinearTopology : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), IsLinearTopology R R
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The forgetful-units adjunction between `CommGrpCat` and `CommMonCat`.  -/
CommGrpCat.forget₂CommMonAdj : CategoryTheory.forget₂ CommGrpCat CommMonCat ⊣ CommMonCat.units
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β}, List.minIdxOn? f (List.replicate n a) = if n = 0 then none else some 0
-- Init.Data.Iterators.Basic
Std.IterStep.done.sizeOf_spec : ∀ {α : Sort u_1} {β : Sort u_2} [inst : SizeOf α] [inst_1 : SizeOf β], sizeOf Std.IterStep.done = 1
-- Lean.Meta.Match.MatcherApp.Transform
/-- Similar to `MatcherApp.addArg`, but returns `none` on failure.  -/
Lean.Meta.MatcherApp.addArg? : Lean.Meta.MatcherApp → Lean.Expr → Lean.MetaM (Option Lean.Meta.MatcherApp)
-- Mathlib.Data.Set.Functor
/-- The coercion from `Set.monad` as an instance is equal to the coercion in `Data.Set.Notation`.  -/
Set.coe_eq_image_val : ∀ {α : Type u} {s : Set α} (t : Set ↑s), Lean.Internal.coeM t = Subtype.val '' t
-- Std.Time.Date.Unit.Year
Std.Time.Year.instInhabitedEra : Inhabited Std.Time.Year.Era
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- The Grothendieck topology associated to a precoverage `J`.
It is defined *inductively* as follows:
1. If `S` is a covering presieve for `J`, then the sieve generated by `S` is a covering
  sieve for the associated Grothendieck topology.
2. The top sieves are in the associated Grothendieck topology.
3. Add all sieves required by the pullback stability condition of a Grothendieck topology.
4. Add all sieves required by the *local character* axiom of a Grothendieck topology.
 -/
CategoryTheory.Precoverage.toGrothendieck : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] → CategoryTheory.Precoverage C → CategoryTheory.GrothendieckTopology C
-- Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
NonarchimedeanGroup.instTotallySeparated : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [NonarchimedeanGroup G] [T2Space G],
  TotallySeparatedSpace G
-- Mathlib.Algebra.Category.ModuleCat.Localization
instSmallLocalizedModule : ∀ (R : Type u) [inst : CommRing R] [Small.{v, u} R] (M : Type v) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  (S : Submonoid R), Small.{v, max v u} (LocalizedModule S M)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] →
              {H : LieSubalgebra R L} →
                (A : Matrix ι ι ℤ) →
                  (h e f : ι → L) →
                    H = LieSubalgebra.lieSpan R L (Set.range h) →
                      LieSubalgebra.lieSpan R L (Set.range e ∪ Set.range f) = ⊤ →
                        LinearIndependent R h →
                          A.Nondegenerate →
                            (∀ (i : ι), IsSl2Triple (h i) (e i) (f i)) →
                              (∀ (i j : ι), ⁅h i, h j⁆ = 0) →
                                (∀ (i j : ι), ⁅h j, e i⁆ = A i j • e i) →
                                  (∀ (i j : ι), ⁅h j, f i⁆ = -A i j • f i) →
                                    (∀ (i j : ι), i ≠ j → ⁅e i, f j⁆ = 0) → LieAlgebra.Basis ι H
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.isometry_ofLp_infty : ∀ {ι : Type u_2} (β : ι → Type u_4) [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)],
  Isometry WithLp.ofLp
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
/-- Given a sequence of complex polynomials `fₚ`, a complex constant `s`, and a real constant `c` such
that `|fₚ(xs)| ≤ c ^ p` for all `p ∈ ℕ` and `x ∈ Ioc 0 1`, then there is also a nonnegative
constant `c'` such that for all nonzero `p ∈ ℕ`, `|P(fₚ, s)| ≤ c' ^ p`.
 -/
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.P_le : ∀ (f : ℕ → Polynomial ℂ) (s : ℂ) (c : ℝ),
  (∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖Polynomial.eval (x • s) (f p)‖ ≤ c ^ p) →
    ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P✝ (f p) s‖ ≤ c' ^ p
-- Lean.Parser.Syntax
Lean.Parser.Command.notation.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.replicate.match_1.eq_1 : ∀ {w : ℕ} (motive : ℕ → BitVec w → Sort u_1) (x : BitVec w) (h_1 : (x : BitVec w) → motive 0 x)
  (h_2 : (n : ℕ) → (x : BitVec w) → motive n.succ x),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, x => h_2 n x) =
    h_1 x
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [Finite ↑s] (f : α → β), Nat.card ↑(f '' s) ≤ Nat.card ↑s
-- Std.Time.Format.Basic
Std.Time.FormatPart.modifier.injEq : ∀ (modifier modifier_1 : Std.Time.Modifier),
  (Std.Time.FormatPart.modifier modifier = Std.Time.FormatPart.modifier modifier_1) = (modifier = modifier_1)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.mulFiber.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (x : M), DiscreteConvolution.mulFiber x = Set.univ.mulAntidiagonal Set.univ x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalRightDistrib.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C],
  autoParam
      (∀ (X : C),
        CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
          (CategoryTheory.MonoidalCategory.tensorRight X))
      CategoryTheory.IsMonoidalRightDistrib.preservesBinaryCoproducts_tensorRight._autoParam →
    CategoryTheory.IsMonoidalRightDistrib C
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.transformWithCache.visit.visitLambda : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            Bool →
              Bool →
                Bool →
                  (x : STWorld IO.RealWorld m) →
                    MonadLiftT (ST IO.RealWorld) m →
                      Array Lean.Expr → Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_mul_right : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Mul M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  nndist (a * c) (b * c) = nndist a b
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the left.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c)
  {Z : self.obj a ⟶ self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp f' g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
      (CategoryTheory.CategoryStruct.comp (self.mapComp f' g) h)
-- Mathlib.Order.Filter.Pi
Filter.le_pi_principal : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : (i : ι) → Set (α i)),
  Filter.principal (Set.univ.pi s) ≤ Filter.pi fun i => Filter.principal (s i)
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.notMem_of_notMem_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {P : M}, P ∉ AddSubmonoid.closure s → P ∉ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey? k = none
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.whiskerRight_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (H : CategoryTheory.SimplicialObject.Homotopy f g) {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) {n : ℕ} (i : Fin (n + 1)), (H.whiskerRight F).h i = F.map (H.h i)
-- Mathlib.Algebra.Order.Archimedean.Basic
le_iff_forall_rat_lt_imp_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  x ≤ y ↔ ∀ (q : ℚ), ↑q < x → ↑q ≤ y
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.autoParam.injEq : ∀ (argName argName_1 : Lean.Name),
  (Lean.Elab.Term.TacticMVarKind.autoParam argName = Lean.Elab.Term.TacticMVarKind.autoParam argName_1) =
    (argName = argName_1)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimitsOfShape.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C],
  autoParam (∀ (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasColimit F)
      CategoryTheory.Limits.HasColimitsOfShape.has_colimit._autoParam →
    CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Topology.Order.IntermediateValue
/-- If `f : α → α` is continuous on `[a, b]`, `a ≤ b`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[a, b]`.

In particular, if `[a, b]` is forward-invariant under `f`,
then `f` has a fixed point on `[a, b]`, see `exists_mem_Icc_isFixedPt_of_mapsTo`.  -/
exists_mem_Icc_isFixedPt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.Icc a b) → a ≤ b → a ≤ f a → f b ≤ b → ∃ c ∈ Set.Icc a b, Function.IsFixedPt f c
-- Mathlib.Data.Set.Prod
Set.prod_subset_prod_iff_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t t₁ : Set β}, s.Nonempty → (s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.mk_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  (c : CategoryTheory.Cokleisli U), { of := c.of } = c
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The setoid on `R × S` used for the Ore localization.  -/
OreLocalization.oreEqv : {R : Type u_1} →
  [inst : Monoid R] →
    (S : Submonoid R) → [OreLocalization.OreSet S] → (X : Type u_2) → [MulAction R X] → Setoid (X × ↥S)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure' x → Prop} →
        {X Y : C} → {x : X ⟶ Y} → W.multiplicativeClosure' x → Prop
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inverse_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F},
  f.toFun.ker = ⊥ → f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Lists are translated with a `cons` after each encoded number.
For example:

```
    [] = []
    [0] = [cons]
    [1] = [bit1, cons]
    [6, 0] = [bit0, bit1, bit1, cons, cons]
```
 -/
Turing.PartrecToTM2.trList : List ℕ → List Turing.PartrecToTM2.Γ'
-- Lean.Expr
/-- Return `true` if the given expression is a metadata.  -/
Lean.Expr.isMData : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.tensor_sum : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {P Q R S : C} {J : Type u_2}
  (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (∑ j ∈ s, g j) =
    ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.tensorHom f (g j)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_of_ceil_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], ⌈a⌉₊ < n → a < ↑n
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The continuous linear map underlying an element of `E →SWOT[σ] F`.  -/
ContinuousLinearMapWOT.toCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : Semiring 𝕜₁] →
      [inst_1 : Semiring 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] → [inst_7 : Module 𝕜₂ F] → (E →SWOT[σ] F) → E →SL[σ] F
-- Mathlib.Algebra.Homology.Monoidal
/-- The structure which allows to construct the monoidal category structure
on `HomologicalComplex C c` from the monoidal category structure on
graded objects.  -/
HomologicalComplex.Monoidal.inducingFunctorData : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  (c : ComplexShape I) →
                    [inst_7 : c.TensorSigns] →
                      [inst_8 : ∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
                        [inst_9 :
                            ∀ (X₁ : C),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                          [inst_10 :
                              ∀ (X₂ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                            [inst_11 :
                                ∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] →
                              [inst_12 :
                                  ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
                                [inst_13 :
                                    ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                                  [inst_14 : DecidableEq I] →
                                    CategoryTheory.Monoidal.InducingFunctorData (HomologicalComplex.forget C c)
-- Mathlib.Analysis.Polynomial.Norm
/-- The supNorm can also be defined with an iSup. Note that this uses the fact that `norm` is both
a `ZeroHom` and `NonnegHom` so is not _a priori_ true from the `gaussNorm` definition.  -/
Polynomial.supNorm_eq_iSup : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A), p.supNorm = ⨆ i, ‖p.coeff i‖
-- Mathlib.Analysis.Matrix.Normed
/-- Seminormed non-unital ring instance (using sup norm of L1 norm) for matrices over a seminormed
non-unital ring. Not declared as an instance because there are several natural choices for defining
the norm of a matrix.  -/
Matrix.linftyOpNonUnitalSemiNormedRing : {n : Type u_4} → {α : Type u_5} → [Fintype n] → [NonUnitalSeminormedRing α] → NonUnitalSeminormedRing (Matrix n n α)