mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_top : LinearGrowth.linearGrowthInf ⊤ = ⊤
-- Mathlib.Tactic.Positivity.Core
/-- Environment extensions for `positivity` declarations  -/
Mathlib.Meta.Positivity.positivityExt : Lean.PersistentEnvExtension Mathlib.Meta.Positivity.Entry
  (Mathlib.Meta.Positivity.Entry × Mathlib.Meta.Positivity.PositivityExt)
  (List Mathlib.Meta.Positivity.Entry × Lean.Meta.DiscrTree Mathlib.Meta.Positivity.PositivityExt)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂')
  (hom₃ : obj₃ ⟶ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp hom₃ mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₁ = hom₁.app j
-- Mathlib.Algebra.Free
FreeAddMagma.traverse_add : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x y : FreeAddMagma α),
  traverse F (x + y) = (fun x1 x2 => x1 + x2) <$> traverse F x <*> traverse F y
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_id_X_eq_join₂ : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R],
  MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X = MvPolynomial.join₂
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
/-- If `Φ : LocalizerMorphism W₁ W₂` corresponds to a class `W₁` that is
the inverse image of `W₂` by the functor `Φ.functor` and that we
have functorial right resolutions, then this is a morphism of localizers
in the other direction.  -/
CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {ρ : CategoryTheory.Functor C₂ C₁} →
                {i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor} →
                  (∀ (X₂ : C₂), W₂ (i.app X₂)) →
                    W₁ = W₂.inverseImage Φ.functor →
                      [W₂.HasTwoOutOfThreeProperty] → CategoryTheory.LocalizerMorphism W₂ W₁
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList.eq_3 : ∀ (k : ℕ), k.succ.succ.primeFactorsList = (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_prod : ∀ {δ : Type u_4} {α : Type u_9} {β : Type u_10} {γ : Type u_11} (s : Set α) (t : Set β) (f : α → Set γ) (g : β → Set δ),
  ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- If `G` is the fundamental group for `F`, it is isomorphic to `Aut F` as groups and
this isomorphism is also a homeomorphism (see `toAutMulEquiv_isHomeomorph`).  -/
CategoryTheory.PreGaloisCategory.toAutMulEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        (G : Type u_1) →
          [inst_2 : Group G] →
            [inst_3 : (X : C) → MulAction G (F.obj X).obj] →
              [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
                [inst_5 : TopologicalSpace G] →
                  [inst_6 : IsTopologicalGroup G] →
                    [inst_7 : CompactSpace G] →
                      [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] → G ≃* CategoryTheory.Aut F
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertListIfNewUnit_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  toInsert.contains k = false →
    Std.Internal.List.getEntry? k (Std.Internal.List.insertListIfNewUnit l toInsert) = Std.Internal.List.getEntry? k l
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X_1 : C₁) {X_2 Y : C₂} (f : X_2 ⟶ Y),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X_1).map f =
    (X.obj (F₁.obj X_1)).map (F₂.map f)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.monomial_smul_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (r : R)
  (j : ℕ) (m : M), (Polynomial.monomial i) r • PolynomialModule.single R j m = PolynomialModule.single R (i + j) (r • m)
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {ι : Type u_4} (f : M ≃ₗ[R] N) (x : Orientation R M ι), (Orientation.map ι f) (-x) = -(Orientation.map ι f) x
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.rightUnitor_def : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor M = SemimoduleCat.MonoidalCategory.rightUnitor M
-- Mathlib.Order.Defs.LinearOrder
lt_or_gt_of_ne : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≠ b → a < b ∨ b < a
-- Mathlib.Algebra.Group.Center
IsMulCentral.left_comm : ∀ {M : Type u_1} {a : M} [inst : Mul M], IsMulCentral a → ∀ (b c : M), a * (b * c) = b * (a * c)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_add_mod_self : ∀ (x y z : Ordinal.{u_4}), (x * y + z) % x = z % x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {H' : Type u_5} {inst_4 : TopologicalSpace H'}
  {E' : Type u_6} {inst_5 : NormedAddCommGroup E'} {inst_6 : NormedSpace 𝕜 E'} {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} {inst_7 : TopologicalSpace G}
  {inst_8 : ChartedSpace H G} {inst_9 : AddMonoid G} {G' : Type u_9} {inst_10 : TopologicalSpace G'}
  {inst_11 : ChartedSpace H' G'} {inst_12 : AddMonoid G'} {toAddMonoidHom : G →+ G'}
  {contMDiff_toFun : ContMDiff I I' n (↑toAddMonoidHom).toFun} {toAddMonoidHom_1 : G →+ G'}
  {contMDiff_toFun_1 : ContMDiff I I' n (↑toAddMonoidHom_1).toFun},
  { toAddMonoidHom := toAddMonoidHom, contMDiff_toFun := contMDiff_toFun } =
      { toAddMonoidHom := toAddMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 } →
    toAddMonoidHom = toAddMonoidHom_1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.not_infinitesimal : ∀ {x : ℝ*}, x.Infinite → ¬x.Infinitesimal
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The identity map as an equivariant additive monoid homomorphism.  -/
DistribMulActionHom.id : (M : Type u_1) →
  [inst : Monoid M] → {A : Type u_4} → [inst_1 : AddMonoid A] → [inst_2 : DistribMulAction M A] → A →+[M] A
-- Mathlib.Data.Vector.Basic
/-- Define `motive v₁ v₂` by case-analysis on `v₁ : Vector α n` and `v₂ : Vector β n`.  -/
List.Vector.casesOn₂ : {α : Type u_1} →
  {m : ℕ} →
    {β : Type u_6} →
      {motive : {n : ℕ} → List.Vector α n → List.Vector β n → Sort u_8} →
        (v₁ : List.Vector α m) →
          (v₂ : List.Vector β m) →
            motive List.Vector.nil List.Vector.nil →
              ({n : ℕ} →
                  (x : α) → (y : β) → (xs : List.Vector α n) → (ys : List.Vector β n) → motive (x ::ᵥ xs) (y ::ᵥ ys)) →
                motive v₁ v₂
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instSMulCommClass : ∀ {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] [inst_1 : SMul T R]
  [SMulCommClass S T R], SMulCommClass S T (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClopen_iff_zeroLocus : ∀ {R : Type u} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  IsClopen s ↔ ∃ e, IsIdempotentElem e ∧ s = PrimeSpectrum.zeroLocus {e}
-- Mathlib.Topology.Category.TopCat.Basic
_private.Mathlib.Topology.Category.TopCat.Basic.0.TopCat.Hom.mk.inj : ∀ {X Y : TopCat} {hom' hom'_1 : C(↑X, ↑Y)}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- The skeleton of a monoidal category has a monoidal structure itself, induced by the equivalence.
 -/
CategoryTheory.Skeleton.instMonoidalCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Skeleton C)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.card_chunk : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts},
  Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≠ 0 →
    (SzemerediRegularity.chunk hP G ε hU).parts.card = 4 ^ P.parts.card
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange]
  [HomotopicalAlgebra.Fibration g] [HomotopicalAlgebra.WeakEquivalence g],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.g_s_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.g (CategoryTheory.CategoryStruct.comp s.s h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp s.r S.f) h
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Copy of a lax monoidal structure with new `ε` and `μ` fields equal to the old ones.

This is useful to fix definitional equalities.  -/
CategoryTheory.Functor.LaxMonoidal.copy : {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} →
              (hF : F.LaxMonoidal) →
                (ε' :
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                      F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                  (μ' :
                      (X Y : C) →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                          F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                    autoParam (ε' = CategoryTheory.Functor.LaxMonoidal.ε F)
                        CategoryTheory.Functor.LaxMonoidal.copy._auto_1 →
                      autoParam (μ' = CategoryTheory.Functor.LaxMonoidal.μ F)
                          CategoryTheory.Functor.LaxMonoidal.copy._auto_3 →
                        F.LaxMonoidal
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonUnitalNonAssocRing : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → NonUnitalNonAssocRing (SkewMonoidAlgebra k G)
-- Mathlib.Data.Set.Lattice
Set.iUnion_range_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (C : ι → Set α) {f : (x : ι) → β → ↑(C x)},
  (∀ (x : ι), Function.Surjective (f x)) → (⋃ y, Set.range fun x => ↑(f x y)) = ⋃ x, C x
-- Mathlib.NumberTheory.Dioph
/-- The constant function with value `n : ℤ`.  -/
Poly.const : {α : Type u_1} → ℤ → Poly α
-- Aesop.Tree.Data
Aesop.NormalizationState.provenByNormalization.injEq : ∀ (postState : Lean.Meta.SavedState) (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)))
  (postState_1 : Lean.Meta.SavedState)
  (script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  (Aesop.NormalizationState.provenByNormalization postState script =
      Aesop.NormalizationState.provenByNormalization postState_1 script_1) =
    (postState = postState_1 ∧ script = script_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsUpper : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_one_of_mem_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α) {x : α},
  x ∈ closure E → thickenedIndicatorAux δ E x = 1
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.ofComp_compatibility : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_3 : G.Full] [inst_4 : G.Faithful] (A : Type u_5) [inst_5 : AddMonoid A] [inst_6 : CategoryTheory.HasShift C A]
  [inst_7 : CategoryTheory.HasShift D A] [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A]
  [inst_10 : H.CommShift A], CategoryTheory.NatTrans.CommShift e.hom A
-- Mathlib.Order.CompleteBooleanAlgebra
compl_sSup : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α}, (sSup s)ᶜ = ⨅ i ∈ s, iᶜ
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_neg_neg_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(A + -A + -A).card ≤ K ^ 2 * ↑A.card
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism arising from `mapComp_eq`.  -/
CategoryTheory.Under.mapComp : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y Z : T} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) ≅
            (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is full on `R`-algebras.  -/
AlgebraicGeometry.algSpec.instFull : ∀ {R : CommRingCat}, (AlgebraicGeometry.algSpec R).Full
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The left action of this bimodule object  -/
Bimod.actLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} →
        (self : Bimod A B) → CategoryTheory.MonoidalCategoryStruct.tensorObj A.X self.X ⟶ self.X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDTreeMap.map f t).get? k = Option.map (f k) (t.get? k)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one
          (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x x_1 : C) (x_2 : D),
  (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D) x
            x_1).unmop.app
      x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2).hom
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap_def : ∀ {n m : ℕ} (hm : n ∣ m), ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
-- Mathlib.RingTheory.SimpleRing.Defs
/-- A ring `R` is **simple** if it has only two two-sided ideals, namely `⊥` and `⊤`.
 -/
IsSimpleRing : (R : Type u_1) → [NonUnitalNonAssocRing R] → Prop
-- Batteries.Data.Array.Match
Array.Matcher.Iterator.mk.inj : ∀ {σ : Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} {inst : BEq α} {m : Array.Matcher α}
  {inst_1 : Std.Iterator σ n α} {inner : Std.IterM n α} {state : Fin (m.table.size + 1)} {inner_1 : Std.IterM n α}
  {state_1 : Fin (m.table.size + 1)},
  { inner := inner, state := state } = { inner := inner_1, state := state_1 } → inner = inner_1 ∧ state = state_1
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instIsOrderedMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α], IsOrderedMonoid αᵃᵒᵖ
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_infs_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α}, (s ⊼ t).Nonempty → t.Nonempty
-- Std.Async.TCP
/-- Enables the Nagle algorithm for all client sockets accepted by this server socket.
 -/
Std.Async.TCP.Socket.Server.noDelay : Std.Async.TCP.Socket.Server → IO Unit
-- Mathlib.Data.Set.Sups
lowerClosure_infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α), lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The `MulEquiv` between the kernel of the restriction map to a normal subgroup `H` of homomorphisms
of type `G →* A` and the group of homomorphisms `G ⧸ H →* A`.
 -/
MonoidHom.domRestrictHomKerEquiv : {G : Type u} →
  [inst : Group G] →
    (A : Type u_1) →
      [inst_1 : CommGroup A] →
        (H : Subgroup G) → [inst_2 : H.Normal] → ↥(MonoidHom.domRestrictHom H A).ker ≃* (G ⧸ H →* A)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp' : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
      (F.mapComp' f₀₂ f₂₃ f ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (F.mapComp' f₀₁ f₁₃ f ⋯))
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : X.Over Y] (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.IsOver
    (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap (X ↘ Y) x)) Y
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.tendsto_ofSeq : ∀ {f : ℕ → ℝ} {lb : Filter ℝ},
  Filter.Germ.Tendsto (Hyperreal.ofSeq f) lb ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) lb
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open left half-plane is an open set in the complex plane.  -/
Complex.isOpen_re_lt : ∀ (x : ℝ), IsOpen {z | z.re < x}
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedMul M] {s : Set α}
  {f g : α → M}, (∀ a ∈ s, f a ≤ g a) → s.mulIndicator f ≤ g
-- Mathlib.Analysis.LocallyConvex.AbsConvex
balancedHull_subset_convexHull_union_neg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.symm_trans : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), φ.symm.trans φ = Representation.Equiv.refl σ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft.inj : ∀ {C : Type u} {X Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C} {f f_1 : Y₁.Hom Y₂},
  CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f = CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f_1 →
    f = f_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
derivWithin_csinh : ∀ {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x → derivWithin (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) * derivWithin f s x
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.lcm_sup : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B] (n₁ n₂ : ℕ)
  (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₁]
  [NeZero n₂], IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
-- Mathlib.GroupTheory.QuotientGroup.Finite
Group.fintypeOfKerOfCodom.eq_1 : ∀ {G : Type u_2} {H : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : Fintype H] (g : G →* H)
  [inst_3 : Fintype ↥g.ker],
  Group.fintypeOfKerOfCodom g =
    Group.fintypeOfKerLeRange (Subgroup.topEquiv.toMonoidHom.comp (Subgroup.inclusion ⋯)) g ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instSmoothMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.Smooth f],
  AlgebraicGeometry.Smooth (f ∣_ V)