mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [inst_5 : X₂.HasTensor X₃]
  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_8 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.injOn_iff_surjOn : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
  [FiniteDimensional K ↥p] {f : V →ₗ[K] V}, (∀ x ∈ p, f x ∈ p) → (Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p)
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRecFromOne_one : ∀ {motive : ℕ → Sort u} {zero : motive 0} {one : motive 1}
  (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (Nat.bit b n)), Nat.binaryRecFromOne zero one bit 1 = one
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)
      (Q.complex.d 1 0) =
    f.f 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_projIcc : ∀ (x : ℝ), Real.arcsin ↑(Set.projIcc (-1) 1 ⋯ x) = Real.arcsin x
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.IsModHom.smul_hom`. -/
CategoryTheory.IsMod_Hom.smul_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : D} {inst_5 : CategoryTheory.ModObj A M}
  {inst_6 : CategoryTheory.ModObj A N} {f : M ⟶ N} [self : CategoryTheory.IsModHom A f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
      CategoryTheory.ModObj.smul
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toReal_smul : ∀ {α : Type u_2} [inst : TopologicalSpace α] (r : NNReal) (f : CompactlySupportedContinuousMap α NNReal),
  (r • f).toReal = r • f.toReal
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a continuous linear map `f` from `E 0` to continuous multilinear maps on `n` variables,
construct the corresponding continuous multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (m 0) (tail m)`  -/
ContinuousLinearMap.uncurryLeft : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → (Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G) → ContinuousMultilinearMap 𝕜 Ei G
-- Mathlib.Order.Filter.Subsingleton
/-- In a nonempty type, a filter is a subsingleton iff
it is less than or equal to a pure filter.  -/
Filter.subsingleton_iff_exists_le_pure : ∀ {α : Type u_1} {l : Filter α} [Nonempty α], l.Subsingleton ↔ ∃ a, l ≤ pure a
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.sectionsGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) → Group ↑(F.comp (CategoryTheory.forget GrpCat)).sections
-- Init.Data.BitVec.Lemmas
BitVec.msb_fill : ∀ {w : ℕ} {v : Bool}, (BitVec.fill w v).msb = (v && decide (0 < w))
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal.  -/
LinearMap.ext_ring : ∀ {R : Type u_1} {S : Type u_5} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₃]
  [inst_3 : Module S M₃] {σ : R →+* S} {f g : R →ₛₗ[σ] M₃}, f 1 = g 1 → f = g
-- Mathlib.Order.SupIndep
iSup_fin_three : ∀ {α : Type u_5} [inst : CompleteLattice α] {f : Fin 3 → α}, ⨆ i, f i = f 0 ⊔ f 1 ⊔ f 2
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.closure_closure_coe_preimage : ∀ {M : Type u_5} [inst : MulOneClass M] {s : Set M}, Submonoid.closure (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.Data.PNat.Factors
PrimeMultiset.mem_ofNatMultiset : ∀ {p : ℕ+} {s : Multiset ℕ} (hs : ∀ p ∈ s, Nat.Prime p), p ∈ (PrimeMultiset.ofNatMultiset s hs).toPNatMultiset ↔ ↑p ∈ s
-- Lean.Server.FileWorker.SemanticHighlighting
/-- The best token is the nonempty token with the highest priority; given equal priorities, earlier
tokens win. Breaking ties in favor of shorter tokens means that more information has the chance to
be displayed.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.untilToken.takeBest : List Lean.Server.FileWorker.AbsoluteLspSemanticToken → Option Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Data.List.Induction
List.twoStepInduction.eq_1 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)),
  List.twoStepInduction nil singleton cons_cons [] = nil
-- Mathlib.Probability.Notation
/-- `ℙ` is a notation for `volume` on a measured space.  -/
ProbabilityTheory.termℙ : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableOn_empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F}, DifferentiableOn 𝕜 f ∅
-- Mathlib.Topology.Connected.LocallyConnected
LocallyConnectedSpace.mk : ∀ {α : Type u_3} [inst : TopologicalSpace α],
  (∀ (x : α), (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id) → LocallyConnectedSpace α
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod_comp_inr : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* P) (g : N →* P), (f.coprod g).comp (MonoidHom.inr M N) = g
-- Mathlib.Logic.Equiv.Defs
/-- If both `α` and `β` have a unique element, then `α ≃ β`.  -/
Equiv.ofUnique : (α : Sort u) → (β : Sort v) → [Unique α] → [Unique β] → α ≃ β
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.le₃₄ : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₃ ≤ x₄
-- Mathlib.Order.Fin.Basic
Fin.instLattice : {n : ℕ} → Lattice (Fin n)
-- Mathlib.Topology.Clopen
continuousOn_boolIndicator_iff_isClopen : ∀ {X : Type u} [inst : TopologicalSpace X] (s U : Set X), ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_p : ∀ {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 ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_p._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_p._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).right.p =
    CategoryTheory.CategoryStruct.comp
      (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
      (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.add_mem : ∀ {M : Type u_1} [inst : Add M] (I : AddSemigroupIdeal M) (x : M) {y : M}, y ∈ I → x + y ∈ I
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_bot : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  [RingHomClass F R S], Ideal.map f ⊥ = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.objEquiv_apply_snd' : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 1)), (x.cast hd).simplex.2 i = (x.cast hd).simplex.2 i
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.auxMat.congr_simp : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M M_1 : Matrix m m S),
  M = M_1 →
    ∀ {inst_1 : DecidableEq m} [inst_2 : DecidableEq m] (k k_1 : m),
      k = k_1 →
        ∀ (a a_1 : m),
          a = a_1 →
            ∀ (a_2 a_3 : m),
              a_2 = a_3 → Algebra.Norm.Transitivity.auxMat M k a a_2 = Algebra.Norm.Transitivity.auxMat M_1 k_1 a_1 a_3
-- Mathlib.Algebra.Ring.Equiv
/-- The 'unopposite' of a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`. Inverse to `RingEquiv.op`.  -/
RingEquiv.unop : {α : Type u_7} →
  {β : Type u_8} → [inst : Add α] → [inst_1 : Mul α] → [inst_2 : Add β] → [inst_3 : Mul β] → αᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β)
-- Mathlib.Data.Finset.Option
Finset.map_some_eraseNone : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)),
  Finset.map Function.Embedding.some (Finset.eraseNone s) = s.erase none
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_to : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (j : ι),
  CategoryTheory.CategoryStruct.comp (f.prev j) (C₂.dTo j) = CategoryTheory.CategoryStruct.comp (C₁.dTo j) (f.f j)
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- **Alias** of `volume_iUnion_setOfPred_liouvilleWith`.

---

The set of numbers satisfying the Liouville condition with some exponent `p > 2` has Lebesgue
measure zero.  -/
volume_iUnion_setOf_liouvilleWith : MeasureTheory.volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₂_contDiffAt : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {x : F},
  ContDiff 𝕜 n g → ContDiffAt 𝕜 n f₁ x → ContDiffAt 𝕜 n f₂ x → ContDiffAt 𝕜 n (fun x => g (f₁ x, f₂ x)) x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it
into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`.  -/
contMDiffOn_iff_of_subset_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {y : M'} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  s ⊆ (chartAt H x).source →
    Set.MapsTo f s (chartAt H' y).source →
      (ContMDiffOn I I' n f s ↔
        ContinuousOn f s ∧ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} [inst_2 : Inhabited (γ k)],
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      ((Std.Internal.List.getValueCast? k l).bind (f k)).get!
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.mk : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        (entries : Array (α × β)) →
          (indexes : Std.HashMap α (Array ℕ)) →
            (∀ (k : α) (p : k ∈ indexes),
                let idx := indexes.get k p;
                idx.size > 0 ∧ ∀ i ∈ idx, i < entries.size) →
              Std.Internal.IndexMultiMap α β
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.str.sizeOf_spec : ∀ (v : String), sizeOf (Lean.IR.LitVal.str v) = 1 + sizeOf v
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionCommMonoid : {α : Type u_1} → [DivisionCommMonoid α] → DivisionCommMonoid (Colex α)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace.mk.inj : ∀ {expandedCoeDecls expandedCoeDecls_1 : List Lean.Name},
  { expandedCoeDecls := expandedCoeDecls } = { expandedCoeDecls := expandedCoeDecls_1 } →
    expandedCoeDecls = expandedCoeDecls_1
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_isSpecial : ∀ (u : PNat.XgcdType), u.IsSpecial → u.reduce.IsSpecial
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.SubsheafClosure.below.restrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))}
  {motive : (Z : C) → (a : F.obj (Opposite.op Z)) → K.SubsheafClosure 𝒮 Z a → Prop} {Z W : C} (h : Z ⟶ W)
  {a : F.obj (Opposite.op W)} (a_1 : K.SubsheafClosure 𝒮 W a),
  CategoryTheory.Precoverage.SubsheafClosure.below a_1 →
    motive W a a_1 → CategoryTheory.Precoverage.SubsheafClosure.below ⋯
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instMulZeroClass : {α : Type u_1} → [MulZeroClass α] → MulZeroClass αᵐᵒᵖ
-- Mathlib.Data.Sum.Order
Sum.inr_le_inr_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : β}, Sum.inr a ≤ Sum.inr b ↔ a ≤ b
-- Batteries.Data.List.Basic
/-- Constructs the intersection of two lists, by filtering the elements of `l₁` that are in `l₂`.
Unlike `bagInter` this does not preserve multiplicity: `[1, 1].inter [1]` is `[1, 1]`.
 -/
List.inter : {α : Type u_1} → [BEq α] → List α → List α → List α
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_4 : ∀ (x : List ℕ) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.comp f k) x = Turing.ToPartrec.stepNormal f k x
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for any `n : ℕ` and any `x ∈ [0, |t|)`,
`|X| ^ n * exp (v * X + x * |X|)` is integrable.  -/
ProbabilityTheory.integrable_pow_abs_mul_exp_add_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v x : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
      0 ≤ x → x < |t| → ∀ (n : ℕ), MeasureTheory.Integrable (fun a => |X a| ^ n * Real.exp (v * X a + x * |X a|)) μ
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.instMonad : Monad PMF
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the second row  -/
CategoryTheory.ShortComplex.SnakeInput.L₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : AddCancelMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addCancelMonoid f hf one mul npow =
    { toAddLeftCancelMonoid := Function.Injective.addLeftCancelMonoid f hf one mul npow, toIsRightCancelAdd := ⋯ }
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a left-unbounded right-open range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Rio.HasRcoIntersection : Type w → Type w
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.EssFiniteType
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instDistribMulAction : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} →
      {A : Type u_5} →
        [inst : Monoid R] → [inst_1 : AddMonoid A] → [DistribMulAction R A] → DistribMulAction R (CStarMatrix m n A)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_combine : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.Linarith.Poly.denoteN ctx (p₁.combine p₂) =
        Lean.Grind.Linarith.Poly.denoteN ctx p₁ + Lean.Grind.Linarith.Poly.denoteN ctx p₂
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_add_mul_left_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime (x + y * z) y → IsRelPrime x y
-- Init.Data.List.MapIdx
List.mapIdx_concat : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α} {e : α},
  List.mapIdx f (l ++ [e]) = List.mapIdx f l ++ [f l.length e]
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_succ_le_ringKrullDim_powerseries : ∀ {R : Type u_1} [inst : CommRing R], ringKrullDim R + 1 ≤ ringKrullDim (PowerSeries R)
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.H.sizeOf_spec : ∀ {B : Type v} [inst : SizeOf B] (a : B), sizeOf (CartanMatrix.Generators.H a) = 1 + sizeOf a
-- Mathlib.Order.Category.PartOrd
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe' : ∀ (X : Preord) (a : ↑(preordToPartOrd.obj (Preord.dual.obj X))),
  (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a =
    (OrderIso.dualAntisymmetrization ↑X).symm a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l →
          ∀ {h : k' ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l},
            (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey k' h = k
-- Mathlib.Order.Filter.Pointwise
/-- `pure` as a `MonoidHom`.  -/
Filter.pureMonoidHom : {α : Type u_2} → [inst : MulOneClass α] → α →* Filter α
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.includeLeft_apply : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (a : A), (GradedTensorProduct.includeLeft 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_iSup : ∀ {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} (I : ι → X.IdealSheafData), (iSup I).support = ⨅ i, (I i).support
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_div_prod : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, (fun x => x.1 / x.2) '' s ×ˢ t = s / t
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ}
  (h : autoParam (m + (j + 1) = n + 1) CategoryTheory.SimplicialObject.σ₀Iter_δ._auto_1),
  autoParam (↑i ≤ j + 1) CategoryTheory.SimplicialObject.σ₀Iter_δ._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.σ₀Iter (j + 1) h) (X.δ i) = X.σ₀Iter j ⋯
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Pretopology.mem_toCoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (J : CategoryTheory.Pretopology C) {X : C} (S : CategoryTheory.Presieve X),
  S ∈ J.toCoverage.coverings X ↔ S ∈ J.coverings X
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h (CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f) = f
-- Mathlib.CategoryTheory.Square
/-- The functor `Square C ⥤ Arrow (Arrow C)` which sends a
commutative square `sq` to the obvious arrow from the top morphism of `sq`
to the bottom morphism of `sq`.  -/
CategoryTheory.Square.toArrowArrowFunctor' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Arrow (CategoryTheory.Arrow C))
-- Mathlib.Analysis.LocallyConvex.Basic
/-- A set `A` is balanced if `a • A` is contained in `A` whenever `a` has norm at most `1`.  -/
Balanced : (𝕜 : Type u_1) → {E : Type u_3} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Set E → Prop
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.token : {α : Type} → Lean.Lsp.ProgressParams α → Lean.Lsp.ProgressToken
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.mk.sizeOf_spec : ∀ (chunk : Std.Http.Chunk) (done : IO.Promise Bool),
  sizeOf { chunk := chunk, done := done } = 1 + sizeOf chunk + sizeOf done
-- Batteries.Data.Float.Lemmas
Float.toBits_inj : ∀ {f f' : Float}, f.toBits = f'.toBits ↔ f = f'
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.involute_v : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  CliffordAlgebra.involute ((CliffordAlgebra.EquivEven.v Q) m) = -(CliffordAlgebra.EquivEven.v Q) m
-- Init.Data.BitVec.Lemmas
BitVec.ult.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.ult y = decide (x.toNat < y.toNat)