mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_map_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).map φ).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_iSup : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_2} {f : ι → Submonoid M},
  (iSup f).saturation = ⨆ i, (f i).saturation
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.comp_counit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  (adj₁.comp adj₂).counit = adj₁.compCounit adj₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f (Std.DHashMap.Const.get? m k)).isSome = true → (Std.DHashMap.Const.alter m k f).size = m.size
-- Init.Data.Array.Lemmas
Array.mem_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, i < xs.size → a ∈ xs.setIfInBounds i a
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.ringInverse_ringInverse : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a b : M₀}, Commute a b → Commute (Ring.inverse a) (Ring.inverse b)
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isEqSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → α → Sort u_2) →
    (x : Option α) → (x_1 : α) → ((a b : α) → motive (some a) b) → ((x : α) → motive none x) → motive x x_1
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_range_embDomain_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α ↪ β) (x : β →₀ M),
  x ∈ Set.range (Finsupp.embDomain f) ↔ ↑x.support ⊆ Set.range ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.IsSplitMono c.inr
-- Std.Sync.StreamMap
_private.Std.Sync.StreamMap.0.Std.StreamMap.mk.sizeOf_spec : ∀ {α β : Type} [inst : SizeOf α] [inst_1 : SizeOf β] (streams : Array (α × Std.Async.Selector β × IO Unit)),
  sizeOf { streams := streams } = 1 + sizeOf streams
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_1 hr
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The image of a subfield along a ring homomorphism is a subfield.  -/
Subfield.map : {K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (K →+* L) → Subfield K → Subfield L
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- [Stacks Tag 01KZ](https://stacks.math.columbia.edu/tag/01KZ) -/
AlgebraicGeometry.IsSeparated.valuativeCriterion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.ValuativeCriterion.Uniqueness f
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
/-- Explicit formula for the norm of the Gaussian function along the vertical
edges.  -/
GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I : ∀ (b : ℂ) (c T : ℝ),
  ‖Complex.exp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ = Real.exp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.under_ne_bot : ∀ (A : Type u_1) [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] {P : Ideal B} [Nontrivial A] [IsDomain B], P ≠ ⊥ → Ideal.under A P ≠ ⊥
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricPMFReal_nonneg : ∀ {p : ℝ} {n : ℕ}, 0 < p → p ≤ 1 → 0 ≤ ProbabilityTheory.geometricPMFReal p n
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι]
  {π : BoxIntegral.TaggedPrepartition I},
  π.IsSubordinate r → J ∈ π.boxes → Metric.diam (BoxIntegral.Box.Icc J) ≤ 2 * ↑(r (π.tag J))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.toWorkDoneProgressParams : Lean.Lsp.SignatureHelpParams → Lean.Lsp.WorkDoneProgressParams
-- Init.System.IO
/-- Monotonically increasing time since an unspecified past point in nanoseconds. There is no relation
to wall clock time.
 -/
IO.monoNanosNow : BaseIO ℕ
-- Mathlib.RingTheory.WittVector.WittPolynomial
/-- `wittPolynomial p R n` is the `n`-th Witt polynomial
with respect to a prime `p` with coefficients in a commutative ring `R`.
It is defined as:

`∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`.  -/
wittPolynomial : ℕ → (R : Type u_1) → [inst : CommRing R] → ℕ → MvPolynomial ℕ R
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rco_eq_zero_iff : ∀ {m n i : ℕ}, (m...n).toArray[i]! = 0 ↔ n ≤ i + m ∨ m = 0 ∧ i = 0
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded.LE` using the modulus of a number.
 -/
Std.Time.Internal.Bounded.LE.byEmod : ℤ → (i : ℤ) → i > 0 → Std.Time.Internal.Bounded.LE 0 (i - 1)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.M : Type → Type
-- Batteries.Data.List.Lemmas
List.isSuffixOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (l₁ l₂ : List α),
  l₁.isSuffixOf? l₂ = Option.map List.reverse (l₁.reverse.isPrefixOf? l₂.reverse)
-- Lean.Message
/-- Lazy message data production, with access to the context as given by
a surrounding `MessageData.withContext` (which is expected to exist).
 -/
Lean.MessageData.lazy : (Lean.PPContext → BaseIO Lean.MessageData) →
  (optParam (Lean.MetavarContext → Bool) fun x => false) →
    (optParam (Unit → BaseIO Lean.MessageData) fun x =>
        pure (Lean.MessageData.ofFormat (Std.Format.text "(invalid MessageData.lazy, missing context)"))) →
      Lean.MessageData
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State : Type
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {i : ι}, (∀ (ω : Ω), ↑i ≤ τ ω) → ↑f i ≤ hτ.measurableSpace
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.le_refl : ∀ {α : Type u} (self : Std.Packages.PreorderOfLEArgs α),
  let this := self.le;
  ∀ (a : α), a ≤ a
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.map_obj_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (φ : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.FreeGroupoid.map φ).obj (CategoryTheory.FreeGroupoid.mk X) = CategoryTheory.FreeGroupoid.mk (φ.obj X)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.ringHom_ext_iff : ∀ {R : Type u_1} {T : Type u_3} [inst : CommRing R] [inst_1 : Semiring T] {p : Polynomial R} {f g : AdjoinRoot p →+* T},
  f = g ↔ f.comp (AdjoinRoot.of p) = g.comp (AdjoinRoot.of p) ∧ f (AdjoinRoot.root p) = g (AdjoinRoot.root p)
-- Mathlib.Topology.Compactness.Compact
/-- Cantor's intersection theorem for `sInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty.  -/
IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)} [hS : Nonempty ↑S],
  DirectedOn (fun x1 x2 => x1 ⊇ x2) S →
    (∀ U ∈ S, U.Nonempty) → (∀ U ∈ S, IsCompact U) → (∀ U ∈ S, IsClosed U) → (⋂₀ S).Nonempty
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.saveCases : Lean.Name → Lean.Meta.Grind.GrindM Unit
-- Aesop.Util.Basic
Aesop.SimpTheorems.containsDecl : Lean.Meta.SimpTheorems → Lean.Name → Bool
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.of_ae_eq : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α}
  {f g : α → γ}, AEMeasurable f μ → f =ᵐ[μ] g → ProbabilityTheory.IdentDistrib f g μ μ
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The discrete Grothendieck topology, in which every sieve is covering.

See https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies.
 -/
CategoryTheory.GrothendieckTopology.discrete : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.map_ι : ∀ {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] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteCoproducts F] (n : ℕ),
  (s.map F).ι n = F.map (s.ι n)
-- Init.Data.Rat.Lemmas
Rat.divInt_sub_divInt : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℤ},
  d₁ ≠ 0 → d₂ ≠ 0 → Rat.divInt n₁ d₁ - Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ - n₂ * d₁) (d₁ * d₂)
-- Mathlib.Data.Matrix.Basic
Matrix.scalar_inj : ∀ {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [Nonempty n]
  {r s : α}, (Matrix.scalar n) r = (Matrix.scalar n) s ↔ r = s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_3 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get! k' = cast ⋯ v
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The colimit cocone for the coproduct over an index type with exactly one term.  -/
CategoryTheory.Limits.colimitCoconeOfUnique : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [Unique β] → (f : β → C) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor f)
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges.congr_simp : ∀ {α : Type u_4} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] (s s_1 : Finset α),
      s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → G.interedges s t = G_1.interedges s_1 t_1
-- Mathlib.Topology.EMetricSpace.Defs
EDist.mk : {α : Type u_2} → (α → α → ENNReal) → EDist α
-- Mathlib.Order.Hom.Basic
OrderHom.comp_const : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (γ : Type u_6) [inst_2 : Preorder γ]
  (f : α →o β) (c : α), f.comp ((OrderHom.const γ) c) = (OrderHom.const γ) (f c)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ → s₃ ⊆ s₁ → ProbabilityTheory.Kernel.IndepSets s₃ s₂ κ μ
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.instIsCoatomic : ∀ {α : Type u} [inst : Semiring α], IsCoatomic (Ideal α)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.isSymm_toMatrix'_iff_isSymm : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {B : LinearMap.BilinForm R₁ (n → R₁)}, (LinearMap.BilinForm.toMatrix' B).IsSymm ↔ B.IsSymm
-- Init.Data.List.Pairwise
List.Pairwise.drop : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {i : ℕ}, List.Pairwise R l → List.Pairwise R (List.drop i l)
-- Mathlib.Order.SuccPred.Limit
WithBot.isPredPrelimit_bot : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α], Order.IsPredPrelimit ⊥
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_fn_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective DFunLike.coe
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i * g i < ∑ i ∈ s, f (σ i) * g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Basic theorem of the form
```
toInt a = a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')`
```
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.c? : Lean.Meta.Grind.Arith.Cutsat.ToIntThms → Option Lean.Expr
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplex_d_ofNat : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G) (n : ℕ),
  (tateComplex M).d (↑n) (↑n + 1) = (groupCohomology.inhomogeneousCochains M).d n (n + 1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.trivial_grp_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
      (CategoryTheory.Limits.pullback.snd i₁ i₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
-- Mathlib.Order.Monotone.Defs
monotone_iff_forall_lt : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f b
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace),
  X.toRingedSpace.basicOpen 0 = ⊥
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.hom T.hom) h)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_mulVec_eq_const : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v w : m → α),
  (Matrix.replicateRow ι v).mulVec w = Function.const ι (v ⬝ᵥ w)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_coe : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {F : Type u_1} [inst_5 : EquivLike F A₁ A₂]
  [inst_6 : AlgEquivClass F R A₁ A₂] (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteProducts F
-- Mathlib.GroupTheory.Nilpotent
/-- The ⊤-specialization of `lowerCentralSeries_pi_le`.  -/
Subgroup.top_lowerCentralSeries_pi_le : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] (n : ℕ),
  ⊤.lowerCentralSeries n ≤ Subgroup.pi Set.univ fun i => ⊤.lowerCentralSeries n
-- Mathlib.Data.ULift
PLift.down_bijective : ∀ {α : Sort u}, Function.Bijective PLift.down
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing.eq_def : ∀ (x : ONote),
  x.fastGrowing =
    let o := x;
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), h =>
      have this := ⋯;
      fun i => a.fastGrowing^[i] i
    | Sum.inr f, h => fun i =>
      have this := ⋯;
      (f i).fastGrowing i
-- Init.Data.Int.Order
Int.natAbs_mul : ∀ (a b : ℤ), (a * b).natAbs = a.natAbs * b.natAbs
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix_comp : ∀ {R : Type u_3} {N : Type u_5} {P : Type u_6} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommRing R] [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] (b : Module.Basis n R N)
  {m : Type w} [inst_6 : DecidableEq m] [inst_7 : Fintype m] [inst_8 : AddCommGroup P] [inst_9 : Module R P]
  (b' : Module.Basis m R P) (Q : QuadraticForm R P) (f : N →ₗ[R] P),
  QuadraticForm.toMatrix b (QuadraticMap.comp Q f) =
    ((LinearMap.toMatrix b b') f).transpose * QuadraticForm.toMatrix b' Q * (LinearMap.toMatrix b b') f
-- Mathlib.Data.W.Basic
_private.Mathlib.Data.W.Basic.0.WType.WType' : {α : Type u_3} → (β : α → Type u_4) → [(a : α) → Fintype (β a)] → ℕ → Type (max 0 u_3 u_4)
-- Lean.Language.Basic
Lean.Language.SyntaxGuarded.mk.injEq : ∀ {α : Type} (stx : Lean.Syntax) (val : α) (stx_1 : Lean.Syntax) (val_1 : α),
  ({ stx := stx, val := val } = { stx := stx_1, val := val_1 }) = (stx = stx_1 ∧ val = val_1)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_mul_conj : ∀ {d : ℤ} (n : ℤ√d), ↑n.norm = n * star n
-- Init.Data.String.Slice
String.Slice.instToString : ToString String.Slice
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.isTrivial : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Bool
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.le_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, ↑f x ≤ 1
-- Aesop.Index.RulePattern
/-- Insert an array of rule pattern substitutions into a rule pattern
substitution map.  -/
Aesop.RulePatternSubstMap.insertArray : Array (Aesop.RuleName × Aesop.Substitution) → Aesop.RulePatternSubstMap → Aesop.RulePatternSubstMap
-- Std.Sync.Broadcast
/-- Try to receive a value from the broadcast receiver, if a message is available right away
return `some value`, otherwise return `none` without blocking.
 -/
Std.Broadcast.Receiver.tryRecv : {α : Type} → Std.Broadcast.Receiver α → BaseIO (Option α)
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.toPointedCone_positive : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : PartialOrder E]
  [inst_7 : IsOrderedAddMonoid E] [inst_8 : PosSMulMono R E] [inst_9 : OrderClosedTopology E],
  ↑(ProperCone.positive R E) = PointedCone.positive R E
-- Mathlib.RingTheory.Bialgebra.Hom
/-- `BialgHomClass F R A B` asserts `F` is a type of bundled bialgebra homomorphisms
from `A` to `B`.  -/
BialgHomClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → [FunLike F A B] → Prop
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_veblen_of_lt : ∀ {o₁ o₂ : Ordinal.{u}}, o₁ < o₂ → ∀ (a : Ordinal.{u}), Ordinal.veblen o₁ (Ordinal.veblen o₂ a) = Ordinal.veblen o₂ a
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.natDegree_smul : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) {S : Type u_1} [inst_1 : Semiring S] [IsDomain S]
  [inst_3 : Module S R] [Module.IsTorsionFree S R] {a : S}, a ≠ 0 → (a • p).natDegree = p.natDegree