mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- UV-compression reduces the size of the shadow of `𝒜` if, for all `x ∈ u` there is `y ∈ v`
such that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key UV-compression fact needed for
Kruskal-Katona.  -/
UV.card_shadow_compression_le : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
  (∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) → (UV.compression u v 𝒜).shadow.card ≤ 𝒜.shadow.card
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : Matrix m n α},
  M.transpose.map f = (M.map f).transpose
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.instDecidableComapAdj : {V : Type u_1} →
  {W : Type u_2} → (f : V → W) → (G : SimpleGraph W) → [DecidableRel G.Adj] → DecidableRel (SimpleGraph.comap f G).Adj
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_obj : ∀ (Ω : Type u) [inst : Field Ω] [inst_1 : IsSepClosed Ω] (X : FintypeCat),
  (CommAlgCat.FiniteEtale.equivOfIsSepClosed Ω).inverse.obj X = Opposite.op (CommAlgCat.FiniteEtale.of Ω (X.obj → Ω))
-- Mathlib.Algebra.Module.Presentation.Free
Module.Relations.solutionFinsupp_isPresentation : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) [inst_1 : IsEmpty relations.R],
  relations.solutionFinsupp.IsPresentation
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_mul : ∀ {R : Type u_1} [inst : Semiring R] {p : SkewPolynomial R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.X * p = (p.sum fun a b => (SkewPolynomial.monomial a) (SkewPolynomial.φ b)) * SkewPolynomial.X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {len w : ℕ} → aig.RefVec w → ℕ → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig len
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq.go : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
        Lean.Meta.LazyDiscrTree.ImportData →
          IO.Ref Lean.Meta.LazyDiscrTree.Cache →
            Lean.Meta.LazyDiscrTree.PreDiscrTree α → ℕ → ℕ → BaseIO (Lean.Meta.LazyDiscrTree.InitResults α)
-- Mathlib.Data.Finset.Sups
Finset.instAssociativeDisjSups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint], Std.Associative fun x1 x2 => x1.disjSups x2
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_iff_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] [IsAddTorsionFree G] (a : G), IsOfFinAddOrder a ↔ a = 0
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.symm_conj_apply : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₂' M₂'),
  e.symm.conj f = (↑e.symm ∘ₛₗ f) ∘ₛₗ ↑e
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.not_hasMultiplicativeReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasGoodReduction R W → ¬WeierstrassCurve.HasMultiplicativeReduction R W
-- Mathlib.Data.Set.Lattice.Image
Set.image_sInter_subset : ∀ {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (f : α → β), f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s
-- Mathlib.Tactic.NormNum.Core
/-- The tree of `norm_num` extensions.  -/
Mathlib.Meta.NormNum.NormNums.tree : Mathlib.Meta.NormNum.NormNums → Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.of_null_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ t = 0 → MeasureTheory.AEDisjoint μ s t
-- Std.Data.DHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.DHashMap.inner : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.DHashMap.Raw α β
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities : Lean.FromJson Lean.Lsp.WorkspaceEditClientCapabilities
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for multiplicative (on coprime arguments) functions.

If `f : ℕ → R`, where `R` is a complete normed commutative ring, `f 0 = 0`, `f 1 = 1`, `f` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n`.  -/
EulerProduct.eulerProduct_tprod : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) → f 0 = 0 → ∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (n : ℕ), f n
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.lift_ι' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ : G ⟶ A.toFunctor) (w : CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.lift f g φ w)
      (CategoryTheory.Subfunctor.equalizer f g).ι =
    CategoryTheory.CategoryStruct.comp φ A.ι
-- Init.Data.Array.Lemmas
Array.getElem_pop : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.pop.size), xs.pop[i] = xs[i]
-- Plausible.Random
/-- Generate a value of type `α` between `lo` and `hi` randomly using generator `g`.
 -/
Plausible.BoundedRandom.randomR : {m : Type u → Type u_1} →
  {α : Type u} →
    {inst : LE α} →
      [self : Plausible.BoundedRandom m α] →
        {g : Type} → (lo hi : α) → lo ≤ hi → [RandomGen g] → Plausible.RandGT g m { a // lo ≤ a ∧ a ≤ hi }
-- Init.Data.Order.Ord
/-- A typeclass for comparison functions satisfying `cmp a b = .eq` if and only if the logical equality
`a = b` holds.

This typeclass distinguishes itself from `LawfulBEqCmp` by using logical equality (`=`) instead of
boolean equality (`==`).
 -/
Std.LawfulEqCmp : {α : Type u} → (α → α → Ordering) → Prop
-- Mathlib.LinearAlgebra.Matrix.ZPow
_private.Mathlib.LinearAlgebra.Matrix.ZPow.0.Matrix.termM : Lean.ParserDescr
-- Mathlib.Algebra.Group.TransferInstance
/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`.  -/
Finite.exists_type_univ_nonempty_mulEquiv : ∀ (G : Type u) [inst : Group G] [Finite G], ∃ G' x x_1, Nonempty (G ≃* G')
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s t : Set α},
  LowerHemicontinuousOn f s → t ⊆ s → LowerHemicontinuousOn f t
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- Given a linear map `f : N → P`, `f ⊗ M` is bijective if and only if `M ⊗ f` is bijective.  -/
LinearMap.lTensor_bij_iff_rTensor_bij : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P),
  Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑(LinearMap.rTensor M f)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.collect : Lean.Meta.FunIndInfo → Lean.MVarId → Lean.MetaM (Array Lean.Expr)
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- If `f, g` is an `F`-cosplit pair, then `F` reflects limits for `parallelPair f g`.  -/
CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F] {A B : C}
  (f g : A ⟶ B) [F.IsCosplitPair f g], CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) F
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.splitMutualPreamble : Array Lean.Syntax → Option (Array Lean.Syntax × Array Lean.Syntax)
-- Std.Async.Basic
/-- Awaits the result of `t α` and returns it inside the `m` monad.
 -/
Std.Async.MonadAwait.await : {t m : Type → Type} → [self : Std.Async.MonadAwait t m] → {α : Type} → t α → m α
-- Mathlib.Data.Matrix.Reflection
/-- `∀` with better defeq for `∀ x : Matrix (Fin m) (Fin n) α, P x`.  -/
Matrix.Forall : {α : Type u_1} → {m n : ℕ} → (Matrix (Fin m) (Fin n) α → Prop) → Prop
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiff.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {n : WithTop ℕ∞}, ContDiff ℝ n f → (∀ (x : G), f x ≠ 0) → ContDiff ℝ n fun y => ‖f y‖
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.sub.inj : ∀ {a b a_1 b_1 : Lean.Grind.CommRing.Expr}, a.sub b = a_1.sub b_1 → a = a_1 ∧ b = b_1
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  [hw : w.GuitartExact] [hw' : w'.GuitartExact], (w.vComp w').GuitartExact
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsClosedImmersion
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.pointwise_smul_subset_iff : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S T : Submonoid M}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] [inst_3 : CategoryTheory.Closed Y] (f : X ⟶ Y) {Z_1 : C} (h : X ⟹ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.curry' f) (Y ⟹ Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp X Y Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Y ⟹ Z)).hom
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Z) h)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_ae_le_condExp_sq : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  m ≤ m₀ →
    ∀ [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.MemLp X 2 μ → ProbabilityTheory.condVar m X μ ≤ᵐ[μ] μ[X ^ 2 | m]
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.State.mk : Array Lean.Meta.Grind.AC.Struct →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
    Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ) → ℕ → Lean.Meta.Grind.AC.State
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_refl : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A : DiscreteQuotient X}, DiscreteQuotient.ofLE ⋯ = id
-- Lean.Meta.Tactic.Grind.Internalize
/-- Adds `e` to congruence table.  -/
Lean.Meta.Grind.addCongrTable : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] {Z : D}
  (h : F.obj (CategoryTheory.Abelian.image f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruImage (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).inv h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruImage f)) h
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.localizerMorphism C).functor = HomotopicalAlgebra.CofibrantObject.ι
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.π_comp_eqToHom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.Limits.biproduct.π f j'
-- Mathlib.Data.Stream.Init
Stream'.enum_eq_zip : ∀ {α : Type u} (s : Stream' α), s.enum = Stream'.zip Prod.mk Stream'.nats s
-- Mathlib.Data.List.ProdSigma
List.product_nil : ∀ {α : Type u_1} {β : Type u_2} (l : List α), l ×ˢ [] = []
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α],
  UniformContinuous fun p => p.1 + p.2
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_ofArrows_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Z : I → C) (f : (i : I) → Z i ⟶ X)
  {X' : C} (e : X' ≅ X),
  CategoryTheory.Sieve.pullback e.hom (CategoryTheory.Sieve.ofArrows Z f) =
    CategoryTheory.Sieve.ofArrows Z fun i => CategoryTheory.CategoryStruct.comp (f i) e.inv
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.exception : Lean.Elab.Tactic.EvalTacticFailure → Lean.Exception
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive commutative monoid, if it
admits a surjective map that preserves `0` and `+` to an additive commutative monoid.  -/
Function.Surjective.addCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : SMul ℕ M₂] →
          [inst_3 : AddCommMonoid M₁] →
            (f : M₁ → M₂) →
              Function.Surjective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddCommMonoid M₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_refl : ∀ {α : Type u} [inst : Add α], (AddEquiv.refl α).withBotCongr = AddEquiv.refl (WithBot α)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
StandardBorelSpace.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α], (∃ x, BorelSpace α ∧ PolishSpace α) → StandardBorelSpace α
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.cmp_veblenWith.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → motive x
-- Aesop.Tree.ExtractScript
Aesop.RappRef.extractSafePrefixScriptCore : Aesop.RappRef → Aesop.ExtractScriptM Unit
-- Init.Data.Array.Lex.Lemmas
List.lt_toArray : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, l₁.toArray < l₂.toArray ↔ l₁ < l₂
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_eq : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (e : σ →₀ ℕ) (r : σ → R),
  (MvPowerSeries.monomial e) (e.prod fun s n => r s ^ n) = e.prod fun s e => (r s • MvPowerSeries.X s) ^ e
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Over.coprod_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {A : C}
  (f : CategoryTheory.Over A), CategoryTheory.Over.coprod.obj f = f.coprodObj
-- Mathlib.Data.Finset.Basic
Finset.insert_erase_invOn : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, Set.InvOn (insert a) (fun s => s.erase a) {s | a ∈ s} {s | a ∉ s}
-- Init.Grind.PP
Lean.Grind.NodeDefUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.quot_lift_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β)
  (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂), Quot.lift f H (FreeGroup.mk L) = f L
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_right_strictMono : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a : α}, StrictMono fun x => a + x
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_eq_cast_of_dvd' : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) {a : ℤ},
  IsCoprime a ↑m → ((DirichletCharacter.changeLevel hm) χ) ↑a = χ ↑a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPushforward_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.functorPushforward (F.comp G) R =
    CategoryTheory.Presieve.functorPushforward G (CategoryTheory.Presieve.functorPushforward F R)
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.getFixedParamPerms : Array Lean.Elab.PreDefinition → Lean.MetaM Lean.Elab.FixedParamPerms
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.nndist_zero_eq_val : ∀ (z : NNReal), nndist 0 z = z
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderOrd.isLE_compare : ∀ {α : Type u} {inst : Ord α} {inst_1 : LE α} [self : Std.LawfulOrderOrd α] (a b : α), (compare a b).isLE = true ↔ a ≤ b
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.mk : ∀ {G : Type u_9} {P : Type u_10} [inst : SMul G P] [toIsLeftCancelSMul : IsLeftCancelSMul G P],
  (∀ (a b : G) (c : P), a • c = b • c → a = b) → IsCancelSMul G P
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) {s : Set β},
  MeasurableSet s →
    Measurable fun p =>
      (κ p.1) (MeasurableSpace.countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (MeasurableSpace.countablePartitionSet n p.2)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n),
  CochainComplex.HomComplex.Cochain.rightShift 0 a n' hn' = 0
-- Init.Data.List.Nat.TakeDrop
List.drop_reverse : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, List.drop i xs.reverse = (List.take (xs.length - i) xs).reverse
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
/-- `IsMinimalPrime p` says that `p` is a minimal prime of the ring.  -/
IsMinimalPrime : {R : Type u_1} → [inst : CommSemiring R] → Ideal R → Prop
-- Mathlib.GroupTheory.IsSubnormal
/-- The image of a subnormal subgroup under a surjective homomorphism is subnormal.  -/
Subgroup.IsSubnormal.map : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {G' : Type u_2} [inst_1 : Group G'] {f : G →* G'},
  Function.Surjective ⇑f → H.IsSubnormal → (Subgroup.map f H).IsSubnormal
-- Mathlib.Data.Num.Bitwise
Num.instXorOp : XorOp Num
-- Mathlib.Order.MinMax
instAssociativeMin : ∀ {α : Type u} [inst : LinearOrder α], Std.Associative min
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.map_le_iff_le_comap : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C)
  (T : CategoryTheory.Subgroupoid D),
  CategoryTheory.Subgroupoid.map φ hφ S ≤ T ↔ S ≤ CategoryTheory.Subgroupoid.comap φ T
-- Mathlib.Tactic.Push
/-- The syntax is `#pull head e`, where `head` is a constant and `e` is an expression,
which will print the `pull head` form of `e`.

`#pull` understands local variables, so you can use them to introduce parameters.
 -/
Mathlib.Tactic.Push.pullCommand : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.pow_cpow_nat_inv : ∀ {x : ℂ} {n : ℕ}, n ≠ 0 → -(Real.pi / ↑n) < x.arg → x.arg ≤ Real.pi / ↑n → (x ^ n) ^ (↑n)⁻¹ = x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall : Type
-- Mathlib.Data.Seq.Defs
/-- Get the first element of a sequence  -/
Stream'.Seq.head : {α : Type u} → Stream'.Seq α → Option α
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
/-- The `G`-action on `X` is proper iff, for each pair of compacts `U, V` in `X`,
the set of `g` such that `U` intersects `g • V` is compact.

See `ProperSMul.isCompact_setOfPred_inter_nonempty`
for a one-way implication with fewer conditions.

**Note**: We assume `CompactlyCoherentSpace (X × X)`
as this is the minimal assumption needed to make the proof work;
but this follows from various more familiar conditions,
such as `FirstCountableTopology X`.
Importing `Mathlib.Topology.Sequences` makes this implication available.
 -/
MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  [inst_3 : MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousSMul G X],
  ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.zsmul : {M N : SemiNormedGrp} → SMul ℤ (M ⟶ N)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instNonemptyMapEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : α ≃ β}, (M.mapEquiv f).Nonempty
-- Std.Tactic.BVDecide.LRAT.Internal.Actions
/-- `Action` where variables have type `PosFin n`, clauses are `DefaultClause`, and ids are `Nat`.
This Action type is meant to be usable for verifying LRAT proofs that operate on default formulas.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction : ℕ → Type