mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Adding the sums of a function over `s` and over `sᶜ` gives the whole sum.
For a version expressed with subtypes, see `Fintype.sum_subtype_add_sum_subtype`.  -/
Finset.sum_add_sum_compl : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), ∑ i ∈ s, f i + ∑ i ∈ sᶜ, f i = ∑ i, f i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.mem_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  (↑m).WF → ∀ {k : α}, k ∈ (↑m).keysArray ↔ m.contains k = true
-- Mathlib.Algebra.DirectSum.Module
/-- If a direct sum of submodules is internal then the submodules are independent.  -/
DirectSum.IsInternal.submodule_iSupIndep : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M}, DirectSum.IsInternal A → iSupIndep A
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.IsCondKernel.disintegrate : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α (β × Ω)} {κCond : ProbabilityTheory.Kernel (α × β) Ω}
  [self : κ.IsCondKernel κCond], κ.fst.compProd κCond = κ
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.desc_mk : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {n : ℕ} {N : ModuleCat R} (φ : M.AlternatingMap N n)
  (x : Fin n → ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.exteriorPower.desc φ)) (ModuleCat.exteriorPower.mk x) = φ x
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
ContinuousLinearMap.norm_iteratedFDeriv_comp_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (L : F →L[𝕜] G) {f : E → F} {x : E} {N : WithTop ℕ∞}
  {n : ℕ}, ContDiffAt 𝕜 N f x → ↑n ≤ N → ‖iteratedFDeriv 𝕜 n (⇑L ∘ f) x‖ ≤ ‖L‖ * ‖iteratedFDeriv 𝕜 n f x‖
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_succ_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) {n : ℕ},
  S.lowerCentralSeries n ≤ AddSubgroup.center G → S.lowerCentralSeries (n + 1) = ⊥
-- Mathlib.Order.WellQuasiOrder
/-- A linear WQO is the same thing as a well-order.  -/
wellQuasiOrderedLE_iff_wellFoundedLT : ∀ {α : Type u_1} [inst : LinearOrder α], WellQuasiOrderedLE α ↔ WellFoundedLT α
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_one : ∀ {α : Type u} [inst : Semiring α], Ideal.span 1 = ⊤
-- Lean.Parser.Basic
/-- Apply `f` to the syntax object produced by `p`  -/
Lean.Parser.withResultOfFn : Lean.Parser.ParserFn → (Lean.Syntax → Lean.Syntax) → Lean.Parser.ParserFn
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_inverse_obj : ∀ (R : Type u) [inst : CommRing R] (A : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commHopfAlgCatEquivCogrpCommAlgCat R).inverse.obj A =
    { X := ↑(Opposite.unop (Opposite.unop A).X), commRing := CommAlgCat.instCommRingObjForgetAlgHomCarrier,
      hopfAlgebra := instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite (Opposite.unop A).X }
-- Init.Data.BitVec.Bootstrap
BitVec.setWidth'.eq_1 : ∀ {n w : ℕ} (le : n ≤ w) (x : BitVec n), BitVec.setWidth' le x = x.toNat#'⋯
-- Lean.Environment
Lean.Kernel.Exception.alreadyDeclared.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name),
  sizeOf (Lean.Kernel.Exception.alreadyDeclared env name) = 1 + sizeOf env + sizeOf name
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_injective : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G), Function.Injective (SkewMonoidAlgebra.single a)
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getMajorPosIfAuxRecursor? : Lean.Name → Option ℕ → Lean.MetaM (Option ℕ)
-- Mathlib.Data.List.Nodup
List.Nodup.injective_get : ∀ {α : Type u} {l : List α}, l.Nodup → Function.Injective l.get
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- Given a cocone `cR` for a functor `R : Cᵒᵖ ⥤ RingCat`, this is the
functor `ModuleCat cR.pt ⥤ PresheafOfModules R` which sends a module `M`
over `cR.pt` to a presheaf of modules whose underlying presheaf of
abelian groups is the constant functor `Cᵒᵖ ⥤ AddCommGrpCat` with value `M`.  -/
PresheafOfModules.constFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (cR : CategoryTheory.Limits.Cocone R) → CategoryTheory.Functor (ModuleCat ↑cR.pt) (PresheafOfModules R)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
coe_basisOfOrthonormalOfCardEqFinrank : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v)
  (card_eq : Fintype.card ι = Module.finrank 𝕜 E), ⇑(basisOfOrthonormalOfCardEqFinrank hv card_eq) = v
-- Mathlib.Data.Set.Card.Arithmetic
finsum_one : ∀ {α : Type u_1} {s : Set α}, ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
-- Mathlib.GroupTheory.Sylow
/-- If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product
of these Sylow subgroups.
 -/
Sylow.directProductOfNormal : {G : Type u} →
  [inst : Group G] →
    [Finite G] →
      (∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal) →
        ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥P) ≃* G
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) {X Y : CategoryTheory.MorphismProperty.Comma L₁ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).functor.map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.LinearAlgebra.LinearPMap
_private.Mathlib.LinearAlgebra.LinearPMap.0.LinearPMap.sSup_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (c : Set (E →ₛₗ.[σ] F)),
  DirectedOn (fun x1 x2 => x1 ≤ x2) c → ∃ f, { domain := sSup (LinearPMap.domain '' c), toFun := f } ∈ upperBounds c
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.replaceDTopology_eq : ∀ {X : Type u_1} {d : DiffeologicalSpace X} {t : TopologicalSpace X} {h : DiffeologicalSpace.dTopology = t},
  d.replaceDTopology t h = d
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.inl_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K),
  (LieAlgebra.SemiDirectSum.inl ψ) x = { left := x, right := 0 }
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn.go : {motive_1 : Lean.Language.SnapshotTree → Sort u} →
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
    {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u} →
        {motive_5 : Task Lean.Language.SnapshotTree → Sort u} →
          (t : Lean.Language.SnapshotTree) →
            ((t : Lean.Language.SnapshotTree) → t.below → motive_1 t) →
              ((t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                  Lean.Language.SnapshotTree.below_1 t → motive_2 t) →
                ((t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                    Lean.Language.SnapshotTree.below_2 t → motive_3 t) →
                  ((t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
                      Lean.Language.SnapshotTree.below_3 t → motive_4 t) →
                    ((t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t) →
                      motive_1 t ×' t.below
-- Mathlib.Tactic.FunProp.Core
/-- Try to apply *function theorems* `thms` to `e`.  -/
Mathlib.Meta.FunProp.tryTheorems : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      Array Mathlib.Meta.FunProp.FunctionTheorem →
        (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
          Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
AddMonoidAlgebra.instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] [inst_3 : Add A]
  [UniqueSums A], IsRightCancelMulZero (AddMonoidAlgebra R A)
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u_1)}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P],
  CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F →
    ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
      [Finite 𝒰.I₀],
      CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_add : ∀ {r₁ r₂ : ENNReal}, r₁ ≠ ⊤ → r₂ ≠ ⊤ → (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal
-- Mathlib.Data.Nat.Squarefree
Nat.sq_mul_squarefree : ∀ (n : ℕ), ∃ a b, b ^ 2 * a = n ∧ Squarefree a
-- Mathlib.Algebra.Group.Defs
CancelMonoid.mk : {M : Type u} → [toLeftCancelMonoid : LeftCancelMonoid M] → [toIsRightCancelMul : IsRightCancelMul M] → CancelMonoid M
-- Init.Prelude
Lean.MonadQuotation.toMonadRef : {m : Type → Type} → [self : Lean.MonadQuotation m] → Lean.MonadRef m
-- Mathlib.NumberTheory.MulChar.Basic
MulCharClass.map_nonunit : ∀ {F : Type u_3} {R : outParam (Type u_4)} {R' : outParam (Type u_5)} {inst : CommMonoid R}
  {inst_1 : CommMonoidWithZero R'} {inst_2 : FunLike F R R'} [self : MulCharClass F R R'] (χ : F) {a : R},
  ¬IsUnit a → χ a = 0
-- Init.Data.Nat.Lemmas
Nat.pow_pred_lt_pow : ∀ {x w : ℕ}, 1 < x → 0 < w → x ^ (w - 1) < x ^ w
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (h : S.Splitting) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃],
  h.isoBinaryBiproduct.hom = CategoryTheory.Limits.biprod.lift h.r S.g
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the forward direction of `isOfFinOrder_inv_iff`.

---

Inverses of elements of finite order have finite order.  -/
IsOfFinOrder.of_inv : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x⁻¹ → IsOfFinOrder x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_lid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 𝕜 E), ‖(TensorProduct.lid 𝕜 E) x‖ = ‖x‖
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- If the `LSeries` of `f` and of `g` both converge somewhere, then they are equal if and only
if `f n = g n` whenever `n ≠ 0`.  -/
LSeries_eq_iff_of_abscissaOfAbsConv_lt_top : ∀ {f g : ℕ → ℂ},
  LSeries.abscissaOfAbsConv f < ⊤ →
    LSeries.abscissaOfAbsConv g < ⊤ → (LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n)
-- Mathlib.Computability.Partrec
Computable.ofOption : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → Option β},
  Computable f → Partrec fun a => ↑(f a)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.mappingCocone_triangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCocone.triangle φ) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.applyComputedFields : Array Lean.Elab.Command.InductiveView → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulRight.congr_simp : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (b b_1 : A), b = b_1 → LinearMap.mulRight R b = LinearMap.mulRight R b_1
-- Mathlib.Data.PNat.Factors
/-- If we start with a multiset of primes, take the product and
then factor it, we get back the original multiset.  -/
PrimeMultiset.factorMultiset_prod : ∀ (v : PrimeMultiset), v.prod.factorMultiset = v
-- Mathlib.Logic.Equiv.Defs
Equiv.symmEquiv_apply_apply : ∀ (α : Sort u_1) (β : Sort u_2) (e : α ≃ β) (a : β), ((Equiv.symmEquiv α β) e) a = e.invFun a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RccSliceData α → Std.Rcc α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp] {k : α}, t.keys.contains k = t.contains k
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Notation for `Integrable` with respect to a non-standard σ-algebra.  -/
MeasureTheory.«termIntegrable[_]» : Lean.ParserDescr
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.lt_rankD_findAux : ∀ {i : ℕ} {self : Batteries.UnionFind} {x : Fin self.size},
  Batteries.UnionFind.parentD (self.findAux x).s i ≠ i →
    self.rank i < self.rank (Batteries.UnionFind.parentD (self.findAux x).s i)
-- Mathlib.Algebra.Field.Basic
same_add_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, b ≠ 0 → (b + a) / b = 1 + a / b
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Monad.comparison R`
sending objects `Y : D` to Eilenberg-Moore algebras for `L ⋙ R` with underlying object `R.obj X`.

We later show that this is full when `R` is full, faithful when `R` is faithful,
and essentially surjective when `R` is reflective.
 -/
CategoryTheory.Monad.comparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → CategoryTheory.Functor D h.toMonad.Algebra
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (h : CategoryTheory.SplitMono f),
  h.op = { section_ := h.retraction.op, id := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The polar coordinate open partial homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and
`ℝ^r₁ × (ℝ × ℝ)^r₂` defined as the identity on the first component and mapping `(zᵢ)ᵢ` to
`(‖zᵢ‖, Arg zᵢ)ᵢ` on the second component.
 -/
NumberField.mixedEmbedding.polarCoord : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.mixedSpace K) (NumberField.mixedEmbedding.realMixedSpace K)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid (Colex α)
-- Lean.Meta.SynthInstance
/-- Helper function for caching synthesized type class instances.  -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.cacheResult : Lean.Meta.SynthInstanceCacheKey →
  Lean.Meta.PreprocessKind✝ → Option Lean.Meta.AbstractMVarsResult → Option Lean.Expr → Lean.MetaM Unit
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_eq_zero_iff_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, 0 ≤ f i) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Uncurry function `f` in `n` arguments.  -/
Mathlib.Meta.FunProp.mkUncurryFun : ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.congr_simp : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] (𝓕 𝓕_1 : MeasureTheory.Filtration ι mΩ),
  𝓕 = 𝓕_1 →
    ∀ (τ τ_1 : ℕ → Ω → WithTop ι),
      τ = τ_1 →
        ∀ (P P_1 : MeasureTheory.Measure Ω),
          P = P_1 → ProbabilityTheory.IsLocalizingSequence 𝓕 τ P = ProbabilityTheory.IsLocalizingSequence 𝓕_1 τ_1 P_1
-- Mathlib.Topology.SeparatedMap
isSeparatedMap_iff_nhds : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ nhds x₁, ∃ s₂ ∈ nhds x₂, Disjoint s₁ s₂
-- Mathlib.RingTheory.Smooth.Basic
/-- Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
with kernel `I` (typically a presentation `R[X] → S`),
`S` is formally smooth iff the `P`-linear map `I/I² → S ⊗[P] Ω[P⁄R]` is split injective.
 -/
Algebra.Extension.formallySmooth_iff_split_injection : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (P : Algebra.Extension R A)
  [Algebra.FormallySmooth R P.Ring], Algebra.FormallySmooth R A ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id
-- Init.Data.Bool
Bool.eq_or_self : ∀ {a b : Bool}, b = (a || b) ↔ a = true → b = true
-- Mathlib.Topology.Homotopy.Path
Path.toHomotopyConst_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} (p : Path x₀ x₁)
  (a : ↑unitInterval × Y), p.toHomotopyConst a = p a.1
-- Mathlib.Condensed.Light.Basic
LightCondensed.id_hom : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] (X : LightCondensed C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.Order.Hom.Basic
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `α →o ULift β` in a
higher universe.  -/
OrderHom.uliftRightMap : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → α →o ULift.{u_8, u_3} β
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.instIsTriangulatedTriangEnvelopeOfNonemptyOfIsTriangulated : ∀ {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.Nonempty] [CategoryTheory.IsTriangulated C], P.triangEnvelope.IsTriangulated
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSpace.pi.eq_1 : ∀ {δ : Type u_4} {X : δ → Type u_6} [m : (a : δ) → MeasurableSpace (X a)],
  MeasurableSpace.pi = ⨆ a, MeasurableSpace.comap (fun b => b a) (m a)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous MeasureTheory.ProbabilityMeasure.toFiniteMeasure
-- Lean.DocString.Markdown
/-- Registry for custom inline element renderers that maps element type names to renderer names.  -/
Lean.Doc.docInlineMdExt : Lean.PersistentEnvExtension (Lean.Name × Lean.Name) (Lean.Name × Lean.Name) Lean.Doc.MdRendererState
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- Every morphism space has zero  -/
CategoryTheory.Limits.HasZeroMorphisms.zero : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.Limits.HasZeroMorphisms C] → (X Y : C) → Zero (X ⟶ Y)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The morphism `h.Q ⟶ S.X₃` induced by `S.g : S.X₂ ⟶ S.X₃` and the fact that
`h.Q` is a cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.RightHomologyData.g' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h : S.RightHomologyData) → h.Q ⟶ S.X₃
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtTreeMap.minEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α × β → α × β
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.map₂_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor C D} (η : F ⟶ G) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.map₂ η).app X =
    match X with
    | CategoryTheory.WithTerminal.of x => η.app x
    | CategoryTheory.WithTerminal.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedAddMonoid` under an injective map.  -/
Function.Injective.isOrderedAddMonoid : ∀ {α : Type u} {β : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : Preorder β] (f : β → α),
  (∀ (x y : β), f (x + y) = f x + f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → IsOrderedAddMonoid β
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (X : CategoryTheory.Abelian.SpectralObject C ι)
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ)
  (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq pq') →
    ∀ (n : ℤ),
      n = data.deg pq + 1 →
        CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Mathlib.Algebra.Group.Action.Defs
/-- Type class for additive monoid actions on types, with notation `g +ᵥ p`.

The `AddAction G P` typeclass says that the additive monoid `G` acts additively on a type `P`.
More precisely this means that the action satisfies the two axioms `0 +ᵥ p = p` and
`(g₁ + g₂) +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)`. A mathematician might simply say that the additive monoid `G`
acts on `P`.

For example, if `A` is an additive group and `X` is a type, if a mathematician says
say "let `A` act on the set `X`" they will usually mean `[AddAction A X]`.


[Wikidata Q288465](https://www.wikidata.org/wiki/Q288465) -/
AddAction : (G : Type u_9) → Type u_10 → [AddMonoid G] → Type (max u_10 u_9)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.nonempty_toType_iff : ∀ {o : Ordinal.{u_1}}, Nonempty o.ToType ↔ o ≠ 0