mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G),
  MeasureTheory.addEquivAddHaarChar φ = μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ)
-- Lean.Data.Lsp.Diagnostics
/-- Custom diagnostic tags provided by the language server.
We use a separate diagnostic field for this to avoid confusing LSP clients with our custom tags.
 -/
Lean.Lsp.LeanDiagnosticTag : Type
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.chainsIso₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.chainsIso₁ A = (Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)).toModuleIso
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- `RootedConnected r` means that there is a path from `r` to any other vertex.  -/
Quiver.RootedConnected : {V : Type u} → [Quiver V] → V → Prop
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.map_constants : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  (c : L.Constants), φ ↑c = ↑c
-- Mathlib.Algebra.RingQuot
RingQuot.instAdd : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → Add (RingQuot r)
-- Mathlib.Order.Minimal
/-- **Alias** of `image_antitone_setOfPred_maximal_mem`. -/
image_antitone_setOf_maximal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) →
    f '' {x | Maximal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ f '' s) x}
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivAt_iff_isLittleO_nhds_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E}, HasLineDerivAt 𝕜 f f' x v ↔ (fun t => f (x + t • v) - f x - t • f') =o[nhds 0] fun t => t
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_add : ∀ {a b : ℕ} (hab : a + b < 2 ^ 32), UInt32.ofNatLT (a + b) hab = UInt32.ofNatLT a ⋯ + UInt32.ofNatLT b ⋯
-- Aesop.EMap
_private.Aesop.EMap.0.Aesop.EMap.getCandidates : {m : Type → Type u_1} → [MonadLiftT Lean.MetaM m] → {α : Type u_2} → Lean.Expr → Aesop.EMap α → m (Array ℕ)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.inf_normalizer_le_normalizer_inf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  Subgroup.normalizer ↑H ⊓ Subgroup.normalizer ↑K ≤ Subgroup.normalizer ↑(H ⊓ K)
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInv_leftInv_le : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M), S.leftInv.leftInv ≤ S
-- Mathlib.RingTheory.HahnSeries.Multiplication
_private.Mathlib.RingTheory.HahnSeries.Multiplication.0.HahnModule.mul_smul' : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : PartialOrder Γ'] [inst_4 : AddAction Γ Γ']
  [inst_5 : IsOrderedCancelVAdd Γ Γ'] [inst_6 : AddCommMonoid V] [inst_7 : Semiring R] [inst_8 : Module R V]
  (x y : HahnSeries Γ R) (z : HahnModule Γ' R V), (x * y) • z = x • y • z
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.leaf.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (vs : Array α), sizeOf (Lean.PersistentArrayNode.leaf vs) = 1 + sizeOf vs
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor C D},
  (∀ ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g],
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G) →
    CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) (s : Set β),
  (fun t => κ.densityProcess ν n a t s) = fun t =>
    ((κ a) (MeasurableSpace.countablePartitionSet n t ×ˢ s) / (ν a) (MeasurableSpace.countablePartitionSet n t)).toReal
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.keyAtIdxD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → ℕ → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : ℕ) →
          (x_2 : α) →
            ((x : ℕ) → (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf x fallback) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (n : ℕ) → (fallback : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback) →
                motive x x_1 x_2
-- Mathlib.Geometry.Diffeology.Basic
/-- Diffeology on a finite-dimensional normed space. We make this a definition instead of an
instance because we also want to have product diffeologies as an instance, and having both would
cause instance diamonds on spaces like `Fin n → ℝ`.  -/
NormedSpace.toDiffeology : (X : Type u_1) →
  [inst : NormedAddCommGroup X] → [inst_1 : NormedSpace ℝ X] → [FiniteDimensional ℝ X] → DiffeologicalSpace X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.mapsTo_sin : ∀ (s : Set ℝ), Set.MapsTo Real.sin s (Set.Icc (-1) 1)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_neg : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (β i)] (p : ENNReal) (i : ι)
  {a : β i}, PiLp.single p i (-a) = -PiLp.single p i a
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot : ∀ {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] [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α : LieModule.Weight K (↥H) L} {x y : ↥H},
  x ∈ LieModule.Weight.ker → y ∈ K ∙ LieAlgebra.IsKilling.coroot α → ((LieModule.traceForm K (↥H) L) x) y = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.id_whiskerRight : ∀ {C : Type u} (X Y : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.HomEquiv ((CategoryTheory.FreeMonoidalCategory.Hom.id X).whiskerRight Y)
    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y))
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.instMulWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] → [inst_3 : Bialgebra R C] → [inst_4 : Algebra R A] → Mul (WithConv (C →ₐ[R] A))
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_lt_comap_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K L : AddSubgroup N},
  Function.Surjective ⇑f → (AddSubgroup.comap f K < AddSubgroup.comap f L ↔ K < L)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeBack_obj_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)) (a : J),
  (CategoryTheory.WithInitial.coconeBack✝.obj t).ι.app a =
    CategoryTheory.Under.homMk (t.ι.app (CategoryTheory.WithInitial.of a)) ⋯
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.map_counit_comp_comul_right_assoc : ∀ {R : Type u_1} {M : Type u_3} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid P] [inst_4 : Module R P] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : Coalgebra R M] (f : M →ₗ[R] M') (g : P →ₗ[R] M),
  TensorProduct.map f CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul ∘ₗ g =
    TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm ∘ₗ g
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_X_eq_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} {t : τ},
  t ∉ Set.range ⇑e → (MvPowerSeries.killCompl e) (MvPowerSeries.X t) = 0
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.instUniqueUnits : Unique Cardinal.{u}ˣ
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {J : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H))
  [inst_3 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J H]
  [inst_5 : ∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C),
  (CategoryTheory.Limits.fiberwiseColimitLimitIso K).hom.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K (CategoryTheory.Grothendieck.ι F X)).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim
            (K.comp
              ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj
                (CategoryTheory.Grothendieck.ι F X)))).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.HasLimit.isoOfNatIso
              (K.associator
                  ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj
                    (CategoryTheory.Grothendieck.ι F X))
                  CategoryTheory.Limits.colim ≪≫
                K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫
                  (K.associator (CategoryTheory.Limits.fiberwiseColim F H)
                      ((CategoryTheory.evaluation C H).obj X)).symm)).hom
          (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H))
              X).inv))
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.comp_comparison_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [inst_3 : CategoryTheory.ComonadicLeftAdjoint R]
  [CategoryTheory.Limits.HasColimit (F.comp R)],
  CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction R)))
-- Mathlib.Order.Bounds.Basic
IsGLB.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α} [NoTopOrder α], IsGLB s a → s.Nonempty
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_mul : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (f₁ f₂ : (i : ι) → E i →L[𝕜] E i),
  (PiTensorProduct.mapL fun i => f₁ i * f₂ i) = PiTensorProduct.mapL f₁ * PiTensorProduct.mapL f₂
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.mk : Lean.NameGenerator → Lean.Core.Cache → Lean.Meta.Cache → Lean.Meta.LazyDiscrTree.Cache
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableDiv G], AEMeasurable f μ → ∀ (c : G), AEMeasurable (fun x => c / f x) μ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.coe_copy : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E)
  (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I), ↑(E.copy F hF J hJ) = F
-- Batteries.Data.List.Lemmas
List.pos_findIdxNth_getElem : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : List α} {h : List.findIdxNth p xs n < xs.length},
  p xs[List.findIdxNth p xs n] = true
-- Mathlib.Order.Category.Preord
instFaithfulPreordCatPreordToCat : preordToCat.Faithful
-- Mathlib.Data.Set.Function
/-- If `f` maps `s` bijectively to `t`, and `t'` is a superset of `t` contained in the range of `f`,
then `f` maps some superset of `s` bijectively to `t'`.  -/
Set.BijOn.exists_extend : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {t' : Set β},
  Set.BijOn f s t → t ⊆ t' → t' ⊆ Set.range f → ∃ s', s ⊆ s' ∧ Set.BijOn f s' t'
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_right_square_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k) →
    ∀ {Z : D} (h_1 : Y' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (F.map f)
          (CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y').symm g) h_1) =
        CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) (CategoryTheory.CategoryStruct.comp k h_1)
-- Mathlib.Order.GaloisConnection.Defs
/-- A Galois connection is a pair of functions `l` and `u` satisfying
`l a ≤ b ↔ a ≤ u b`. They are special cases of adjoint functors in category theory,
but do not depend on the category theory library in mathlib.  -/
GaloisConnection : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Prop
-- Mathlib.RingTheory.PowerBasis
PowerBasis.liftEquiv'_symm_apply_apply : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} {B : Type u_5} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Algebra A S] [inst_5 : IsDomain B] (pb : PowerBasis A S)
  (a : { y // y ∈ (minpoly A pb.gen).aroots B }), ⇑(pb.liftEquiv'.symm a) = ⇑((pb.basis.constr A) fun i => ↑a ^ ↑i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.continuousAt_arcsin : ∀ {x : ℝ}, ContinuousAt Real.arcsin x
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.subtype_comp_inclusion : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (hH : H ≤ K),
  K.subtype.comp (AddSubgroup.inclusion hH) = H.subtype
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_smul_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, (fun x => x.1 • x.2) '' s ×ˢ t = s • t
-- Mathlib.Combinatorics.Colex
Finset.Colex.insert_le_insert : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} [inst_1 : DecidableEq α],
  a ∉ s → b ∉ s → (toColex (insert a s) ≤ toColex (insert b s) ↔ a ≤ b)
-- Std.Async.TCP
/-- Creates a `Selector` that resolves once `s` has a connection available. Calling this function
does not start the connection wait, so it must not be called in parallel with `accept`.
 -/
Std.Async.TCP.Socket.Server.acceptSelector : Std.Async.TCP.Socket.Server → Std.Async.Selector Std.Async.TCP.Socket.Client
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- A subgroup is either the trivial subgroup or contains a non-identity element.  -/
Subgroup.bot_or_exists_ne_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ∨ ∃ x ∈ H, x ≠ 1
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e e_1 : ↑(p ⁻¹' {x})),
  e = e_1 → hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.prod_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set (α × β)),
  MeasurableSet s → (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
-- Mathlib.Probability.Moments.ComplexMGF
/-- If two random variables have the same moment-generating function then they have
the same `complexMGF` on the vertical strip `{z | z.re ∈ interior (integrableExpSet X μ)}`.

TODO: once we know that equal `mgf` implies equal distributions, we will be able to show that
the `complexMGF` are equal everywhere, not only on the strip.
This lemma will be used in the proof of the equality of distributions.  -/
ProbabilityTheory.eqOn_complexMGF_of_mgf' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'},
  ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' →
    (μ = 0 ↔ μ' = 0) →
      Set.EqOn (ProbabilityTheory.complexMGF X μ) (ProbabilityTheory.complexMGF Y μ')
        {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}
-- Mathlib.Data.Sym.Card
/-- Over `Fin (n + 1)`, the multisets of size `k + 1` containing `0` are equivalent to those of size
`k`, as demonstrated by respectively erasing or appending `0`.  -/
Sym.e1 : {n k : ℕ} → { s // 0 ∈ s } ≃ Sym (Fin n.succ) k
-- Mathlib.Algebra.Free
FreeAddSemigroup.mk.injEq : ∀ {α : Type u} (head : α) (tail : List α) (head_1 : α) (tail_1 : List α),
  ({ head := head, tail := tail } = { head := head_1, tail := tail_1 }) = (head = head_1 ∧ tail = tail_1)
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.repeatEq.match_1.splitter : (motive : (x : ℕ) → TypeVec.{u_1} x → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      ((x : TypeVec.{u_1} 0) → motive 0 x) → ((n : ℕ) → (α : TypeVec.{u_1} n.succ) → motive n.succ α) → motive x x_1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_mem_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α} {b : β}, b ∈ s → a • b ∈ a • s
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under an additive
group action. Phrased as a set union. See `AddAction.selfEquivSigmaOrbits` for the type
isomorphism.  -/
AddAction.univ_eq_iUnion_orbit : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α], Set.univ = ⋃ x, x.orbit
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂_app_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (x x_1 x_2 : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂ C).app x).app x_1).app x_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator x x_2 x_1).inv
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.num n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | x => h_3 x) =
    h_1 n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instInhabited : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] → [inst_1 : TopologicalSpace M] → Inhabited (MeasureTheory.VectorMeasure α M)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_eq : ∀ {arr : Array Batteries.UFNode} {i : ℕ} (h : i < arr.size), Batteries.UnionFind.parentD arr i = arr[i].parent
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Rcc α → Std.DTreeMap.Internal.RccSliceData α β
-- Init.Data.Option.Basic
Option.all_some : ∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.all p (some x) = p x
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.lift_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_3 : CategoryTheory.Mono S.f] {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.lift k hk) (CategoryTheory.CategoryStruct.comp S.f h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.Data.Finset.Defs
Finset.subset_of_le : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s ⊆ t
-- Mathlib.Data.Finsupp.Encodable
instCountableFinsupp : ∀ {α : Type u_1} {β : Type u_2} [Countable α] [Countable β] [inst : Zero β], Countable (α →₀ β)
-- Init.Data.List.Lemmas
List.filter_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → List.filter p (List.replicate n a) = []
-- Mathlib.Order.DirSupClosed
DirSupInacc.inter : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α], DirSupInacc s → DirSupInacc t → DirSupInacc (s ∩ t)
-- Mathlib.Order.Hom.Basic
OrderIso.surjective : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Surjective ⇑e
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (f₂₃ : j ⟶ l) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁ f₂₃).obj 0)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ}
  (desc desc_1 :
    {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M'))
  (e_desc : desc = desc_1)
  (fac :
    ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
      d.postcomp (desc d') = d')
  (postcomp_injective :
    ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
      d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'),
  { desc := desc, fac := fac, postcomp_injective := postcomp_injective } =
    { desc := desc_1, fac := ⋯, postcomp_injective := postcomp_injective }