mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy),
  CategoryTheory.CategoryStruct.comp (self.s 0) (X.left.δ 1) =
    CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) self.s'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_f_fst_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0)
  (p : ℤ) {Z : C} (h : K.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p) h) =
    CategoryTheory.CategoryStruct.comp (α.f p) h
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of `zeta n K L` is `1`
if `n` is odd.  -/
IsCyclotomicExtension.norm_zeta_eq_one : ∀ {n : ℕ} [inst : NeZero n] {K : Type u} (L : Type v) [inst_1 : Field K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : IsCyclotomicExtension {n} K L],
  n ≠ 2 → Irreducible (Polynomial.cyclotomic n K) → (Algebra.norm K) (IsCyclotomicExtension.zeta n K L) = 1
-- Mathlib.ModelTheory.Substructures
/-- A substructure of a structure `M` is a set closed under application of function symbols.  -/
FirstOrder.Language.Substructure : (L : FirstOrder.Language) → (M : Type w) → [L.Structure M] → Type w
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The actual recurrence  -/
AkraBazziRecurrence.h_rec : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (n : ℕ), self.n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.logRatio.eq_1 : ∀ (c : ENNReal), ProbabilityTheory.Fernique.logRatio c = Real.log (c.toReal / (1 - c).toReal) / (8 * (1 + √2) ^ 2)
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.mk.inj : ∀ {α : Type} {varName : Lean.Name} {categoryAttr : Lean.KeyedDeclsAttribute α}
  {combinatorAttr : Lean.ParserCompiler.CombinatorAttribute} {varName_1 : Lean.Name}
  {categoryAttr_1 : Lean.KeyedDeclsAttribute α} {combinatorAttr_1 : Lean.ParserCompiler.CombinatorAttribute},
  { varName := varName, categoryAttr := categoryAttr, combinatorAttr := combinatorAttr } =
      { varName := varName_1, categoryAttr := categoryAttr_1, combinatorAttr := combinatorAttr_1 } →
    varName = varName_1 ∧ categoryAttr = categoryAttr_1 ∧ combinatorAttr = combinatorAttr_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β},
  (Std.DHashMap.Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.Probability.Martingale.Basic
/-- A family of functions `f : ι → Ω → E` is a martingale with respect to a filtration `ℱ` if `f`
is strongly adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ i] =ᵐ[μ] f i`.  -/
MeasureTheory.Martingale : {Ω : Type u_1} →
  {E : Type u_2} →
    {ι : Type u_3} →
      [inst : Preorder ι] →
        {m0 : MeasurableSpace Ω} →
          [inst_1 : NormedAddCommGroup E] →
            [NormedSpace ℝ E] → (ι → Ω → E) → MeasureTheory.Filtration ι m0 → MeasureTheory.Measure Ω → Prop
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk_mapInvariantsOfRes_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {H : Type u_6} [inst_10 : Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R H W} (φ : H →* G)
  (f : ContIntertwiningMap (π.restrict φ) π') (v : V) (hv : v ∈ π.invariants),
  ↑((ContIntertwiningMap.mapInvariantsOfRes φ f) ⟨v, hv⟩) = f v
-- Init.Data.Int.Lemmas
Int.sub_eq_iff_eq_add' : ∀ {b a c : ℤ}, a - b = c ↔ a = b + c
-- Mathlib.Analysis.Normed.Group.Hom
/-- The norm of the `0` operator is `0`.  -/
NormedAddGroupHom.opNorm_zero : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂], ‖0‖ = 0
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x y : CategoryTheory.Abelian.Ext X Y n),
  R.extEquivCohomologyClass (x - y) = R.extEquivCohomologyClass x - R.extEquivCohomologyClass y
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Order.Partition.Basic
Partition.le_of_mem : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] (P : Partition s), x ∈ P → x ≤ s
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.tsum_sub : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f g : β → α} [T2Space α] [L.NeBot],
  Summable f L → Summable g L → ∑'[L] (b : β), (f b - g b) = ∑'[L] (b : β), f b - ∑'[L] (b : β), g b
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- Generalization of `Finset.prod_comm` to the case when the inner `Finset`s depend on the outer
variable.  -/
Finset.prod_comm' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α}
  {s' : α → Finset γ},
  (∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') →
    ∀ {f : γ → α → β}, ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y
-- Lean.Expr
Lean.instEmptyCollectionMVarIdSet : EmptyCollection Lean.MVarIdSet
-- Mathlib.Analysis.Normed.Ring.Units
/-- The `nonunits` in a normed ring with summable geometric series are contained in the
complement of the ball of radius `1` centered at `1 : R`.  -/
nonunits.subset_compl_ball : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], nonunits R ⊆ (Metric.ball 1 1)ᶜ
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hasSum_int_cosKernel₀ : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum
      (fun n =>
        if n = 0 then 0 else Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) * ↑(Real.exp (-Real.pi * ↑n ^ 2 * t)))
      (↑(HurwitzZeta.cosKernel (↑a) t) - 1)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A graph that has an injective homomorphism to an acyclic graph is acyclic.  -/
SimpleGraph.IsAcyclic.comap : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G'),
  Function.Injective ⇑f → G'.IsAcyclic → G.IsAcyclic
-- Mathlib.NumberTheory.Real.Irrational
irrational_sub_ratCast_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (x - ↑q) ↔ Irrational x
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularFormClass.bounded_at_infty_comp_ofComplex : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F)
  [ModularFormClass F Γ k],
  IsCusp OnePoint.infty Γ → (Filter.comap Complex.im Filter.atTop).BoundedAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_right' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A Borel space `Ω` embeds measurably into `ℝ` (with embedding `e`), hence we can get a `Kernel α Ω`
from a `Kernel α ℝ` by taking the comap by `e`.
Here we take the comap of a modification of `η : Kernel α ℝ`, useful when `η a` is a probability
measure with all its mass on `range e` almost everywhere with respect to some measure and we want to
ensure that the comap is a Markov kernel.
We thus take the comap by `e` of a kernel defined piecewise: `η` when
`η a (range (embeddingReal Ω))ᶜ = 0`, and an arbitrary deterministic kernel otherwise.  -/
ProbabilityTheory.Kernel.borelMarkovFromReal : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    (Ω : Type u_5) →
      [Nonempty Ω] →
        [inst : MeasurableSpace Ω] →
          [StandardBorelSpace Ω] → ProbabilityTheory.Kernel α ℝ → ProbabilityTheory.Kernel α Ω
-- Lean.Expr
/-- A function application.

For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as
``Expr.app (.const `Nat.succ []) (.const `Nat.zero [])``.
Note that multiple arguments are represented using partial application.

For example, the two argument application `f x y` is represented as
`Expr.app (.app f x) y`.
 -/
Lean.Expr.app : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Convex.Slope
/-- If for any three points `x < y < z`, the slope of the secant line of `f : 𝕜 → 𝕜` on `[x, y]` is
less than the slope of the secant line of `f` on `[y, z]`, then `f` is convex.  -/
convexOn_of_slope_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  Convex 𝕜 s →
    (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) → ConvexOn 𝕜 s f
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.fold_iter : ∀ {γ : Type u} {α β : Type v} {α_1 : Type u_1} {f : α_1 → β → α_1} {init : α_1}
  [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.Iterators.Finite α Id] {s : Std.Slice γ},
  Std.Iter.fold f init (Std.Slice.Internal.iter s) = Std.Slice.foldl f init s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbol.go : Lean.Lsp.DocumentSymbol → Lean.Json
-- Mathlib.Order.Monotone.Defs
Monotone.comp_monotoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, Monotone g → MonotoneOn f s → MonotoneOn (g ∘ f) s
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The map `(· + f)`.  -/
CategoryTheory.AddGrpObj.addRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A : C} → [CategoryTheory.AddGrpObj A] → (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A) → (A ≅ A)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forIn_eq_forInUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)}
  {init : δ}, Std.DTreeMap.Raw.forIn f init t = Std.DTreeMap.Raw.Const.forInUncurried (fun a b => f a.1 a.2 b) init t
-- Mathlib.Data.Matrix.Basis
Matrix.single_eq_single_vecMulVec_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : MulZeroOneClass α] (i : m) (j : n), Matrix.single i j 1 = Matrix.vecMulVec (Pi.single i 1) (Pi.single j 1)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- Exactness of `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₂'_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.Exact
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_image_coe_quotient : ∀ {G : Type u_1} [inst : CommGroup G] (s : Set G),
  MulAction.stabilizer (G ⧸ MulAction.stabilizer G s) (QuotientGroup.mk '' s) = ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.div : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, f.NeBot → g.NeBot → (f / g).NeBot
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRooSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRooSlice._auto_1) →
      Std.Roo.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RooSlice α β)
-- Init.Data.Array.Lemmas
Array.filter_replicate_of_pos : ∀ {stop n : ℕ} {α : Type u_1} {p : α → Bool} {a : α},
  stop = n → p a = true → Array.filter p (Array.replicate n a) 0 stop = Array.replicate n a
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lid_tensor : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.lid R (TensorProduct R M N) =
    (TensorProduct.assoc R R M N).symm ≪≫ₗ LinearEquiv.rTensor N (TensorProduct.lid R M)
-- Mathlib.Data.PNat.Xgcd
PNat.gcdA'_coe : ∀ (a b : ℕ+), ↑(a.gcdA' b) = ↑(a.gcdW b) + a.gcdX b
-- Mathlib.Tactic.HigherOrder
/-- The `higher_order` attribute. From a lemma of the shape `∀ x, f (g x) = h x` derive an
auxiliary lemma of the form `f ∘ g = h` for reasoning about higher-order functions.

Syntax: `[higher_order]` or `[higher_order name]` where the given name is used for the
generated theorem.  -/
Mathlib.Tactic.higherOrderAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.Analysis.Normed.Group.Int
nnnorm_zsmul_le : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] (n : ℤ) (a : α), ‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra is equivalent to its push forward along an injective linear map.  -/
LieSubalgebra.equivMapOfInjective : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} →
            [inst_3 : LieRing L₂] →
              [inst_4 : LieAlgebra R L₂] →
                (f : L →ₗ⁅R⁆ L₂) → (K : LieSubalgebra R L) → Function.Injective ⇑f → ↥K ≃ₗ⁅R⁆ ↥(LieSubalgebra.map f K)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.toFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) {X Y : C} (i : X ⟶ Y),
  S.toFunctor.map i = MonCat.ofHom (((MonCat.Hom.hom (M.map i)).submonoidComap (S.obj Y)).comp (Submonoid.inclusion ⋯))
-- Init.PropLemmas
or_congr_right : ∀ {b c a : Prop}, (b ↔ c) → (a ∨ b ↔ a ∨ c)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ : B}
  {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryTheory.CategoryStruct.id b₀) (a : X ⟶ Y) {Z : ↑(F.obj b₀)}
  (h : (F.map f).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map a) h) =
    CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app Y) h)
-- Lean.DocString.Extension
Lean.addVersoModuleDocSnippet : Lean.Environment → Lean.VersoModuleDocs.Snippet → Except String Lean.Environment
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- `shiftIso 0` is the obvious isomorphism.  -/
CategoryTheory.SingleFunctors.shiftIso_zero : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (a : A),
  self.shiftIso 0 a a ⋯ = (self.functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_one_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_eq_one_iff._auto_1 → (CFC.sqrt a = 1 ↔ a = 1)
-- Mathlib.Probability.Kernel.CondDistrib
/-- `condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of
`condKernel`.  -/
ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β},
  Measurable X →
    Measurable Y →
      ∀ {κ : ProbabilityTheory.Kernel β Ω} [ProbabilityTheory.IsFiniteKernel κ],
        MeasureTheory.Measure.map (fun x => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ →
          ⇑(ProbabilityTheory.condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.tensorLeft_linear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C] (X : C),
  CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorLeft X)
-- Mathlib.RepresentationTheory.Intertwining
LinearMap.intertwiningMap_of_isIntertwiningMap.congr_simp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f f_1 : V →ₗ[A] W) (e_f : f = f_1)
  (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)),
  LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f hf = LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f_1 ⋯
-- Mathlib.SetTheory.ZFC.Rank
/-- `PSet.rank` is equal to the `IsWellFounded.rank` over `∈`.  -/
PSet.rank_eq_wfRank : ∀ {x : PSet.{u}}, Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) x
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.HasSheafify J (Type w)] [J.WEqualsLocallyBijective (Type w)],
  P.IsConservativeFamilyOfPoints →
    ∀ {X : C} {ι : Type u_1} [Small.{w, u_1} ι] {U : ι → C} (f : (i : ι) → U i ⟶ X),
      CategoryTheory.Sieve.ofArrows U f ∈ J X ↔
        ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
          ∃ i y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), IsCompact ↑s
-- Lean.Elab.DefView
/-- Snapshot after elaboration of a definition header.  -/
Lean.Elab.HeaderProcessedSnapshot : Type
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMapl_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (self : ρ.IntertwiningMap σ),
  (Representation.IntertwiningMap.toLinearMapl ρ σ) self = self.toLinearMap
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorObj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).X = CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X
-- Mathlib.Topology.UniformSpace.Defs
UniformContinuous.eq_1 : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
  UniformContinuous f = Filter.Tendsto (fun x => (f x.1, f x.2)) (uniformity α) (uniformity β)
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppExprLegacy : Lean.Environment → Lean.MetavarContext → Lean.LocalContext → Lean.Options → Lean.Expr → IO Std.Format
-- Mathlib.Algebra.Group.Conj
/-- We say that `a` is conjugate to `b` if for some unit `c` we have `c * a * c⁻¹ = b`.  -/
IsConj : {α : Type u} → [Monoid α] → α → α → Prop
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.mk.injEq : ∀ (toCommandContextInfo : Lean.Elab.CommandContextInfo) (parentDecl? : Option Lean.Name)
  (autoImplicits : Array Lean.Expr) (toCommandContextInfo_1 : Lean.Elab.CommandContextInfo)
  (parentDecl?_1 : Option Lean.Name) (autoImplicits_1 : Array Lean.Expr),
  ({ toCommandContextInfo := toCommandContextInfo, parentDecl? := parentDecl?, autoImplicits := autoImplicits } =
      { toCommandContextInfo := toCommandContextInfo_1, parentDecl? := parentDecl?_1,
        autoImplicits := autoImplicits_1 }) =
    (toCommandContextInfo = toCommandContextInfo_1 ∧ parentDecl? = parentDecl?_1 ∧ autoImplicits = autoImplicits_1)
-- Std.Time.Time.Unit.Second
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
 -/
Std.Time.Second.Ordinal.ofFin : {leap : Bool} → Fin (if leap = true then 61 else 60) → Std.Time.Second.Ordinal leap
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.sub_eq_add : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a - b = a + b
-- Init.Data.SInt.Lemmas
Int64.neg_ne_zero : ∀ {a : Int64}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.addSubgroupClosure_add : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G}, s.Nonempty → ↑(AddSubgroup.closure s) + s = ↑(AddSubgroup.closure s)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instIsCentralScalar : ∀ {k : Type u_1} {G : Type u_2} {S : Type u_3} [inst : AddMonoid k] [inst_1 : SMulZeroClass S k]
  [inst_2 : SMulZeroClass Sᵐᵒᵖ k] [IsCentralScalar S k], IsCentralScalar S (SkewMonoidAlgebra k G)
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_base_mul : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → padicValNat p (p * n) = padicValNat p n + 1
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.sup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
  Filter.Tendsto f x₁ y → Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊔ x₂) y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_inv_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
            (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).inv.app
      X =
    X.iso.inv
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintClientCapabilities : Lean.ToJson Lean.Lsp.InlayHintClientCapabilities
-- Mathlib.RingTheory.Multiplicity
emultiplicity_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), emultiplicity a 0 = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- Rectangles of countably spanning sets are countably spanning.  -/
IsCountablySpanning.prod : ∀ {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {D : Set (Set β)},
  IsCountablySpanning C → IsCountablySpanning D → IsCountablySpanning (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D)