mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- An alternate constructor for strict pseudofunctors that does not
require the `mapId` or `mapComp` fields, and that adapts the compatibility conditions
to the fact that the pseudofunctor is strict  -/
CategoryTheory.StrictPseudofunctor.mk' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictPseudofunctorCore B C → CategoryTheory.StrictPseudofunctor B C
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_iff_preimage_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  LowerSemicontinuousOn f s ↔ ∀ (b : γ), ∃ v, IsClosed v ∧ s ∩ f ⁻¹' Set.Iic b = s ∩ v
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, m.contains a = false → Std.DHashMap.Raw.Const.get! m a = default
-- Mathlib.Data.Finset.Sum
Finset.toRight_image_swap : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (Finset.image Sum.swap u).toRight = u.toLeft
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Asymptotics.IsThetaTVS.eq_1 : ∀ (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  (l : Filter α) (f : α → E) (g : α → F), f =Θ[𝕜; l] g = (f =O[𝕜; l] g ∧ g =O[𝕜; l] f)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) (W : C),
  h.homIso W = (Equiv.ulift.trans h.homEquiv).toIso
-- Init.Data.Vector.Erase
Vector.getElem?_eraseIdx_of_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n) {j : ℕ}, j < i → (xs.eraseIdx i h)[j]? = xs[j]?
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.primPart.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p.primPart = if p = 0 then 1 else Classical.choose ⋯
-- Lean.PrettyPrinter.Parenthesizer
/-- Run `x` and parenthesize the result using `mkParen` if necessary.
If `canJuxtapose` is false, we assume the category does not have a token-less juxtaposition syntax a la function application and deactivate rule 2.  -/
Lean.PrettyPrinter.Parenthesizer.maybeParenthesize : Lean.Name →
  Bool →
    (Lean.Syntax → Lean.Syntax) → ℕ → Lean.PrettyPrinter.ParenthesizerM Unit → Lean.PrettyPrinter.ParenthesizerM Unit
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C}
  (h_1 : CategoryTheory.Functor.id C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv
      (CategoryTheory.CategoryStruct.comp (t.truncLEι a) h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncLTι b) h_1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mono_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∀ [inst_2 : S.HasRightHomology], CategoryTheory.Mono S.fromOpcycles
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.subtractionMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : SubtractionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.subtractionMonoid f hf one mul inv div npow zpow =
    { toSubNegMonoid := Function.Injective.subNegMonoid f hf one mul inv div npow zpow, neg_neg := ⋯, neg_add_rev := ⋯,
      neg_eq_of_add := ⋯ }
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_units_conj' : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (y : 𝔸ˣ) (x : 𝔸),
  NormedSpace.exp (↑y⁻¹ * x * ↑y) = ↑y⁻¹ * NormedSpace.exp x * ↑y
-- Mathlib.Analysis.Convex.Join
convexJoin_left_comm : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (s t u : Set E),
  convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSMul' : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul βᵒᵈ α
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Lift a linear map between finitely generated modules to `FGModuleCat R`.  -/
FGModuleCat.ofHom : {R : Type u} →
  [inst : Ring R] →
    {V W : Type v} →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          [inst_3 : Module.Finite R V] →
            [inst_4 : AddCommGroup W] →
              [inst_5 : Module R W] →
                [inst_6 : Module.Finite R W] → (V →ₗ[R] W) → (FGModuleCat.of R V ⟶ FGModuleCat.of R W)
-- Mathlib.Probability.Distributions.Fernique
/-- For `μ` a probability measure whose product with itself is invariant by rotation and for `a, c`
with `2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a}`, the integral `∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μ`
is bounded by a quantity that does not depend on `a`.  -/
ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ {c : ENNReal},
      c ≤ μ {x | ‖x‖ ≤ a} →
        2⁻¹ < c →
          ∫⁻ (x : E), ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
            ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c)) +
              ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.get! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.whiskerRightMkNatTrans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  {h₁ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)}
  {h₂ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)}
  {h₃ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
      CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)}
  {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (H : CategoryTheory.Functor C D),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H =
    CategoryTheory.Limits.reflexivePair.mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.comap_inf : ∀ {α : Type u_2} {γ : Type u_3} {u₁ u₂ : UniformSpace γ} {f : α → γ},
  UniformSpace.comap f (u₁ ⊓ u₂) = UniformSpace.comap f u₁ ⊓ UniformSpace.comap f u₂
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_filter : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {p : BoxIntegral.Box ι → Prop},
  J ∈ π.filter p ↔ J ∈ π ∧ p J
-- Init.Data.Rat.Lemmas
Rat.normalize_mul_right : ∀ {d : ℕ} {n : ℤ} {a : ℕ} (d0 : d ≠ 0) (a0 : a ≠ 0), Rat.normalize (n * ↑a) (d * a) ⋯ = Rat.normalize n d d0
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_add_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 1) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) → (f + g).prod h = f.prod h * g.prod h
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.distortion_toSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).distortion = π.distortion
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → IsRelPrime (-x) y
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_reverse : ∀ {α : Type u_1} {a : α} {t : RBTree.RBNode α}, a ∈ t.reverse ↔ a ∈ t
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.length_eq : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  s₁.Equivalent s₂ → s₁.length = s₂.length
-- Lean.Elab.Coinductive
/-- The flag that is `true` if the predicate was defined via `coinductive` keyword and `false`
otherwise. When we elaborate a mutual definition, we allow mixing `coinductive` and `inductive`
keywords, and hence we need to record this information.
 -/
Lean.Elab.Command.CoinductiveElabData.isGreatest : Lean.Elab.Command.CoinductiveElabData → Bool
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_left_of_le : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ (x : α), C ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
HasFDerivWithinAt.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {s : Set E} {x : E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_eventually_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {r : α → β → Prop},
  (∃ b, ∀ᶠ (a : α) in Filter.atTop, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atTop, ∃ b, ∀ (a : α), a₀ ≤ a → r a b
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any limit cone over a pair into a bilimit bicone.  -/
CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {J : Type u_1} →
        [Fintype J] →
          {f : J → C} →
            {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} →
              (ht : CategoryTheory.Limits.IsLimit t) → (CategoryTheory.Limits.Bicone.ofLimitCone ht).IsBilimit
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftObj.tensor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [Mathlib.Tactic.Coherence.LiftObj X] →
          [Mathlib.Tactic.Coherence.LiftObj Y] →
            Mathlib.Tactic.Coherence.LiftObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The associator isomorphism: `(f ≫ g) ≫ h ≅ f ≫ g ≫ h`  -/
CategoryTheory.Bicategory.associator : {B : Type u} →
  [self : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ≅
              CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If each point of `α` admits a neighbourhood `V ∈ 𝔖`,
then the evaluation of `f : α →ᵤ[𝔖] β` at `x : α` is continuous in `(f, x)`
on the set of `(f, x)` such that `f` is continuous at `x`.  -/
UniformOnFun.continuousOn_eval₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : TopologicalSpace α],
  (∀ (x : α), ∃ V ∈ 𝔖, V ∈ nhds x) →
    ContinuousOn (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) {fx | ContinuousAt ((UniformOnFun.toFun 𝔖) fx.1) fx.2}
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.face_singleton_compl_le_boundary : ∀ {n : ℕ} (i : Fin (n + 1)), SSet.stdSimplex.face {i}ᶜ ≤ SSet.boundary n
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i._auto_3),
  CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.iCycles f₁ f₂ n₁) =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Given an `R`-module `M` and a function `m → n` between arbitrary types,
construct a linear map `(n → M) →ₗ[R] (m → M)`  -/
LinearMap.funLeft : (R : Type u_1) →
  (M : Type u_5) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {m : Type u_9} → {n : Type u_10} → (m → n) → (n → M) →ₗ[R] m → M
-- Mathlib.Topology.Compactness.Compact
/-- Sets that are contained in a compact set form a bornology. Its `cobounded` filter is
`Filter.cocompact`. See also `Bornology.relativelyCompact` the bornology of sets with compact
closure.  -/
Bornology.inCompact : (X : Type u) → [TopologicalSpace X] → Bornology X
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a right extension from a 1-morphism and a 2-morphism.  -/
CategoryTheory.Bicategory.RightExtension.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (h : b ⟶ c) → (CategoryTheory.CategoryStruct.comp f h ⟶ g) → CategoryTheory.Bicategory.RightExtension f g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.struct.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.struct = 1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  S.homologyι = CategoryTheory.CategoryStruct.comp S.rightHomologyIso.inv S.rightHomologyι
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Mod.trivialAction_mod_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : CategoryTheory.Mon C) (X : C),
  CategoryTheory.ModObj.smul = CategoryTheory.SemiCartesianMonoidalCategory.snd M.X X
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divByMonic_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} [Nontrivial R], q.Monic → (p /ₘ q = 0 ↔ p.degree < q.degree)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_isSome_getEntry?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → Std.DTreeMap.Internal.Impl.contains k t = (t.getEntry?ₘ k).isSome
-- Mathlib.Algebra.Ring.Subring.Units
Units.mem_posSubgroup : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (u : Rˣ),
  u ∈ Units.posSubgroup R ↔ 0 < ↑u
-- Std.Internal.UV.System
/-- Information about a single CPU core.
 -/
Std.Internal.UV.System.CPUInfo : Type
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.comap_ne_bot`. -/
Ideal.IntegralClosure.comap_ne_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, I ≠ ⊥ → Ideal.comap (algebraMap R A) I ≠ ⊥
-- Mathlib.Order.Filter.Basic
Filter.congr_sets : ∀ {α : Type u} {f : Filter α} {s t : Set α}, {x | x ∈ s ↔ x ∈ t} ∈ f → (s ∈ f ↔ t ∈ f)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom_assoc : ∀ (X : AlgebraicGeometry.Scheme) {x y z : ↥X} (e : x = y) (e' : y = z) {Z : CommRingCat} (h : X.residueField z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e').hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom h
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_def : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (p q : M),
  Convexity.convexCombPair s t hs ht h p q = Convexity.iConvexComb (Convexity.StdSimplex.duple 0 1 hs ht h) ![p, q]
-- Init.Data.Float.Float32
/-- Computes the hyperbolic tangent of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`tanhf`.
 -/
Float32.tanh : Float32 → Float32
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J),
  ↑(Ideal.quotientEquivAlgOfEq R₁ h) = Ideal.Quotient.factorₐ R₁ ⋯
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsIsColocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.isColocal.IsClosedUnderIsomorphisms
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left : ∀ (R : Type u) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsAlgebraic (↥⊥) S], Algebra.IsAlgebraic R S
-- Mathlib.ModelTheory.Basic
/-- The homomorphism commutes with the interpretations of the function symbols  -/
FirstOrder.Language.StrongHomClass.map_fun : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  {inst : FunLike F M N} {inst_1 : L.Structure M} {inst_2 : L.Structure N} [self : L.StrongHomClass F M N] (φ : F)
  {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a surjective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is surjective.  -/
AddSubmonoid.LocalizationMap.map_surjective_of_surjective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {Q : Type u_4} [inst_3 : AddCommMonoid Q],
  Function.Surjective ⇑g → ∀ (k : (AddSubmonoid.map g S).LocalizationMap Q), Function.Surjective ⇑(f.map ⋯ k)
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0.induct_unfolding : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (x : Lean.Grind.AC.Var), motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var x)) →
    (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
        have s' := s.erase0;
        (x == 0) = true → motive s s.erase0 → motive (Lean.Grind.AC.Seq.cons x s) s') →
      (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
          have s' := s.erase0;
          ¬(x == 0) = true →
            (s' == Lean.Grind.AC.Seq.var 0) = true →
              motive s s.erase0 → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x)) →
        (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
            have s' := s.erase0;
            ¬(x == 0) = true →
              ¬(s' == Lean.Grind.AC.Seq.var 0) = true →
                motive s s.erase0 → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.cons x s')) →
          ∀ (s : Lean.Grind.AC.Seq), motive s s.erase0
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.moduleLeft : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : Semiring R] →
            (v : AbsoluteValue R S) → [inst_3 : AddCommMonoid T] → [Module R T] → Module (WithAbs v) T
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.eventually_cofinite_not_isRoot : ∀ {R : Type u_2} [inst : CommRing R] [IsDomain R] {P : Polynomial R}, P ≠ 0 → ∀ᶠ (x : R) in Filter.cofinite, ¬P.IsRoot x
-- Lean.Message
Lean.instToJsonSerialMessage.toJson : Lean.SerialMessage → Lean.Json
-- Init.Data.Ord.Basic
Ordering.eq_eq_of_isLE_of_isGE : ∀ {o : Ordering}, o.isLE = true → o.isGE = true → o = Ordering.eq
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toMagmaCatIso_hom : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y] (e : X ≃* Y), e.toMagmaCatIso.hom = MagmaCat.ofHom e.toMulHom
-- Mathlib.Order.Hom.Basic
OrderHom.curry_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β →o γ) (x : α × β), ((RelIso.symm OrderHom.curry) f) x = (f x.1) x.2
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mul_apply_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] (x : R),
  ‖(ContinuousLinearMap.mul 𝕜 R) x‖ ≤ ‖x‖
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.smul_induction : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {motive : Monoid.CoprodI.Word M → Prop},
  motive Monoid.CoprodI.Word.empty →
    (∀ (i : ι) (m : M i) (w : Monoid.CoprodI.Word M), motive w → motive (Monoid.CoprodI.of m • w)) →
      ∀ (w : Monoid.CoprodI.Word M), motive w