mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Riemann-Lebesgue lemma for functions on a finite-dimensional real vector space, formulated via
dual space.  -/
tendsto_integral_exp_smul_cocompact : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [IsTopologicalAddGroup V] [T2Space V]
  [inst_6 : MeasurableSpace V] [BorelSpace V] [inst_8 : Module ℝ V] [ContinuousSMul ℝ V] [FiniteDimensional ℝ V]
  (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure],
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-w v) • f v ∂μ) (Filter.cocompact (StrongDual ℝ V)) (nhds 0)
-- Mathlib.Topology.Compactness.SigmaCompact
iUnion_closure_compactCovering : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X],
  ⋃ n, closure (compactCovering X n) = Set.univ
-- Init.Data.Vector.Range
Vector.map_add_range' : ∀ {a : ℕ} (s n step : ℕ), Vector.map (fun x => a + x) (Vector.range' s n step) = Vector.range' (a + s) n step
-- Init.Data.Array.Lemmas
Array.prod_push : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {xs : Array α} {x : α}, (xs.push x).prod = xs.prod * x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_minKey? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {fallback : α},
  l.minKeyD fallback = l.minKey?.getD fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk.sizeOf_spec : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : SizeOf R]
  {point : WeierstrassCurve.Projective.PointClass R} (nonsingular : W'.NonsingularLift point),
  sizeOf { point := point, nonsingular := nonsingular } = 1 + sizeOf point + sizeOf nonsingular
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig newWidth → Sort u_1) (w n : ℕ)
  (inner : aig.RefVec w) (h : newWidth = w * n)
  (h_1 :
    (w n : ℕ) → (inner : aig.RefVec w) → (h : newWidth = w * n) → motive { w := w, n := n, inner := inner, h := h }),
  (match { w := w, n := n, inner := inner, h := h } with
    | { w := w, n := n, inner := inner, h := h } => h_1 w n inner h) =
    h_1 w n inner h
-- Mathlib.Data.Set.Countable
/-- If `s : Set α` is a nonempty countable set, then there exists a map
`f : ℕ → α` such that `s = range f`.  -/
Set.Countable.exists_eq_range : ∀ {α : Type u} {s : Set α}, s.Countable → s.Nonempty → ∃ f, s = Set.range f
-- Mathlib.Algebra.CharZero.Defs
NeZero.charZero_one : ∀ {M : Type u_2} [inst : AddMonoidWithOne M] [CharZero M], NeZero 1
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The Cartesian product of two incidence algebras.  -/
IncidenceAlgebra.prod : {𝕜 : Type u_2} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : Ring 𝕜] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] → IncidenceAlgebra 𝕜 α → IncidenceAlgebra 𝕜 β → IncidenceAlgebra 𝕜 (α × β)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_forall : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t → (∀ x ∈ t, f x = 0) → ∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_3 : ∀ (motive : PosNum → PosNum → Sort u_1) (x : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (x = PosNum.one → False) →
    (match PosNum.one, x with
      | PosNum.one, PosNum.one => h_1 ()
      | x, PosNum.one => h_2 x
      | PosNum.one, x => h_3 x
      | a.bit0, b.bit0 => h_4 a b
      | a.bit0, b.bit1 => h_5 a b
      | a.bit1, b.bit0 => h_6 a b
      | a.bit1, b.bit1 => h_7 a b) =
      h_3 x
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.mem_coindV : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V) (f : C(H, V)),
  f ∈ ContRepresentation.coindV φ π ↔ ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)
-- Init.Prelude
/-- Reflexivity of heterogeneous equality.  -/
HEq.refl : ∀ {α : Sort u} (a : α), a ≍ a
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A bijective `Semigroup` homomorphism is an isomorphism  -/
MulEquiv.ofBijective : {M : Type u_9} →
  {N : Type u_10} →
    {F : Type u_11} →
      [inst : Mul M] →
        [inst_1 : Mul N] → [inst_2 : FunLike F M N] → [MulHomClass F M N] → (f : F) → Function.Bijective ⇑f → M ≃* N
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_true : ∀ {σs : List (Type u)} {φ : Prop}, φ → ⌜φ⌝ ⊣⊢ₛ ⌜True⌝
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalClosedFunctorOppositeLightProfiniteModuleCat : (R : Type u) →
  [inst : CommRing R] → CategoryTheory.MonoidalClosed (CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R))
-- Init.Data.Float.Float32
/-- Computes the absolute value of a floating-point number.

This function has a logical model in terms of `Float32.Model`. It is implemented in compiled code by
the C function `fabsf`.
 -/
Float32.abs : Float32 → Float32
-- Mathlib.Topology.Algebra.UniformConvergence
/-- Let `𝔖 : Set (Set α)`. If `G` is a uniform additive group,
then `α →ᵤ[𝔖] G` is a uniform additive group as well.  -/
instIsUniformAddGroupUniformOnFun : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] {𝔖 : Set (Set α)} [inst_1 : UniformSpace G] [IsUniformAddGroup G],
  IsUniformAddGroup (UniformOnFun α G 𝔖)
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseName : Std.Internal.Parsec.String.Parser String
-- Mathlib.Algebra.Group.Irreducible.Lemmas
Even.not_addIrreducible : ∀ {M : Type u_2} [inst : AddMonoid M] {x : M}, Even x → ¬AddIrreducible x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [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 → (m.insertMany l).get? k' = some k
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin.congr_simp : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s s_1 : Set A),
  s = s_1 → NonUnitalAlgebra.adjoin R s = NonUnitalAlgebra.adjoin R s_1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- An additive action of an additive monoid on a type `β` gives an additive action on `Set β`.  -/
Set.addActionSet : {α : Type u_2} → {β : Type u_3} → [inst : AddMonoid α] → [AddAction α β] → AddAction α (Set β)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
_private.Mathlib.Algebra.Category.FGModuleCat.Basic.0.FGModuleCat.coevaluation_evaluation : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (FGModuleCat.FGModuleCatDual K V)
        (FGModuleCat.FGModuleCatCoevaluation K V))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (FGModuleCat.FGModuleCatDual K V) V
            (FGModuleCat.FGModuleCatDual K V)).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (FGModuleCat.FGModuleCatEvaluation K V)
          (FGModuleCat.FGModuleCatDual K V))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (FGModuleCat.FGModuleCatDual K V)).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (FGModuleCat.FGModuleCatDual K V)).inv
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.max! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_res_apply' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type u_2} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U)
  [inst_3 : CategoryTheory.ConcreteCategory C FC] (s : CC (F.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i)) s) =
    (CategoryTheory.ConcreteCategory.hom (F.germ V x ⋯)) s
-- Init.Data.SInt.Lemmas
Int16.toInt64_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a ring with no zero divisors has no zero divisors.  -/
Subring.instNoZeroDivisorsSubtypeMem : ∀ {R : Type u_1} [inst : NonAssocRing R] [NoZeroDivisors R] (s : Subring R), NoZeroDivisors ↥s
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sub_mul_sub_nonneg_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftMono R] (x : R), a ≤ b → (0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentCoordChange_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {w x y z : M} {v : E},
  z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source →
    (tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opEquiv_unitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.opEquiv C).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.ShortComplex C)ᵒᵖ)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(f ≫ g) ◁ η`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Init.Data.Array.Lemmas
/-- Variant of `map_const` using a lambda rather than `Function.const`.  -/
Array.map_const' : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {b : β}, Array.map (fun x => b) xs = Array.replicate xs.size b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.fullyFaithfulForget₂Mon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C =
    CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.AddGrp.toAddMon
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIoo.eq_1 : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  SummationFilter.symmetricIoo G = { filter := Filter.map (fun g => Finset.Ioo (-g) g) Filter.atTop }
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : N),
  (f.addEquivOfAddEquiv k H) x = (f.map ⋯ k) x
-- Mathlib.Logic.Basic
/-- See `IsEmpty.forall_iff` for the `False` version.  -/
forall_true_left : ∀ (p : True → Prop), (∀ (x : True), p x) ↔ p True.intro
-- Mathlib.Order.Interval.Set.Defs
Set.Ioi_def : ∀ {α : Type u_1} [inst : Preorder α] (a : α), {x | a < x} = Set.Ioi a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mem_toCloseds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] {x : α} {s : TopologicalSpace.NonemptyCompacts α},
  x ∈ s.toCloseds ↔ x ∈ s
-- Aesop.Tree.Data
Aesop.Goal.setForwardRuleMatches : Aesop.ForwardRuleMatches → Aesop.Goal → Aesop.Goal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffOn.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => Real.cos (f x)) s
-- Mathlib.Data.Multiset.Defs
Multiset.instMembership : {α : Type u_1} → Membership α (Multiset α)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocks_length : ∀ {n : ℕ} (c : Composition n), c.blocks.length = c.length
-- Init.Data.Array.Lemmas
Array.filter_eq_append_iff : ∀ {α : Type u_1} {xs ys zs : Array α} {p : α → Bool},
  Array.filter p xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Array.filter p as = ys ∧ Array.filter p bs = zs
-- Mathlib.Algebra.BigOperators.Finprod
map_finprod : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {f : α → M} {G : Type u_7}
  [inst_2 : FunLike G M N] [MonoidHomClass G M N] (g : G),
  Function.HasFiniteMulSupport f → g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.of_pow : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R},
  ¬IsUnit f → ∀ {n : ℕ}, n ≠ 0 → (f ^ n).Separable → f.Separable ∧ n = 1
-- Mathlib.Data.Quot
Quot.factor_mk_eq : ∀ {α : Type u_4} (r s : α → α → Prop) (h : ∀ (x y : α), r x y → s x y), Quot.factor r s h ∘ Quot.mk r = Quot.mk s
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_ΨSq : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)
-- Mathlib.Algebra.Group.End
Equiv.swap_mul_swap_mul_swap : ∀ {α : Type u_4} [inst : DecidableEq α] {x y z : α},
  x ≠ y → x ≠ z → Equiv.swap y z * Equiv.swap x y * Equiv.swap y z = Equiv.swap z x
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- See `LinearIndependent.finCons` for a family of elements in a vector space.  -/
LinearIndependent.finCons' : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : ℕ} (x : M)
  (v : Fin m → M),
  LinearIndependent R v →
    (∀ (c : R), ∀ y ∈ Submodule.span R (Set.range v), c • x + y = 0 → c = 0) → LinearIndependent R (Fin.cons x v)
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabChoice : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.abs_def' : ∀ (q : ℚ), |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.setIntegral_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] {f : β × γ → E} {s : Set β} {t : Set γ},
  MeasurableSet s →
    MeasurableSet t →
      MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a) →
        ∫ (z : β × γ) in s ×ˢ t, f z ∂(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- Corners are preserved under `2`-Freiman homomorphisms.  -/
IsCorner.image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H} {x₁ y₁ x₂ y₂ : G},
  IsAddFreimanHom 2 s t f →
    A ⊆ s ×ˢ s → IsCorner A x₁ y₁ x₂ y₂ → IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_nonempty : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  (G.neighborFinset v).Nonempty ↔ ¬G.IsIsolated v
-- Mathlib.Data.Finset.Insert
Finset.insertPiProd_snd : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i)
  (i : α) (hi : i ∈ s), (Finset.insertPiProd f x).2 i hi = x i ⋯
-- Init.Data.Nat.Basic
Nat.not_beq_eq_true_eq : ∀ (a b : ℕ), ((!a == b) = true) = ¬a = b
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousCore' 𝒜`
is the largest homogeneous ideal of `A` contained in `I`, as an ideal.  -/
Ideal.homogeneousCore' : {ι : Type u_1} → {σ : Type u_2} → {A : Type u_3} → [inst : Semiring A] → [SetLike σ A] → (ι → σ) → Ideal A → Ideal A
-- Mathlib.Data.Fintype.Pi
Fintype.mem_piFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} {t : (a : α) → Finset (δ a)}
  {f : (a : α) → δ a}, f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SFinite.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∃ m, (∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (m n)) ∧ μ = MeasureTheory.Measure.sum m) → MeasureTheory.SFinite μ
-- Mathlib.Data.Ordmap.Invariants
Ordnode.emem_iff_all : ∀ {α : Type u_1} {x : α} {t : Ordnode α}, Ordnode.Emem x t ↔ ∀ (P : α → Prop), Ordnode.All P t → P x
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Applying `P` to a morphism of `Type`  -/
PFunctor.map : (P : PFunctor.{uA, uB}) → {α : Type v₁} → {β : Type v₂} → (α → β) → ↑P α → ↑P β
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
/-- A function `f : α × β → StieltjesFunction ℝ` with the property `IsCondKernelCDF f κ ν` gives a
Markov kernel from `α × β` to `ℝ`, by taking for each `p : α × β` the measure defined by `f p`.  -/
ProbabilityTheory.IsCondKernelCDF.toKernel : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {x : MeasurableSpace β} →
        {κ : ProbabilityTheory.Kernel α (β × ℝ)} →
          {ν : ProbabilityTheory.Kernel α β} →
            (f : α × β → StieltjesFunction ℝ) →
              ProbabilityTheory.IsCondKernelCDF f κ ν → ProbabilityTheory.Kernel (α × β) ℝ
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.mk.injEq : ∀ (heq : Bool) (hIdx xIdx : ℕ) (heq_1 : Bool) (hIdx_1 xIdx_1 : ℕ),
  ({ heq := heq, hIdx := hIdx, xIdx := xIdx } = { heq := heq_1, hIdx := hIdx_1, xIdx := xIdx_1 }) =
    (heq = heq_1 ∧ hIdx = hIdx_1 ∧ xIdx = xIdx_1)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left : ∀ {R : Type u} [inst : CommRing R] {M N P : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] [inst_7 : Coalgebra R M]
  [inst_8 : Coalgebra R N] [inst_9 : Coalgebra R P], CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
        h_1)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.support_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  [inst_2 : DecidableEq M] (n : M) (p : MvPolynomial σ R),
  ((MvPolynomial.weightedHomogeneousComponent w n) p).support = {c ∈ p.support | (Finsupp.weight w) c = n}
-- Mathlib.Data.Nat.SuccPred
/-- A special case of `Order.covBy_iff_add_one_eq` for use by simp.  -/
Nat.covBy_iff_add_one_eq : ∀ {m n : ℕ}, m ⋖ n ↔ m + 1 = n
-- Lean.Parser.Extension
/-- Resolve the given parser name and return a list of candidates.  -/
_private.Lean.Parser.Extension.0.Lean.Parser.resolveParserNameCore : Lean.Environment → Lean.Options → Lean.Name → List Lean.OpenDecl → Lean.Ident → List Lean.Parser.ParserResolution
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_comp_includeRight : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  (↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeLeft
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.eraseRules : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- In a linearly ordered monoid, we are happy for `bot_eq_one` to be a `@[simp]` lemma.  -/
bot_eq_one' : ∀ {α : Type u} [inst : Monoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedMul α] [inst_3 : OrderBot α], ⊥ = 1