mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make a morphism in `P.Over Q X` from a morphism in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Over.homMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          {A B : P.Over Q X} →
            (f : A.left ⟶ B.left) →
              autoParam (CategoryTheory.CategoryStruct.comp f B.hom = A.hom)
                  CategoryTheory.MorphismProperty.Over.homMk._auto_1 →
                autoParam (Q f) CategoryTheory.MorphismProperty.Over.homMk._auto_3 → (A ⟶ B)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofChoiceInfo.injEq : ∀ (i i_1 : Lean.Elab.ChoiceInfo), (Lean.Elab.Info.ofChoiceInfo i = Lean.Elab.Info.ofChoiceInfo i_1) = (i = i_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Init.Omega.Constraint
Lean.Omega.Constraint.not_sat_of_isImpossible : ∀ {c : Lean.Omega.Constraint}, c.isImpossible = true → ∀ {t : ℤ}, ¬c.sat t = true
-- Mathlib.GroupTheory.Coset.Basic
rightAddCoset_mem_rightAddCoset : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → AddOpposite.op a +ᵥ ↑s = ↑s
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.rel.refl : ∀ {α : Sort u} {b : α} {x : Lean.Order.FlatOrder b}, x.rel x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸}
  {a' : E →L[𝕜] 𝔸}, HasFDerivAt a a' x → ∀ (b : 𝔸), HasFDerivAt (fun y => b * a y) (b • a') x
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) (f : MvPowerSeries σ R) (p : ℕ),
  MvPowerSeries.IsWeightedHomogeneous w ((MvPowerSeries.weightedHomogeneousComponent w p) f) p
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- A (colimit) cocone over a diagram `F : J ⥤ C` is van Kampen if for every cocone `c'` over the
pullback of the diagram `F' : J ⥤ C'`, `c'` is colimiting iff `c'` is the pullback of `c`.

TODO: Show that this is iff the functor `C ⥤ Catᵒᵖ` sending `x` to `C/x` preserves it.
TODO: Show that this is iff the inclusion functor `C ⥤ Span(C)` preserves it.
 -/
CategoryTheory.IsVanKampenColimit : {J : Type v'} →
  [inst : CategoryTheory.Category.{u', v'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F → Prop
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.reindex_isTotallyUnimodular : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {n' : Type u_4} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R)
  (em : m ≃ m') (en : n ≃ n'), ((Matrix.reindex em en) A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Topology.SeparatedMap
IsLocallyInjective_iff_isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyInjective f ↔ Topology.IsOpenEmbedding (toPullbackDiag f)
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_pos_rat_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x : K},
  0 < x → ∃ q, 0 < q ∧ ↑q < x
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cocone.equivStructuredArrow F).unitIso =
    CategoryTheory.NatIso.ofComponents CategoryTheory.Limits.Cocone.eta ⋯
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.responseError.inj : ∀ {id : Lean.JsonRpc.RequestID} {code : Lean.JsonRpc.ErrorCode} {message : String} {data? : Option Lean.Json}
  {id_1 : Lean.JsonRpc.RequestID} {code_1 : Lean.JsonRpc.ErrorCode} {message_1 : String} {data?_1 : Option Lean.Json},
  Lean.JsonRpc.MessageMetaData.responseError id code message data? =
      Lean.JsonRpc.MessageMetaData.responseError id_1 code_1 message_1 data?_1 →
    id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.lt_ord_of_lt : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {l m : Profinite.NobelingProof.Products I}
  {o : Ordinal.{u}},
  m < l → (∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) → ∀ i ∈ ↑m, Profinite.NobelingProof.ord I i < o
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.RingObjCat C} (f : X ⟶ Y),
  (CategoryTheory.RingObjCat.forget C).map f = f.hom
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A finite product of proper spaces is proper.  -/
pi_properSpace : ∀ {β : Type v} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  [h : ∀ (b : β), ProperSpace (X b)], ProperSpace ((b : β) → X b)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.mul_comm : ∀ (a b : ZNum), a * b = b * a
-- Mathlib.Data.Finite.Defs
Function.Bijective.finite_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → (Finite α ↔ Finite β)
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_iff_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α], Order.pred a = b ↔ b ⋖ a
-- Mathlib.Analysis.MeanInequalitiesPow
Real.pow_arith_mean_le_arith_mean_pow_of_even : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) → ∑ i ∈ s, w i = 1 → ∀ {n : ℕ}, Even n → (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Inv α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s : Finset α) (f : α → β), s⁻¹.inf f = s.inf fun x => f x⁻¹
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.ball_openAddSubgroup.eq_1 : ∀ (S : Type u_1) [inst : SeminormedAddGroup S] [inst_1 : IsUltrametricDist S] {r : ℝ} (hr : 0 < r),
  IsUltrametricDist.ball_openAddSubgroup S hr =
    { carrier := Metric.ball 0 r, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, isOpen' := ⋯ }
-- Mathlib.RingTheory.Valuation.AlgebraInstances
/-- Given an algebra between two field extensions `L` and `E` of a field `K` with a valuation `v`,
create an algebra between their two rings of integers.  -/
ValuationSubring.algebra : {K : Type u_1} →
  [inst : Field K] →
    (v : Valuation K (WithZero (Multiplicative ℤ))) →
      (L : Type u_2) →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            (E : Type u_3) →
              [inst_3 : Field E] →
                [inst_4 : Algebra K E] →
                  [inst_5 : Algebra L E] →
                    [IsScalarTower K L E] →
                      Algebra ↥(integralClosure (↥v.valuationSubring) L) ↥(integralClosure (↥v.valuationSubring) E)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addXYZ P Q = (P 1 ^ 2 * Q 2) • Q
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_le_self : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.restrict s ≤ μ
-- Init.Data.Range.Polymorphic.SInt
Int16.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int16
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.map_pow : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (a : M) (n : ℕ), f (a ^ n) = f a ^ n
-- Init.Data.Nat.Basic
Nat.ne_zero_iff_zero_lt : ∀ {n : ℕ}, n ≠ 0 ↔ 0 < n
-- Mathlib.Computability.Language
instReprSymbol.repr : {T : Type u_4} → {N : Type u_5} → [Repr T] → [Repr N] → Symbol T N → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits, then `F.unop : C ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F],
  CategoryTheory.Limits.PreservesColimits F.unop
-- Mathlib.RepresentationTheory.Basic
Representation.ofDistribMulAction_apply_apply : ∀ {k : Type u_1} {G : Type u_2} {A : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid A]
  [inst_3 : Module k A] [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (g : G) (a : A),
  ((Representation.ofDistribMulAction k G A) g) a = g • a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α),
  Neg.neg '' Set.uIcc a b = Set.uIcc (-a) (-b)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeUnop_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop),
  (CategoryTheory.Limits.coconeOfConeUnop c).ι = CategoryTheory.NatTrans.removeUnop c.π
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSpace.comap_le_comap_pi : ∀ {β : Type u_2} {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {g : (a : δ) → β → X a}
  (a : δ), MeasurableSpace.comap (g a) inferInstance ≤ MeasurableSpace.comap (fun b c => g c b) MeasurableSpace.pi
-- Mathlib.Algebra.Group.Units.Equiv
/-- Left addition in an `AddGroup` is a permutation of the underlying type.  -/
Equiv.addLeft : {G : Type u_5} → [AddGroup G] → G → Equiv.Perm G
-- Init.Omega.Constraint
Lean.Omega.Constraint.addInequality_sat : ∀ {c : ℤ} {x y : Lean.Omega.Coeffs}, c + x.dot y ≥ 0 → { lowerBound := some (-c), upperBound := none }.sat' x y = true
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.range_r_app_union_range_b_app : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ) (n : SimplexCategoryᵒᵖ),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((SSet.relativeCellComplexOfMono.r i d).app n)) ∪
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((SSet.relativeCellComplexOfMono.b i d).app n)) =
    Set.univ
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.fromStructuredArrow_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)}
  (f : X ⟶ Y),
  ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).map f).hom = CategoryTheory.StructuredArrow.Hom.right f
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nndist_eq_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 1 (α × β)), nndist x y = nndist x.fst y.fst + nndist x.snd y.snd
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim.eq_2 : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.rev = b
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the reverse direction of `Order.isSuccLimit_toDual_iff`. -/
Order.IsPredLimit.dual : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsPredLimit a → Order.IsSuccLimit (OrderDual.toDual a)
-- Mathlib.Data.Finset.Max
Multiset.exists_max_image : ∀ {α : Type u_7} {R : Type u_8} [inst : LinearOrder R] (f : α → R) {s : Multiset α}, s ≠ 0 → ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The power basis `{1, Y}` for `R[W]` over `R[X]`.  -/
WeierstrassCurve.Affine.CoordinateRing.basis : {R : Type r} →
  [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → Module.Basis (Fin 2) (Polynomial R) W'.CoordinateRing
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero.eq_2 : ∀ (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.zero =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
      fun x => 0
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_sInf : ∀ {M : Type u_2} [inst : Mul M] (S : Set (Subsemigroup Mᵐᵒᵖ)), (sInf S).unop = sInf (Subsemigroup.op ⁻¹' S)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isOpenMap_over : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme), IsOpenMap ⇑(AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
_private.Mathlib.Combinatorics.Additive.PluenneckeRuzsa.0.Finset.mul_aux : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A B C : Finset G},
  A.Nonempty →
    A ⊆ B →
      (∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card) →
        ∀ A' ⊆ A, (A * C).card * A'.card ≤ (A' * C).card * A.card
-- Init.Data.Option.Lemmas
Option.mem_filter_iff : ∀ {α : Type u_1} {p : α → Bool} {a : α} {o : Option α}, a ∈ Option.filter p o ↔ a ∈ o ∧ p a = true
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instSMulDistribClass : ∀ (K : Type u_1) [inst : Field K] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulSemiringAction G K],
  SMulDistribClass G (NumberField.RingOfIntegers K) K
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.mk.sizeOf_spec : ∀ (propagateUp propagateDown : Lean.Meta.Grind.Propagator) (evalTactic : Lean.Meta.Grind.EvalTactic),
  sizeOf { propagateUp := propagateUp, propagateDown := propagateDown, evalTactic := evalTactic } = 1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt_symmₗ : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Trivialization.linearMapAt R e b) ((Bundle.Trivialization.symmₗ R e b) y) = y
-- Mathlib.Data.Finset.Card
Finset.strongInduction_eq : ∀ {α : Type u_1} {p : Finset α → Sort u_4} (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) (s : Finset α),
  Finset.strongInduction H s = H s fun t x => Finset.strongInduction H t
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.other.sizeOf_spec : ∀ (name : Lean.Name), sizeOf (Lean.Meta.Origin.other name) = 1 + sizeOf name
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [inst_3 : DistribSMul R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x → ∀ (c : R), iteratedDeriv n (c • f) x = c • iteratedDeriv n f x
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_toDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRightRegular (OrderDual.toDual a) ↔ IsAddRightRegular a
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.instMonadGetStructM : Lean.Meta.Grind.AC.MonadGetStruct Lean.Meta.Grind.AC.M✝
-- Mathlib.Order.Filter.Finite
Filter.eventually_all_finset : ∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
  (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.bayesRisk_fintype : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : Fintype Θ] [MeasurableSingletonClass Θ],
  ProbabilityTheory.bayesRisk ℓ P π =
    ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ∑ θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}
-- Lean.Meta.Tactic.TryThis
/-- Returns the syntax for an `exact` or `refine` (as indicated by `useRefine`) tactic corresponding to
`e` as well as a `MessageData` representation with hover information.
If `exposeNames` is `true`, prepends the tactic with `expose_names.` Note that the tactic is
always generated within `withExposedNames` to avoid generating unprintable characters.
 -/
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.mkExactSuggestionSyntax : Lean.Expr → Bool → Lean.MetaM (Lean.TSyntax `tactic × Lean.MessageData)
-- Mathlib.Order.DirectedInverseSystem
/-- A directed system is a functor from a category (directed poset) to another category.  -/
DirectedSystem : {ι : Type u_1} → [inst : Preorder ι] → (F : ι → Type u_4) → (⦃i j : ι⦄ → i ≤ j → F i → F j) → Prop
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_refl : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  ↑AlgEquiv.refl = LinearEquiv.refl R A₁
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.tensorHom_hom : ∀ {R : Type u} [inst : CommRing R] {A B C D : CommAlgCat R} (f : A ⟶ C) (g : B ⟶ D),
  CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    Algebra.TensorProduct.map (CommAlgCat.Hom.hom f) (CommAlgCat.Hom.hom g)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.levels : Lean.Elab.Structural.IndGroupInst → List Lean.Level
-- Std.Http.Data.Response
Std.Http.Response.Builder.mk.injEq : ∀ (line : Std.Http.Response.Head) (extensions : Std.Http.Extensions) (line_1 : Std.Http.Response.Head)
  (extensions_1 : Std.Http.Extensions),
  ({ line := line, extensions := extensions } = { line := line_1, extensions := extensions_1 }) =
    (line = line_1 ∧ extensions = extensions_1)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedOfMonoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f], AlgebraicGeometry.QuasiSeparated f
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.nndist_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x y : EuclideanSpace 𝕜 n),
  nndist x y = NNReal.sqrt (∑ i, nndist (x.ofLp i) (y.ofLp i) ^ 2)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Semiring (Unitization R A)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.instDecidableNoSibling : {α : Type u_1} → {s : Batteries.PairingHeapImp.Heap α} → Decidable s.NoSibling
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) → [grp : CategoryTheory.GrpObj X] → CategoryTheory.Grp C
-- Mathlib.Data.ZMod.Basic
AddSubgroupClass.coe_zmod_smul : ∀ {n : ℕ} {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  {K : S} [inst_3 : Module (ZMod n) G] (a : ZMod n) (x : ↥K), ↑(a • x) = a • ↑x
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Entails.eval : {α : Type u} → {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Entails α β] → (α → Bool) → β → Prop
-- Mathlib.RingTheory.Multiplicity
Finset.emultiplicity_prod : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {β : Type u_3} {p : α},
  Prime p → ∀ (s : Finset β) (f : β → α), emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.handleMutual : Lean.Linter.MissingDocs.Handler
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.ofSubcomplex_faces : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset : faces ⊆ K.faces)
  (down_closed : IsLowerSet faces), (K.ofSubcomplex faces subset down_closed).faces = faces
-- Mathlib.Analysis.RCLike.Basic
RCLike.conjAe_coe : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.conjAe = ⇑(starRingEnd K)
-- Mathlib.LinearAlgebra.Basis.Basic
LinearEquiv.ofEq.congr_simp : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p q : Submodule R M) (h : p = q), LinearEquiv.ofEq p q h = LinearEquiv.ofEq p q h
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_eq_zero : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I = 0 → ∀ (z : K), RCLike.im z = 0
-- Init.Data.Format.Basic
Std.Format.tag.sizeOf_spec : ∀ (a : ℕ) (a_1 : Std.Format), sizeOf (Std.Format.tag a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Order.Rel.GaloisConnection
/-- `rightDual` maps every element `I` to `leftFixedPoints`.  -/
SetRel.rightDual_mem_leftFixedPoint : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (I : Set β), R.rightDual I ∈ R.leftFixedPoints
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.nhdsNE_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜}, f₁ =ᶠ[nhdsWithin x {x}ᶜ] f → deriv f₁ =ᶠ[nhdsWithin x {x}ᶜ] deriv f
-- Init.Data.String.Defs
String.instLEPos_1 : {s : String.Slice} → LE s.Pos
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.copy_ok : ∀ (q : Turing.PartrecToTM2.Λ') (s : Option Turing.PartrecToTM2.Γ') (a b c d : List Turing.PartrecToTM2.Γ'),
  StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some q.copy, var := s, stk := Turing.PartrecToTM2.K'.elim a b c d }
    { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (b.reverseAux a) [] c (b.reverseAux d) }
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getElem!_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], m₁.Equiv m₂ → m₁[k]! = m₂[k]!
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {B : Set X} {f : X → ENNReal},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      Measurable f → MeasurableSet B → ∀ (x₀ : X), ∫⁻ (x : X) in B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_modify_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : (t.modify k f).isEmpty = false}, (t.modify k f).minKey he = t.minKey ⋯
-- Mathlib.Order.Category.BddLat
BddLat.hom_comp : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z),
  Lat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Lat.Hom.hom g).comp (Lat.Hom.hom f)