mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`.  -/
Module.End.maxGenEigenspace_eq : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R), f.maxGenEigenspace μ = (f.genEigenspace μ) ↑(f.maxGenEigenspaceIndex μ)
-- Lean.Elab.Level
Lean.Elab.Level.instMonadOptionsLevelElabM : Lean.MonadOptions Lean.Elab.Level.LevelElabM
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Set.Ioc (OrderDual.toDual b) (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ico a b
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_zero : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A], IsNilpotent.exp 0 = 1
-- Aesop.Tree.Data
Aesop.GoalState.provenByNormalization.sizeOf_spec : sizeOf Aesop.GoalState.provenByNormalization = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CochainComplex (ModuleCat k) ℕ}
  (h : groupCohomology.inhomogeneousCochains C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap g ψ) h)
-- Init.Data.Array.DecidableEq
Array.beq_toList : ∀ {α : Type u_1} [inst : BEq α] (xs ys : Array α), (xs.toList == ys.toList) = (xs == ys)
-- Mathlib.Data.Seq.Computation
Computation.pure_def : ∀ {α : Type u} (a : α), pure a = Computation.pure a
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ι_colimMap_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (α : G ⟶ F) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap α) h) =
    CategoryTheory.CategoryStruct.comp (α.app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h)
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instInhabitedComponent : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] → (j : CategoryTheory.ConnectedComponents J) → Inhabited j.Component
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] {f g : α →+*o β}, f = g ↔ ∀ (a : α), f a = g a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.WF) {l : List α} {k : α}
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)) k h' = ()
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.mul_const_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (x * a⁻¹)) (c * a)
-- Aesop.Stats.File
Aesop.StatsFileRecord.declaration : Aesop.StatsFileRecord → Option Lean.Name
-- Mathlib.Analysis.Normed.Group.Basic
dist_mulIndicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedGroup E] (s t : Set α) (f : α → E) (x : α),
  dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_id : ∀ {Z : AlgebraicGeometry.Scheme} (I : Z.IdealSheafData), I.map (CategoryTheory.CategoryStruct.id Z) = I
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated], F.PreservesZeroMorphisms
-- Mathlib.RingTheory.HopfAlgebra.Convolution
AlgHom.counitAlgHom_comp_antipodeAlgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : HopfAlgebra R A],
  (Bialgebra.counitAlgHom R A).comp (HopfAlgebra.antipodeAlgHom R A) = Bialgebra.counitAlgHom R A
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M),
  CategoryTheory.CategoryStruct.comp f (g₁ + g₂) =
    CategoryTheory.CategoryStruct.comp f g₁ + CategoryTheory.CategoryStruct.comp f g₂
-- Mathlib.Analysis.Convex.Quasiconvex
MonotoneOn.quasiconvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → QuasiconvexOn 𝕜 s f
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_sub : ∀ {a b : ℤ} {hab₁ : Int32.minValue.toInt ≤ a - b} {hab₂ : a - b ≤ Int32.maxValue.toInt},
  Int32.ofIntLE (a - b) hab₁ hab₂ = Int32.ofInt a - Int32.ofInt b
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- **Hermite Theorem**. Let `N` be an integer. There are only finitely many number fields
(in some fixed extension of `ℚ`) of discriminant bounded by `N`.  -/
NumberField.finite_of_discr_bdd : ∀ (A : Type u_2) [inst : Field A] [inst_1 : CharZero A] (N : ℕ), {K | |NumberField.discr ↥↑K| ≤ ↑N}.Finite
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.cons.inj : ∀ {a a_1 a_2 a_3 : Turing.ToPartrec.Code}, a.cons a_1 = a_2.cons a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P Q : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  Q.IsInvertedBy F → P ≤ Q → P.IsInvertedBy F
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.forwardRuleMatches : Aesop.NormM.State → Aesop.ForwardRuleMatches
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'}
  (e₀ : X ≅ X') (e₁ : Y ≅ Y')
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
      CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
      CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι._auto_3)
  (c : CategoryTheory.Limits.Fork f g),
  ((CategoryTheory.Limits.Fork.equivOfIsos e₀ e₁ comm₁ comm₂).functor.obj c).ι =
    CategoryTheory.CategoryStruct.comp c.ι e₀.hom
-- Mathlib.Topology.Order.NhdsSet
Iio_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b ≤ c → Set.Iio c ∈ nhdsSet (Set.Ico a b)
-- Mathlib.Data.Set.Lattice
Set.subset_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
  s i j ⊆ ⋃ i', ⋃ j', s i' j'
-- Init.Data.Nat.Lemmas
Nat.sub_min_sub_left : ∀ (a b c : ℕ), min (a - b) (a - c) = a - max b c
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_map_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : β → ENNReal) (g : α → β), ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.indicator : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.Integrable f μ → MeasurableSet s → MeasureTheory.Integrable (s.indicator f) μ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_apply_le_norm_cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄,
  x ∈ quasispectrum 𝕜 a →
    autoParam (ContinuousOn f (quasispectrum 𝕜 a)) norm_apply_le_norm_cfcₙ._auto_1 →
      autoParam (f 0 = 0) norm_apply_le_norm_cfcₙ._auto_3 →
        autoParam (p a) norm_apply_le_norm_cfcₙ._auto_5 → ‖f x‖ ≤ ‖cfcₙ f a‖
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.toString : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → it.s = String.ofList (l.reverseAux r)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addEntry : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → β → Lean.Environment
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restriction_d_eq_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] {i j : ι} {i' j' : ι'} (hi : e.f i = i')
  (hj : e.f j = j') {Z : C} (h : (K.restriction e).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j) h =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (K.d i' j')
        (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj).inv h))
-- Mathlib.Data.List.Perm.Lattice
List.Perm.bagInter_symm : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), (l₁.bagInter l₂).Perm (l₂.bagInter l₁)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuationDef.eq_1 : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (r : RatFunc F),
  RatFunc.inftyValuationDef F r = if r = 0 then 0 else WithZero.exp r.intDegree
-- Mathlib.Data.Set.Image
Set.image_union : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s ∪ t) = f '' s ∪ f '' t
-- Mathlib.Algebra.Divisibility.Units
dvd_pow_self_iff : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α} {n : ℕ}, x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonGetWidgetSourceParams.toJson : Lean.Widget.GetWidgetSourceParams → Lean.Json
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_const : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10}
  [inst_2 : IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (x : N),
  Convexity.StdSimplex.map (fun x_1 => x) f = Convexity.StdSimplex.single x
-- Mathlib.Order.Category.BddLat
BddLat.isBoundedOrder : (self : BddLat) → BoundedOrder ↑self.toLat
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.liftEquivRight_apply : ∀ (R : Type uR) (S : Type uS) (B : Type uB) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (C : Type u_3) [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra S C] [inst_8 : IsScalarTower R S C] (f : B →ₐ[R] C),
  (Algebra.TensorProduct.liftEquivRight R S B C) f = Algebra.TensorProduct.lift (Algebra.ofId S C) f ⋯
-- Mathlib.Logic.Basic
not_beq_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, a ≠ b → ¬(a == b) = true
-- Std.Http.Data.URI.Basic
/-- Attempts to set the URI scheme (e.g., "http", "https").
Returns `none` if the scheme is not a valid RFC 3986 scheme.
The stored scheme is normalized to lowercase.
 -/
Std.Http.URI.Builder.setScheme? : Std.Http.URI.Builder → String → Option Std.Http.URI.Builder
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_one_iff_exists : ∀ {α : Type u_1}, Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_map_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₃ = f.f (c.next i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l → Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.insertMany t l) k' = v
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.isEquiv_iff_valuationSubring : ∀ {K : Type u} [inst : Field K] {Γ₁ : Type u_2} {Γ₂ : Type u_3} [inst_1 : LinearOrderedCommGroupWithZero Γ₁]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₂] (v₁ : Valuation K Γ₁) (v₂ : Valuation K Γ₂),
  v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_at : ∀ {n : ℕ} (i : Fin (n + 1)), (finSuccEquiv' i) i = none
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.countable : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f.IsCycleOn s → s.Countable
-- Mathlib.FieldTheory.Perfect
/-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
a map from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
It's given by `x ↦ x ^ p`, see `rootsExpandToRoots_apply`.  -/
Polynomial.rootsExpandToRoots : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      (p : ℕ) →
        [ExpChar R p] →
          (f : Polynomial R) →
            [inst_3 : DecidableEq R] → ↥((Polynomial.expand R p) f).roots.toFinset ↪ ↥f.roots.toFinset
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Definition: the positive part of the logarithm.  -/
Real.posLog : ℝ → ℝ
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.coe_symm_toEquiv : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), ⇑h.symm = ⇑h.symm
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_nnnorm_add_nnnorm_sub : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₁_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.isSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsPositive → IsSelfAdjoint T
-- Lean.Util.ShareCommon
Lean.ShareCommon.shareCommon : {α : Type u_1} → α → α
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.coe_nnreal_ennreal : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {f : α → NNReal} {g : β → NNReal},
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib (fun x => ↑(f x)) (fun x => ↑(g x)) μ ν
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.leadCoeff.eq_2 : ∀ (p : Int.Internal.Linear.Poly),
  (∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
      p = Int.Internal.Linear.Poly.add a v p_1 → False) →
    p.leadCoeff = 1
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.norm_integral_le_of_norm_le_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
  0 ≤ R → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * R * C
-- Mathlib.Algebra.Lie.Semisimple.Lemmas
LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful : ∀ (k : Type u_1) (L : Type u_2) (M : Type u_3) [inst : Field k] [CharZero k] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra k L] [Module.Finite k L] [inst_5 : AddCommGroup M] [inst_6 : Module k M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule k L M] [Module.Finite k M] [LieModule.IsIrreducible k L M]
  [LieModule.IsFaithful k L M] [LieModule.IsTriangularizable k L M],
  LieAlgebra.HasCentralRadical k L ∧ ∀ (x : L), x ∈ LieAlgebra.center k L ↔ (LieModule.toEnd k L M) x ∈ k ∙ LinearMap.id
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans X Y)
  (θ : CategoryTheory.Oplax.StrongTrans Y Z) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).symm ≪≫
      CategoryTheory.Bicategory.whiskerRightIso (η.naturality f) (θ.app b) ≪≫
        CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b) ≪≫
          CategoryTheory.Bicategory.whiskerLeftIso (η.app a) (θ.naturality f) ≪≫
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).symm
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.symm_monoidHomCongrLeft : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂]
  [inst_2 : CommMonoid N] (e : M₁ ≃* M₂), e.monoidHomCongrLeft.symm = e.symm.monoidHomCongrLeft
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.continuous_C : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R], Continuous ⇑PowerSeries.C
-- Mathlib.Order.Monotone.Monovary
StrictAnti.trans_monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : PartialOrder ι], StrictAnti f → Monovary g f → Antitone g
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Combine a family of continuous linear equivalences into a continuous linear equivalence of
pi-types.  -/
ContinuousLinearEquiv.piCongrRight : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {ι : Type u_9} →
      {M : ι → Type u_10} →
        [inst_1 : (i : ι) → TopologicalSpace (M i)] →
          [inst_2 : (i : ι) → AddCommMonoid (M i)] →
            [inst_3 : (i : ι) → Module R₁ (M i)] →
              {N : ι → Type u_11} →
                [inst_4 : (i : ι) → TopologicalSpace (N i)] →
                  [inst_5 : (i : ι) → AddCommMonoid (N i)] →
                    [inst_6 : (i : ι) → Module R₁ (N i)] →
                      ((i : ι) → M i ≃L[R₁] N i) → ((i : ι) → M i) ≃L[R₁] (i : ι) → N i
-- Mathlib.Topology.Compactness.Paracompact
/-- A topological space is called paracompact, if every open covering of this space admits a locally
finite refinement. We use the same universe for all types in the definition to avoid creating a
class like `ParacompactSpace.{u v}`. Due to lemma `precise_refinement` below, every open covering
`s : α → Set X` indexed on `α : Type v` has a *precise* locally finite refinement, i.e., a locally
finite refinement `t : α → Set X` indexed on the same type such that each `∀ i, t i ⊆ s i`.  -/
ParacompactSpace : (X : Type v) → [TopologicalSpace X] → Prop
-- Mathlib.Data.Finsupp.Lex
Finsupp.lex_lt_of_lt_of_preorder : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : Preorder N] (r : α → α → Prop) [IsStrictOrder α r]
  {x y : α →₀ N}, x < y → ∃ i, (∀ (j : α), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (t_hd : α) (t_tl : Stream'.Seq α)
  (h_1 : Unit → motive none) (h_2 : (t_hd : α) → (t_tl : Stream'.Seq α) → motive (some (t_hd, t_tl))),
  (match some (t_hd, t_tl) with
    | none => h_1 ()
    | some (t_hd, t_tl) => h_2 t_hd t_tl) =
    h_2 t_hd t_tl
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExtractCoeff.mk.sizeOf_spec : ∀ {e : Q(ℕ)} (k e' : Q(ℕ)) (ve' : Mathlib.Tactic.Ring.Common.ExProdNat e') (p : Q(«$e» = «$e'» * «$k»)),
  sizeOf { k := k, e' := e', ve' := ve', p := p } = 1 + sizeOf k + sizeOf e' + sizeOf ve' + sizeOf p
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The equiv version of `Fin.predAbove_zero`.  -/
finSuccEquiv'_zero : ∀ {n : ℕ}, finSuccEquiv' 0 = finSuccEquiv n
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.mk.sizeOf_spec : ∀ (levelNames : List Lean.Name) (syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl)
  (pendingMVars : List Lean.MVarId) (mvarErrorInfos : List Lean.Elab.Term.MVarErrorInfo)
  (levelMVarErrorInfos : List Lean.Elab.Term.LevelMVarErrorInfo) (mvarArgNames : Lean.MVarIdMap Lean.Name)
  (letRecsToLift : List Lean.Elab.Term.LetRecToLift),
  sizeOf
      { levelNames := levelNames, syntheticMVars := syntheticMVars, pendingMVars := pendingMVars,
        mvarErrorInfos := mvarErrorInfos, levelMVarErrorInfos := levelMVarErrorInfos, mvarArgNames := mvarArgNames,
        letRecsToLift := letRecsToLift } =
    1 + sizeOf levelNames + sizeOf syntheticMVars + sizeOf pendingMVars + sizeOf mvarErrorInfos +
          sizeOf levelMVarErrorInfos +
        sizeOf mvarArgNames +
      sizeOf letRecsToLift
-- Std.Time.DateTime.Timestamp
/-- Converts a `Timestamp` to a `Day.Offset`.
 -/
Std.Time.Timestamp.toDaysSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Day.Offset
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- `prehaar K₀ U K` is a weighted version of the index, defined as `(K : U)/(K₀ : U)`.
In the applications `K₀` is compact with non-empty interior, `U` is open containing `1`,
and `K` is any compact set.
The argument `K` is a (bundled) compact set, so that we can consider `prehaar K₀ U` as an
element of `haarProduct` (below).  -/
MeasureTheory.Measure.haar.prehaar : {G : Type u_1} → [Group G] → [inst : TopologicalSpace G] → Set G → Set G → TopologicalSpace.Compacts G → ℝ