mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.LibrarySuggestions.Basic
/-- Respect the `Config.filter` option by implementing it as a post-filter.
If a premise selection implementation does not natively handle the filter,
it should be wrapped with this function.
 -/
Lean.LibrarySuggestions.Selector.postFilter : Lean.LibrarySuggestions.Selector → Lean.LibrarySuggestions.Selector
-- Mathlib.Topology.Sets.Compacts
IsOpen.exists_positiveCompacts_closure_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [R1Space α] [LocallyCompactSpace α] {U : Set α},
  IsOpen U → U.Nonempty → ∃ K, closure ↑K ⊆ U
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.splits_of_separable : ∀ {k : Type u} {inst : Field k} [self : IsSepClosed k] (p : Polynomial k), p.Separable → p.Splits
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_mk_lift : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : Algebra.IsAlgebraic k K] (φ : k →+* ℂ),
  (NumberField.InfinitePlace.mk (NumberField.ComplexEmbedding.lift K φ)).comap (algebraMap k K) =
    NumberField.InfinitePlace.mk φ
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) ⁻¹' Set.Ioc b c = Set.Ico (a - c) (a - b)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.apply_one : ∀ {E : Type u_3} [inst : AddGroup E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 0 then 0 else 1
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter.eq_1 : ∀ (i : ℕ) {n m : ℕ} (hi : n + i = m),
  SimplexCategory.σ₀Iter i hi =
    SimplexCategory.Hom.mk { toFun := fun j => if ↑j < i then 0 else ⟨↑j - i, ⋯⟩, monotone' := ⋯ }
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `IsLocalization S T`, then `M[S⁻¹]` is a `T`-module.
This should eventually be replaced with `IsLocalizedModule f N` and `Module T N`.  -/
LocalizedModule.moduleOfIsLocalization : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {T : Type u_1} →
              [inst_3 : CommSemiring T] → [inst_4 : Algebra R T] → [IsLocalization S T] → Module T (LocalizedModule S M)
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α},
  s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty
-- Mathlib.Tactic.FunProp.Mor
/-- If the given expression is a sequence of morphism applications `f a₁ .. aₙ`, return `f`.
Otherwise return the input expression.
 -/
Mathlib.Meta.FunProp.Mor.getAppFn : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ofHom_apply : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (f : X ↪o Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (PartOrdEmb.ofHom f)) x = f x
-- Mathlib.Topology.Order.Monotone
/-- If an antitone function sending `top` to `bot` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed supremum of the composition.  -/
Antitone.map_iInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β}
  {g : ι → α}, ContinuousAt f (iInf g) → Antitone f → f ⊤ = ⊥ → f (iInf g) = iSup (f ∘ g)
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.antipodeAlgHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : HopfAlgebra R A] (a : A),
  (HopfAlgebra.antipodeAlgHom R A) a = (HopfAlgebraStruct.antipode R) a
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.mul_left : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a * c) (b * c)
-- Mathlib.Data.Set.Subsingleton
Set.singleton_ne_univ : ∀ {α : Type u} [Nontrivial α] (a : α), {a} ≠ Set.univ
-- Mathlib.Order.Filter.Bases.Basic
/-- The sequence of sets is antitone.  -/
Filter.HasAntitoneBasis.antitone : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasAntitoneBasis s → Antitone s
-- Mathlib.Data.Fintype.Card
Fintype.existsUnique_iff_card_one : ∀ {α : Type u_4} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p], (∃! a, p a) ↔ {x | p x}.card = 1
-- Mathlib.Order.Filter.Germ.Basic
/-- Lift a binary function `β → γ → δ` to a function `Germ l β → Germ l γ → Germ l δ`.  -/
Filter.Germ.map₂ : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → {l : Filter α} → (β → γ → δ) → l.Germ β → l.Germ γ → l.Germ δ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.deriv_cos' : deriv Complex.cos = fun x => -Complex.sin x
-- Mathlib.Topology.Compactness.Compact
/-- A set belongs to `coclosedCompact` if and only if the closure of its complement is compact.  -/
Filter.mem_coclosedCompact_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.coclosedCompact X ↔ IsCompact (closure sᶜ)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_eq_none_iff : ∀ {α : Type u} {s : Stream'.Seq α}, s.head = none ↔ s = Stream'.Seq.nil
-- Mathlib.Data.FunLike.Graded
GradedEquivLike.mk : ∀ {E : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {σ : outParam (Type u_4)} {τ : outParam (Type u_5)}
  {ι : outParam (Type u_6)} [inst : SetLike σ A] [inst_1 : SetLike τ B] {𝒜 : outParam (ι → σ)} {ℬ : outParam (ι → τ)}
  [inst_2 : EquivLike E A B], (∀ (e : E) {i : ι} {x : A}, e x ∈ ℬ i ↔ x ∈ 𝒜 i) → GradedEquivLike E 𝒜 ℬ
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A comonoid object in a functor category sends any object to a comonoid object.  -/
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (A : CategoryTheory.Functor C D) → [CategoryTheory.ComonObj A] → C → CategoryTheory.Comon D
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.accPt_comap_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → ∀ {x : X} {l : Filter Y}, AccPt x (Filter.comap f l) ↔ AccPt (f x) l
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ),
  sq.unop.X₂ = Opposite.unop sq.X₂
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) {X_1 Y : SimplexCategoryᵒᵖ}
  (θ : X_1 ⟶ Y), (AlgebraicTopology.DoldKan.Γ₀.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_nonempty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ioi a).Nonempty ↔ ¬IsMax a
-- Init.Tactics
/-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables.  -/
Lean.Parser.Tactic.DecideConfig.zetaReduce : Lean.Parser.Tactic.DecideConfig → Bool
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.symm_bijective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)},
  Function.Bijective ContinuousMap.Homotopy.symm
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHSubOffset_1 : HSub Std.Time.PlainTime Std.Time.Millisecond.Offset Std.Time.PlainTime
-- Mathlib.CategoryTheory.Groupoid
/-- A `SmallGroupoid` is a groupoid
where the objects and morphisms live in the same universe.
 -/
CategoryTheory.SmallGroupoid : Type u → Type (u + 1)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- The projective seminorm on `⨂[𝕜] i, Eᵢ`. It sends an element `x` of `⨂[𝕜] i, Eᵢ` to the
infimum over all expressions of `x` as `∑ j, ⨂ₜ[𝕜] mⱼ i` (with the `mⱼ` ∈ `Π i, Eᵢ`)
of `∑ j, Π i, ‖mⱼ i‖`.  -/
PiTensorProduct.projectiveSeminorm : {ι : Type u_1} →
  [Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_1 : NormedField 𝕜] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] → Seminorm 𝕜 (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.algebraMap_eq : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A},
  algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x) = HomogeneousLocalization.fromZeroRingHom 𝒜 x
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- `•` and `⁅⬝, ⬝⁆`  are left commutative  -/
LieDerivation.SMulBracketCommClass.smul_bracket_comm : ∀ {S : Type u_4} {L : Type u_5} {α : Type u_6} {inst : SMul S α} {inst_1 : LieRing L} {inst_2 : AddCommGroup α}
  {inst_3 : LieRingModule L α} [self : LieDerivation.SMulBracketCommClass S L α] (s : S) (l : L) (a : α),
  s • ⁅l, a⁆ = ⁅l, s • a⁆
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- **Alias** of the forward direction of `isCauSeq_neg`. -/
IsCauSeq.of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β}, IsCauSeq abv (-f) → IsCauSeq abv f
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
`f` has `p` as a finite power series on the ball of radius `r > 0` around `x` if
`f (x + y) = ∑' pₘ yᵐ` for all `‖y‖ < r` and `pₙ = 0` for `n ≤ m`.  -/
HasFiniteFPowerSeriesOnBall : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → FormalMultilinearSeries 𝕜 E F → E → ℕ → ENNReal → Prop
-- Init.Data.Nat.Lemmas
Nat.sub_max_sub_right : ∀ (a b c : ℕ), max (a - c) (b - c) = max a b - c
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The right homotopy relation on the category of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.homRel : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] → HomRel (HomotopicalAlgebra.CofibrantObject C)
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The empty hypergraph (bottom) on a type.  -/
Hypergraph.instBot : (α : Type u_4) → Bot (Hypergraph α)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instUniqueCarrierCarrierCommRingCatSpecOf : {K : Type u_1} → [inst : Field K] → Unique ↥(AlgebraicGeometry.Spec (CommRingCat.of K))
-- Lean.Hygiene
_private.Lean.Hygiene.0.Lean.sanitizeSyntaxAux : Lean.Syntax → StateM Lean.NameSanitizerState Lean.Syntax
-- Mathlib.Algebra.GroupWithZero.Defs
MonoidWithZero.toMonoid : {M₀ : Type u} → [self : MonoidWithZero M₀] → Monoid M₀
-- Mathlib.Tactic.NormNum.BigOperators
/-- `n` unifies with `succ n'` for this specific `n'`  -/
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ : {n : Q(ℕ)} → (n' : Q(ℕ)) → «$n» =Q «$n'».succ → Mathlib.Meta.Nat.UnifyZeroOrSuccResult n
-- Lean.Setup
Lean.ModuleArtifacts.mk.sizeOf_spec : ∀ (lean? olean? oleanServer? oleanPrivate? ilean? irSig? ir? c? bc? : Option System.FilePath),
  sizeOf
      { lean? := lean?, olean? := olean?, oleanServer? := oleanServer?, oleanPrivate? := oleanPrivate?,
        ilean? := ilean?, irSig? := irSig?, ir? := ir?, c? := c?, bc? := bc? } =
    1 + sizeOf lean? + sizeOf olean? + sizeOf oleanServer? + sizeOf oleanPrivate? + sizeOf ilean? + sizeOf irSig? +
          sizeOf ir? +
        sizeOf c? +
      sizeOf bc?
-- Mathlib.Topology.Separation.Basic
/-- Specialization forms a partial order on a t0 topological space.  -/
specializationOrder : (X : Type u_3) → [inst : TopologicalSpace X] → [T0Space X] → PartialOrder X
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
/-- The real logarithm, defined via the continuous functional calculus. This can be used on
matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc.  -/
CFC.log : {A : Type u_1} →
  [inst : NormedRing A] →
    [inst_1 : StarRing A] → [inst_2 : NormedAlgebra ℝ A] → [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → A → A
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A morphism which is a coequalizer for its kernel pair is an effective epi.  -/
CategoryTheory.effectiveEpi_of_kernelPair : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B)
  [inst_1 : CategoryTheory.Limits.HasPullback f f]
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)), CategoryTheory.EffectiveEpi f
-- Init.Data.UInt.Lemmas
UInt64.neg_mul_not_eq_add_mul : ∀ {a b : UInt64}, -(a * ~~~b) = a + a * b
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.eq_def : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) (x : List α),
  List.findM? p x =
    match x with
    | [] => pure none
    | a :: as => do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => List.findM? p as
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- A subgroup of the permutation group of index ≤ 2 contains the alternating group.  -/
Equiv.Perm.alternatingGroup_le_of_index_le_two : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {G : Subgroup (Equiv.Perm α)},
  G.index ≤ 2 → alternatingGroup α ≤ G
-- Mathlib.Computability.Primrec.Basic
Primrec₂.right : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec₂ fun x b => b
-- Mathlib.Topology.Homotopy.Lifting
/-- Monodromy of a covering map as a functor. Definition 2.1 in
https://ncatlab.org/nlab/show/monodromy.  -/
IsCoveringMap.monodromyFunctor : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → CategoryTheory.Functor (FundamentalGroupoid X) (Type u_1)
-- Init.Data.List.Find
List.head_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (h : List.filterMap f l ≠ []),
  (List.filterMap f l).head h = (List.findSome? f l).get ⋯
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.isOpenMap_im : IsOpenMap UpperHalfPlane.im
-- Lean.Parser.Term
/-- `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
 -/
Lean.Parser.Term.pipeProj : Lean.Parser.TrailingParser
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] {M₁ : Type u_3} {M₂ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommGroup M₂] [inst_7 : Module 𝕜₁ M₁]
  [inst_8 : Module 𝕜₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] [inst_10 : ContinuousConstSMul 𝕜₁ M₁]
  [inst_11 : IsTopologicalAddGroup M₂] [inst_12 : ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
  (hf : IsCompactOperator ⇑f), ContinuousLinearMap.mkOfIsCompactOperator hf ∈ compactOperator σ₁₂ M₁ M₂
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_inv_apply : ∀ {X Y : PartOrdEmb} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.CWComplex.mkFinite_cell : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo_iff_image_subset :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ),
  Topology.CWComplex.cell C n = Topology.RelCWComplex.cell C n
-- Mathlib.Order.CompleteLattice.Defs
isLUB_iff_sSup_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, IsLUB s a ↔ sSup s = a
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulOneClass α] → [inst_3 : MulOneClass β] → FunLike (α →*o β) α β
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonDependencyBuildMode.toJson : Lean.Lsp.DependencyBuildMode → Lean.Json
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_below_dvd`. -/
Ideal.inertiaDeg'_below_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], q.inertiaDeg R ∣ r.inertiaDeg R
-- Init.Meta.Defs
/-- Creates an identifier referring to a constant `c`. The identifier's position is copied from `src`.

This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally be captured.
 -/
Lean.mkCIdentFrom : Lean.Syntax → Lean.Name → optParam Bool false → Lean.Ident
-- Init.Data.Nat.Lemmas
Nat.sub_eq_max_sub : ∀ (n m : ℕ), n - m = max n m - m
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_7 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont') (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.fix, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_7 f k
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Tactic.CasesM
/-- Returns true if any of the patterns match the expression.  -/
Mathlib.Tactic.matchPatterns : Array Lean.Meta.AbstractMVarsResult → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
/-- The completion of a seminormed group, as an endofunctor on `SemiNormedGrp`.  -/
SemiNormedGrp.completion : CategoryTheory.Functor SemiNormedGrp SemiNormedGrp
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural cone over the forgetful functor `Under X ⥤ T` with cone point `X`.  -/
CategoryTheory.Under.forgetCone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → (X : T) → CategoryTheory.Limits.Cone (CategoryTheory.Under.forget X)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_le : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : ENNReal},
  (∀ (d' : NNReal), (MeasureTheory.Measure.hausdorffMeasure ↑d') s = ⊤ → ↑d' ≤ d) → dimH s ≤ d
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_30 : HSub Std.Time.Day.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.noConfusionType : Sort v✝ → Lean.Meta.NormCast.Label → Lean.Meta.NormCast.Label → Sort v✝
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_zero : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), Polynomial.smeval 0 x = 0
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.ne : ∀ {α : Type u_1} {M N : Matroid α}, N.IsStrictRestriction M → N ≠ M
-- Mathlib.Topology.Continuous
ContinuousAt.preimage_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}
  {t : Set Y}, ContinuousAt f x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhds x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instTopologicalSpace : {X : Type u_1} →
  {R : Type u_3} →
    [inst : Zero X] →
      [inst_1 : Zero R] →
        [inst_2 : TopologicalSpace X] → [inst_3 : TopologicalSpace R] → TopologicalSpace (ContinuousMapZero X R)
-- Mathlib.RingTheory.Ideal.Height
exists_spanRank_le_and_le_height_of_le_height : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R) (r : ℕ),
  ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_iff_isChain`. -/
List.IsChain.sortedLT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.IsChain (fun x1 x2 => x1 < x2) l → l.SortedLT
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.retraction.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f],
  CategoryTheory.retraction f = ⋯.some.retraction
-- Mathlib.Order.Notation
Max.ext : ∀ {α : Type u} {x y : Max α}, max = max → x = y
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instSMulMemClass : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  SMulMemClass (LieSubalgebra R L) R L
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.smul_lTensor : ∀ {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) {S : Type u_22} [inst_7 : CommSemiring S] [inst_8 : SMul R S]
  [inst_9 : Module S M] [IsScalarTower R S M] [inst_11 : SMulCommClass R S M] (s : S) (m : TensorProduct R M N),
  s • (LinearMap.lTensor M f) m = (LinearMap.lTensor M f) (s • m)
-- Mathlib.Algebra.Group.Submonoid.Defs
OneMemClass.one.eq_1 : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] (S' : A),
  OneMemClass.one S' = { one := ⟨1, ⋯⟩ }