mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₂_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {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_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₂.Rel i₂ (c₂.next i₂) → ⋯ = ⋯
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- In a Henstock prepartition, there are at most `2 ^ Fintype.card ι` boxes with a given tag.  -/
BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [inst : Fintype ι],
  π.IsHenstock → ∀ (x : ι → ℝ), {J ∈ π.boxes | π.tag J = x}.card ≤ 2 ^ Fintype.card ι
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey? = some k
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.ControlInfo.mk.sizeOf_spec : ∀ (breaks continues returnsEarly : Bool) (numRegularExits : ℕ) (noFallthrough : Bool) (reassigns : Lean.NameSet),
  sizeOf
      { breaks := breaks, continues := continues, returnsEarly := returnsEarly, numRegularExits := numRegularExits,
        noFallthrough := noFallthrough, reassigns := reassigns } =
    1 + sizeOf breaks + sizeOf continues + sizeOf returnsEarly + sizeOf numRegularExits + sizeOf noFallthrough +
      sizeOf reassigns
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_eq_ofNat : ∀ n < UInt32.size, UInt32.ofNatClamp n = UInt32.ofNat n
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C) (i : CategoryTheory.Arrow.leftFunc ⟶ Z)
  (p : Z ⟶ CategoryTheory.Arrow.rightFunc)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam)
  (hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) (hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f))
  (Z_1 : CategoryTheory.Functor (CategoryTheory.Arrow C) C) (i_1 : CategoryTheory.Arrow.leftFunc ⟶ Z_1)
  (p_1 : Z_1 ⟶ CategoryTheory.Arrow.rightFunc)
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 p_1 = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam)
  (hi_1 : ∀ (f : CategoryTheory.Arrow C), W₁ (i_1.app f)) (hp_1 : ∀ (f : CategoryTheory.Arrow C), W₂ (p_1.app f)),
  ({ Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
      { Z := Z_1, i := i_1, p := p_1, fac := fac_1, hi := hi_1, hp := hp_1 }) =
    (Z = Z_1 ∧ i ≍ i_1 ∧ p ≍ p_1)
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.instIsIrreducibleRootSystem_of_isSimple : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_5 : H.IsCartanSubalgebra]
  [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsSimple K L],
  (LieAlgebra.IsKilling.rootSystem H).IsIrreducible
-- ProofWidgets.Component.OfRpcMethod
/-- The elaborator `mk_rpc_widget%` allows writing certain widgets in Lean instead of JavaScript.
Specifically, it translates an RPC method of type `MyProps → RequestM (RequestTask Html)`
into a widget component of type `Component MyProps`.

Even more specifically, we can write:
```lean
open Lean Server

structure MyProps where
  ...
  deriving RpcEncodable

@[server_rpc_method]
def MyComponent.rpc (ps : MyProps) : RequestM (RequestTask Html) :=
  ...

@[widget_module]
def MyComponent : Component MyProps :=
  mk_rpc_widget% MyComponent.rpc
```

This is convenient because we can program the logic that computes an output HTML tree
given input props in Lean directly.

⚠️ However, note that there are several limitations on what such component can do
compared to ones written natively in TypeScript or JavaScript:
- It must be pure, i.e. cannot directly store any React state.
  Child components may store state as usual.
- It cannot pass closures as props to the child components that it returns.
  For example, it is not currently possible to write click event handlers in Lean
  and pass them to a `<button onClick={..}>` child.
- Every time the input props change, the infoview has to send a message to the Lean server
  in order to invoke the RPC method.
  Thus there can be a noticeable visual delay between the input props changing
  and the display updating.
  Consequently, components whose props change at a high frequency
  (e.g. depending on the mouse position)
  should not be implemented using this method.

💡 Note that an inverse transformation is already possible.
Given `MyComponent : Component MyProps`, we can write:
```lean
open Lean Server

@[server_rpc_method]
def MyComponent.rpc (ps : MyProps) : RequestM (RequestTask Html) :=
  RequestM.asTask do
    return Html.ofComponent MyComponent ps #[]
```
 -/
ProofWidgets.«termMk_rpc_widget%_» : Lean.ParserDescr
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- The entropy of `T` restricted to `F`, obtained by taking the supremum
of `coverEntropyInfEntourage` over entourages. Note that this supremum is approached by taking
small entourages. This second version uses a `liminf`, and is chosen as an alternative
definition for topological entropy.  -/
Dynamics.coverEntropyInf : {X : Type u_1} → [UniformSpace X] → (X → X) → Set X → EReal
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_toAddSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {x : R}, x ∈ s.toAddSubmonoid ↔ x ∈ s
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_le_one_div : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I : Submodule R A}, 1 ≤ 1 / I ↔ I ≤ 1
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.mk : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α},
  (∃ i, p i) → (∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j) → Filter.IsBasis p s
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.id.inj : ∀ {e : Lean.Expr} {isoLift : Mathlib.Tactic.BicategoryLike.IsoLift} {f : Mathlib.Tactic.BicategoryLike.Mor₁}
  {e_1 : Lean.Expr} {isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift} {f_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f = Mathlib.Tactic.BicategoryLike.Mor₂.id e_1 isoLift_1 f_1 →
    e = e_1 ∧ isoLift = isoLift_1 ∧ f = f_1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.zeroSection.eq_1 : ∀ {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : (x : B) → Zero (E x)] (x : B),
  Bundle.zeroSection F E x = ⟨x, 0⟩
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.unitsOfForallIsUnit_apply : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : NormedRing R] [inst_2 : CompleteSpace R]
  {f : C(X, R)} (h : ∀ (x : X), IsUnit (f x)) (x : X), (ContinuousMap.unitsOfForallIsUnit h) x = ⋯.unit
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A ⟶ K.X i')
  (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) {Z : C} (h : K.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj ⋯) (CategoryTheory.CategoryStruct.comp (K.homologyπ i) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_bilinear_hasDerivAt_eq_sub : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {L : E →L[ℝ] F →L[ℝ] G} {u : ℝ → E} {v : ℝ → F} {u' : ℝ → E} {v' : ℝ → F} {m n : G} [CompleteSpace G],
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (fun x => (L (u x)) (v' x) + (L (u' x)) (v x)) MeasureTheory.volume →
        Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atBot (nhds m) →
          Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atTop (nhds n) →
            ∫ (x : ℝ), (L (u x)) (v' x) + (L (u' x)) (v x) = n - m
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M},
  IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂ ↔ ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- In a bicategory, we can compose the 1-morphisms `f : a ⟶ b` and `g : b ⟶ c` to obtain
a 1-morphism `f ≫ g : a ⟶ c`. This composition does not need to be strictly associative,
but there is a specified associator, `α_ f g h : (f ≫ g) ≫ h ≅ f ≫ (g ≫ h)`.
There is an identity 1-morphism `𝟙 a : a ⟶ a`, with specified left and right unitor
isomorphisms `λ_ f : 𝟙 a ≫ f ≅ f` and `ρ_ f : f ≫ 𝟙 a ≅ f`.
These associators and unitors satisfy the pentagon and triangle equations.

See https://ncatlab.org/nlab/show/bicategory.
 -/
CategoryTheory.Bicategory : Type u → Type (max (max u (v + 1)) (w + 1))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.minKey! = default
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.top_mul_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α], ⊤ * ⊤ = ⊤
-- Init.MetaTypes
/-- If false (default: true), extracts only top-level lets, otherwise allows descending into subterms.
When false, `proofs` and `types` are ignored, and lets appearing in the types or values of the
top-level lets are not themselves extracted.  -/
Lean.Meta.ExtractLetsConfig.descend : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Data.Set.Image
Function.Injective.subsingleton_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ {s : Set α}, (f '' s).Subsingleton ↔ s.Subsingleton
-- LeanSearchClient.Syntax
LeanSearchClient.getLeanSearchQueryJson : String → optParam ℕ 6 → Lean.CoreM (Array Lean.Json)
-- Mathlib.Algebra.Group.Basic
neg_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a = 0 ↔ a = 0
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_eq_zero_iff : ∀ {n : ℕ} {b : Bool}, Nat.bit b n = 0 ↔ n = 0 ∧ b = false
-- Mathlib.Algebra.Algebra.Operations
Submodule.bot_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), ⊥ * M = ⊥
-- Mathlib.Algebra.Lie.Derivation.Killing
LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal : ∀ {R : Type u_1} {L : Type u_2} [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  {D : LieDerivation R L L},
  D ∈ (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule →
    ∀ (x : L),
      (LieDerivation.ad R L) (D x) ∈
        Submodule.map (LieDerivation.ad R L).range.subtype (LinearMap.ker (killingForm R ↥(LieDerivation.ad R L).range))
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- The definitions `LieDerivation.ad` and `LieAlgebra.ad` agree.  -/
LieDerivation.coe_ad_apply_eq_ad_apply : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L),
  ↑((LieDerivation.ad R L) x) = (LieAlgebra.ad R L) x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A rotation of a nonzero vector equals that vector if and only if the angle is zero.  -/
Orientation.rotation_eq_self_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → ∀ (θ : Real.Angle), (o.rotation θ) x = x ↔ θ = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G →₀ A` satisfying the 1-cycle condition, produces a 1-cycle for the representation on
`A` induced by the `DistribMulAction`.  -/
groupHomology.cyclesOfIsCycle₁ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              (x : G →₀ A) → groupHomology.IsCycle₁ x → ↥(groupHomology.cycles₁ (Rep.ofDistribMulAction k G A))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j j_1 : ι) (e_j : j = j_1) (hj : c.next i = j)
  (h : K.d i j = 0) [inst_2 : K.HasHomology i], K.isoHomologyι i j hj h = K.isoHomologyι i j_1 ⋯ ⋯
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `CommRing` across an `Equiv`  -/
Equiv.commRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [CommRing β] → CommRing α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- If `A : Cᵒᵖ ⥤ Type v` is a presheaf, then we have an equivalence between presheaves lying over
`A` and the category of presheaves on `CostructuredArrow yoneda A`. There is a quasicommutative
triangle involving this equivalence, see
`CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow`.

This is Lemma 1.4.12 in [Kashiwara2006].  -/
CategoryTheory.overEquivPresheafCostructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Over A ≌
        CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)
-- Mathlib.Data.Num.ZNum
ZNum.of_to_int : ∀ (n : ZNum), ↑↑n = n
-- Mathlib.Data.Part
Part.mem_coe : ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ ↑o ↔ a ∈ o
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.id.injEq : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (f : Mathlib.Tactic.BicategoryLike.Mor₁)
  (e_1 : Lean.Expr) (isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift) (f_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f = Mathlib.Tactic.BicategoryLike.Mor₂.id e_1 isoLift_1 f_1) =
    (e = e_1 ∧ isoLift = isoLift_1 ∧ f = f_1)
-- Mathlib.Probability.Independence.Process.Basic
/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.Kernel.IndepFun.process_indepFun₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  (∀ (i : S), AEMeasurable (X i) (P.bind ⇑κ)) →
    AEMeasurable Y (P.bind ⇑κ) →
      (∀ (I : Finset S), ProbabilityTheory.Kernel.IndepFun (fun ω i => X (↑i) ω) Y κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) Y κ P
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrLeft_apply : ∀ {ι : Type u_4} {ι' : Type u_5} {β : ι' → Type u_6} [inst : (j : ι') → UniformSpace (β j)] (e : ι ≃ ι')
  (a : (b : ι) → β (e.symm.symm b)) (a_1 : ι'),
  (UniformEquiv.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' β e.symm).symm a a_1
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A mixin class for strict multiplicativity of the norm, `‖a * b‖ = ‖a‖ * ‖b‖` (rather than
`≤` as in the definition of `NormedRing`). Many `NormedRing`s satisfy this stronger property,
including all `NormedDivisionRing`s and `NormedField`s.  -/
NormMulClass : (α : Type u_5) → [Norm α] → [Mul α] → Prop
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for universally closed morphisms.  -/
AlgebraicGeometry.UniversallyClosed.of_valuativeCriterion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.ValuativeCriterion.Existence f → AlgebraicGeometry.UniversallyClosed f
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.continuousWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → ContinuousWithinAt f s x
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match a.neg with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_2 a
-- Init.Data.SInt.Lemmas
Int8.ofInt_eq_ofIntLE_div : ∀ {a b : ℤ} (ha₁ : Int8.minValue.toInt ≤ a) (ha₂ : a ≤ Int8.maxValue.toInt) (hb₁ : Int8.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int8.maxValue.toInt), Int8.ofInt (a.tdiv b) = Int8.ofIntLE a ha₁ ha₂ / Int8.ofIntLE b hb₁ hb₂
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- The product of a finite family of `OpenPartialHomeomorph`s.  -/
OpenPartialHomeomorph.pi : {ι : Type u_7} →
  [Finite ι] →
    {X : ι → Type u_8} →
      {Y : ι → Type u_9} →
        [inst : (i : ι) → TopologicalSpace (X i)] →
          [inst_1 : (i : ι) → TopologicalSpace (Y i)] →
            ((i : ι) → OpenPartialHomeomorph (X i) (Y i)) → OpenPartialHomeomorph ((i : ι) → X i) ((i : ι) → Y i)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance_eq_balance! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced}
  {hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balance! k v l r
-- Mathlib.Algebra.Module.Injective
/-- A linear map `I ⟶ Q` by `x ↦ f' (x • y)` where `f'` is the maximal extension  -/
Module.Baer.ExtensionOfMaxAdjoin.idealTo : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        (f : M →ₗ[R] Q) →
                          [inst_7 : Fact (Function.Injective ⇑i)] →
                            (y : N) → ↥(Module.Baer.ExtensionOfMaxAdjoin.ideal i f y) →ₗ[R] Q
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemiprimaryRing.mk : ∀ {R : Type u_1} [inst : Ring R],
  IsSemisimpleRing (R ⧸ Ring.jacobson R) → IsNilpotent (Ring.jacobson R) → IsSemiprimaryRing R
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.IdNode.mk.injEq : ∀ (vPos hPosSrc hPosTar : ℕ) (id : Mathlib.Tactic.BicategoryLike.Atom₁) (vPos_1 hPosSrc_1 hPosTar_1 : ℕ)
  (id_1 : Mathlib.Tactic.BicategoryLike.Atom₁),
  ({ vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, id := id } =
      { vPos := vPos_1, hPosSrc := hPosSrc_1, hPosTar := hPosTar_1, id := id_1 }) =
    (vPos = vPos_1 ∧ hPosSrc = hPosSrc_1 ∧ hPosTar = hPosTar_1 ∧ id = id_1)
-- Mathlib.GroupTheory.NoncommCoprod
MulHom.noncommCoprod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Semigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  f.noncommCoprod g comm = { toFun := fun mn => f mn.1 * g mn.2, map_mul' := ⋯ }
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.herglotzRieszKernel.eq_1 : ∀ (c w z : ℂ), herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getKey! : {α : Type u} → {β : α → Type v} → [BEq α] → [Inhabited α] → α → List ((a : α) × β a) → α
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.mem_fixedField_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (H : Subgroup Gal(E/F))
  (x : E), x ∈ IntermediateField.fixedField H ↔ ∀ f ∈ H, f x = x
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.Spec.birdDet.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (A_2 : Matrix (Fin (k + 1)) (Fin (k + 1)) R),
  BirdDet.Spec.birdDet A_2 = (-1) ^ k * (BirdDet.Spec.stepEntry A_2)^[k] A_2 0 0
-- Mathlib.Data.Finset.Max
Finset.min'_erase_ne_self : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty), (s.erase x).min' s0 ≠ x