mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Bundle
/-- `Bundle.TotalSpace F E` is the total space of the bundle. It consists of pairs
`(proj : B, snd : E proj)`.
 -/
Bundle.TotalSpace : {B : Type u_1} → Type u_4 → (B → Type u_5) → Type (max u_1 u_5)
-- Mathlib.Data.NNReal.Defs
/-- While not very useful, this instance uses the same representation as `Real.instRepr`.  -/
instReprNNReal : Repr NNReal
-- Mathlib.Data.Opposite
Opposite.equivToOpposite_symm_coe : ∀ {α : Sort u}, ⇑Opposite.equivToOpposite.symm = Opposite.unop
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The submodule corresponding to a projective subspace `s`, consisting of the representatives of
points in `s` together with zero. This is the inverse of `Submodule.projectivization`.  -/
Projectivization.Subspace.submodule : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization.Subspace K V ≃o Submodule K V
-- Mathlib.RingTheory.Morita.Matrix
fromModuleCatToModuleCatLinearEquiv_apply : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i : ι) (x : ↥(MatrixModCat.toModuleCatObj R (ι → M) i)),
  (fromModuleCatToModuleCatLinearEquiv R M i) x = ∑ i_1, ↑x i_1
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`.  -/
CategoryTheory.Limits.Types.pi_lift_π_apply : ∀ {β : Type v} [inst : Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift s)) x) =
    (CategoryTheory.ConcreteCategory.hom (s b)) x
-- Mathlib.Algebra.Group.Basic
add_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + (b - c) = a + b - c
-- Mathlib.Algebra.Star.Basic
star_star_mul : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] (x y : R), star (star x * y) = star y * x
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- Computes `J(a | b)` (or `-J(a | b)` if `flip` is set to `true`) given assumptions, by reducing
`a` to odd by repeated division and then using quadratic reciprocity to swap `a`, `b`.  -/
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSymAux : (a : ℕ) → ℕ → Bool → a > 0 → ℤ
-- Mathlib.Computability.Language
Language.reverse_eq_image : ∀ {α : Type u_1} (l : Language α), l.reverse = List.reverse '' l
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_id : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], LinearMap.baseChange A LinearMap.id = LinearMap.id
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.
 -/
Std.DTreeMap.Internal.Impl.Const.mergeWith : {α : Type u} →
  {β : Type v} →
    [Ord α] →
      (α → β → β → β) →
        (t₁ : Std.DTreeMap.Internal.Impl α fun x => β) →
          (Std.DTreeMap.Internal.Impl α fun x => β) → t₁.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α fun x => β
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.freeDFinsuppEquiv_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : (i : ι) → Fintype (κ i)] [inst_4 : (i : ι) → DecidableEq (κ i)]
  [inst_5 : DecidableEq ι'] [inst_6 : Fintype ι'] (f : Π₀ (x : ((i : ι) → κ i) × ι'), R)
  (x : (i : ι) → Π₀ (x : κ i), R), (MultilinearMap.freeDFinsuppEquiv f) x = ∑ p, f p • fun₀ | p.2 => ∏ i, (x i) (p.1 i)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Raw.Const.get m x ⋯)).isSome).getD fallback
-- Std.Time.Format.Modifier
Std.Time.Modifier.B.inj : ∀ {presentation presentation_1 : Std.Time.Text},
  Std.Time.Modifier.B presentation = Std.Time.Modifier.B presentation_1 → presentation = presentation_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertIfNew_eq_insertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {h : l.Balanced},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v l h).impl = Std.DTreeMap.Internal.Impl.insertIfNew! k v l
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.mem_iff_one_sub_mem : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {t : β},
  t ∈ Set.Ioo 0 1 ↔ 1 - t ∈ Set.Ioo 0 1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The inverse of a 1×1 or 0×0 matrix is always diagonal.

While we could write this as `of fun _ _ => (A default default)⁻¹ʳ` on the RHS, this is
less useful because:

* It wouldn't work for 0×0 matrices.
* More things are true about diagonal matrices than constant matrices, and so more lemmas exist.

`Matrix.diagonal_unique` can be used to reach this form, while `Ring.inverse_eq_inv` can be used
to replace `Ring.inverse` with `⁻¹`.
 -/
Matrix.inv_subsingleton : ∀ {m : Type u} {α : Type v} [inst : CommRing α] [Subsingleton m] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  (A : Matrix m m α), A⁻¹ = Matrix.diagonal fun i => Ring.inverse (A i i)
-- Mathlib.Topology.KrullDimension
/-- If `f : Y → X` is inducing, then `dim(Y) ≤ dim(X)`.  -/
Topology.IsInducing.topologicalKrullDim_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Y → X},
  Topology.IsInducing f → topologicalKrullDim Y ≤ topologicalKrullDim X
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.inf : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : AddSubmonoid M},
  s₁.AddSaturated → s₂.AddSaturated → (s₁ ⊓ s₂).AddSaturated
-- Mathlib.Order.Interval.Basic
Interval.semilatticeSup : {α : Type u_1} → [inst : Lattice α] → SemilatticeSup (Interval α)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).right = η.right.app { len := 0 }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.instTrans : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Trans Std.DTreeMap.Equiv Std.DTreeMap.Equiv Std.DTreeMap.Equiv
-- Aesop.Frontend.Command
_private.Aesop.Frontend.Command.0.Aesop.Frontend.Parser.evalStatsReport?.unsafe_1 : Lean.Name → Lean.CoreM (Option Aesop.StatsReport)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokens : Lean.ToJson Lean.Lsp.SemanticTokens
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.mk : List Lean.Meta.RefinedDiscrTree.Key →
  ℕ →
    Lean.Meta.RefinedDiscrTree.TrieIndex →
      Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key) → Lean.Meta.RefinedDiscrTree.PartialMatch✝
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₀_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (f : Fin 0 → ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.exteriorPower.iso₀ M).hom) (ModuleCat.exteriorPower.mk f) = 1
-- Lean.Elab.Do.Legacy
/-- Return `true` if the given `letDecl` contains binders.  -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.letDeclHasBinders : Lean.Syntax → Bool
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A nonzero element of a generalized eigenspace is a generalized eigenvector.
(Def 8.8 of [axler2024])  -/
Module.End.HasGenEigenvector : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ → M → Prop
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- `liftOfRightInverse f hf g hg` is the unique group homomorphism `φ`

* such that `φ.comp f = g` (`MonoidHom.liftOfRightInverse_comp`),
* where `f : G₁ →+* G₂` has a RightInverse `f_inv` (`hf`),
* and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.

See `MonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.

```
   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
```
 -/
MonoidHom.liftOfRightInverse : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : Group G₁] →
        [inst_1 : Group G₂] →
          [inst_2 : Group G₃] →
            (f : G₁ →* G₂) → (f_inv : G₂ → G₁) → Function.RightInverse f_inv ⇑f → { g // f.ker ≤ g.ker } ≃ (G₂ →* G₃)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The proof that is the limit cone  -/
CategoryTheory.Limits.LimitCone.isLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (self : CategoryTheory.Limits.LimitCone F) → CategoryTheory.Limits.IsLimit self.cone
-- Mathlib.Data.Set.Function
Set.leftInvOn_id : ∀ {α : Type u_1} (s : Set α), Set.LeftInvOn id id s
-- Init.Data.List.Find
List.idxOf?_eq_none_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, List.idxOf? a l = none ↔ a ∉ l
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  AddCommMonCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Mathlib.Data.Set.Lattice
/-- A specialization of `iInter₂_subset`.  -/
Set.biInter_subset_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α}, x ∈ s → ⋂ x ∈ s, t x ⊆ t x
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_finset_logSizeBallSeq_card_eq_zero : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), (PairReduction.logSizeBallSeq J hJ a c J.card).finset.card = 0
-- Std.Data.ExtTreeMap.Lemmas
_private.Std.Data.ExtTreeMap.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.eq_3 : ∀ {α : Type u_1} (x : α → α → Bool) (a b : α) (xs : List α),
  (a :: b :: xs).mergeSort x =
    ((↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).1).mergeSort x).merge
      ((↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).2).mergeSort x) x
-- Mathlib.Analysis.Convolution
/-- The symmetric definition of convolution.  -/
MeasureTheory.convolution_eq_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G],
  MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.mk : Lean.MVarId → Lean.MVarId → Std.HashSet Lean.FVarId → Std.HashSet Lean.FVarId → Bool → Aesop.GoalDiff
-- Mathlib.Order.CompleteLattice.Basic
sInf_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst_1 : InfSet β] {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → sInf (s ×ˢ t) = (sInf s, sInf t)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
Pi.compRightL.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] {α : Type u_6} (f : α → ι),
  Pi.compRightL R φ f = { toFun := fun v i => v (f i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.id_comp : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : U ⥤q V), 𝟭q U ⋙q F = F
-- Mathlib.Topology.Instances.Matrix
continuous_matrixOf : ∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace α]
  {f : α → m → n → R}, (Continuous fun x => Matrix.of (f x)) ↔ Continuous f
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.elabInitGrindNorm : Lean.Elab.Command.CommandElab
-- Mathlib.Data.Set.NAry
Set.Nonempty.of_image2_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  (Set.image2 f s t).Nonempty → s.Nonempty
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.mul_one : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation F (x.mul MonCat.Colimits.Prequotient.one) x
-- Mathlib.Data.Set.Insert
Set.eq_of_mem_insert_of_notMem : ∀ {α : Type u_1} {s : Set α} {a b : α}, b ∈ insert a s → b ∉ s → b = a
-- Mathlib.Data.Seq.Computation
Computation.length_bind : ∀ {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [_T1 : s.Terminates]
  [_T2 : (f s.get).Terminates], (s.bind f).length = (f s.get).length + s.length
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If a wide equalizer of `f` exists, we can access the inclusion `wideEqualizer f ⟶ X` by
saying `wideEqualizer.ι f`.  -/
CategoryTheory.Limits.wideEqualizer.ι : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        (f : J → (X ⟶ Y)) →
          [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] → CategoryTheory.Limits.wideEqualizer f ⟶ X
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_add : ∀ {α : Type u_1} [inst : Add α] (a b : αˢʸᵐ), SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_3),
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.H n₁).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯)
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.preimageEquivFiber_symm_apply_coe : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : PrimeSpectrum (p.asIdeal.Fiber S)),
  ↑((PrimeSpectrum.preimageEquivFiber R S p).symm q) =
    PrimeSpectrum.comap Algebra.TensorProduct.includeRight.toRingHom q
-- Lean.Elab.AutoBound
Lean.Elab.AutoBoundImplicitContext.mk.inj : ∀ {autoImplicitEnabled : Bool} {boundVariables : Lean.PArray Lean.Expr} {autoImplicitEnabled_1 : Bool}
  {boundVariables_1 : Lean.PArray Lean.Expr},
  { autoImplicitEnabled := autoImplicitEnabled, boundVariables := boundVariables } =
      { autoImplicitEnabled := autoImplicitEnabled_1, boundVariables := boundVariables_1 } →
    autoImplicitEnabled = autoImplicitEnabled_1 ∧ boundVariables = boundVariables_1
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_left_of_ge : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ (x : α), f x ≤ C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → Set β),
      Monotone seq →
        ⋃ i, seq i = Set.univ →
          (∀ (m : ℕ), MeasurableSet (seq m)) →
            Filter.Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) Filter.atTop (nhds ((κ a).real Set.univ))
-- Mathlib.LinearAlgebra.Matrix.Trace
AddMonoidHom.map_trace : ∀ {n : Type u_3} {R : Type u_6} {S : Type u_7} [inst : Fintype n] [inst_1 : AddCommMonoid R] [inst_2 : AddCommMonoid S]
  {F : Type u_8} [inst_3 : FunLike F R S] [AddMonoidHomClass F R S] (f : F) (A : Matrix n n R),
  f A.trace = (A.map ⇑f).trace
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_closedBall_smul : ∀ (z : Complex.UnitClosedDisc) (w : Complex.UnitDisc), ↑(z • w) = ↑z * ↑w
-- Mathlib.SetTheory.ZFC.PSet
PSet.instIsWellFoundedMem : IsWellFounded PSet.{u_1} fun x1 x2 => x1 ∈ x2
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.toFrame : {α : Type u_1} → [self : CompleteDistribLattice α] → Order.Frame α
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimage.comp_π_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  {Z : C} (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0 ↔
    CategoryTheory.CategoryStruct.comp f g = 0
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_restrict_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {t : Set γ} (ht : MeasurableSet t),
  κ.compProd (η.restrict ht) = (κ.compProd η).restrict ⋯
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a (not necessarily associative) ring
is isomorphic to the center of its opposite.  -/
Subring.centerToMulOpposite : {R : Type u} → [inst : NonAssocRing R] → ↥(Subring.center R) ≃+* ↥(Subring.center Rᵐᵒᵖ)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (f' : F)
  (s : Set E) (x v : E),
  HasLineDerivWithinAt 𝕜 f f' s x v = HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_le_coe : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, ↑I ≤ ↑J ↔ I ≤ J
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_map : ∀ {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {k : β → α} {l : Filter β},
  f =O[𝕜; Filter.map k l] g ↔ (f ∘ k) =O[𝕜; l] (g ∘ k)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_biUnionTagged : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J),
  BoxIntegral.integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, BoxIntegral.integralSum f vol (πi J)
-- Std.Async.UDP
/-- Associates the UDP socket with the given address and port, so every message sent by this socket is
automatically sent to that destination.
 -/
Std.Async.UDP.Socket.connect : Std.Async.UDP.Socket → Std.Net.SocketAddress → IO Unit
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a `LinearIsometryEquiv`.
For an unbundled version see `ContinuousLinearMap.flip`.  -/
ContinuousLinearMap.flipₗᵢ : (𝕜 : Type u_1) →
  (E : Type u_4) →
    (Fₗ : Type u_7) →
      (Gₗ : Type u_9) →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup Fₗ] →
            [inst_2 : SeminormedAddCommGroup Gₗ] →
              [inst_3 : NontriviallyNormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜 Fₗ] →
                    [inst_6 : NormedSpace 𝕜 Gₗ] → (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ
-- Mathlib.Data.Set.Lattice
Set.iInter_univ : ∀ {α : Type u_1} {ι : Sort u_5}, ⋂ x, Set.univ = Set.univ
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The generators of the lower Borel subalgebra.  -/
LieAlgebra.Basis.f : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] → [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → ι → L
-- Mathlib.RingTheory.DedekindDomain.Different
_private.Mathlib.RingTheory.DedekindDomain.Different.0.«term_ᵛ» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.isUnit_iff_norm_eq_one : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] {u : ↥(Valued.integer K)},
  IsUnit u ↔ ‖u‖ = 1
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Every structure groupoid is contained in the groupoid of all open partial homeomorphisms.  -/
instStructureGroupoidOrderTop : {H : Type u_1} → [inst : TopologicalSpace H] → OrderTop (StructureGroupoid H)
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A ⊗[R] B` is a field, then for any `R`-algebra `S`
and injections of `A` and `B` into `S`, their images are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_isField' : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type v}
  [inst_3 : Ring A] {B : Type w} [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  IsField (TensorProduct R A B) →
    ∀ (fa : A →ₐ[R] S) (fb : B →ₐ[R] S),
      Function.Injective ⇑fa → Function.Injective ⇑fb → fa.range.LinearDisjoint fb.range
-- Mathlib.Algebra.Free
FreeAddSemigroup.instTraversable : Traversable FreeAddSemigroup
-- Mathlib.Order.Bounds.Image
/-- An antitone map sends a least element of a set to a greatest element of its
image.  -/
Antitone.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {a : α} {s : Set α}, IsLeast s a → IsGreatest (f '' s) (f a)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.eventually_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β],
  Asymptotics.IsEquivalent l u v → (∀ᶠ (t : α) in l, v t < 0) → ∀ᶠ (x : α) in l, u x < 0