mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.SubMulAction
VAddMemClass.ofVAddAssocClass : ∀ (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [inst : SetLike S α] [inst_1 : VAdd M N]
  [inst_2 : VAdd M α] [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α],
  VAddMemClass S M α
-- Mathlib.Algebra.Order.Group.PosPart
posPart_eq_of_posPart_pos : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α}, 0 < a⁺ → a⁺ = a
-- Mathlib.Data.Real.Basic
Real.decidableEq : (a b : ℝ) → Decidable (a = b)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_exp_neg_mul_sq_iff : ∀ {b : ℝ}, MeasureTheory.Integrable (fun x => Real.exp (-b * x ^ 2)) MeasureTheory.volume ↔ 0 < b
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x ↔ ∀ (p : MvPolynomial ι R), (MvPolynomial.aeval x) p = 0 → p = 0
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_map_iff' : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [hl : l.NeBot] {f : β → α},
  Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `insert` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.insertₘ : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → (k : α) → β k → (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_eq_adjoin_X : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (s : Set σ),
  MvPolynomial.supported R s = Algebra.adjoin R (MvPolynomial.X '' s)
-- Init.Data.List.Count
List.countP.eq_1 : ∀ {α : Type u} (p : α → Bool) (l : List α), List.countP p l = List.countP.go p l 0
-- Lean.Elab.AssertExists
Lean.Elab.Command.AssertExists.mk : Bool → Lean.Name → Lean.Name → Lean.Elab.Command.AssertExists
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
/-- The sequence with `n`-th term `harmonic n - log (n + 1)`.  -/
Real.eulerMascheroniSeq : ℕ → ℝ
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_of_notMem : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {a : α}, a ∉ s → ∀ (f : α → M), s.mulIndicator f a = 1
-- Mathlib.Order.Filter.Map
Filter.comap_coe_neBot_of_le_principal : ∀ {γ : Type u_3} {s : Set γ} {l : Filter γ} [h : l.NeBot], l ≤ Filter.principal s → (Filter.comap Subtype.val l).NeBot
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
/-- If a primitive `f` satisfies `f.IsEisensteinAt 𝓟`, where `𝓟.IsPrime`,
then `f` is irreducible.  -/
Polynomial.IsEisensteinAt.irreducible : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {𝓟 : Ideal R} {f : Polynomial R},
  f.IsEisensteinAt 𝓟 → 𝓟.IsPrime → f.IsPrimitive → 0 < f.natDegree → Irreducible f
-- Mathlib.FieldTheory.SeparableClosure
/-- The separable degree multiplied by the inseparable degree is equal
to the (infinite) field extension degree.  -/
Field.sepDegree_mul_insepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.sepDegree F E * Field.insepDegree F E = Module.rank F E
-- Mathlib.Algebra.Homology.SpectralObject.Homology
/-- The exact sequence expressing `E^n(f₁, f₂, f₃ ≫ f₄)` as the cokernel
of the differential `E^{n-1}(f₃, f₄, f₅) ⟶ E^n(f₁, f₂, f₃)`  -/
CategoryTheory.Abelian.SpectralObject.dCokernelSequence : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ i₄ i₅ : ι} →
              (i₀ ⟶ i₁) →
                (i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₄ : i₃ ⟶ i₄) →
                      (i₄ ⟶ i₅) →
                        (f₃₄ : i₂ ⟶ i₄) →
                          CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄ →
                            (n₀ n₁ n₂ n₃ : ℤ) →
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1 →
                                autoParam (n₁ + 1 = n₂)
                                    CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3 →
                                  autoParam (n₂ + 1 = n₃)
                                      CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5 →
                                    CategoryTheory.ShortComplex C
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_dirac : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {x : E} (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (MeasureTheory.Measure.dirac x) L = Complex.exp (↑(L x) * Complex.I)
-- Mathlib.Analysis.Convex.Between
wbtw_iff_sameRay_vsub : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y)
-- Mathlib.Order.RelSeries
/-- For any type `α`, each term of `α` gives a relation series with the right most index to be 0.
 -/
RelSeries.singleton : {α : Type u_1} → (r : SetRel α α) → α → RelSeries r
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.eval_indicator_apply_eq_zero : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Fintype σ] [inst_2 : Field K] (a b : σ → K),
  a ≠ b → (MvPolynomial.eval a) (MvPolynomial.indicator b) = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom_injective`. -/
SchwartzMap.coeHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], Function.Injective ⇑(FunLike.coeAddMonoidHom F α β)
-- Mathlib.Topology.Algebra.GroupWithZero
Continuous.div₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α],
  Continuous f → Continuous g → (∀ (x : α), g x ≠ 0) → Continuous fun x => f x / g x
-- Lean.MonadEnv
Lean.isRecCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.pos' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < r
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ), Polynomial.homogenize 0 n = 0
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.toMatrix_row_sum_one : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [inst_4 : Fintype ι] (q : ι' → P)
  (i : ι'), ∑ j, b.toMatrix q i j = 1
-- Mathlib.Order.GameAdd
/-- If `a` is accessible under `rα` and `b` is accessible under `rβ`, then `(a, b)` is
accessible under `Prod.GameAdd rα rβ`. Notice that `Prod.lexAccessible` requires the
stronger condition `∀ b, Acc rβ b`.  -/
Acc.prod_gameAdd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b : β},
  Acc rα a → Acc rβ b → Acc (Prod.GameAdd rα rβ) (a, b)
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.coe_commutant : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : VonNeumannAlgebra H), ↑S.commutant = (↑S).centralizer
-- Mathlib.LinearAlgebra.Pi
/-- `pi` construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules.  -/
LinearMap.pi : {R : Type u} →
  {M₂ : Type w} →
    {ι : Type x} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : Module R M₂] →
            {φ : ι → Type i} →
              [inst_3 : (i : ι) → AddCommMonoid (φ i)] →
                [inst_4 : (i : ι) → Module R (φ i)] → ((i : ι) → M₂ →ₗ[R] φ i) → M₂ →ₗ[R] (i : ι) → φ i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` this sends `A : Rep k H` to the `n`th
"corestriction" map `Hₙ(G, Res(f)(A)) ⟶ Hₙ(H, A)` induced by `f` and the identity
map on `Res(f)(A)`.  -/
groupHomology.coresNatTrans : (k : Type u) →
  {G H : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (f : G →* H) → (n : ℕ) → (Rep.resFunctor f).comp (groupHomology.functor k G n) ⟶ groupHomology.functor k H n
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.surjective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  Function.Surjective ⇑e
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.filter.eq_1 : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s), h.filter = h.filterBasis.filter
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.dual : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ t o₂ → Ordnode.Valid' o₂ t.dual o₁
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The range of a linear map defined on a finite-dimensional space is also finite-dimensional.  -/
LinearMap.finiteDimensional_range : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂),
  FiniteDimensional K ↥f.range
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.ringInverse_nonneg_iff_nonneg_of_isUnit : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  {a : A}, IsUnit a → (0 ≤ Ring.inverse a ↔ 0 ≤ a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.alter m k f) k' =
      if (k == k') = true then f (Std.DHashMap.Raw.Const.get? m k) else Std.DHashMap.Raw.Const.get? m k'
-- Mathlib.Data.List.Perm.Subperm
List.subperm_singleton_iff : ∀ {α : Type u_1} {l : List α} {a : α}, l.Subperm [a] ↔ l = [] ∨ l = [a]
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The standard projective resolution of `k` as a trivial `k`-linear `G`-representation.  -/
Rep.standardResolution : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.ProjectiveResolution (Rep.trivial k G k)
-- Mathlib.Algebra.Group.Basic
eq_div_of_mul_eq'' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, c * a = b → a = b / c
-- Lean.Meta.Check
/-- Adds note about definitions not unfolded because of the module system, if any.  -/
Lean.Meta.mkUnfoldAxiomsNote : Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Linearly constructing a semilinear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`.  -/
TensorProduct.uncurry : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (M : Type u_7) →
            (N : Type u_8) →
              (P₂ : Type u_17) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority : Type
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- A functor between two categories `C` and `D` can be lifted to a pseudofunctor between the
corresponding locally discrete bicategories.
 -/
CategoryTheory.Functor.toPseudofunctor : {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] →
        CategoryTheory.Functor C D →
          CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete C) (CategoryTheory.LocallyDiscrete D)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.eq_neg_self_iff : ∀ {θ : Real.Angle}, θ = -θ ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.support_add_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x y : HahnSeries Γ R),
  (x + y).support ⊆ x.support ∪ y.support
-- Mathlib.RingTheory.IsPrimary
Submodule.isPrimary_finsetInf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {s : Finset ι} {f : ι → Submodule R M} {i : ι},
  i ∈ s →
    (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
      (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
-- Lean.Declaration
Lean.QuotVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {kind : Lean.QuotKind} {toConstantVal_1 : Lean.ConstantVal}
  {kind_1 : Lean.QuotKind},
  { toConstantVal := toConstantVal, kind := kind } = { toConstantVal := toConstantVal_1, kind := kind_1 } →
    toConstantVal = toConstantVal_1 ∧ kind = kind_1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
/-- Conjugation by the square root of an element, i.e. `sqrt c * a * sqrt c`.  -/
CFC.conjSqrt : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : Ring A] →
      [inst_2 : StarRing A] →
        [inst_3 : TopologicalSpace A] →
          [StarOrderedRing A] →
            [inst_5 : Algebra ℝ A] →
              [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] →
                [NonnegSpectrumClass ℝ A] → [SeparatelyContinuousMul A] → A → A →L[ℝ] A
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The limit of `J : SingleObj M ⥤ Type u` is equivalent to the fixed points of the
induced action on `J.obj (SingleObj.star M)`.  -/
CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints : {M : Type v} →
  [inst : Monoid M] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) →
      CategoryTheory.Limits.limit J ≃ ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))
-- Std.Async.System
/-- The time spent on the CPU.
 -/
Std.Async.System.CPUInfo.times : Std.Async.System.CPUInfo → Std.Async.System.CPUTimes
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofHom_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] (f : X →ₐc[R] Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CommBialgCat.ofHom f)) x = f x
-- Mathlib.Analysis.Analytic.Uniqueness
/-- If an analytic function vanishes around a point, then it is uniformly zero along
a connected set. Superseded by `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero` which
does not assume completeness of the target space.  -/
AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  {f : E → F} {U : Set E},
  AnalyticOnNhd 𝕜 f U → IsPreconnected U → ∀ {z₀ : E}, z₀ ∈ U → f =ᶠ[nhds z₀] 0 → Set.EqOn f 0 U
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.Set.tprod.match_1.eq_2 : ∀ {ι : Type u_1} {α : ι → Type u_2} (motive : List ι → ((i : ι) → Set (α i)) → Sort u_3) (i : ι) (is : List ι)
  (t : (i : ι) → Set (α i)) (h_1 : (x : (i : ι) → Set (α i)) → motive [] x)
  (h_2 : (i : ι) → (is : List ι) → (t : (i : ι) → Set (α i)) → motive (i :: is) t),
  (match i :: is, t with
    | [], x => h_1 x
    | i :: is, t => h_2 i is t) =
    h_2 i is t
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `φ`-equivariant functions `X → Y`,
where `φ : M → N`, where `M` and `N` act additively on `X` and `Y` respectively

We use the same notation as for multiplicative actions, as conflicts are unlikely.  -/
«AddActionHomLocal≺» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) ⁻¹' Set.Iic b = Set.Iic (b + a)
-- Init.Data.ToString.Basic
instToStringNat : ToString ℕ
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_pos : ∀ {o : Ordinal.{u_3}}, 0 < o → ∀ (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}), 0 < o.blsub f
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- A functor which commutes with the shift by `ℤ` is triangulated if
it sends distinguished triangles to distinguished triangles.  -/
CategoryTheory.Functor.IsTriangulated : {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) →
              [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] →
                            [CategoryTheory.Pretriangulated C] → [CategoryTheory.Pretriangulated D] → Prop
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.add_measure : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ ν : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → AEMeasurable f ν → AEMeasurable f (μ + ν)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι) = ↑I.support ∩ ↑↑U
-- Lean.Data.Lsp.Basic
/-- Options for `DeleteFile`.  -/
Lean.Lsp.DeleteFile.Options : Type
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.natDegree_basis : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → (Lagrange.basis s v i).natDegree = s.card - 1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_inverse_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.mapIso i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp i.hom X.hom
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqDSimpArgs : BEq Lean.Elab.Tactic.Grind.DSimpArgs
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.foldM_filterMapWithPostcondition.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (x : Option γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (∀ (c : γ), x = some c → False) →
    (match x with
      | some c => h_1 c
      | x => h_2 x) =
      h_2 x
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_one_left : ∀ {R : Type u_1} [inst : Semiring R] (p : PowerSeries R),
  (PowerSeries.trunc 1) p = Polynomial.C ((PowerSeries.coeff 0) p)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.op : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → α} {a : α}, HasSum f a L → HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a) L
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.Limits.pullback.snd
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
              (𝒰.f k))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f k))
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup : {α : Type u_3} → [self : ConditionallyCompletePartialOrder α] → ConditionallyCompletePartialOrderSup α
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A finite product of semisimple rings is semisimple.  -/
instIsSemisimpleRingForallOfFinite : ∀ {ι : Type u_7} [Finite ι] (R : ι → Type u_6) [inst : (i : ι) → Ring (R i)] [∀ (i : ι), IsSemisimpleRing (R i)],
  IsSemisimpleRing ((i : ι) → R i)
-- Mathlib.CategoryTheory.Square
/-- the top-right object  -/
CategoryTheory.Square.X₂ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → C
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
      (S₂.mapRightHomologyIso F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv
      (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFinset_apply_of_notMem : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {a : α}, a ∉ s → (PMF.uniformOfFinset s hs) a = 0