mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toLinearOrder : {α : Type u_3} → [self : LinearOrderedCommMonoidWithZero α] → LinearOrder α
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.zeroEquiv.eq_1 : ∀ (R : Type u) [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  exteriorPower.zeroEquiv R M =
    LinearEquiv.ofLinearMap (exteriorPower.alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1))
      { toFun := fun r => r • (exteriorPower.ιMulti R 0) fun a => Fin.casesOn a fun i hi => ⋯.elim, map_add' := ⋯,
        map_smul' := ⋯ }
      ⋯ ⋯
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.topology_eq_withSeminorms : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} [topology : TopologicalSpace E], WithSeminorms p → topology = p.moduleFilterBasis.topology
-- Lean.Meta.Sym.Util
/-- Normalizes universe levels in constants and sorts.
 -/
Lean.Meta.Sym.normalizeLevels : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.h1CotangentEquivCotangent_comp_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  ↑P.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S =
    Algebra.Extension.h1Cotangentι ∘ₗ Algebra.Extension.H1Cotangent.map (Algebra.Extension.defaultHom R S P)
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.dvd_map_of_isScalarTower' : ∀ (R : Type u_3) {S : Type u_4} (K : Type u_5) (L : Type u_6) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field K] [inst_3 : Ring L] [inst_4 : Algebra R S] [inst_5 : Algebra R K] [inst_6 : Algebra S L]
  [inst_7 : Algebra K L] [inst_8 : Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S),
  minpoly K ((algebraMap S L) s) ∣ Polynomial.map (algebraMap R K) (minpoly R s)
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isGLB_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α} {x : α},
  IsGLB (⇑f '' s) (f x) ↔ IsGLB s x
-- Mathlib.RingTheory.Perfectoid.Untilt
PreTilt.untilt_iterate_frobeniusEquiv_symm_pow : ∀ {O : Type u_1} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) O] (x : PreTilt O p) (n : ℕ),
  PreTilt.untilt ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x) ^ p ^ n = PreTilt.untilt x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- Plancherel's theorem for Schwartz functions.  -/
SchwartzMap.integral_inner_fourier_fourier : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {H : Type u_4} [inst_5 : NormedAddCommGroup H]
  [inst_6 : InnerProductSpace ℂ H] [CompleteSpace H] (f g : SchwartzMap V H),
  ∫ (ξ : V), inner ℂ ((FourierTransform.fourier f) ξ) ((FourierTransform.fourier g) ξ) = ∫ (x : V), inner ℂ (f x) (g x)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Submodule.finiteQuotient_iff : ∀ {M : Type u_3} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M),
  Finite (M ⧸ N) ↔ Module.finrank ℤ ↥N = Module.finrank ℤ M
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom_hom : ∀ {X Y : AddGrpCat} (f : X ⟶ Y), AddGrpCat.ofHom (AddGrpCat.Hom.hom f) = f
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.val_ofFinEmb : ∀ (n : ℕ) (β : Type u_2) (f : Fin n ↪ β), ↑(Set.powersetCard.ofFinEmb n β f) = Finset.map f Finset.univ
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {s : Set E} {x v : E},
  LineDifferentiableWithinAt 𝕜 f s x v → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → LineDifferentiableWithinAt 𝕜 f₁ s x v
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.instCoeOut : {α : Type u_1} → [inst : HeytingAlgebra α] → CoeOut (Heyting.Regular α) α
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.iff_preservesFiniteLimits_tensorRight : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  Module.Flat R ↑M ↔ CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorRight M)
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.HasRcoIntersection.mk : {α : Type w} → (Std.Rio α → Std.Rco α → Std.Rco α) → Std.Rio.HasRcoIntersection α
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- The injection `x ↦ LinearMap.inl E F x` as a linear isometry.  -/
LinearIsometry.inl : (𝕜 : Type u_9) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_10) →
      (F : Type u_11) →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → E →ₗᵢ[𝕜] E × F
-- Mathlib.FieldTheory.IntermediateField.Basic
toSubalgebra_toIntermediateField' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : Subalgebra K L)
  (hS : IsField ↥S), (S.toIntermediateField' hS).toSubalgebra = S
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).g' =
    CategoryTheory.CategoryStruct.comp h.g' φ.τ₃
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Raw.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Raw.Const.get? m a
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.isometry_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  [inst_2 : Fact (1 ≤ p)] (i : α), Isometry (lp.single p i)
-- Mathlib.RingTheory.Polynomial.Dickson
/-- The `(m * n)`-th Dickson polynomial of the first kind is the composition of the `m`-th and
`n`-th.  -/
Polynomial.dickson_one_one_mul : ∀ (R : Type u_1) [inst : CommRing R] (m n : ℕ),
  Polynomial.dickson 1 1 (m * n) = (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_smul : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {S : Type u_4}
  [inst_7 : Monoid S] [inst_8 : DistribMulAction S M] [inst_9 : SMulCommClass R S M]
  [inst_10 : LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M), ⇑(r • D) = r • ⇑D
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams.mk.inj : ∀ {partialResultToken? partialResultToken?_1 : Option Lean.Lsp.ProgressToken},
  { partialResultToken? := partialResultToken? } = { partialResultToken? := partialResultToken?_1 } →
    partialResultToken? = partialResultToken?_1
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- A `DyckStep` is either `U` or `D`, corresponding to `(` and `)` respectively.  -/
DyckStep : Type
-- Mathlib.Order.PartialSups
bddAbove_range_partialSups : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  {f : ι → α}, BddAbove (Set.range ⇑(partialSups f)) ↔ BddAbove (Set.range f)
-- Mathlib.Order.Minimal
MinimalFor.anti : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] {P Q : ι → Prop} {f : ι → α} {i : ι},
  MinimalFor P f i → Q ≤ P → Q i → MinimalFor Q f i
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatβ_3 : Lean.ParserDescr
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprAndKind : Lean.ToExpr Mathlib.Tactic.ITauto.AndKind
-- Std.Internal.Do.PredTrans
/-- Adds a state argument to a predicate transformer.

Given a state-dependent transformer `σ → PredTrans l e (α × σ)`, produces a transformer
over `σ → l` that threads the state through postconditions.  -/
Std.Internal.Do.pushArg : {σ : Type u} →
  {Pred : Type v} →
    {EPred : Type w} →
      {α : Type z} → (σ → Std.Internal.Do.PredTrans Pred EPred (α × σ)) → Std.Internal.Do.PredTrans (σ → Pred) EPred α
-- Lean.Declaration
Lean.ConstantInfo.axiomInfo.sizeOf_spec : ∀ (val : Lean.AxiomVal), sizeOf (Lean.ConstantInfo.axiomInfo val) = 1 + sizeOf val
-- Mathlib.LinearAlgebra.Matrix.Hadamard
/-- `Matrix.hadamard` (denoted as `⊙` within the Matrix namespace) defines the Hadamard product,
which is the pointwise product of two matrices of the same size.  -/
Matrix.hadamard : {α : Type u_1} → {m : Type u_2} → {n : Type u_3} → [Mul α] → Matrix m n α → Matrix m n α → Matrix m n α
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coconeOfConeLeftOp : {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.Cone F.leftOp → CategoryTheory.Limits.Cocone F
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- A morphism of schemes `f : X ⟶ Y` is formally unramified if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is formally unramified.

See `FormallyUnramified.hom_ext` and `FormallyUnramified.of_hom_ext`
for the infinitesimal lifting criterion.  -/
AlgebraicGeometry.FormallyUnramified : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.GroupTheory.Submonoid.Center
MulEquivClass.apply_mem_center_iff : ∀ {M : Type u_3} {N : Type u_1} {F : Type u_2} [inst : EquivLike F M N] [inst_1 : Mul M] [inst_2 : Mul N]
  [MulEquivClass F M N] (e : F) {x : M}, e x ∈ Set.center N ↔ x ∈ Set.center M
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The simple reflections of `W` generate `W` as a group.  -/
CoxeterSystem.subgroup_closure_range_simple : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W),
  Subgroup.closure (Set.range cs.simple) = ⊤
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
the variant {lean}`it.ensureTermination.toTreeSet` always terminates after finitely many steps.
 -/
Std.IterM.toTreeSet : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → Std.IterM m β → (cmp : β → β → Ordering) → m (Std.TreeSet β cmp)
-- Mathlib.Topology.Separation.Basic
ContinuousAt.eventually_ne : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {g : X → Y}
  {x : X} {y : Y}, ContinuousAt g x → g x ≠ y → ∀ᶠ (z : X) in nhds x, g z ≠ y
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrRight_refl : ∀ {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → UniformSpace (X i)],
  (UniformEquiv.piCongrRight fun i => UniformEquiv.refl (X i)) = UniformEquiv.refl ((i : ι) → X i)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c`,
on morphisms.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} →
            (P ⟶ Q) →
              (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P ⟶
                CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj Q)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))
  (x : CategoryTheory.Discrete J),
  ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).π.app x =
    match x with
    | { as := j } => CategoryTheory.Over.homMk (c.π.app (some j)) ⋯
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Creates the packed signed zero representation for the given specification.  -/
Float.Model.UnpackedFloat.packedZero : (spec : Float.Model.Format) → Float.Model.UnpackedFloat.Sign → BitVec spec.numBits
-- Mathlib.Algebra.Group.Shrink
Shrink.instNeg : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Neg α] → Neg (Shrink.{v, u_2} α)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasSum_eval₂ : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    PowerSeries.HasEval a →
      ∀ (f : PowerSeries R), HasSum (fun d => φ ((PowerSeries.coeff d) f) * a ^ d) (PowerSeries.eval₂ φ a f)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction' : ∀ {κ : Type u_2} {Z : Type u_3} {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)}
  [inst : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)]
  {mZ : MeasurableSpace Z} [inst_3 : TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] [Finite κ]
  {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure ((j : κ) → Y j)}
  {ξ : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ),
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * g p.2 ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (y : (j : κ) → Y j), g y ∂ν) →
    ξ = μ.prod ν
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.size_toArray : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.HasSize α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.toArray.size = r.size
-- Mathlib.Data.Set.Image
/-- **Alias** of `_private.Mathlib.Data.Set.Image.0.Set.subset_image_sdiff`. -/
Set.subset_image_diff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' s \ f '' t ⊆ f '' (s \ t)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext_left_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y : C}
  {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
-- Mathlib.Order.PartialSups
le_partialSups_of_le : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α) {i j : ι}, i ≤ j → f i ≤ (partialSups f) j
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsNonneg.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, (∀ (x : M), 0 ≤ (B x) x) → B.IsNonneg
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.fst = κ.map Prod.fst
-- Lean.Meta.WHNF
/-- If `e` is a projection function that satisfies `p`, then reduce it  -/
Lean.Meta.reduceProjOf? : Lean.Expr → (Lean.Name → Bool) → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.Index
Subgroup.dvd_index_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G →* G'},
  f.ker ≤ H → H.index ∣ (Subgroup.map f H).index
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_comp_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
      (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_roi : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_roi._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e.1 bound).isGT) t.toList
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_sSup_of_directedOn : ∀ {R : Type u} [inst : NonAssocRing R] {S : Set (Subring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Lean.Server.References
Lean.Server.ModuleImport.mk.sizeOf_spec : ∀ (module : Lean.Name) (uri : Lean.Lsp.DocumentUri) (isAll isPrivate : Bool) (metaKind : Lean.Lsp.LeanImportMetaKind),
  sizeOf { module := module, uri := uri, isAll := isAll, isPrivate := isPrivate, metaKind := metaKind } =
    1 + sizeOf module + sizeOf uri + sizeOf isAll + sizeOf isPrivate + sizeOf metaKind
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_add_im : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ↑(RCLike.re z) + ↑(RCLike.im z) * RCLike.I = z
-- Mathlib.CategoryTheory.Action.Limits
Action.functorCategoryEquivalence_linear : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {R : Type u_3} [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R V],
  CategoryTheory.Functor.Linear R (Action.functorCategoryEquivalence V G).functor
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.closure_one_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (t : Set N),
  Submonoid.closure ({1} ×ˢ t) = ⊥.prod (Submonoid.closure t)
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.mk : Std.CloseableChannel ByteArray → Std.CloseableChannel ByteArray → Std.Http.Internal.Mock.SharedState✝
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ₀.congr_simp : ∀ {κ₁ κ₂ : Cardinal.{w}} {X : Type w}
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B))
  (m m_1 :
    (B : Set X) →
      (hB : HasCardinalLT (↑B) κ₂) → (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X),
  m = m_1 →
    ∀ (B B_1 : Set X) (e_B : B = B_1) (hB : HasCardinalLT (↑B) κ₂) (a a_1 : X),
      a = a_1 →
        Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ₀✝ Y m B hB a =
          Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ₀✝ Y m_1 B_1 ⋯ a_1
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- There is a rational power between any two positive elements of an archimedean ordered field.  -/
exists_rat_pow_btwn : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {n : ℕ},
  n ≠ 0 → ∀ {x y : K}, x < y → 0 < y → ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.isLimitConstCone.congr_simp : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) [inst_2 : CategoryTheory.IsConnected J],
  CategoryTheory.Limits.isLimitConstCone J X = CategoryTheory.Limits.isLimitConstCone J X
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacksAgainst.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.HasPullbacksAlong f) → P.HasPullbacksAgainst P'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.lt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_1 ⋯
-- Batteries.Classes.Order
Batteries.TotalBLE.mk : ∀ {α : Sort u_1} {le : α → α → Bool}, (∀ {a b : α}, le a b = true ∨ le b a = true) → Batteries.TotalBLE le
-- Mathlib.Algebra.Order.Field.Basic
div_lt_iff_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (b / c < a ↔ a * c < b)
-- Batteries.Logic
Eq.congr : ∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.mk : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.coe.Preconnected → H.Preconnected
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom h.homologyIso.inv = S.rightHomologyIso.hom
-- Mathlib.NumberTheory.Primorial
Squarefree.dvd_primorial : ∀ {n : ℕ}, Squarefree n → n ∣ primorial n
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Result.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {E : Q(«$α») → Type u_1} →
      {e : Q(«$α»)} → (expr : Q(«$α»)) → E expr → Q(«$e» = «$expr») → Mathlib.Tactic.Ring.Common.Result E e
-- Mathlib.Algebra.Order.Field.Basic
_private.Mathlib.Algebra.Order.Field.Basic.0.exists_mul_left_lt₀ : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  a * b < c → ∃ a' > a, a' * b < c