mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Types
Lean.Doc.Block.dl.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b]
  (items : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))),
  sizeOf (Lean.Doc.Block.dl items) = 1 + sizeOf items
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : PartialOrder μ]
  [CanonicallyOrderedAdd μ] [inst_4 : Finset.HasAntidiagonal μ] [inst_5 : DecidableEq μ] (s : Finset ι),
  s.piAntidiag 0 = {0}
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- When `C` has pushouts, a morphism `f : X ⟶ Y` induces a functor `Under X ⥤ Under Y`,
by pushing a morphism forward along `f`.  -/
CategoryTheory.Under.pushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Limits.HasPushoutsAlong f] →
          CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Under Y)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_eq_sum_mapIdx_aux : ∀ (b : ℕ) (l : List ℕ),
  (List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i => a * b ^ i) l (List.range l.length)).sum
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Measurable.eventuallyMeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l] {β : Type u_2}
  [inst_1 : MeasurableSpace β] {f : α → β}, Measurable f → EventuallyMeasurable m l f
-- Mathlib.Analysis.Fourier.FourierTransform
_private.Mathlib.Analysis.Fourier.FourierTransform.0.term𝕊 : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.mono : ∀ {𝕜 : 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} {x : E} {s t : Set E},
  DifferentiableWithinAt 𝕜 f t x → s ⊆ t → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.t_id : ∀ (self : TopCat.GlueData.MkCore) (i : self.J), ⇑(CategoryTheory.ConcreteCategory.hom (self.t i i)) = id
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_eq_getD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α},
  Std.ExtDHashMap.Const.get! m a = Std.ExtDHashMap.Const.getD m a default
-- Mathlib.CategoryTheory.Yoneda
/-- Version of `representableByEquiv` with more general universe assumptions.  -/
CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      (X : C) → F.RepresentableBy X ≃ (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ≅ F)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt : ∀ {M : Type u_1} [inst : MonoidWithZero M] [inst_1 : PartialOrder M] [PosMulStrictMono M] [PosMulReflectLT M]
  {e₁ e₂ f₁ f₂ L : M}, e₁ = L * f₁ → e₂ = L * f₂ → 0 < L → (e₁ < e₂) = (f₁ < f₂)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_mul_simple_cancel_right : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B),
  w * cs.simple i * cs.simple i = w
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isTransitive_iff_sUnion_subset : ∀ {x : ZFSet.{u}}, x.IsTransitive ↔ x.sUnion ⊆ x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- Write the iterated derivative as the composition of a continuous linear equiv and the iterated
Fréchet derivative  -/
iteratedDeriv_eq_equiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F},
  iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A multiple of the difference of two points added to the second point lies in their affine
span.  -/
smul_vsub_rev_vadd_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ line[k, p₁, p₂]
-- Lean.Data.Lsp.Basic
Lean.Lsp.ChangeAnnotation.mk : String → Bool → Option String → Lean.Lsp.ChangeAnnotation
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.map_nhds_of_mem : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (x : X), Set.range f ∈ nhds (f x) → Filter.map f (nhds x) = nhds (f x)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions.horn_ι : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → SSet.innerAnodyneExtensions (SSet.horn n i).ι
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_diff : ∀ {α : Type u} (s t : Set α) [Finite ↑s], Finite ↑(s \ t)
-- Mathlib.Tactic.Simps.Basic
/-- An adding rule `+fieldName`  -/
Simps.ProjectionRule.add : Lean.Name → Lean.Syntax → Simps.ProjectionRule
-- Init.Data.Int.Gcd
Int.lcm_eq_natAbs_left : ∀ {b a : ℤ}, b ∣ a → a.lcm b = a.natAbs
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.le_of_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] {x : A} {s : NonUnitalStarSubalgebra R A},
  IsClosed ↑s → x ∈ s → NonUnitalStarAlgebra.elemental R x ≤ s
-- Std.Sync.CancellationToken
Std.CancellationToken.mk.injEq : ∀ (state state_1 : Std.Mutex Std.CancellationToken.State),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Std.Time.Format.Modifier
Std.Time.Modifier.h.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.h presentation) = 1 + sizeOf presentation
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.insert_indep_iff : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcCallParams : Lean.FromJson Lean.Lsp.RpcCallParams
-- Mathlib.CategoryTheory.GuitartExact.Opposite
/-- If `w : TwoSquare T L R B`, and `g : B.op.obj X₃ ⟶ R.op.obj X₂`, this is
the obvious equivalence of categories between
`(w.op.StructuredArrowRightwards g)ᵒᵖ` and `w.CostructuredArrowDownwards g.unop`.  -/
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₃ : C₃ᵒᵖ} →
                            {X₂ : C₂ᵒᵖ} →
                              (g : B.op.obj X₃ ⟶ R.op.obj X₂) →
                                (w.op.StructuredArrowRightwards g)ᵒᵖ ≌ w.CostructuredArrowDownwards g.unop
-- Mathlib.RingTheory.Algebraic.Integral
/-- Tower law for `Module.finrank` in a tower of domains `R → S → T`. This is a variant of
`Module.finrank_mul_finrank` that assumes the rings are domains instead of the modules being
free.  -/
Module.finrank_mul_finrank' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_4)
  [inst_3 : CommRing T] [IsDomain T] [inst_5 : Algebra S T] [inst_6 : Algebra R T] [IsScalarTower R S T]
  [FaithfulSMul S T], Module.finrank R S * Module.finrank S T = Module.finrank R T
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldrM_eq_foldrM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.TreeMap.Raw.foldrM (fun a x d => f a d) init t = Array.foldrM f init t.keysArray
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToColimit.mk.inj : ∀ {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} {c : CategoryTheory.Limits.Cocone (K.comp F)} {t : CategoryTheory.Limits.IsColimit c}
  {toLiftableCocone : CategoryTheory.LiftableCocone K F c}
  {makesColimit : CategoryTheory.Limits.IsColimit toLiftableCocone.liftedCocone}
  {toLiftableCocone_1 : CategoryTheory.LiftableCocone K F c}
  {makesColimit_1 : CategoryTheory.Limits.IsColimit toLiftableCocone_1.liftedCocone},
  { toLiftableCocone := toLiftableCocone, makesColimit := makesColimit } =
      { toLiftableCocone := toLiftableCocone_1, makesColimit := makesColimit_1 } →
    toLiftableCocone = toLiftableCocone_1 ∧ makesColimit ≍ makesColimit_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeUnop.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.unop),
  CategoryTheory.Limits.coneOfCoconeUnop c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeUnop c.ι }
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.add : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B₁ B₂ : LinearMap.BilinForm R M}, B₁.IsAlt → B₂.IsAlt → (B₁ + B₂).IsAlt
-- Init.Data.Array.Attach
Array.getElem?_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} (h : ∀ a ∈ xs, p a) (i : ℕ),
  (Array.pmap f xs h)[i]? = Option.pmap f xs[i]? ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_le_iff_le_sin : ∀ {x y : ℝ}, x ∈ Set.Icc (-1) 1 → y ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → (Real.arcsin x ≤ y ↔ x ≤ Real.sin y)
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.abs_cartanMatrix_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [inst_9 : DecidableEq ι] {i j : ↥b.support},
  |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeqHom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
`coeqHom f f' : j' ⟶ coeq f f'` such that
`coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
Its existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.coeqHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {j j' : C} → (f f' : j ⟶ j') → j' ⟶ CategoryTheory.IsFiltered.coeq f f'
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The extremal numbers of `⊤` are equal to the number of edges in `turanGraph`.  -/
SimpleGraph.extremalNumber_top : ∀ {n : ℕ} {α : Type u_2} [inst : Fintype α] [Nontrivial α],
  SimpleGraph.extremalNumber n ⊤ = (SimpleGraph.turanGraph n (Fintype.card α - 1)).edgeFinset.card
-- Init.Data.SInt.Bitwise
instAssociativeInt16HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Combinatorics.Graph.Basic
/-- Given a proof that the edge `e` is incident with the vertex `x` in `G`,
noncomputably find the other end of `e`. (If `e` is a loop, this is equal to `x` itself).  -/
Graph.Inc.other : {α : Type u_1} → {β : Type u_2} → {x : α} → {e : β} → {G : Graph α β} → G.Inc e x → α
-- Init.Data.Fin.Lemmas
Fin.instIsLinearOrder : ∀ {n : ℕ}, Std.IsLinearOrder (Fin n)
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.introsClean.heqImpOfEqImp : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero.  -/
IsLocalMax.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalMax f a → deriv f a = 0
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_mulRight : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  ⇑(Homeomorph.mulRight a) = fun x => x * a
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.cartanEquivDual_apply_apply : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] (x x_1 : ↥H),
  ((LieAlgebra.IsKilling.cartanEquivDual H) x) x_1 =
    (LinearMap.trace K L) ((LieModule.toEnd K (↥H) L) x * (LieModule.toEnd K (↥H) L) x_1)
-- Mathlib.Analysis.Normed.Module.RieszLemma
/-- A version of Riesz lemma: given a proper closed subspace `F`, one may find an element of norm `1`
which is at distance at least `r` of every element of `F`, for any `r < 1`.
For a version with weaker assumptions on the underlying field, see `riesz_lemma` or
`riesz_lemma_of_norm_lt`.
 -/
riesz_lemma_of_lt_one : ∀ {𝕜 : Type u_4} [inst : RCLike 𝕜] {E : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∀ {r : ℝ}, r < 1 → ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone φ = HomologicalComplex.homotopyCofiber φ
-- Mathlib.Algebra.Order.Field.Basic
two_inv_lt_one : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α], 2⁻¹ < 1
-- Init.Data.List.Basic
List.isEqv_cons₂ : ∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : α → α → Bool},
  (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen : ∀ {R : CommRingCat} {f : ↑R},
  IsLocalization.Away f ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
-- Std.Data.DTreeMap.Raw.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.Raw.Equiv : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Prop
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivAt.tendsto_slope_zero_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : Preorder 𝕜],
  HasDerivAt f f' x → Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds f')
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.le_one : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  (f i) x ≤ 1
-- Init.Data.BitVec.Lemmas
BitVec.neg_zero : ∀ (n : ℕ), -0#n = 0#n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.map Sigma.fst t.toList = t.keys
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.ext_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {f g : A →ₜ* B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.hasFPowerSeriesAt_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    HasFPowerSeriesAt (ProbabilityTheory.mgf X μ)
      (FormalMultilinearSeries.ofScalars ℝ fun n =>
        (∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (v * X ω)) x ∂μ) / ↑n.factorial)
      v
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of the node in the string diagram, counting strings in domains.  -/
Mathlib.Tactic.Widget.StringDiagram.AtomNode.hPosSrc : Mathlib.Tactic.Widget.StringDiagram.AtomNode → ℕ
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The statement we induct on in the `C : R → R[X]` case of Chevalley's theorem with complexity
bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.Statement : (R₀ : Type u_1) →
  (R : Type u_2) →
    [inst : CommRing R₀] →
      [inst_1 : CommRing R] → [Algebra R₀ R] → (n : ℕ) → ChevalleyThm.PolynomialC.InductionObj✝ R n → Prop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
  (v = u → p ≍ SimpleGraph.Walk.nil → False) → p.drop 0 = p.copy ⋯ ⋯
-- Mathlib.Data.Set.Function
Set.BijOn.forall : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop},
  Set.BijOn f s t → ((∀ b ∈ t, p b) ↔ ∀ a ∈ s, p (f a))
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.hext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
  (α β : X.Hom Y), α.base = β.base → α.c ≍ β.c → α = β
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef.mk.injEq : ∀ {α : Type} (ref ref_1 : IO.Ref (Lean.Meta.RefinedDiscrTree α)), ({ ref := ref } = { ref := ref_1 }) = (ref = ref_1)
-- Mathlib.Algebra.CharP.IntermediateField
IntermediateField.expChar : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  (p : ℕ) [ExpChar F p], ExpChar (↥L) p
-- Init.Data.UInt.Lemmas
UInt32.not_le : ∀ {a b : UInt32}, ¬a ≤ b ↔ b < a
-- Mathlib.Analysis.Normed.Ring.Units
Ideal.closure.congr_simp : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsTopologicalRing R] (I I_1 : Ideal R),
  I = I_1 → I.closure = I_1.closure
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.ε_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.AddGrp.forget₂Mon C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddMon C))
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence : ∀ {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} {A B : C} (f : A ⟶ B)
  [F.IsEquivalence], CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The canonical truncation of a homological complex relative to an embedding
of complex shapes `e` which satisfies `e.IsTruncLE`.  -/
HomologicalComplex.truncLE : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [e.IsTruncLE] →
                    [∀ (i' : ι'), K.HasHomology i'] → [CategoryTheory.Limits.HasZeroObject C] → HomologicalComplex C c'
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.toTopEdgeLabeling_get : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableRel G.Adj] {x y : V} (H : x ≠ y),
  SimpleGraph.EdgeLabeling.get G.toTopEdgeLabeling x y H = if G.Adj x y then 1 else 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.omega_pos : 0 < Hyperreal.omega
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → Option γ},
  (Std.TreeMap.filterMap f t).toArray = Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) t.toArray
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm c) = 1 + sizeOf c
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.inductionOn₂ : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}
  {motive : Std.ExtDHashMap α β → Std.ExtDHashMap α β → Prop} (m₁ m₂ : Std.ExtDHashMap α β),
  (∀ (a b : Std.DHashMap α β), motive (Std.ExtDHashMap.mk a) (Std.ExtDHashMap.mk b)) → motive m₁ m₂
-- Mathlib.Algebra.Group.Translate
translate_add_right : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : Add α] (a : G) (f g : G → α),
  translate a (f + g) = translate a f + translate a g
-- Mathlib.Topology.Piecewise
ContinuousOn.if' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {p : α → Prop}
  {f g : α → β} [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) →
    (∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) →
      ContinuousOn f (s ∩ {a | p a}) →
        ContinuousOn g (s ∩ {a | ¬p a}) → ContinuousOn (fun a => if p a then f a else g a) s
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x₀ : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x₀
-- Mathlib.Topology.ContinuousOn
/-- See also `Continuous.comp_continuousOn'` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`.  -/
Continuous.comp_continuousOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α},
  Continuous g → ContinuousOn f s → ContinuousOn (g ∘ f) s
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem : Type