mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.id_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : G.Coalgebra),
  CategoryTheory.Comonad.Coalgebra.Hom.id A = CategoryTheory.CategoryStruct.id A
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mulAction' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : Monoid S] →
              [inst_4 : SMul S R] →
                [inst_5 : MulAction S M] → [IsScalarTower S R M] → (P : Submodule R M) → MulAction S (M ⧸ P)
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.algebra_isAlgebraic_bot_right : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial R],
  Algebra.IsAlgebraic R ↥⊥
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_spanSingleton : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] (x : K),
  (FractionalIdeal.extendedHom L B) (FractionalIdeal.spanSingleton (nonZeroDivisors A) x) =
    FractionalIdeal.spanSingleton (nonZeroDivisors B) ((IsFractionRing.map ⋯) x)
-- Mathlib.Data.Fintype.Basic
Multiset.count_univ : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (a : α), Multiset.count a Finset.univ.val = 1
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toListRev_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n},
  (xs.iterM m).toListRev = pure xs.toList.reverse
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.coe_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  { X := X, p := CategoryTheory.CategoryStruct.id X, idem := ⋯ }.X = X
-- Lean.Meta.WHNF
/-- When `true`, unfolding a `[reducible]` class field at `TransparencyMode.reducible` also unfolds
the associated instance projection at `TransparencyMode.instances`.

**Motivation:** Consider `a ≤ b` where `a b : Nat` and `LE.le` is `[reducible]`. Unfolding `LE.le`
gives `instLENat.1 a b`, which is stuck because `instLENat` is `[instance_reducible]` (not
`[reducible]`). Similarly, `stM m (ExceptT ε m) α` unfolds to an instance projection that is stuck
at `.reducible`. Without this option, marking a class field as `[reducible]` is pointless when the
instance providing it is only `[instance_reducible]`. This option makes the `[reducible]` annotation
on class fields work as the user expects by temporarily bumping to `.instances` for the projection.

See `unfoldDefault` for the implementation.
 -/
Lean.Meta.backward.whnf.reducibleClassField : Lean.Option Bool
-- Mathlib.Topology.Neighborhoods
/-- The intersection of a dense set with an open dense set is a dense set.  -/
Dense.inter_of_isOpen_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, Dense s → Dense t → IsOpen t → Dense (s ∩ t)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.sub_of_left : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, p.Monic → q.degree < p.degree → (p - q).Monic
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.formatGeneric.go : ((typ : Std.Time.Modifier) → Option (Std.Time.TypeFormat typ)) →
  Std.Time.DateFormat → String → Std.Time.FormatString → Option String
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_singleton : ∀ {α : Type u_1} (x : α), FreeMonoid.ofList [x] = FreeMonoid.of x
-- Mathlib.Tactic.CongrExclamation
/-- `congr!` tries to prove the main goal by repeatedly applying congruence rules. For example, on a
goal of the form `⊢ f a1 a2 ... = f b1 b2 ...`, `congr!` will make new goals `⊢ a1 = b1`,
`⊢ a2 = b2`, ...

`congr!` is a more powerful version of the `congr` tactic that uses congruence lemmas (tagged with
`@[congr]`), reflexivity rules (tagged with `@[refl]`) and proof discharging strategies. The full
list of congruence proof strategies is documented in the module `Mathlib.Tactic.CongrExclamation`.
The `congr!` tactic is used by the `convert` and `convert_to` tactics.

* `congr! n`, where `n` is a positive numeral, controls the depth with which congruence is
  applied. For example, if the main goal is `n + n + 1 = 2 * n + 1`, then `congr! 1` results in one
  goal, `⊢ n + n = 2 * n`, and `congr! 2` (or more) results in two (impossible) goals
  `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
  By default, the depth is unlimited.
* `congr! with x ⟨y₁, y₂⟩ (z₁ | z₂)` names or pattern-matches the variables introduced by
  congruence rules, like `rintro x ⟨y₁, y₂⟩ (z₁ | z₂)` would.
* `congr! (config := cfg)` uses the configuration options in `cfg` to control the congruence
  rules (see `Congr!.Config`).
 -/
Congr!.congr! : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) =
    CategoryTheory.Limits.pullback.fst i₁ i₂
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The geometric sequence `fun n ↦ ψ^n` is a solution of `fibRec`.  -/
Real.geom_goldenConj_isSol_fibRec : Real.fibRec.IsSolution fun x => Real.goldenConj ^ x
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nnnorm_eq_iSup_nnnorm : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)), ‖f‖₊ = ⨆ x, ‖f x‖₊
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut.mk : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [toIsCut : Std.Internal.IsCut cmp cut],
  (∀ (k : α) {k' : α}, cut k' = Ordering.eq → cut k = cmp k' k) → Std.Internal.IsStrictCut cmp cut
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.dart_edge_eq_mk'_iff' : ∀ {V : Type u_1} {G : SimpleGraph V} {d : G.Dart} {u v : V},
  d.edge = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulOneClassOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass Mᵐᵒᵖ], DomMulAct.instMulOneClassOfMulOpposite = inst
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhdsWithin_coe_image : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (x : X),
  nhdsWithin (↑x) (OnePoint.some '' s) = Filter.map OnePoint.some (nhdsWithin x s)
-- Init.Conv
/-- * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
  or else fails.
* `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses
  with inaccessible names to the given names.
* `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
Lean.Parser.Tactic.Conv.case : Lean.ParserDescr
-- Mathlib.Data.Vector3
Vector3.insert_fs : ∀ {α : Type u_1} {n : ℕ} (a b : α) (v : Vector3 α n) (i : Fin2 (n + 1)),
  Vector3.insert a (Vector3.cons b v) i.fs = Vector3.cons b (Vector3.insert a v i)
-- Init.Data.SInt.Bitwise
Int8.not_zero : ~~~0 = -1
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.mk.sizeOf_spec : ∀ (fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (pureHandle : Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic))
  (handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse))
  (pureOnDidChange : Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit)
  (onDidChange : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit)
  (lastTaskMutex : Std.Mutex (Lean.Server.ServerTask Unit)) (initState : Dynamic) (stateRef : IO.Ref Dynamic)
  (completeness : Lean.Server.RequestHandlerCompleteness),
  sizeOf
      { fileSource := fileSource, pureHandle := pureHandle, handle := handle, pureOnDidChange := pureOnDidChange,
        onDidChange := onDidChange, lastTaskMutex := lastTaskMutex, initState := initState, stateRef := stateRef,
        completeness := completeness } =
    1 + sizeOf lastTaskMutex + sizeOf initState + sizeOf stateRef + sizeOf completeness
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` has normal form at `x`, then `f` equals `f.toNF`.  -/
toMeromorphicNFAt_eq_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, toMeromorphicNFAt f x = f ↔ MeromorphicNFAt f x
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- By the universal property for free modules, any surjective map `(Fin n → R) →ₗ[R] (Fin m → R)`
has an injective splitting `(Fin m → R) →ₗ[R] (Fin n → R)`
from which the strong rank condition gives the necessary inequality for the rank condition.
 -/
rankCondition_of_strongRankCondition : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R], RankCondition R
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.instPartialOrderElemFinset : {α : Type u_1} → {n : ℕ} → PartialOrder ↑(Set.powersetCard α n)
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The fork map in the equalizer diagram we will construct.  -/
CategoryTheory.Comonad.CofreeEqualizer.ι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → (X : T.Coalgebra) → X ⟶ T.cofree.obj X.A
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ},
  (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat))
-- Mathlib.LinearAlgebra.Multilinear.Pi
/-- When only one member of the family of multilinear maps is nonzero, the result consists only of
the component from that member.  -/
MultilinearMap.piFamily_single_left_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] [inst_5 : Fintype ι] [inst_6 : (i : ι) → DecidableEq (κ i)]
  (p : (i : ι) → κ i) (f : MultilinearMap R (fun i => M i (p i)) (N p)) (x : (i : ι) → (j : κ i) → M i j),
  (MultilinearMap.piFamily (Pi.single p f)) x = Pi.single p (f fun i => x i (p i))
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_le_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {c : NNReal}, dist x y ≤ ↑c ↔ nndist x y ≤ c
-- Mathlib.GroupTheory.OrderOfElement
powCoprime_one : ∀ {n : ℕ} {G : Type u_6} [inst : Group G] (h : (Nat.card G).Coprime n), (powCoprime h) 1 = 1
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] [F.HasRightDerivedFunctor W], L.HasLeftKanExtension F
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_precompL_le : ∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ),
  ‖ContinuousLinearMap.precompL Eₗ L‖ ≤ ‖L‖
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β} {s : (i : ι) → κ i → Set β},
  f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j
-- Mathlib.Topology.Constructions
OrderDual.instDiscreteTopology : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X], DiscreteTopology Xᵒᵈ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` has a derivative at `f' x` for all `x` in
`[a, b]` and `f'` is integrable on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`.  -/
intervalIntegral.integral_eq_sub_of_hasDerivAt : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.add_omega0_opow : ∀ {a b : Ordinal.{u}}, a < Ordinal.omega0 ^ b → a + Ordinal.omega0 ^ b = Ordinal.omega0 ^ b
-- Lean.Declaration
Lean.QuotVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (kind : Lean.QuotKind),
  sizeOf { toConstantVal := toConstantVal, kind := kind } = 1 + sizeOf toConstantVal + sizeOf kind
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.comp_contDiffWithinAt_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {g : F → G} {n : WithTop ℕ∞}
  {y : F} (x : E), ContDiffAt 𝕜 n g y → ContDiffWithinAt 𝕜 n f s x → f x = y → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_const_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {a : α},
  (s.sup fun x => a) ≤ a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k)[a]? = if (k == a) = true then none else m[a]?
-- Mathlib.RingTheory.Trace.Basic
IntermediateField.AdjoinSimple.trace_gen_eq_zero : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  ¬IsIntegral K x → (Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x) = 0
-- Lean.Parser.Term
Lean.Parser.Term.defaultOrOfNonempty.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Sym.Pattern
/-- If `some argsInfo`, `argsInfo` stores whether the pattern variables are instances/proofs.
It is `none` if no pattern variables are instance/proof.
 -/
Lean.Meta.Sym.Pattern.varInfos? : Lean.Meta.Sym.Pattern → Option Lean.Meta.Sym.ProofInstInfo
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_f_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ),
  CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) ((AlgebraicTopology.DoldKan.Q q).f n) =
    (AlgebraicTopology.DoldKan.Q q).f n
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_mul_basis_toMatrix`. -/
BilinForm.toMatrix_mul_basis_toMatrix : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) [inst_6 : DecidableEq o] (c : Module.Basis o R₁ M₁) (B : LinearMap.BilinForm R₁ M₁),
  (b.toMatrix ⇑c).transpose * (LinearMap.BilinForm.toMatrix b) B * b.toMatrix ⇑c = (LinearMap.BilinForm.toMatrix c) B
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.setIntegral_traj_partialTraj' : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] {a b : ℕ},
  a ≤ b →
    ∀ {u : (i : ↥(Finset.Iic a)) → X ↑i} {f : ((i : ↥(Finset.Iic b)) → X ↑i) → ((n : ℕ) → X n) → E},
      MeasureTheory.Integrable (Function.uncurry f)
          (((ProbabilityTheory.Kernel.partialTraj κ a b) u).compProd (ProbabilityTheory.Kernel.traj κ b)) →
        ∀ {A : Set ((i : ↥(Finset.Iic b)) → X ↑i)},
          MeasurableSet A →
            ∫ (x : (i : ↥(Finset.Iic b)) → X ↑i) in A,
                ∫ (y : (n : ℕ) → X n),
                  f x y ∂(ProbabilityTheory.Kernel.traj κ b) x ∂(ProbabilityTheory.Kernel.partialTraj κ a b) u =
              ∫ (y : (n : ℕ) → X n) in Preorder.frestrictLe b ⁻¹' A,
                f (Preorder.frestrictLe b y) y ∂(ProbabilityTheory.Kernel.traj κ a) u
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.isIntertwining' : ∀ {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]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (self : ContIntertwiningMap π₁ π₂) (g : G),
  self.toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL self.toContinuousLinearMap
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c_1 → c = c_1
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
CategoryTheory.extendCofan_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C}
  (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt),
  (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {H : J.OneHypercoverFamily}, (∀ {X : C}, ∀ S ∈ J X, ∃ E, ∃ (_ : H E), E.sieve₀ ≤ S) → H.IsGenerating
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.leftCancelSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : LeftCancelSemigroup M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Injective.leftCancelSemigroup f hf mul =
    { toSemigroup := Function.Injective.semigroup f hf mul, toIsLeftCancelMul := ⋯ }
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_right_of_left_le'' : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {x y z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β},
  ConvexOn 𝕜 s f → x ∈ s → z ∈ s → x < y → y ≤ z → f x ≤ f y → f y ≤ f z
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_monoidHom_refl : ∀ {M : Type u_4} [inst : MulOneClass M], ↑(MulEquiv.refl M) = MonoidHom.id M
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.comp_apply : ∀ {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A bivariate polynomial `Q₁` that satisfies `Q₁ * Φ = θ`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₁ : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → Polynomial (Polynomial K)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Finite.measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α}, s.Finite → MeasurableSet s
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve division.

See note [hom simp lemma priority]  -/
map_div : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
  [MonoidHomClass F G H] (f : F) (a b : G), f (a / b) = f a / f b
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_sub : ∀ (R : Type u) {M : Type v} [inst : SubNegZeroMonoid R] [inst_1 : Sub M] (m₁ m₂ : M),
  TrivSqZeroExt.inr (m₁ - m₂) = TrivSqZeroExt.inr m₁ - TrivSqZeroExt.inr m₂
-- Init.Prelude
Nat.ctorIdx_zero : Nat.ctorIdx 0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_full_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (D : Set C) {c d : C} {f : c ⟶ d},
  f ∈ (CategoryTheory.Subgroupoid.full D).arrows c d ↔ c ∈ D ∧ d ∈ D
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.coe_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜] (s : AbsConvexOpenSets 𝕜 E), ↑s ∈ nhds 0
-- Init.Data.UInt.Bitwise
UInt8.toNat_shiftLeft : ∀ (a b : UInt8), (a <<< b).toNat = a.toNat <<< (b.toNat % 8) % 2 ^ 8
-- Mathlib.RingTheory.HopkinsLevitzki
_private.Mathlib.RingTheory.HopkinsLevitzki.0.IsSemiprimaryRing.finite_of_isNoetherian_or_isArtinian : ∀ (R₀ : Type u_1) (R : Type u_2) (M : Type u) [inst : Ring R₀] [inst_1 : Ring R] [inst_2 : Module R₀ R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R]
  [inst_8 : IsScalarTower R₀ R R] [Module.Finite R₀ (R ⧸ Ring.jacobson R)],
  IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_neg : ∀ {α : Type u_1} {G : Type u_8} [inst : AddGroup G] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ G),
  Finsupp.filter p (-f) = -Finsupp.filter p f
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x : α),
  ⇑e ⁻¹' Set.Iio (e x) = Set.Iio x
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertYear : Std.Time.Year → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Analysis.Fourier.ZMod
/-- Fourier inversion formula, discrete case.  -/
ZMod.dft_dft : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  ZMod.dft (ZMod.dft Φ) = fun j => ↑N • Φ (-j)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_zsmul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (x : G) (n : ℤ),
  SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x
-- Mathlib.CategoryTheory.Retract
/-- If a morphism `f` is a retract of `g`, then `f.op` is a retract of `g.op`.  -/
CategoryTheory.RetractArrow.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z W : C} → {f : X ⟶ Y} → {g : Z ⟶ W} → CategoryTheory.RetractArrow f g → CategoryTheory.RetractArrow f.op g.op