mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_mono : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  Monotone Nat.floor
-- Mathlib.Data.EReal.Operations
EReal.add_ne_top_iff_ne_top_right : ∀ {x y : EReal}, x ≠ ⊥ → x ≠ ⊤ → (x + y ≠ ⊤ ↔ y ≠ ⊤)
-- Mathlib.Data.ENat.Basic
ENat.mul_right_strictMono : ∀ {a : ℕ∞}, a ≠ 0 → a ≠ ⊤ → StrictMono fun x => a * x
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.denote_insertSorted : ∀ (ctx : Nat.Internal.Linear.Context) (k : ℕ) (m : Nat.Internal.SOM.Mon) (p : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (Nat.Internal.SOM.Poly.insertSorted k m p) =
    Nat.Internal.SOM.Poly.denote ctx p + k * Nat.Internal.SOM.Mon.denote ctx m
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_bijective : ∀ {n : ℕ} (R : Type u_1) [inst : Ring R] [inst_1 : CharP R n] [inst_2 : Fintype R],
  Fintype.card R = n → Function.Bijective ⇑(ZMod.castHom ⋯ R)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 1]` which avoids `2`.  -/
SSet.horn₃₁.ι₂ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 1).toSSet
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.IsChain.cons_of_imp`. -/
List.IsChain.cons_of_imp_of_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} {b : α},
  (∀ (c : α), R a c → R b c) → List.IsChain R (a :: l) → List.IsChain R (b :: l)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.inv` -/
UniformCauchySeqOn.fun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn (fun i i_1 => (f i i_1)⁻¹) l s
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.MakesOverArrow.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {u : F.obj (Opposite.op X)},
  (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) u = CategoryTheory.yonedaEquiv s →
    CategoryTheory.OverPresheafAux.MakesOverArrow η s u
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimit_toDual_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a
-- Mathlib.Tactic.MinImports
/-- `getIrredundantImports env importNames` takes an `Environment` and a `NameSet` as inputs.
Assuming that `importNames` are module names,
it returns the `NameSet` consisting of a minimal collection of module names whose transitive
closure is enough to parse (and elaborate) `cmd`.  -/
Mathlib.Command.MinImports.getIrredundantImports : Lean.Environment → Lean.NameSet → Lean.NameSet
-- Mathlib.Data.List.Sort
List.sortedLE_mergeSort : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α], (l.mergeSort fun x1 x2 => decide (x1 ≤ x2)).SortedLE
-- Lean.Message
Lean.instToStringMessageSeverity : ToString Lean.MessageSeverity
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg : ∀ {x y : ℝ*}, ¬x.Infinitesimal → 0 < x → y.InfiniteNeg → (x * y).InfiniteNeg
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_hom_apply_2_2 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.2 = x.2
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} (p : ENNReal)
  {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (g : α → F) (b : E → F → G) (c : NNReal),
      (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
        MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤
          ↑c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g ⊤ μ
-- Mathlib.Data.Rat.Floor
Rat.isInt_round : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℤ), Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt (round r) m
-- Mathlib.Algebra.Group.Submonoid.BigOperators
SubmonoidClass.coe_finsetProd : ∀ {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [inst : CommMonoid M] [inst_1 : SetLike B M]
  [inst_2 : SubmonoidClass B M] (f : ι → ↥S) (s : Finset ι), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_def : ∀ (R : Type u_3) [inst : CommSemiring R] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.ι R = { toFun := fun m => ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- Given a morphism `f : X ⟶ Y` in a model category,
this structure contains the data of a factorization `i ≫ p = f`
with `i` a cofibration, `p` a trivial fibration which
has a section `s` that is a cofibration.
That this structure is nonempty when `X`
and `Y` are cofibrant is Ken Brown's factorization lemma.  -/
HomotopicalAlgebra.CofibrantBrownFactorization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [HomotopicalAlgebra.ModelCategory C] → {X Y : C} → (X ⟶ Y) → Type (max u_1 v_1)
-- Mathlib.Algebra.Order.Field.Basic
monotone_div_right_of_nonneg : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α},
  0 ≤ a → Monotone fun x => x / a
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_app : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens),
  AlgebraicGeometry.Scheme.Hom.app (X.homOfLE e) W = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Order.LatticeIntervals
Set.Ico.semilatticeInf : {α : Type u_1} → [inst : SemilatticeInf α] → {a b : α} → SemilatticeInf ↑(Set.Ico a b)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_X_mul : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S],
  (Polynomial.X * p).smeval x = x * p.smeval x
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensor_hom_ext : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{u, u, v} k G} {M : ModuleCat k}
  {f g : ((Rep.coinvariantsTensor k G).obj A).obj B ⟶ M},
  (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f) = (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g) →
    f = g
-- Mathlib.Tactic.Positivity.Core
/-- The main combinator which combines multiple `positivity` results.
It assumes `t₁` has already been run for a result, and runs `t₂` and takes the best result.
It will skip `t₂` if `t₁` is already a proof of `.positive`, and can also combine
`.nonnegative` and `.nonzero` to produce a `.positive` result.  -/
Mathlib.Meta.Positivity.orElse : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {pα? : Option Q(PartialOrder «$α»)} →
        {e : Q(«$α»)} →
          Mathlib.Meta.Positivity.Strictness zα e pα? →
            Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?) →
              Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If a presieve contains a split epi, it generates the maximal sieve.  -/
CategoryTheory.Sieve.generate_of_contains_isSplitEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {R : CategoryTheory.Presieve X} (f : Y ⟶ X)
  [CategoryTheory.IsSplitEpi f], R f → CategoryTheory.Sieve.generate R = ⊤
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_add : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C₁ C₂ : ConvexCone R M), ↑(C₁ + C₂) = ↑C₁ + ↑C₂
-- Mathlib.Topology.EMetricSpace.Defs
/-- Characterizing uniformities associated to a (generalized) distance function `D`
in terms of the elements of the uniformity.  -/
uniformity_dist_of_mem_uniformity : ∀ {α : Type u} {β : Type v} [inst : LT β] {U : Filter (α × α)} (z : β) (D : α → α → β),
  (∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) →
    U = ⨅ ε, ⨅ (_ : ε > z), Filter.principal {p | D p.1 p.2 < ε}
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `PlainDate` to a `WallTime`.
 -/
Std.Time.PlainDate.toWallTime : Std.Time.PlainDate → Std.Time.WallTime
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift_inr : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) (g : G),
  (SemidirectProduct.lift fn fg h) (SemidirectProduct.inr g) = fg g
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the least upper bound of `s` and `b` is the least upper bound of `t`,
then `a ⊔ b` is the least upper bound of `s ∪ t`.  -/
IsLUB.union : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] {a b : γ} {s t : Set γ}, IsLUB s a → IsLUB t b → IsLUB (s ∪ t) (a ⊔ b)
-- Aesop.Options.Public
Aesop.instInhabitedStrategy : Inhabited Aesop.Strategy
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).reverse = p.reverse.copy hv hu
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op)
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app Y) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) f
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_descHomology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : S.cycles ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.toCycles k = 0),
  CategoryTheory.CategoryStruct.comp S.homologyπ (S.descHomology k hk) = k
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.lt_of_parentD : ∀ {arr : Array Batteries.UFNode} {i : ℕ}, Batteries.UnionFind.parentD arr i ≠ i → i < arr.size
-- Init.Prelude
/-- Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : UInt32) ≤ 7 by decide`
 -/
UInt32.decLe : (a b : UInt32) → Decidable (a ≤ b)
-- Mathlib.Algebra.Order.Field.GeomSum
geom₂_sum_of_lt : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K]
  [inst_4 : Sub K] [OrderedSub K] {x y : K},
  x < y → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.lsub_lt_ord_lift_of_isRegular : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} (Cardinal.mk ι) < c → (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ ^ p ^ s - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `p ^ p ^ s` if `s ≤ k` and `p ^ (k - s + 1) ≠ 2`.  -/
IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ},
  s ≤ k → p ^ (k - s + 1) ≠ 2 → (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.Tactic.ITauto
/-- A reified inductive type for propositional logic.  -/
Mathlib.Tactic.ITauto.IProp : Type
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionOptions.mk.injEq : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions)
  (codeActionKinds? : Option (Array Lean.Lsp.CodeActionKind)) (resolveProvider? : Option Bool)
  (toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions)
  (codeActionKinds?_1 : Option (Array Lean.Lsp.CodeActionKind)) (resolveProvider?_1 : Option Bool),
  ({ toWorkDoneProgressOptions := toWorkDoneProgressOptions, codeActionKinds? := codeActionKinds?,
        resolveProvider? := resolveProvider? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, codeActionKinds? := codeActionKinds?_1,
        resolveProvider? := resolveProvider?_1 }) =
    (toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧
      codeActionKinds? = codeActionKinds?_1 ∧ resolveProvider? = resolveProvider?_1)
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.smulAntidiagonal_mono_left : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s u : Set G} {t : Set P} (a : P),
  u ⊆ s →
    ∀ (hst : (s.smulAntidiagonal t a).Finite) (hut : (u.smulAntidiagonal t a).Finite),
      Finset.SMulAntidiagonal a hut ⊆ Finset.SMulAntidiagonal a hst
-- Mathlib.RepresentationTheory.Intertwining
/-- An unbundled version of `IntertwiningMap`.  -/
Representation.IsIntertwiningMap : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] → Representation A G V → Representation A G W → (V →ₗ[A] W) → Prop
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_mul_Ioi_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → (fun x => a * x) '' Set.Ioi 0 = Set.Ioi 0
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.notMem_uIcc_of_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < c → b < c → c ∉ Set.uIcc a b
-- Mathlib.Logic.Function.OfArity
Function.ofArity_succ : ∀ (α β : Type u) (n : ℕ), Function.OfArity α β n.succ = (α → Function.OfArity α β n)
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instFullEtaleSpec : ∀ {S : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.AffineEtale.Spec S).Full
-- Mathlib.Geometry.Manifold.Notation
/-- `mfderiv[u] f x` elaborates to `mfderivWithin I J f u x`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termMfderiv[_]__» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂)
  (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂ c₄).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁ c₃).hom
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)
-- Mathlib.Data.Nat.Factorial.BigOperators
_private.Mathlib.Data.Nat.Factorial.BigOperators.0.Nat.factorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- The ring version of `AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum`.  -/
addMonoidAlgebraRingEquivDirectSum : {ι : Type u_1} →
  {M : Type u_3} →
    [inst : DecidableEq ι] →
      [inst_1 : AddMonoid ι] →
        [inst_2 : Semiring M] → [(m : M) → Decidable (m ≠ 0)] → AddMonoidAlgebra M ι ≃+* DirectSum ι fun x => M
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.bind_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {g : Z ⟶ Y} (h₁ : S f),
  R h₁ g → S.bind R (CategoryTheory.CategoryStruct.comp g f)
-- Lean.PrettyPrinter.Parenthesizer
/-- Registers a parenthesizer for a parser combinator.

`@[combinator_parenthesizer c, expose]` registers a declaration of type `Lean.PrettyPrinter.Parenthesizer`
for the `Parser` declaration `c`. Note that, unlike with `@[parenthesizer]`, this is not a node kind
since combinators usually do not introduce their own node kinds. The tagged declaration may
optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is
replaced with `Parenthesizer` in the parameter types.
 -/
Lean.PrettyPrinter.combinatorParenthesizerAttribute : Lean.ParserCompiler.CombinatorAttribute
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_pos_of_pos : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 < z → 0 < z⁻¹
-- Init.Classical
/-- The Hilbert epsilon function.  -/
Classical.epsilon : {α : Sort u} → [h : Nonempty α] → (α → Prop) → α
-- Lean.Parser.Types
Lean.Parser.ParserState.recoveredErrors : Lean.Parser.ParserState → Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_dist_eq_card : ∀ {α : Type u_2} {β : Type u_3} [inst : Dist α] [inst_1 : Dist β] (f g : WithLp 0 (α × β)),
  dist f g = (if dist f.fst g.fst = 0 then 0 else 1) + if dist f.snd g.snd = 0 then 0 else 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filterMap f t) k fallback =
      ((Std.ExtDTreeMap.Const.get? t k).bind (f k')).getD fallback
-- Mathlib.Order.Monotone.Basic
antitone_int_of_succ_le : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α}, (∀ (n : ℤ), f (n + 1) ≤ f n) → Antitone f
-- Mathlib.Geometry.Manifold.Immersion
/-- Prefer using `IsImmersionAtOfComplement.continuousAt` instead  -/
Manifold.IsImmersionAtOfComplement.continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), ContinuousOn f h.domChart.source
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_one : ∀ {α : Type u_1} [inst : One α], SymAlg.unsym 1 = 1
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The functor which sends `X : C` to the graded object which is `X` in degree `j`
and the initial object in other degrees.  -/
CategoryTheory.GradedObject.single : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [CategoryTheory.Limits.HasInitial C] →
        [DecidableEq J] → J → CategoryTheory.Functor C (CategoryTheory.GradedObject J C)
-- Mathlib.Order.Heyting.Basic
/-- Transfer `GeneralizedCoheytingAlgebra` across an `Equiv`.  -/
Equiv.generalizedCoheytingAlgebra : {α : Type u_2} → {β : Type u_3} → α ≃ β → [GeneralizedCoheytingAlgebra β] → GeneralizedCoheytingAlgebra α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp S.leftHomologyIso.inv h) =
    CategoryTheory.CategoryStruct.comp S.leftHomologyπ h
-- Mathlib.Order.Disjoint
Disjoint.ne_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → (a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Given a matrix with invertible determinant, we get an element of `GL n R`.  -/
Matrix.GeneralLinearGroup.mk' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → (A : Matrix n n R) → Invertible A.det → GL n R
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineMap.span_eq_top_of_surjective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁},
  Function.Surjective ⇑f → affineSpan k s = ⊤ → affineSpan k (⇑f '' s) = ⊤
-- ProofWidgets.Component.FilterDetails
/-- What is shown in the filtered state.  -/
ProofWidgets.FilterDetailsProps.filtered : ProofWidgets.FilterDetailsProps → ProofWidgets.Html
-- Mathlib.Analysis.Normed.Group.Continuity
/-- See `tendsto_norm_zero` for a version with pointed neighborhoods.  -/
tendsto_norm_zero : ∀ {E : Type u_4} [inst : SeminormedAddGroup E], Filter.Tendsto (fun a => ‖a‖) (nhds 0) (nhds 0)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.monObjAsOverPullback_mul : ∀ {M S T : AlgebraicGeometry.Scheme} [inst : M.Over S] {f : T ⟶ S} [inst_1 : CategoryTheory.MonObj (M.asOver S)],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk (M ↘ S))
        (CategoryTheory.Over.mk (M ↘ S)))
      ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.mul)
-- Init.Prelude
/-- An overloaded operation to find the greater of two values of type `α`.
 -/
Max : Type u → Type u
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatExtendScalarsPseudofunctor_obj : ∀ (b : CategoryTheory.LocallyDiscrete CommRingCat),
  CommRingCat.moduleCatExtendScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑b.as)
-- Mathlib.GroupTheory.Perm.Sign
/-- `swapFactors` represents a permutation as a product of a list of transpositions.
The representation is nonunique and depends on the linear order structure.
For types without linear order `truncSwapFactors` can be used.  -/
Equiv.Perm.swapFactors : {α : Type u} →
  [inst : DecidableEq α] → [Fintype α] → [LinearOrder α] → (f : Equiv.Perm α) → { l // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }
-- Init.Data.Nat.Basic
Nat.le_of_succ_le : ∀ {n m : ℕ}, n.succ ≤ m → n ≤ m