mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.instTrans : Trans Function.Embedding Function.Embedding Function.Embedding
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Peel off a single integral from a `lmarginal` integral at the end (compare with
`lmarginal_insert`, which peels off an integral at the beginning).  -/
MeasureTheory.lmarginal_insert' : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ}, i ∉ s → ∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : X i), f (Function.update x i xᵢ) ∂μ i ∂μ
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- The function underlying this family of bump functions  -/
ContDiffBumpBase.toFun : {E : Type u_3} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → ContDiffBumpBase E → ℝ → E → ℝ
-- Mathlib.Topology.Defs.Filter
/-- A set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.  -/
Topology.term𝓝 : Lean.ParserDescr
-- Aesop.RulePattern.Cache
Aesop.RulePatternCache.mk.inj : ∀ {map map_1 : Std.HashMap Lean.Expr Aesop.RulePatternCache.Entry}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.Cochain₀.inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (γ : CategoryTheory.PresheafOfGroups.ZeroCochain G U) (i : I), γ⁻¹ i = (γ i)⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.comp_right_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : B} (h : Z.right ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).right h =
    CategoryTheory.CategoryStruct.comp f.right (CategoryTheory.CategoryStruct.comp g.right h)
-- Mathlib.Data.List.Sigma
List.kerase_append_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  a ∈ l₁.keys → List.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.mk.sizeOf_spec : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : SizeOf R] [inst_8 : SizeOf M] [inst_9 : SizeOf N] [inst_10 : SizeOf ι]
  (toContinuousMultilinearMap : ContinuousMultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap.toFun v = 0),
  sizeOf { toContinuousMultilinearMap := toContinuousMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
    1 + sizeOf toContinuousMultilinearMap
-- Init.Control.Id
Id.instMonad : Monad Id
-- Mathlib.RingTheory.Spectrum.Prime.Chevalley
PrimeSpectrum.isConstructible_range_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.FinitePresentation → Topology.IsConstructible (Set.range (PrimeSpectrum.comap f))
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
/-- Smooth embedding of `M` into `(E × ℝ) ^ ι`.  -/
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : FiniteDimensional ℝ E] →
          {H : Type uH} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners ℝ E H} →
                {M : Type uM} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      [IsManifold I (↑⊤) M] →
                        [T2Space M] →
                          [inst_8 : Fintype ι] →
                            {s : Set M} →
                              SmoothBumpCovering ι I M s →
                                ContMDiffMap I (modelWithCornersSelf ℝ (ι → E × ℝ)) M (ι → E × ℝ) ↑⊤
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x) → HasDerivWithinAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) s x
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_const_left : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => C + f x) l Filter.atBot
-- Init.Data.Option.List
Option.pairwise_toList : ∀ {α : Type u_1} {P : α → α → Prop} {o : Option α}, List.Pairwise P o.toList
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.of_linearIndependent_row : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {A : Matrix n n R}, LinearIndependent R A.row → A.Nonsingular
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.arg.sizeOf_spec : ∀ (arg : ℕ) (all : Bool) (next : Mathlib.Tactic.Conv.Path),
  sizeOf (Mathlib.Tactic.Conv.Path.arg arg all next) = 1 + sizeOf arg + sizeOf all + sizeOf next
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_eq : ∀ {c : ℝ} {f g : ℕ → Bool} {n : ℕ}, f n = g n → Cardinal.cantorFunctionAux c f n = Cardinal.cantorFunctionAux c g n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM f t = t.toListModel.forM fun a => f a.fst a.snd
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `le_inv_mul_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
 -/
mul_le_of_le_inv_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ c⁻¹ * b → c * a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  {Y Z : Cᴹᵒᵖ} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).unmop =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.unmop X.unmop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id_assoc : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (CategoryTheory.CategoryStruct.id d))
      h =
    h
-- Mathlib.Topology.Algebra.Constructions
AddUnits.continuous_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : AddMonoid N] {f : M →+ N}, Continuous ⇑f → Continuous ⇑(AddUnits.map f)
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.nilpotencyClass_le_one_iff : ∀ {G : Type u_1} [inst : Group G] [Group.IsNilpotent G], Group.nilpotencyClass G ≤ 1 ↔ IsMulCommutative G
-- Mathlib.Topology.Continuous
continuousAt_def : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X},
  ContinuousAt f x ↔ ∀ A ∈ nhds (f x), f ⁻¹' A ∈ nhds x
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- `RingFunc.neg`, but with the defeq type `Language.ring.Functions 1` instead
of `RingFunc 1`  -/
FirstOrder.Ring.negFunc : FirstOrder.Language.ring.Functions 1
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.sSup_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S : Set (CategoryTheory.Subfunctor F)) (U : C), (sSup S).obj U = sSup ((fun T => T.obj U) '' S)
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivAt_abs_neg : ∀ {x : ℝ}, x < 0 → HasDerivAt (fun x => |x|) (-1) x
-- Mathlib.Order.Category.HeytAlg
_private.Mathlib.Order.Category.HeytAlg.0.HeytAlg.Hom.mk.injEq : ∀ {X Y : HeytAlg} (hom' hom'_1 : HeytingHom ↑X ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter (fun k x => f k) t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true)
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.rootSet.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] (I : LieIdeal K L),
  I.rootSet = {α | LieAlgebra.rootSpace H ⇑↑α ≤ LieSubmodule.restr I H}
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_inv_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) (X_1 : A),
  (CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.1.obj X_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filterMap f m) k =
    ((Std.ExtDHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Presieve.overEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X)
  (S' : CategoryTheory.Presieve Y.left),
  (RelIso.symm (CategoryTheory.Presieve.overEquiv Y)) S' =
    CategoryTheory.Presieve.functorPullback (CategoryTheory.Over.forget X) S'
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofList_equiv_foldl : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List (α × β)},
  (Std.HashMap.Raw.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- Cyclically permute 3 nested instances of `Finset.prod`.  -/
Finset.prod_comm_cycle : ∀ {κ : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α}
  {u : Finset κ} {f : γ → α → κ → β}, ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β}, k ∈ t₂ → Std.ExtDTreeMap.Const.getD (t₁ \ t₂) k fallback = fallback
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.symm : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ : Set (Set Ω)},
  ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ → ProbabilityTheory.CondIndepSets m' hm' s₂ s₁ μ
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse.eq_2 : ∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a : V} (x b : V) (p : Quiver.Path a b) (e : b ⟶ x),
  (p.cons e).reverse = (Quiver.reverse e).toPath.comp p.reverse
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The structure for rewrite lemmas stored in the `RefinedDiscrTree`.  -/
Mathlib.Tactic.LibraryRewrite.RewriteLemma : Type
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_symm : ∀ {α : Type u_1}, FreeAddMonoid.toList.symm = FreeAddMonoid.ofList
-- Mathlib.RingTheory.Smooth.Flat
RingHom.Smooth.flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Smooth → f.Flat
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_inv : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Inv (γ a b)]
  (x : (a : α) → (b : β a) → γ a b), Sigma.uncurry x⁻¹ = (Sigma.uncurry x)⁻¹
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- The indexed suprema of two functions are comparable if the functions are pointwise comparable  -/
Directed.ciSup_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {f g : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f →
    Directed (fun x1 x2 => x1 ≤ x2) g → BddAbove (Set.range g) → (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup g
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- A typeclass carrying a choice of lift of an object from `C` to `FreeMonoidalCategory C`.
It must be the case that `projectObj id (LiftObj.lift x) = x` by defeq.  -/
Mathlib.Tactic.Coherence.LiftObj : {C : Type u} → C → Type u
-- Mathlib.Analysis.Normed.Affine.AddTorsor
DilationEquiv.smulTorsor_preimage_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] {P : Type u_3} [inst_4 : PseudoMetricSpace P] [inst_5 : NormedAddTorsor E P] {c : P}
  {k : 𝕜} (hk : k ≠ 0), ⇑(DilationEquiv.smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.inv.match_1.splitter : {ι : Type u_1} →
  {G : ι → Type u_2} →
    [inst : (i : ι) → Group (G i)] →
      (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord G x x_1 → Sort u_3) →
        (x x_1 : ι) →
          (x_2 : Monoid.CoprodI.NeWord G x x_1) →
            ((x : ι) → (x_3 : G x) → (h : x_3 ≠ 1) → motive x x (Monoid.CoprodI.NeWord.singleton x_3 h)) →
              ((x x_3 j k : ι) →
                  (w₁ : Monoid.CoprodI.NeWord G x j) →
                    (h : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord G k x_3) → motive x x_3 (w₁.append h w₂)) →
                motive x x_1 x_2
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_univ_prod_of_one_le' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} [MulLeftMono N]
  [inst_3 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 1 ≤ f x) → ∏ x ∈ s, f x ≤ ∏ x, f x
-- Mathlib.Order.Irreducible
InfPrime.infIrred : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfPrime a → InfIrred a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Mathlib.Data.Real.Basic
Real.instMul : Mul ℝ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomHomBraiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] {X Y : C} [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y], CategoryTheory.IsAddMonHom (β_ X Y).hom
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.minimaxRisk.eq_1 : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  [inst : MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧),
  ProbabilityTheory.minimaxRisk ℓ P =
    ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ⨆ θ, ∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.π_homologyIsoSc'_inv : ∀ {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 k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ (K.homologyIsoSc' i j k hi hk).inv =
    CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.homologyπ j)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.injective_noncommPiCoprod_of_iSupIndep : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y},
  iSupIndep H → Function.Injective ⇑(AddSubgroup.noncommPiCoprod hcomm)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLED.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLED k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).getD fallback
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_eq_pullbackWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_6} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {V : E' → E'} {s : Set E},
  VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V s =
    VectorField.pullbackWithin 𝕜 f V s
-- Mathlib.Tactic.Linter.MinImports
/-- The number of transitive imports needed to build the file up to the current command.  -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.importSize : Mathlib.Linter.ImportState✝ → ℕ
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_zero_add_char : ∀ (c : Char), (0 + c).byteIdx = c.utf8Size
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_mul : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a * b) = ISize.ofBitVec a * ISize.ofBitVec b
-- Mathlib.Order.Interval.Basic
Interval.instUniqueOfIsEmpty : {α : Type u_1} → [inst : LE α] → [IsEmpty α] → Unique (Interval α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.one_cpow : ∀ (x : ℂ), 1 ^ x = 1
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.zero_smul_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] (t : Set β), 0 • t ⊆ 0
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.orthogonal_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  (↑T).rangeᗮ = (↑(ContinuousLinearMap.adjoint T)).ker
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_positive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulMono R M] {x : M},
  x ∈ ConvexCone.positive R M ↔ 0 ≤ x
-- Init.Core
/-- Auxiliary type used to compile `do` notation. It is the same as
`DoResultPRBC α β σ` except that `break` and `continue` are not available
because we are not in a loop context.
 -/
DoResultPR : Type u → Type u → Type u → Type u
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instIsAddApply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}, IsAddApply (ContDiffMapSupportedIn E F n K) E F
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.zpow : ∀ {R : Type u_1} [inst : Group R] [inst_1 : StarMul R] {x : R}, IsSelfAdjoint x → ∀ (n : ℤ), IsSelfAdjoint (x ^ n)
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseNeg : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.negAddCancel : FirstOrder.Field.FieldAxiom
-- Mathlib.Data.Set.Card.Arithmetic
Finset.exists_disjoint_union_of_even_card_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Even s.card ↔ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.card = u.card
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations are transitive.  -/
AddCon.trans : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {x y z : M}, c x y → c y z → c x z
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.sub_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α β : u ⟶ v), (α - β).right = α.right - β.right
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
SeminormedCommRing.mul_comm : ∀ {α : Type u_5} [self : SeminormedCommRing α] (a b : α), a * b = b * a
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instEpiToImage : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y), CategoryTheory.Epi (A.toImage f)
-- Mathlib.RingTheory.Trace.Basic
/-- `embeddingsMatrix A C b : Matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is
`σ (b i)`. It is mostly useful for fields when `Fintype.card κ = finrank A B` and `C` is
algebraically closed.  -/
Algebra.embeddingsMatrix : {κ : Type w} →
  (A : Type u) →
    {B : Type v} →
      (C : Type z) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] → [inst_3 : CommRing C] → [inst_4 : Algebra A C] → (κ → B) → Matrix κ (B →ₐ[A] C) C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.instInhabitedState : Inhabited Lean.Meta.Grind.EMatch.State
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.tryClearManyS.tacticBuilder : Lean.MVarId → Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.orbit.coe_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {x : MulAction.orbitRel.Quotient G α}
  {a : ↑x.orbit}, ↑(g • a) = g • ↑a