mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.Compact
/-- An elimination theorem for empty intersections of a family of sets
in a compact subset which are closed in the compact subset
but not necessarily in the ambient space.  -/
IsCompact.elim_finite_subfamily_isClosed_subtype : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ {ι : Type u_3} (t : ι → Set X) {I : Set ι},
      (∀ i ∈ I, IsClosed (Subtype.val ⁻¹' t i)) → s ∩ ⋂ i ∈ I, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- The AGM distributes over multiplication.  -/
NNReal.agm_mul_distrib : ∀ {x y k : NNReal}, (k * x).agm (k * y) = k * x.agm y
-- Mathlib.Order.Zorn
/-- A variant of Zorn's lemma. If every nonempty chain of a nonempty type has an upper bound, then
there is a maximal element.
 -/
exists_maximal_of_nonempty_chains_bounded : ∀ {α : Type u_1} {r : α → α → Prop} [Nonempty α],
  (∀ (c : Set α), IsChain r c → c.Nonempty → ∃ ub, ∀ a ∈ c, r a ub) →
    (∀ {a b c : α}, r a b → r b c → r a c) → ∃ m, ∀ (a : α), r m a → r a m
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For any `Semiring A`, we collect the homogeneous ideals of `A` into a type.  -/
HomogeneousIdeal : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            (𝒜 : ι → σ) → [inst_3 : DecidableEq ι] → [inst_4 : AddMonoid ι] → [GradedRing 𝒜] → Type u_3
-- Mathlib.Data.Fintype.Vector
Sym.instFintype : {α : Type u_1} → [DecidableEq α] → [Fintype α] → {n : ℕ} → Fintype (Sym α n)
-- Init.Data.Nat.Dvd
Nat.one_dvd : ∀ (n : ℕ), 1 ∣ n
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.gt_ult : ∀ {w : ℕ} (x y : BitVec w), x > y ↔ y.ult x = true
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_mul : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A B : GL n R),
  ↑(A * B) = ↑A * ↑B
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.instHasOrthogonalProjectionTop : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊤.HasOrthogonalProjection
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.initialOfCorepresentableBy_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)} {X : C}
  (h : F.CorepresentableBy X),
  (CategoryTheory.Functor.Elements.initialOfCorepresentableBy h).snd = h.homEquiv (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Data.Set.Basic
Set.ofPred_bot : ∀ {α : Type u}, {_x | ⊥} = ∅
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.ext : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {x y : ChartedSpace H M},
  ChartedSpace.atlas = ChartedSpace.atlas → ChartedSpace.chartAt = ChartedSpace.chartAt → x = y
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C]
  [hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C],
  (∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.IsVanKampenColimit c) →
    CategoryTheory.FinitaryExtensive C
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- A type synonym for non-unital rings where an alternative monoid structure is introduced.
If `R` is a non-unital semiring, then `PreQuasiregular R` is equipped with the monoid structure
with binary operation `fun x y ↦ y + x + x * y` and identity `0`. Elements of `R` which are
invertible in this monoid satisfy the predicate `IsQuasiregular`.  -/
PreQuasiregular : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const.unop_functor_op_obj_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂),
  (Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = CategoryTheory.CategoryStruct.id (Opposite.unop X)
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.ParserAttribute.add : Lean.Name → Lean.Name → Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameForward : Lean.ParserDescr
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- Over a noetherian ring the intersection of two CoFG submodules is CoFG.  -/
Submodule.CoFG.inf : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {S T : Submodule R M}, S.CoFG → T.CoFG → (S ⊓ T).CoFG
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mk.sizeOf_spec : ∀ (toOrderHom : ℝ →o ℝ) (map_add_one' : ∀ (x : ℝ), toOrderHom.toFun (x + 1) = toOrderHom.toFun x + 1),
  sizeOf { toOrderHom := toOrderHom, map_add_one' := map_add_one' } = 1 + sizeOf toOrderHom
-- Init.Data.List.Nat.Sublist
List.prefix_map_iff_of_injective : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → β},
  Function.Injective f → (List.map f l₁ <+: List.map f l₂ ↔ l₁ <+: l₂)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_succ_right_eq_push : ∀ {m n : ℕ}, m < n → (m<...n + 1).toArray = (m<...n).toArray.push n
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_findRev?_eq_none : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.findRev? p = none → ∀ (i : Fin n), p i = false
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_iUnion : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} (s : ι → Set R),
  Subsemiring.closure (⋃ i, s i) = ⨆ i, Subsemiring.closure (s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- `|x - sin x| ≤ |x|³ / 6` for every real `x`.  -/
Real.abs_sub_sin_le : ∀ (x : ℝ), |x - Real.sin x| ≤ |x| ^ 3 / 6
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.mul : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] → [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → Mul (Monoid.PushoutI φ)
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_zero : ∀ {n : ℕ} [inst : NeZero n], Fin.castPred 0 ⋯ = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_eq_sliceTo_skipSuffixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.dropEndWhile pat = s.sliceTo (s.skipSuffixWhile pat)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.mk.sizeOf_spec : ∀ (ref declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) (isClass allowIndices allowSortPolymorphism : Bool)
  (shortDeclName declName : Lean.Name) (levelNames : List Lean.Name) (binders : Lean.Syntax)
  (type? : Option Lean.Syntax) (ctors : Array Lean.Elab.Command.CtorView)
  (computedFields : Array Lean.Elab.Command.ComputedFieldView) (derivingClasses : Array Lean.Elab.DerivingClassView)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (isCoinductive : Bool),
  sizeOf
      { ref := ref, declId := declId, modifiers := modifiers, isClass := isClass, allowIndices := allowIndices,
        allowSortPolymorphism := allowSortPolymorphism, shortDeclName := shortDeclName, declName := declName,
        levelNames := levelNames, binders := binders, type? := type?, ctors := ctors, computedFields := computedFields,
        derivingClasses := derivingClasses, docString? := docString?, isCoinductive := isCoinductive } =
    1 + sizeOf ref + sizeOf declId + sizeOf modifiers + sizeOf isClass + sizeOf allowIndices +
                          sizeOf allowSortPolymorphism +
                        sizeOf shortDeclName +
                      sizeOf declName +
                    sizeOf levelNames +
                  sizeOf binders +
                sizeOf type? +
              sizeOf ctors +
            sizeOf computedFields +
          sizeOf derivingClasses +
        sizeOf docString? +
      sizeOf isCoinductive
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddMonoid β],
  MeasureTheory.FinMeasAdditive μ 0
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.smul_left_injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → ∀ (i : ι), Function.Injective fun r => r • v i
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMinOrderElemIoo : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x y : α}, NoMinOrder ↑(Set.Ioo x y)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Whether a given 2-isomorphism is structural or not.  -/
Mathlib.Tactic.BicategoryLike.Mor₂Iso.isStructural : Mathlib.Tactic.BicategoryLike.Mor₂Iso → Bool
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast?_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getValueCast? a l =
    Std.Internal.List.Option.dmap✝ (Std.Internal.List.getEntry? a l) fun p h => cast ⋯ p.snd
-- Init.MethodSpecsSimp
OrElse.orElse_eq_hOrElse : ∀ {α : Type u_1} [inst : OrElse α], OrElse.orElse = HOrElse.hOrElse
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.pure_apply : ∀ {α : Type u_1} (a a' : α), (PMF.pure a) a' = if a' = a then 1 else 0
-- Mathlib.GroupTheory.Coxeter.Basic
/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the left
by a simple reflection, then it holds for all elements of `W`.  -/
CoxeterSystem.simple_induction_left : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : W → Prop} (w : W),
  p 1 → (∀ (w : W) (i : B), p w → p (cs.simple i * w)) → p w
-- Mathlib.RingTheory.PowerSeries.Log
/-- Power series for `log(1 + X) = X - X²/2 + X³/3 - ⋯`.  -/
PowerSeries.log : (A : Type u_1) → [inst : CommRing A] → [Algebra ℚ A] → PowerSeries A
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioc (f n) (f (Order.pred n))` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ioc_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioc (f n) (f (Order.pred n)))
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.const_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → ∀ (c : F), DiffContOnCl 𝕜 (fun x => c - f x) s
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex : Unique ↑(stdSimplex ℝ (Fin ({ len := 0 }.len + 1)))
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_3.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.inner size k v l r →
    lr = Std.DTreeMap.Internal.Impl.leaf →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_4 size k v l r lrs lrk lrv lrl lrr) ≍
        h_3 size k v l r
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If F preserves one limit cone for the diagram K,
then it preserves any limit cone for K.  -/
CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cone K} (h : CategoryTheory.Limits.IsLimit t)
  (hF : CategoryTheory.Limits.IsLimit (F.mapCone t)), CategoryTheory.Limits.PreservesLimit K F
-- Init.Data.Option.Lemmas
Option.any_true : ∀ {α : Type u_1} {o : Option α}, Option.any (fun x => true) o = o.isSome
-- Mathlib.CategoryTheory.IsoCat
/-- A functor that is an isomorphism of categories assembles into an `IsoCat`,
with `Functor.strictInv` as its inverse.  -/
CategoryTheory.Functor.asIsomorphism : {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] →
        (F : CategoryTheory.Functor C D) → [F.IsIso] → CategoryTheory.IsoCat C D
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augment_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C)
  (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀)
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f),
  (X.augment X₀ f w).left = X
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCodetector.hasCodetector : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.HasCodetector C],
  ∃ G, CategoryTheory.IsCodetector G
-- Init.Prelude
/-- An array of syntaxes of kind `ks`.
 -/
Lean.TSyntaxArray : Lean.SyntaxNodeKinds → Type
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.allExcept.injEq : ∀ («namespace» : Lean.Name) (exceptions : Array Lean.Name) (namespace_1 : Lean.Name) (exceptions_1 : Array Lean.Name),
  (Lean.Lsp.OpenNamespace.allExcept «namespace» exceptions =
      Lean.Lsp.OpenNamespace.allExcept namespace_1 exceptions_1) =
    («namespace» = namespace_1 ∧ exceptions = exceptions_1)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddCommGroup : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddCommGroup A] → AddCommGroup (CStarMatrix m n A)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The maps into the coinduced topology as homs in `TopModuleCat R`.  -/
TopModuleCat.toCoinduced : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} →
        {I : Type u_1} →
          {X : I → TopModuleCat R} → (f : (i : I) → (X i).toModuleCat ⟶ M) → (i : I) → X i ⟶ TopModuleCat.coinduced f
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.RpcProcedure.mk : (UInt64 → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)) → Lean.Server.RpcProcedure
-- Mathlib.Analysis.InnerProductSpace.Orientation
OrthonormalBasis.abs_det_adjustToOrientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι] (v : ι → E),
  |(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|
-- Mathlib.Order.Disjoint
Complementeds.mk_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], ⟨⊤, ⋯⟩ = ⊤
-- Mathlib.NumberTheory.Dioph
Poly.add_apply : ∀ {α : Type u_1} (f g : Poly α) (x : α → ℕ), (f + g) x = f x + g x
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapIdx.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → Array β → Sort u_3) →
      (x : List α) →
        (x_1 : Array β) →
          ((acc : Array β) → motive [] acc) →
            ((a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc) → motive x x_1
-- Mathlib.Topology.UniformSpace.UniformEmbedding
completeSpace_extension : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {m : β → α},
  IsUniformInducing m → DenseRange m → (∀ (f : Filter β), Cauchy f → ∃ x, Filter.map m f ≤ nhds x) → CompleteSpace α
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instContainsIdentitiesTrWOfContainsZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero], P.trW.ContainsIdentities
-- Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization
Submonoid.LocalizationMap.map_prime : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {S : Submonoid M}
  (f : S.LocalizationMap N) {m : M}, Prime m → f m ≠ 0 → ¬IsUnit (f m) → Prime (f m)
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedCPUInfo.default : Std.Internal.UV.System.CPUInfo
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.le_tfae : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p →
    IsStarProjection q → [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
-- Mathlib.CategoryTheory.Join.Basic
/-- Whiskering `mkFunctor F G α` with the universal transformation gives back `α`.  -/
CategoryTheory.Join.mkFunctor_edgeTransform : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) (CategoryTheory.Join.mkFunctor F G α) = α
-- Mathlib.Algebra.DualQuaternion
Quaternion.imI_fst_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.fst q.imI
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_ofNat : ∀ {R : Type u_1} {n : ℕ} [inst : NatCast R] [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.of_trim : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {m₀' : MeasurableSpace α} (hm₀ : m₀' ≤ m₀),
  MeasureTheory.AEStronglyMeasurable f (μ.trim hm₀) → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.isoEquivHom_symm_apply_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X Y : C) (f : X ⟶ Y),
  ((CategoryTheory.Groupoid.isoEquivHom X Y).symm f).inv = CategoryTheory.inv f
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.toHom_comp_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Embedding N P), Function.Injective h.toHom.comp
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t),
  CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (P.desc r) = Q.desc r
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCoseparator.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCoseparator G = (CategoryTheory.ObjectProperty.singleton G).IsCoseparating
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.readonly.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.readonly = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, (t.insertManyIfNewUnit l).contains k = (t.contains k || l.contains k)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_imaginaryPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A]
  (f : ℂ → ℂ) (a : A),
  autoParam (ContinuousOn f (spectrum ℂ ↑(imaginaryPart a))) cfc_imaginaryPart._auto_1 →
    autoParam (IsStarNormal a) cfc_imaginaryPart._auto_3 → cfc f ↑(imaginaryPart a) = cfc (fun x => f ↑x.im) a
-- Std.Http.Data.Version
Std.Http.Version.v30.sizeOf_spec : sizeOf Std.Http.Version.v30 = 1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_ne_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} [n.AtLeastTwo]
  {signs : Finset (Fin (n + 1))}, s.ExcenterExists signs → ∀ (i j : Fin (n + 1)), s.touchpoint signs i ≠ s.points j
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.numeratorUnit.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (s : ↥S),
  OreLocalization.numeratorUnit s = { val := ↑s /ₒ 1, inv := 1 /ₒ s, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ico_add_Icc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ico a b + Finset.Icc c d ⊆ Finset.Ico (a + c) (b + d)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.post_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} (F : CategoryTheory.Functor T D) (Y : CategoryTheory.Under X),
  (CategoryTheory.Under.post F).obj Y = CategoryTheory.Under.mk (F.map Y.hom)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_coe : ∀ {α : Type u_1}, ↑(PartialEquiv.refl α) = id
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_natCast : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] {n : ℕ},
  n ≠ 0 → ArchimedeanClass.mk ↑n = 0
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.take : ∀ {s : Substring.Raw}, s.Valid → ∀ (n : ℕ), (s.take n).Valid
-- Init.Data.Int.Lemmas
Int.negSucc_add_ofNat : ∀ (m n : ℕ), Int.negSucc m + ↑n = Int.subNatNat n m.succ