mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.eq_zero_of_epi_kernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] [CategoryTheory.Epi (CategoryTheory.Limits.kernel.ι f)],
  f = 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionHomLeft : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {d d' : C}
  (f : d ⟶ d') (x : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f x =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) {Z : ↑(G.obj c)}
  (h : (α.app c).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.comp f g)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((α.naturality (CategoryTheory.CategoryStruct.comp f g)).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((G.mapComp f g).hom.toNatTrans.app ((α.app a).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).inv.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((α.naturality g).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
          (CategoryTheory.CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) h)))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.comp_coprod : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace N] [inst_3 : TopologicalSpace M₁]
  [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : ContinuousAdd M]
  [inst_8 : AddCommMonoid N] [inst_9 : Module R N] [inst_10 : ContinuousAdd N] [inst_11 : AddCommMonoid M₁]
  [inst_12 : Module R M₁] [inst_13 : AddCommMonoid M₂] [inst_14 : Module R M₂] (f : M →L[R] N) (g₁ : M₁ →L[R] M)
  (g₂ : M₂ →L[R] M), f ∘SL g₁.coprod g₂ = (f ∘SL g₁).coprod (f ∘SL g₂)
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toMulLeftMono : ∀ {α : Type u_1} [inst : IdemSemiring α], MulLeftMono α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom
-- Init.Data.Fin.Lemmas
Fin.val_eq_zero_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, ↑a = 0 ↔ a = 0
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.mk.injEq : ∀ (position : String.Pos.Raw) (label : Lean.Elab.InlayHintLabel) (kind? : Option Lean.Elab.InlayHintKind)
  (textEdits : Array Lean.Elab.InlayHintTextEdit) (tooltip? : Option String) (paddingLeft paddingRight : Bool)
  (position_1 : String.Pos.Raw) (label_1 : Lean.Elab.InlayHintLabel) (kind?_1 : Option Lean.Elab.InlayHintKind)
  (textEdits_1 : Array Lean.Elab.InlayHintTextEdit) (tooltip?_1 : Option String) (paddingLeft_1 paddingRight_1 : Bool),
  ({ position := position, label := label, kind? := kind?, textEdits := textEdits, tooltip? := tooltip?,
        paddingLeft := paddingLeft, paddingRight := paddingRight } =
      { position := position_1, label := label_1, kind? := kind?_1, textEdits := textEdits_1, tooltip? := tooltip?_1,
        paddingLeft := paddingLeft_1, paddingRight := paddingRight_1 }) =
    (position = position_1 ∧
      label = label_1 ∧
        kind? = kind?_1 ∧
          textEdits = textEdits_1 ∧ tooltip? = tooltip?_1 ∧ paddingLeft = paddingLeft_1 ∧ paddingRight = paddingRight_1)
-- Mathlib.CategoryTheory.Monad.Basic
/-- A morphism of comonads is a natural transformation compatible with ε and δ.  -/
CategoryTheory.ComonadHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Comonad C → CategoryTheory.Comonad C → Type (max u₁ v₁)
-- Lean.Data.Options
Lean.instInhabitedOption.default : {α : Type} → [Inhabited α] → Lean.Option α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {j j' : J} (f : j' ⟶ j),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Limits.colimit.ι F j) =
    CategoryTheory.Limits.colimit.ι F j'
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- Surjectivity (in a concrete category) as a `MorphismProperty`  -/
CategoryTheory.MorphismProperty.surjective : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → CategoryTheory.MorphismProperty C
-- Mathlib.LinearAlgebra.Contraction
lTensorHomEquivHomLTensor_toLinearMap : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  ↑(lTensorHomEquivHomLTensor R M P Q) = TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic.0.termσₙ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h))
-- Init.Data.Order.Ord
Std.TransCmp.gt_of_isGE_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  (cmp a b).isGE = true → cmp b c = Ordering.gt → cmp a c = Ordering.gt
-- Mathlib.Order.Fin.Basic
/-- While in many cases `Fin.castOrderIso` is better than `Equiv.cast`/`cast`, sometimes we want to
apply a generic lemma about `cast`.  -/
Fin.castOrderIso_toEquiv : ∀ {m n : ℕ} (h : n = m), (Fin.castOrderIso h).toEquiv = Equiv.cast ⋯
-- Std.Http.Data.Response
Std.Http.Response.instReprHead.repr : Std.Http.Response.Head → ℕ → Std.Format
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
LowerSemicontinuousWithinAt.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  LowerSemicontinuousWithinAt f s x →
    LowerSemicontinuousWithinAt g s x →
      ContinuousAt (fun p => p.1 + p.2) (f x, g x) → LowerSemicontinuousWithinAt (fun z => f z + g z) s x
-- Lean.CoreM
Lean.Core.Cache.mk.injEq : ∀ (instLevelType instLevelValue instLevelType_1 instLevelValue_1 : Lean.Core.InstantiateLevelCache),
  ({ instLevelType := instLevelType, instLevelValue := instLevelValue } =
      { instLevelType := instLevelType_1, instLevelValue := instLevelValue_1 }) =
    (instLevelType = instLevelType_1 ∧ instLevelValue = instLevelValue_1)
-- Mathlib.Algebra.Order.UpperLower
mul_lowerClosure : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s t : Set α),
  s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Sum.inl) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.copy_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {K' H' : C} (eK : K' ≅ h.K) (eH : H' ≅ h.H),
  (h.copy eK eH).H = H'
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.lipschitz : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), LipschitzWith 1 ⇑f
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInvolutiveNeg.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveNeg α], Colex.instInvolutiveNeg = { toNeg := Colex.instNeg, neg_neg := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.forget_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) {X Y : F.Grothendieck}
  (f : X ⟶ Y), (CategoryTheory.Pseudofunctor.Grothendieck.forget F).map f = f.base
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.fst = f
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.forget_obj_of : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (CategoryTheory.AdditiveFunctor.forget C D).obj (CategoryTheory.AdditiveFunctor.of F) = F
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationOfFinite : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} [Finite X], MeasureTheory.IsFiniteMeasure μ.variation
-- Mathlib.Algebra.Group.Ext
SubNegMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : SubNegMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ Neg.neg = Neg.neg
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w} [inst_1 : CategoryTheory.SmallCategory α]
  [CategoryTheory.FinCategory α] [CategoryTheory.Limits.HasColimitsOfShape α C] {I : Type v}
  [inst_4 : CategoryTheory.SmallCategory I] [inst_5 : CategoryTheory.IsFiltered I],
  CategoryTheory.Limits.PreservesColimitsOfShape α (CategoryTheory.Ind.lim I)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.congr_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g : α → F} {l : Filter α},
  f₁ =o[𝕜; l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =o[𝕜; l] g
-- Mathlib.Topology.Separation.Profinite
/-- A T0 space with a clopen basis is totally separated.  -/
totallySeparatedSpace_of_t0_of_basis_clopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X],
  TopologicalSpace.IsTopologicalBasis {s | IsClopen s} → TotallySeparatedSpace X
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.obj₂ = (DerivedCategory.singleFunctor C 0).obj S.X₂
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- Let `b` be a basis of `M` indexed by a linearly ordered type `I` and `s` be a finset of `I`
of cardinality `n`. Let `t` be a finset of `I` of cardinality `n` such that `s ≠ t`. If we apply
the linear form on `⋀[R]^n M` defined by `b` and `s` to the exterior product of the
`b i` for `i ∈ t`, then we get `0`.  -/
exteriorPower.ιMultiDual_apply_nondiag : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s t : ↑(Set.powersetCard I n)),
  s ≠ t → (exteriorPower.ιMultiDual R n b s) (exteriorPower.ιMulti_family R n (⇑b) t) = 0
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.prod_normalizedFactors_eq_self : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I : Ideal T},
  I ≠ ⊥ → (UniqueFactorizationMonoid.normalizedFactors I).prod = I
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstLENat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Algebra.Support
LocallyFinite.smul_right : ∀ {X : Type u_1} {M : Type u_7} {R : Type u_8} {ι : Type u_9} [inst : TopologicalSpace X] [inst_1 : Zero M]
  [inst_2 : SMulZeroClass R M] {f : ι → X → M},
  (LocallyFinite fun i => Function.support (f i)) →
    ∀ (s : ι → X → R), LocallyFinite fun i => Function.support (s i • f i)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.face_mk : ∀ {n : ℕ} (l u : Fin (n + 1) → ℝ) (h : ∀ (i : Fin (n + 1)), l i < u i) (i : Fin (n + 1)),
  { lower := l, upper := u, lower_lt_upper := h }.face i =
    { lower := l ∘ i.succAbove, upper := u ∘ i.succAbove, lower_lt_upper := ⋯ }
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.go_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α]
  (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size }),
  Std.DHashMap.Internal.Raw₀.expand.go✝ 0 source target =
    List.foldl (fun acc p => Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd) target
      (Std.DHashMap.Internal.toListModel source)
-- Mathlib.Order.CompletePartialOrder
/-- A complete lattice is a complete partial order.  -/
CompleteLattice.toCompletePartialOrder : {α : Type u_2} → [CompleteLattice α] → CompletePartialOrder α
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Ioi x) x = sInf (slope f x '' {y | y ∈ S ∧ x < y})
-- Mathlib.Topology.MetricSpace.CantorScheme
CantorScheme.ClosureAntitone.antitone : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : TopologicalSpace α],
  CantorScheme.ClosureAntitone A → CantorScheme.Antitone A
-- Mathlib.Probability.Process.Stopping
MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m} {τ σ : Ω → WithTop ι} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [inst_4 : TopologicalSpace ι] [OrderTopology ι]
  [SecondCountableTopology ι] (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hσ : MeasureTheory.IsStoppingTime ℱ σ)
  [MeasureTheory.SigmaFinite (μ.trim ⋯)],
  μ[f | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f | hτ.measurableSpace]
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.sigmaIsoHom_surj : ∀ {S : Type u_1} {Y : Type u_2} (f : S → Y) [inst : TopologicalSpace S],
  Function.Surjective ⇑(TopologicalSpace.Fiber.sigmaIsoHom f)
-- Mathlib.Analysis.Seminorm
/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
the rescaling element that shows up in applications.  -/
rescale_to_shell_semi_normed_zpow : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {x : E}, ‖x‖ ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_subsingleton : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [Subsingleton ι] (f : ι → M) (a : ι),
  ∑ x, f x = f a
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.HasColimit.whiskerLeft_isoOfNatIso_ι_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F G : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] [inst_4 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J)
  {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (w.hom.app j))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι G j))
-- Mathlib.Analysis.CStarAlgebra.lpSpace
instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal : {I : Type u_1} →
  {A : I → Type u_2} → [inst : (i : I) → NonUnitalCommCStarAlgebra (A i)] → NonUnitalCommCStarAlgebra ↥(lp A ⊤)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.set_smul_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [SMulCommClass α R M] (s : Set α) (t : Set M),
  s • Submodule.span R t = Submodule.span R (s • t)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.hm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : HomotopicalAlgebra.AttachCells g f) (i : self.ι),
  CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) self.m =
    CategoryTheory.CategoryStruct.comp (g (self.π i)) (self.cofan₂.inj i)
-- Lean.Parser.Term
Lean.Parser.Term.anonymousCtor.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.brecOn.eq : ∀ {α : Type u} {motive : Batteries.PairingHeapImp.Heap α → Sort u_1} (t : Batteries.PairingHeapImp.Heap α)
  (F_1 : (t : Batteries.PairingHeapImp.Heap α) → Batteries.PairingHeapImp.Heap.below t → motive t),
  Batteries.PairingHeapImp.Heap.brecOn t F_1 = F_1 t (Batteries.PairingHeapImp.Heap.brecOn.go t F_1).2
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- The dimension of a finite-dimensional space is preserved under linear equivalence.  -/
LinearEquiv.finrank_eq : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M ≃ₗ[R] N), Module.finrank R M = Module.finrank R N
-- Mathlib.Algebra.CharP.Defs
NeZero.of_not_dvd : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {n p : ℕ} [CharP R p], ¬p ∣ n → NeZero ↑n
-- Mathlib.Geometry.Convex.Star
Convexity.IsConvexSet.isStarConvexSet : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : Set X},
  Convexity.IsConvexSet R s → x ∈ s → Convexity.IsStarConvexSet R x s
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.splits_charpoly : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), (MulSemiringAction.charpoly G b).Splits
-- Init.Data.Nat.Basic
Nat.exists_eq_succ_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → ∃ k, n = k.succ
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `P.Over.map` is left adjoint to `P.Over.pullback` if pullbacks of morphisms satisfying `P`
exist along `f` and are also in `P`, and `f` is in both `P` and `Q`.  -/
CategoryTheory.MorphismProperty.Over.mapPullbackAdj : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          [inst_2 : P.IsStableUnderComposition] →
            [inst_3 : Q.IsStableUnderBaseChange] →
              (f : X ⟶ Y) →
                [inst_4 : P.HasPullbacksAlong f] →
                  [inst_5 : P.IsStableUnderBaseChangeAlong f] →
                    [Q.HasOfPostcompProperty Q] →
                      (hPf : P f) →
                        Q f →
                          (CategoryTheory.MorphismProperty.Over.map Q hPf ⊣
                            CategoryTheory.MorphismProperty.Over.pullback P Q f)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (x : M), (IsLocalizedModule.iso S f).symm (f x) = LocalizedModule.mk x 1
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.exists_eq_append_singleton : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.endPos),
  (p.next hp).Splits t₁ t₂ → ∃ t₁', t₁ = t₁' ++ String.singleton (p.get hp)
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withType : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → [MonadLiftT Lean.MetaM m] → m α → m α
-- Mathlib.Data.Prod.TProd
Set.elim_preimage_pi : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] {l : List ι},
  l.Nodup → ∀ (h : ∀ (i : ι), i ∈ l) (t : (i : ι) → Set (α i)), List.TProd.elim' h ⁻¹' Set.univ.pi t = Set.tprod l t
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 d x → fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x
-- Std.Internal.UV.System
/-- Sets the title of the current process.
 -/
Std.Internal.UV.System.setProcessTitle : String → IO Unit