mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearMapAt_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] (b : B),
  ⇑(Bundle.Trivialization.continuousLinearMapAt R e b) = ⇑(Bundle.Trivialization.linearMapAt R e b)
-- Mathlib.Probability.Decision.BayesEstimator
/-- An estimator for an estimation problem that for `(P ∘ₘ π)`-almost every `x` is of
the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`.  -/
ProbabilityTheory.HasArgminEstimator.argminEstimator : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} →
            {ℓ : Θ → 𝓨 → ENNReal} →
              {P : ProbabilityTheory.Kernel Θ 𝓧} →
                {π : MeasureTheory.Measure Θ} →
                  [inst : StandardBorelSpace Θ] →
                    [inst_1 : Nonempty Θ] →
                      [inst_2 : ProbabilityTheory.IsFiniteKernel P] →
                        [inst_3 : MeasureTheory.IsFiniteMeasure π] → ProbabilityTheory.HasArgminEstimator ℓ P π → 𝓧 → 𝓨
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.take_eq_take : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x : ↥T} {m n : ℕ},
  Descriptive.Tree.take m x = Descriptive.Tree.take n x ↔ min m (↑x).length = min n (↑x).length
-- Lean.Parser.Do
Lean.Parser.Term.doForDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.instSetLike = { coe := fun s => s.carrier, coe_injective := ⋯ }
-- Mathlib.Data.Finset.Insert
Multiset.toFinset_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a}.toFinset = {a}
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Associates.unique' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {p q : Multiset (Associates α)},
  (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ext : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] {f g : M₁ ≃SL[σ₁₂] M₂}, ⇑f = ⇑g → f = g
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), ¬Order.IsPredLimit (Order.pred a)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toCoweightBasis_repr_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem] (i : ↥b.support), b.toCoweightBasis.repr (P.coroot ↑i) = fun₀ | i => 1
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.isTriangulated_iff_of_iso : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂)
  [inst_12 : F₁.CommShift ℤ] [inst_13 : F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ],
  F₁.IsTriangulated ↔ F₂.IsTriangulated
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.isClosedEmbedding_embedProduct : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousAdd α],
  Topology.IsClosedEmbedding ⇑(AddUnits.embedProduct α)
-- Mathlib.Topology.Order.LeftRight
nhdsLT_sup_nhdsWithin_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Iio a) ⊔ nhdsWithin a {a} = nhdsWithin a (Set.Iic a)
-- Mathlib.Algebra.GroupWithZero.Basic
NeZero.mul : ∀ {M₀ : Type u_1} [inst : Zero M₀] [inst_1 : Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y],
  NeZero (x * y)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNormedRing : {α : Type u} →
  [inst : TopologicalSpace α] → {R : Type u_1} → [inst_1 : NormedRing R] → NormedRing (BoundedContinuousFunction α R)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.modByMonicHom_mk : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic) (f : Polynomial R),
  (AdjoinRoot.modByMonicHom hg) ((AdjoinRoot.mk g) f) = f %ₘ g
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq_one_of_eraseLead_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f ≠ 0 → f.eraseLead = 0 → f.support.card = 1
-- Init.Data.UInt.Bitwise
instCommutativeUSizeHAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- The cycles of a permutation commute with it  -/
Equiv.Perm.self_mem_cycle_factors_commute : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α},
  c ∈ g.cycleFactorsFinset → Commute c g
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.mk.inj : ∀ {α : Type u} {toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α}
  {eq_of_compare :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      ∀ (a b : α), compare a b = Ordering.eq → a = b)
      Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam}
  {min :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Min α)
      Std.Packages.LinearOrderOfOrdArgs.min._autoParam}
  {max :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Max α)
      Std.Packages.LinearOrderOfOrdArgs.max._autoParam}
  {min_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := min;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam}
  {max_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := max;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam}
  {toLinearPreorderOfOrdArgs_1 : Std.Packages.LinearPreorderOfOrdArgs α}
  {eq_of_compare_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      ∀ (a b : α), compare a b = Ordering.eq → a = b)
      Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam}
  {min_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      Min α)
      Std.Packages.LinearOrderOfOrdArgs.min._autoParam}
  {max_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      Max α)
      Std.Packages.LinearOrderOfOrdArgs.max._autoParam}
  {min_eq_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      let this_2 := min_1;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam}
  {max_eq_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      let this_2 := max_1;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam},
  { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs, eq_of_compare := eq_of_compare, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
      { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs_1, eq_of_compare := eq_of_compare_1, min := min_1,
        max := max_1, min_eq := min_eq_1, max_eq := max_eq_1 } →
    toLinearPreorderOfOrdArgs = toLinearPreorderOfOrdArgs_1 ∧ min = min_1 ∧ max = max_1
-- Std.Time.Zoned.ZoneRules
/-- Creates `ZoneRules` for the given `TimeZone`.
 -/
Std.Time.TimeZone.ZoneRules.ofTimeZone : Std.Time.TimeZone → Std.Time.TimeZone.ZoneRules
-- Init.Data.Vector.Lemmas
Vector.toArray_setIfInBounds : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α},
  (xs.setIfInBounds i x).toArray = xs.toArray.setIfInBounds i x
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The function that induces the topology on `E →WOT[𝕜] F`, namely the function that takes
an `A` and maps it to `fun ⟨x, y⟩ => y (A x)` in `E × F⋆ → 𝕜`, bundled as a linear map to make
it easier to prove that it is a TVS.  -/
ContinuousLinearMapWOT.inducingFn : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_3) →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] → (E →SWOT[σ] F) →ₗ[𝕜₂] E × StrongDual 𝕜₂ F → 𝕜₂
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L'))
  (X_1 : D),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).counitIso.inv.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Std.Http.Protocol.H1.Reader
/-- Initial state waiting for HTTP start line.
 -/
Std.Http.Protocol.H1.Reader.State.needStartLine : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Defining property of `sigNeg`.  -/
sigNeg_isGreatest : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R],
  IsGreatest {r | ∃ V, Module.finrank R ↥V = r ∧ (QuadraticMap.restrict (-Q) V).PosDef} (sigNeg Q)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- The canonical identification between the tangent bundle to the model space and the product,
as a homeomorphism. For the diffeomorphism version, see `tangentBundleModelSpaceDiffeomorph`.  -/
tangentBundleModelSpaceHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] → (I : ModelWithCorners 𝕜 E H) → TangentBundle I H ≃ₜ ModelProd H E
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_zsmul_of_dvd : ∀ {R : Type u_1} [inst : NonUnitalRing R] {x y : R} (z : ℤ), x ∣ y → x ∣ z • y
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The ring equivalence between `𝓞 (WithVal v)` and an integral closure of
`ℤ` in `K`.  -/
NumberField.RingOfIntegers.withValEquiv : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : Field K] →
        (v : Valuation K Γ₀) →
          (R : Type u_4) →
            [inst_2 : CommRing R] →
              [inst_3 : Algebra R K] → [IsIntegralClosure R ℤ K] → NumberField.RingOfIntegers (WithVal v) ≃+* R
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.instFinite : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Finite V] [Finite W], Finite (G →g H)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The identity map is a homeomorphism from `ProbabilityMeasure Ω` with the topology of
convergence in distribution to `ProbabilityMeasure Ω` with the Lévy-Prokhorov (pseudo)metric.  -/
MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph : {Ω : Type u_1} →
  [inst : PseudoMetricSpace Ω] →
    [inst_1 : MeasurableSpace Ω] →
      [inst_2 : OpensMeasurableSpace Ω] →
        [TopologicalSpace.SeparableSpace Ω] →
          MeasureTheory.ProbabilityMeasure Ω ≃ₜ MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_div : ∀ (a b : UInt16), (a / b).toUInt32 = a.toUInt32 / b.toUInt32
-- Lean.DocString.Parser
/-- The position at which the document content starts, used to allow headers on the first line of a
docstring (e.g. `/-! # Header -/`). With the default value `⟨1, 0⟩`, the beginning-of-line check
is unaffected for normal documents.
 -/
Lean.Doc.Parser.BlockCtxt.docStartPosition : Lean.Doc.Parser.BlockCtxt → Lean.Position
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α},
  (t.insertManyIfNewUnit l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} {x y : CategoryTheory.Kleisli T}
  {f g : x ⟶ y}, f = g ↔ f.of = g.of
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_of_isEmpty : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [IsEmpty α] (f : α → E) (p : ENNReal), MeasureTheory.lpNorm f p μ = 0
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `lowerBoundP cut` retrieves the largest entry comparing `lt` or `eq` under `cut`,
if it exists. If multiple keys in the map return `eq` under `cut`, any of them may be returned.
 -/
RBTree.RBSet.lowerBoundP? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → Option α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' Y' : D}
  (f' g' : X' ⟶ Y') [inst_5 : CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
  (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g'),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))) =
    CategoryTheory.CategoryStruct.comp q (CategoryTheory.Limits.coequalizer.π f' g')
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofBitVec : ∀ {b : BitVec 16}, { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getValueCast? k (⟨k, v⟩ :: l) = some v
-- Mathlib.Data.List.Cycle
/-- The `Multiset` of lists that can make the cycle.  -/
Cycle.lists : {α : Type u_1} → Cycle α → Multiset (List α)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.π m` is the first projection in the following pullback square:

```
U --h.π m--> (Ω₀ : C)
|                |
m             Ω₀.arrow
|                |
v                v
X -----h.χ m---> Ω
```
 -/
CategoryTheory.SubobjectRepresentableBy.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β},
  κ = η ↔ ∀ (a : α), κ a = η a
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ_δ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_δ._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δ_δ._auto_3) {Z : C}
  (h_1 : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.δ f g n₁ n₂ hn₂) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `countable_setOfPred_covBy_right`.

---

The set of points which are isolated on the right is countable when the space is
second-countable.  -/
countable_setOf_covBy_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | ∃ y, x ⋖ y}.Countable
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.mergeWith.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (mergeFn : (a : α) → β a → β a → β a)
  (t₁ t₂ : Std.DTreeMap.Internal.Impl α β) (ht₁ : t₁.Balanced),
  Std.DTreeMap.Internal.Impl.mergeWith mergeFn t₁ t₂ ht₁ =
    Std.DTreeMap.Internal.Impl.foldl
      (fun t a b₂ =>
        (Std.DTreeMap.Internal.Impl.alter a
            (fun x =>
              match x with
              | none => some b₂
              | some b₁ => some (mergeFn a b₁ b₂))
            t.impl ⋯).toBalancedTree)
      { impl := t₁, balanced_impl := ht₁ } t₂
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isConj_of : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : ↥(alternatingGroup α)},
  IsConj ↑σ ↑τ → (↑σ).support.card + 2 ≤ Fintype.card α → IsConj σ τ
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The obvious morphism `L ⟶ S f n`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            (n : ℤ) → L ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S✝ f n
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.size_withComputedSize : ∀ {α : Type u} {β : α → Type v} {self : Array (Std.DHashMap.Internal.AssocList α β)},
  (Std.DHashMap.Internal.withComputedSize self).size = Std.DHashMap.Internal.computeSize self
-- Mathlib.Algebra.GroupWithZero.Associated
instDecidableRelAssociatedOfIsLeftCancelMulZeroOfDvd : {M : Type u_1} →
  [inst : MonoidWithZero M] →
    [IsLeftCancelMulZero M] → [DecidableRel fun x1 x2 => x1 ∣ x2] → DecidableRel fun x1 x2 => Associated x1 x2
-- Mathlib.NumberTheory.Niven
/-- `exp(q * π * I)` for `q : ℚ` is integral over `ℤ`.  -/
Complex.isIntegral_exp_rat_mul_pi_mul_I : ∀ (q : ℚ), IsIntegral ℤ (Complex.exp (↑q * ↑Real.pi * Complex.I))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instMin : {R : Type u} → {M : Type v} → [inst : VAdd R M] → Min (SubAddAction R M)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.isClosed' : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (self : ClosedAddSubgroup G), IsClosed (↑self).carrier
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- The coproduct is the pushout under the initial object.  -/
isPushoutOfIsInitialIsCoproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ X) →
            (k : W ⟶ Y) →
              (H₁ : CategoryTheory.Limits.IsInitial W) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g ⋯)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.mk.inj : ∀ {ι : Type u_3} {M : Type u_4} {inst : AddCommMonoid M} {I : WithTop (BoxIntegral.Box ι)}
  {toFun : BoxIntegral.Box ι → M}
  {sum_partition_boxes' :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J}
  {toFun_1 : BoxIntegral.Box ι → M}
  {sum_partition_boxes'_1 :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun_1 Ji = toFun_1 J},
  { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' } =
      { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 } →
    toFun = toFun_1
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.visitedExpr : Lean.CollectFVars.State → Lean.ExprSet
-- Lean.Elab.Tactic.Omega.Core
/-- `combo`, implemented on `Fact`.  -/
Lean.Elab.Tactic.Omega.Fact.combo : ℤ → Lean.Elab.Tactic.Omega.Fact → ℤ → Lean.Elab.Tactic.Omega.Fact → Lean.Elab.Tactic.Omega.Fact
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.hasBadIndexDep? : Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq_k.eq_1 : ∀ (e : Lean.Grind.AC.Expr),
  e.toSeq_k = Lean.Grind.AC.Expr.rec Lean.Grind.AC.Seq.var (fun a x x_1 ihb => a.toSeq'_k ihb) e
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceLErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size),
  (Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr).Balanced
-- Mathlib.RepresentationTheory.Tannaka
/-- The representation on `G → k` induced by multiplication on the left in `G`.  -/
TannakaDuality.FiniteGroup.leftRegular : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Representation k G (G → k)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixingSubgroup_fixedPoints : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] [Finite G],
  fixingSubgroup G ↑(FixedPoints.intermediateField ↥H) = H