mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- An additive submonoid `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with
`n•g ∈ H` we have `n = 0` or `g ∈ H`. We use the name `NSMulSaturated` to distinguish from
`Submonoid.MulSaturated`.  -/
AddSubmonoid.NSMulSaturated : {G : Type u_1} → [inst : AddMonoid G] → AddSubmonoid G → Prop
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ConfirmRupHintFoldEntailsMotive.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (_idx : ℕ)
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool),
  f.ConfirmRupHintFoldEntailsMotive _idx acc =
    (acc.1.size = n ∧
      Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f acc.1 ∧
        (acc.2.2.1 = true →
          Std.Tactic.BVDecide.LRAT.Internal.Incompatible (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) acc.1 f))
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Ring α] [inst_2 : StarRing α] (d : ℤ),
  (↑d).conjTranspose = ↑d
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Binary coproducts are symmetric.  -/
CategoryTheory.Limits.BinaryCofan.isColimitFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryCofan X Y} →
        CategoryTheory.Limits.IsColimit c →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk c.inr c.inl)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.swap_mem_stabilizer : ∀ {α : Type u_2} [inst : DecidableEq α] {a b : α} {s : Set α},
  a ∈ s → b ∈ s → Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) s
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  {inst_1 : CategoryTheory.Category.{v', u'} J} {X : C}
  {toLimitPresentation : CategoryTheory.Limits.LimitPresentation J X}
  {prop_diag_obj : ∀ (j : J), P (toLimitPresentation.diag.obj j)}
  {toLimitPresentation_1 : CategoryTheory.Limits.LimitPresentation J X}
  {prop_diag_obj_1 : ∀ (j : J), P (toLimitPresentation_1.diag.obj j)},
  { toLimitPresentation := toLimitPresentation, prop_diag_obj := prop_diag_obj } =
      { toLimitPresentation := toLimitPresentation_1, prop_diag_obj := prop_diag_obj_1 } →
    toLimitPresentation = toLimitPresentation_1
-- Lean.Server.AsyncList
_private.Lean.Server.AsyncList.0.Lean.AsyncList.getFinishedPrefixWithTimeout.go : {ε α : Type} →
  List (Lean.Server.ServerTask Unit) →
    Lean.Server.ServerTask (Unit ⊕ Except ε (Lean.AsyncList ε α)) →
      Lean.AsyncList ε α → BaseIO (List α × Option ε × Bool)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.mk.inj : ∀ {σ : Type} {ref : Lean.Syntax} {var? : Option Lean.Elab.Term.Do.Var} {funName : Lean.Syntax}
  {pvars : Array Lean.Syntax} {rhs : σ} {ref_1 : Lean.Syntax} {var?_1 : Option Lean.Elab.Term.Do.Var}
  {funName_1 : Lean.Syntax} {pvars_1 : Array Lean.Syntax} {rhs_1 : σ},
  { ref := ref, var? := var?, funName := funName, pvars := pvars, rhs := rhs } =
      { ref := ref_1, var? := var?_1, funName := funName_1, pvars := pvars_1, rhs := rhs_1 } →
    ref = ref_1 ∧ var? = var?_1 ∧ funName = funName_1 ∧ pvars = pvars_1 ∧ rhs = rhs_1
-- Mathlib.Algebra.Order.Monovary
Monovary.sub_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Monovary f₁ g → Antivary f₂ g → Monovary (f₁ - f₂) g
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_eq_zero_iff : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [inst_5 : (i : ι) → DecidableEq (β i)]
  {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ}, f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.instIsMultiplicativeStrictMapPathsPathsPathComposition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  (W.paths.strictMap (CategoryTheory.pathComposition C)).IsMultiplicative
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.uniqueAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Subsingleton M],
  MonoidAlgebra.uniqueAlgEquiv R M =
    { toEquiv := (MonoidAlgebra.uniqueRingEquiv M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.zpow_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → ∀ (n : ℤ), UniformContinuous fun x => f x ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₃_desc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₃ (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₃
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.instIsSiftedOrEmptyProd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  [CategoryTheory.IsSiftedOrEmpty C] [CategoryTheory.IsSiftedOrEmpty D], CategoryTheory.IsSiftedOrEmpty (C × D)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_mul_ascFactorial : ∀ (n l k : ℕ), n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.range_pullbackFst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.Limits.pullback.fst g f) =
    ↑((TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f))
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.deriv_Gamma_add_one : ∀ (s : ℂ), s ≠ 0 → deriv Complex.Gamma (s + 1) = Complex.Gamma s + s * deriv Complex.Gamma s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      compare k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l →
              ∀
                {h' :
                  Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true},
                Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k' h' = v
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  MeasureTheory.addFundamentalInterior G s ∪ MeasureTheory.addFundamentalFrontier G s = s
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- For a set `W`, `T` is a neighborhood of `0` which is open, stable under negation and satisfies
`T + W ⊆ W`.  -/
IsTopologicalAddGroup.addNegClosureNhd : {G : Type u_1} → [TopologicalSpace G] → Set G → Set G → [AddGroup G] → Prop
-- Mathlib.Analysis.Convex.Function
/-- If `f` is concave on `s`, so is `(g ∘ f)` on `g ⁻¹' s` for a linear `g`.  -/
ConcaveOn.comp_linearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] [inst_8 : SMul 𝕜 β] {f : F → β} {s : Set F},
  ConcaveOn 𝕜 s f → ∀ (g : E →ₗ[𝕜] F), ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
-- Mathlib.Analysis.LocallyConvex.Separation
geometric_hahn_banach_point_open : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {t : Set E} {x : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ t → IsOpen t → x ∉ t → ∃ f, ∀ b ∈ t, f x < f b
-- Mathlib.Algebra.CharP.Basic
instExpCharProd : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (S : Type u_2) [inst_1 : Semiring S] (p : ℕ) [ExpChar R p] [ExpChar S p],
  ExpChar (R × S) p
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the uniform structures of uniform convergence and pointwise
convergence induce the same uniform structure on `ι`.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.

Consider using `Equicontinuous.isUniformInducing_uniformFun_iff_pi` and
`Equicontinuous.inducing_uniformFun_iff_pi` instead, to avoid rewriting instances.  -/
Equicontinuous.comap_uniformFun_eq : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [CompactSpace X],
  Equicontinuous F →
    UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i => α)
-- Mathlib.MeasureTheory.Measure.Hausdorff
AntilipschitzWith.hausdorffMeasure_preimage_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {K : NNReal} {d : ℝ},
  AntilipschitzWith K f →
    0 ≤ d →
      ∀ (s : Set Y),
        (MeasureTheory.Measure.hausdorffMeasure d) (f ⁻¹' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₃_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₃.Exact
-- Mathlib.Data.Set.Insert
Set.ne_insert_of_notMem : ∀ {α : Type u_1} {s : Set α} (t : Set α) {a : α}, a ∉ s → s ≠ insert a t
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_mod : ∀ (m n : ℕ), ↑(m % n) = ↑m % ↑n
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.all.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) (p : (a : α) → β a → Bool),
  m.all p =
    (do
        let __s ←
          forIn m (none, ()) fun a __s =>
              if ¬p a.fst a.snd = true then pure (ForInStep.done (some false, ()))
              else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure true).run
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.map_le_iff_le_comap : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] {f : L →ₐ[K] L'} {s : IntermediateField K L}
  {t : IntermediateField K L'}, IntermediateField.map f s ≤ t ↔ s ≤ IntermediateField.comap f t
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabDIte : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.prod_swap : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β), (μ.prod ν).map ⋯ = ν.prod μ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorZipperIdSigma.eq_1 : ∀ {α : Type u} {β : α → Type v},
  Std.DTreeMap.Internal.instIteratorZipperIdSigma =
    { IsPlausibleStep := fun it step => it.internalState.step = step,
      step := fun it => pure (Std.Shrink.deflate ⟨it.internalState.step, ⋯⟩) }
-- Mathlib.ModelTheory.LanguageMap
/-- The identity equivalence from a first-order language to itself.  -/
FirstOrder.Language.LEquiv.refl : (L : FirstOrder.Language) → L ≃ᴸ L
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.Normal.mem_comm : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → ∀ {a b : G}, a + b ∈ H → b + a ∈ H
-- Lean.Meta.DiscrTree.Util
/-- The number of values stored in a `Trie`.
 -/
Lean.Meta.DiscrTree.Trie.size : {α : Type} → Lean.Meta.DiscrTree.Trie α → ℕ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- An exact formula for integration with a single trapezoid (the "midpoint rule").  -/
trapezoidal_integral_one : ∀ (f : ℝ → ℝ) (a b : ℝ), trapezoidal_integral f 1 a b = (b - a) / 2 * (f a + f b)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The operator norm of the orthogonal projection onto a nontrivial subspace is `1`.  -/
Submodule.norm_orthogonalProjectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K ≠ ⊥ → ‖K.orthogonalProjectionOnto‖ = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.distinct_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.Pairwise (fun a b => (a == b) = false) m.keys
-- Mathlib.Topology.Algebra.ProperAction.Basic
QuotientGroup.instT2Space : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} [IsClosed ↑H],
  T2Space (G ⧸ H)
-- Lean.Server.InfoUtils
/-- Fold an info tree as follows, while ensuring that the correct `ContextInfo` is supplied at each stage:

* Nodes are combined with the initial value `init` using `f`, and the result is then combined with the children using a left fold
* On InfoTree holes, we just return the initial value.

This is like `InfoTree.foldInfo`, but it also passes the whole node to `f` instead of just the head.
 -/
Lean.Elab.InfoTree.foldInfoTree : {α : Type u_1} → α → (Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) → Lean.Elab.InfoTree → α
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_insertRup : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
      (f.insertRupUnits c.negate).2 = true →
        Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H}
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (c : CategoryTheory.Limits.Cocone G) (X : C),
  (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c).ι.app X =
    CategoryTheory.Limits.colimit.desc ((CategoryTheory.Grothendieck.ι F X).comp G)
      (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Grothendieck.ι F X) c)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector from a vertex to its `faceOppositeCentroid` is `(n+1)` times the vector from the
`centroid` to that `faceOppositeCentroid`.  -/
Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i -ᵥ s.points i = (↑n + 1) • (s.faceOppositeCentroid i -ᵥ s.centroid)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoCofanPt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt 𝒜 f).hom h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i) h
-- Lean.Parser.Syntax
/-- `infixr:prec "op" => f` is equivalent to `notation:prec x:prec1 "op" y:prec => f x y`, where `prec1 := prec + 1`.
 -/
Lean.Parser.Command.infixr : Lean.Parser.Parser
-- Init.Omega.Constraint
Lean.Omega.Constraint.addEquality_sat : ∀ {c : ℤ} {x y : Lean.Omega.Coeffs},
  c + x.dot y = 0 → { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.mk.sizeOf_spec : ∀ (html : ProofWidgets.Html) (idx : ℕ), sizeOf { html := html, idx := idx } = 1 + sizeOf html + sizeOf idx
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- There are `t` vertices in each part.  -/
SimpleGraph.CompleteEquipartiteSubgraph.card_mem_parts : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (self : G.CompleteEquipartiteSubgraph r t) {p : Finset V},
  p ∈ self.parts → p.card = t
-- Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
CategoryTheory.SimplicialObject.instSimplicialCategory : {D : Type u} →
  [inst : CategoryTheory.Category.{v, u} D] → CategoryTheory.SimplicialCategory (CategoryTheory.SimplicialObject D)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.eq : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁},
  Path.Homotopic.Quotient.mk p = Path.Homotopic.Quotient.mk q ↔ p.Homotopic q
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.neg_smul_neg : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)), -f • -g = f • g
-- Mathlib.Data.Int.Cast.Basic
Nat.cast_pred : ∀ {R : Type u} [inst : AddGroupWithOne R] {n : ℕ}, 0 < n → ↑(n - 1) = ↑n - 1
-- Init.Data.SInt.Basic
/-- Adds two 64-bit signed integers, wrapping around on over- or underflow.  Usually accessed via the
`+` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.add : Int64 → Int64 → Int64
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic.0.tacticC_simp : Lean.ParserDescr
-- Mathlib.Algebra.Group.Basic
mul_left_surjective : ∀ {G : Type u_3} [inst : Group G] (a : G), Function.Surjective fun x => a * x
-- Mathlib.Data.Fintype.Perm
/-- Given a list, produce a list of all permutations of its elements.  -/
permsOfList : {α : Type u_1} → [DecidableEq α] → List α → List (Equiv.Perm α)
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R),
  CategoryTheory.injectiveDimension M = ⨆ p, CategoryTheory.injectiveDimension (M.localizedModule p.asIdeal.primeCompl)
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right_dvd_mul_lcm : ∀ (k m n : ℕ), k.lcm (m * n) ∣ k.lcm m * k.lcm n
-- Mathlib.RingTheory.Valuation.Integers
/-- **Alias** of `Valuation.Integers.coe_span_singleton_eq_setOfPred_le_v_algebraMap`. -/
Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ (x : O), ↑(Ideal.span {x}) = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.symm₂_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (F : p.Homotopy q)
  (x : ↑unitInterval × ↑unitInterval), F.symm₂ x = F (x.1, unitInterval.symm x.2)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Mapping an orthonormal basis along a `LinearIsometryEquiv`.  -/
OrthonormalBasis.map : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {G : Type u_7} →
                [inst_4 : NormedAddCommGroup G] →
                  [inst_5 : InnerProductSpace 𝕜 G] → OrthonormalBasis ι 𝕜 E → (E ≃ₗᵢ[𝕜] G) → OrthonormalBasis ι 𝕜 G
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instIdempotentOpHAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The second projection of `prod F G`, onto `G`.  -/
CategoryTheory.FunctorToTypes.prod.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → CategoryTheory.FunctorToTypes.prod F G ⟶ G
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- If `R ⋙ U` has a left adjoint, the domain of `R` has reflexive coequalizers and `U` is a monadic
functor, then `R` has a left adjoint.
This is a special case of `isRightAdjoint_triangle_lift` which is often more useful in practice.
 -/
CategoryTheory.isRightAdjoint_triangle_lift_monadic : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (U : CategoryTheory.Functor B C) [CategoryTheory.MonadicRightAdjoint U] {R : CategoryTheory.Functor A B}
  [CategoryTheory.Limits.HasReflexiveCoequalizers A] [(R.comp U).IsRightAdjoint], R.IsRightAdjoint
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.η_app_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η F).app ((F.obj n).obj X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F n (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app X)
      ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor n).hom).app X)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.EssentiallySmall.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∃ S x, Nonempty (C ≌ S)) → CategoryTheory.EssentiallySmall.{w, v, u} C
-- Init.Data.SInt.Bitwise
Int8.not_neg_one : ~~~(-1) = 0
-- Mathlib.Topology.Order.Basic
tendstoIcoClassNhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α),
  Filter.TendstoIxxClass Set.Ico (nhds a) (nhds a)
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_apply_of_notMem_of_mem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s →
    x ∉ s → y ∈ s → (ProbabilityTheory.bernoulliMeasure x y p) s = ↑(unitInterval.toNNReal (unitInterval.symm p))
-- Mathlib.Data.Ordmap.Invariants
/-- A left balance operation. This will rebalance a concatenation, assuming the original nodes are
not too far from balanced.  -/
Ordnode.balanceL' : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α