mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GCDMonoid.Nat
Int.associated_iff : ∀ {a b : ℤ}, Associated a b ↔ a = b ∨ a = -b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a b c : B} {a' : C} (f : a ⟶ b)
  (g : b ⟶ c) (h : G.obj c ⟶ a') {Z : F.obj a ⟶ a'}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))
          h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Bicategory.associator (η.app a)
                          (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom
                      h_1))))))))
-- Aesop.Forward.Match.Types
Aesop.instInhabitedCompleteMatch.default : Aesop.CompleteMatch
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mk.inj : ∀ {α : Type u} {task task_1 : Task α}, { task := task } = { task := task_1 } → task = task_1
-- Mathlib.Data.Finset.Image
Finset.map_refl : ∀ {α : Type u_1} {s : Finset α}, Finset.map (Function.Embedding.refl α) s = s
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- The `L`-series of a modular form (including its Archimedean `Γ`-factor).  -/
ModularForm.Λ : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.IsArithmetic] →
    {k : ℤ} → 0 < k → {F : Type u_1} → [inst : FunLike F UpperHalfPlane ℂ] → F → [ModularFormClass F Γ k] → ℂ → ℂ
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.projSup_map : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {ι : Type v}
  (Us : ι → TopologicalSpace.Opens X)
  {X_1 Y : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X)} (e : X_1 ⟶ Y),
  (Alexandrov.projSup Us).map e = (CategoryTheory.ObjectProperty.homMk (CategoryTheory.homOfLE ⋯)).op
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toEmbedding : M ↪ N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
      FirstOrder.Language.Embedding.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Embedding.map_rel'._autoParam)
  (toEmbedding_1 : M ↪ N)
  (map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding_1.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEmbedding_1.toFun ∘ x))
      FirstOrder.Language.Embedding.map_fun'._autoParam)
  (map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEmbedding_1.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Embedding.map_rel'._autoParam),
  ({ toEmbedding := toEmbedding, map_fun' := map_fun', map_rel' := map_rel' } =
      { toEmbedding := toEmbedding_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 }) =
    (toEmbedding = toEmbedding_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- This could be a general list definition, but it is also somewhat specialized to this
application. `splitAtPred p L` will search `L` for the first element satisfying `p`.
If it is found, say `L = l₁ ++ a :: l₂` where `a` satisfies `p` but `l₁` does not, then it returns
`(l₁, some a, l₂)`. Otherwise, if there is no such element, it returns `(L, none, [])`.  -/
Turing.PartrecToTM2.splitAtPred : {α : Type u_1} → (α → Bool) → List α → List α × Option α × List α
-- Mathlib.NumberTheory.ClassNumber.FunctionField
FunctionField.RingOfIntegers.instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers : (Fq : Type u_1) →
  (F : Type u_2) →
    [inst : Field Fq] →
      [Fintype Fq] →
        [inst_2 : Field F] →
          [inst_3 : Algebra (Polynomial Fq) F] →
            [inst_4 : Algebra (RatFunc Fq) F] →
              [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] →
                [FunctionField Fq F] →
                  [Algebra.IsSeparable (RatFunc Fq) F] → Fintype (ClassGroup ↥(FunctionField.ringOfIntegers Fq F))
-- Batteries.Data.PairingHeap
/-- It is an empty heap.  -/
Batteries.PairingHeapImp.Heap.WF.nil : ∀ {α : Type u_1} {le : α → α → Bool}, Batteries.PairingHeapImp.Heap.WF le Batteries.PairingHeapImp.Heap.nil
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] (f : α → β), MeasureTheory.VectorMeasure.map 0 f = 0
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_ord_toType : ∀ (c : Cardinal.{u_1}), Cardinal.mk c.ord.ToType = c
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).contains k = true → m₁.contains k = false → m₂.contains k = true
-- Mathlib.Data.Set.Function
Set.SurjOn.surjective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.SurjOn f s Set.univ → Function.Surjective f
-- Mathlib.Data.Set.Function
Set.EqOn.comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f₁ f₂ : α → β} {g : β → γ},
  Set.EqOn f₁ f₂ s → Set.EqOn (g ∘ f₁) (g ∘ f₂) s
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerToAddOpposite_symm_apply_coe : ∀ {M : Type u_2} [inst : Add M] (r : ↥(AddSubsemigroup.center Mᵃᵒᵖ)),
  ↑(AddSubsemigroup.centerToAddOpposite.symm r) = AddOpposite.unop ↑r
-- Mathlib.RingTheory.FractionalIdeal.Operations
Ideal.fg_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  Function.Injective ⇑(algebraMap R P) → ∀ (I : Ideal R), IsUnit ↑I → I.FG
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  AlgebraicTopology.DoldKan.QInfty.f n = (AlgebraicTopology.DoldKan.Q n).f n
-- Mathlib.Data.List.Pairwise
/-- **Alias** of the reverse direction of `List.pwFilter_eq_self`. -/
List.Pairwise.pwFilter : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {l : List α}, List.Pairwise R l → List.pwFilter R l = l
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) {X₁ Y₁ : C₁}
  (f : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃),
  (((CategoryTheory.Functor.curry₃.obj F).map f).app X₂).app X₃ =
    F.map (f, CategoryTheory.CategoryStruct.id X₂, CategoryTheory.CategoryStruct.id X₃)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.dedup_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {n : ℕ}, n ≠ 0 → (n • s).dedup = s.dedup
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {x x_1 : B} (f : x ⟶ x_1),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.congr_linearEquiv_symm : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommGroup W] [inst_4 : Module R W] (e : V ≃ₗ[R] W),
  (SpecialLinearGroup.congr_linearEquiv e).symm = SpecialLinearGroup.congr_linearEquiv e.symm
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (f.insertRupUnits units).1.ratUnits = f.ratUnits
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (inner inner_1 : Std.DTreeMap.Internal.Impl α β)
  (e_inner : inner = inner_1) (wf : inner.WF), { inner := inner, wf := wf } = { inner := inner_1, wf := ⋯ }
-- Mathlib.Data.Rel
SetRel.comp_eq_self : ∀ {α : Type u_1} {R : SetRel α α} [R.IsRefl] [R.IsTrans], R.comp R = R
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.resolutionMap_comp : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) (i : ℕ),
  ContinuousCohomology.resolutionMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g)
      i =
    CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map (ContinuousCohomology.resolutionMap φ f i))
      (ContinuousCohomology.resolutionMap ψ g i)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.comp_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1),
  f.comp (AffineMap.lineMap p₀ p₁) = AffineMap.lineMap (f p₀) (f p₁)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShift_of_leftAdjoint : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A], adj.CommShift A
-- Mathlib.Order.FixedPoints
/-- **Knaster-Tarski Theorem**: The fixed points of `f` form a complete lattice.  -/
fixedPoints.completeLattice : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → CompleteLattice ↑(Function.fixedPoints ⇑f)
-- Mathlib.Data.Multiset.Fintype
Multiset.toEnumFinset_subset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {m₁ m₂ : Multiset α}, m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_pair`. -/
EMetric.diam_pair : ∀ {X : Type u_2} {x y : X} [inst : PseudoEMetricSpace X], Metric.ediam {x, y} = edist x y
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.IsEntriesNode.mk : ∀ {α : Type u_1} {β : Type u_2} (entries : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  Lean.PersistentHashMap.IsEntriesNode (Lean.PersistentHashMap.Node.entries entries)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.instLawfulIteratorLoopDefaultImplementation : ∀ {β : Type w} (α : Type w) (m : Type w → Type w') (n : Type x → Type x') [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : Std.Iterator α m β] [Std.Iterators.Finite α m], Std.LawfulIteratorLoop α m n
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the `n`th power of a field element `x` (with `n : ℤ`)
is `|n|` times the logarithmic height of `x`.  -/
Height.logHeight₁_zpow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K) (n : ℤ),
  Height.logHeight₁ (x ^ n) = ↑n.natAbs * Height.logHeight₁ x
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Raw.Const.ofList : {α : Type u} →
  {β : Type v} →
    List (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.Const.ofList._auto_1) → Std.DTreeMap.Raw α (fun x => β) cmp
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.mk : Std.HashSet UInt64 → Lean.FVarIdSet → Lean.Meta.Grind.Arith.CollectDecVars.State
-- Mathlib.Algebra.Lie.Extension
/-- An equivalence of extended Lie algebras induced by translation by a coboundary.  -/
LieAlgebra.LieEquiv.ofCoboundary : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) →
                      (x : LieModule.Cohomology.oneCochain R L M) →
                        ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x →
                          LieAlgebra.ofTwoCocycle c ≃ₗ⁅R⁆ LieAlgebra.ofTwoCocycle c'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- An additive monoid object `M` is commutative if and only if `X ⟶ M` is commutative for all
`X`.  -/
CategoryTheory.isCommAddMonObj_iff_isAddCommutative : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommAddMonObj M ↔ ∀ (X : C), IsAddCommutative (X ⟶ M)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.extract.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → String.Pos.Raw → Sort u_1) (s : String) (b e : String.Pos.Raw)
  (h_1 : (s : String) → (b e : String.Pos.Raw) → motive s b e),
  (match s, b, e with
    | s, b, e => h_1 s b e) =
    h_1 s b e
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- If `i : X ⟶ Y` is a monomorphism of simplicial sets, then it is a relative cell
complex with basic cells given by boundary inclusions `∂Δ[d] ⟶ Δ[d]`, one for each
nondegenerate `d`-simplex of `Y` not in the range of `X`.  -/
SSet.relativeCellComplexOfMono : {X Y : SSet} →
  (i : X ⟶ Y) → [CategoryTheory.Mono i] → HomotopicalAlgebra.RelativeCellComplex (fun n x => (SSet.boundary n).ι) i
-- Std.Data.Iterators.Producers.Slice
/-- Returns an iterator over the given slice. This iterator will emit the elements of the slice
in increasing order of the indices.
 -/
Std.Slice.iter : {γ : Type u_1} → {α β : Type u_2} → [Std.ToIterator (Std.Slice γ) Id α β] → Std.Slice γ → Std.Iter β
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mem_ofSubmodule'_iff : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} {N : Submodule (MonoidAlgebra A G) ρ.asModule} {w : W},
  w ∈ Subrepresentation.ofSubmodule' N ↔ w ∈ N
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `avgRisk_const_right` for a simpler result when `P` is a Markov kernel.  -/
ProbabilityTheory.avgRisk_const_right' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (ν : MeasureTheory.Measure 𝓨)
  (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ P (ProbabilityTheory.Kernel.const 𝓧 ν) π =
    ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂ν ∂π
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app._auto_1),
  (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso C n).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X)))
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_powerset : ∀ (x : ZFSet.{u}), x.powerset.card = 2 ^ x.card
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A single point is coplanar.  -/
coplanar_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), Coplanar k {p}
-- Std.Time.Time.Unit.Second
Std.Time.Second.instOrdOrdinal : {leap : Bool} → Ord (Std.Time.Second.Ordinal leap)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_assoc : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ s₃ : Finset α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.dedup_add : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), (s + t).dedup = s.ndunion t.dedup
-- Init.Data.String.Basic
String.Slice.Pos.toReplaceEnd : {s : String.Slice} → (p₀ pos : s.Pos) → pos ≤ p₀ → (s.sliceTo p₀).Pos
-- Init.Data.Iterators.Consumers.Loop
/-- An implementation of `for h : ... in ... do ...` notation for partial iterators.
 -/
Std.Iter.Partial.instForIn' : {α β : Type w} →
  {n : Type x → Type x'} →
    [Monad n] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id n] →
          ForIn' n (Std.Iter.Partial β) β { mem := fun it out => it.it.IsPlausibleIndirectOutput out }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Lean.Util.CollectAxioms
/-- Cache mapping constants to their (sorted) axiom dependencies.  -/
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.seen : Lean.CollectAxioms.State✝ → Lean.NameMap (Array Lean.Name)
-- Mathlib.Probability.Moments.SubGaussian
/-- Auxiliary lemma for `ae_eq_zero_of_hasSubgaussianMGF_zero'`.  -/
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ},
  Measurable X → ProbabilityTheory.Kernel.HasSubgaussianMGF X 0 κ ν → X =ᵐ[ν.bind ⇑κ] 0
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_X : ∀ {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] (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
  (P : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.FunctorExtension₁.obj F).obj P).X = (F.obj P.X).X
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.row_ne_zero : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nontrivial R]
  (g : Matrix.SpecialLinearGroup n R) (i : n), ↑g i ≠ 0
-- Mathlib.Algebra.Order.Field.Power
/-- **Alias** of the reverse direction of `Odd.zpow_neg_iff`. -/
Odd.zpow_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → a < 0 → a ^ n < 0
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [CategoryTheory.Balanced C] [S.HasHomology],
  S.Exact ∧ CategoryTheory.Mono S.f ↔
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
-- Mathlib.Order.Nucleus
Nucleus.coe_top : ∀ {X : Type u_1} [inst : SemilatticeInf X] [inst_1 : OrderTop X], ⇑⊤ = ⊤
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.substrEq.loop.eq_def : ∀ (s1 s2 : String) (off1 off2 stop1 : String.Pos.Raw),
  String.Pos.Raw.substrEq.loop✝ s1 s2 off1 off2 stop1 =
    if _h : off1.byteIdx < stop1.byteIdx then
      have c₁ := String.Pos.Raw.get s1 off1;
      have c₂ := String.Pos.Raw.get s2 off2;
      c₁ == c₂ && String.Pos.Raw.substrEq.loop✝ s1 s2 (off1 + c₁) (off2 + c₂) stop1
    else true
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
CommCStarAlgebra.nnnorm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCommCStarAlgebra A] {a b : A}, a * b = 0 → ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊
-- Init.Grind.ToInt
/-- The embedding into the integers takes addition to addition, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Add : (α : Type u) → [Add α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Algebra.Group.Action.Defs
VAdd.comp.vadd.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : VAdd M α] (g : N → M) (n : N) (a : α),
  VAdd.comp.vadd g n a = g n +ᵥ a
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousOn_iff_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhdsWithin x s