mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C`,
if `(F₁' F₂' : D ⥤ E)` are functors which lift functors `(F₁ F₂ : C ⥤ E)`,
a natural transformation `τ : F₁ ⟶ F₂` uniquely lifts to a natural transformation `F₁' ⟶ F₂'`.  -/
CategoryTheory.Localization.liftNatTrans : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                [L.IsLocalization W] →
                  (F₁ F₂ : CategoryTheory.Functor C E) →
                    (F₁' F₂' : CategoryTheory.Functor D E) →
                      [CategoryTheory.Localization.Lifting L W F₁ F₁'] →
                        [CategoryTheory.Localization.Lifting L W F₂ F₂'] → (F₁ ⟶ F₂) → (F₁' ⟶ F₂')
-- Lean.Parser.Basic
/-- If the leading token is an identifier `<foo>`, and there are parsers `P` associated with the token
`<foo>`, then the parser executes `P`. Otherwise, it executes only the parsers associated with the
auxiliary token “ident”, which parses identifiers.
 -/
Lean.Parser.LeadingIdentBehavior.symbol : Lean.Parser.LeadingIdentBehavior
-- Mathlib.Algebra.Order.Hom.Basic
/-- the image of a sum is less or equal than the sum of the images.  -/
SubadditiveHomClass.map_add_le_add : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Add α} {inst_1 : Add β} {inst_2 : LE β}
  {inst_3 : FunLike F α β} [self : SubadditiveHomClass F α β] (f : F) (a b : α), f (a + b) ≤ f a + f b
-- Mathlib.GroupTheory.OrderOfElement
mod_card_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] (a : G) (n : ℤ), (n % ↑(Fintype.card G)) • a = n • a
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.quotPrecheck : Lean.Option Bool
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.val_unitsLift_symm_apply_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousMul M] (f : C(X, M)ˣ) (x : X), ↑((ContinuousMap.unitsLift.symm f) x) = ↑f x
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_self : ∀ (n : ℕ), (Polynomial.hermite n).coeff n = 1
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_int_mod : ∀ (l : List ℤ) (n : ℤ), l.prod % n = (List.map (fun x => x % n) l).prod % n
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousOn.fun_const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {s : Set β},
  ContinuousOn g s → ∀ (c : M), ContinuousOn (fun i => c +ᵥ g i) s
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupSeminormClass.toNonnegHomClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [AddGroupSeminormClass F α β], NonnegHomClass F α β
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.isPreprimitive_ofFixingAddSubgroup_addConj_iff : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {s : Set α} {g : G},
  AddAction.IsPreprimitive ↥(fixingAddSubgroup G s) ↥(SubAddAction.ofFixingAddSubgroup G s) ↔
    AddAction.IsPreprimitive ↥(fixingAddSubgroup G (g +ᵥ s)) ↥(SubAddAction.ofFixingAddSubgroup G (g +ᵥ s))
-- Mathlib.Topology.Compactness.Lindelof
Tendsto.isLindelof_insert_range_of_coLindelof : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {y : Y},
  Filter.Tendsto f (Filter.coLindelof X) (nhds y) → Continuous f → IsLindelof (insert y (Set.range f))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toCat_obj : ∀ (X : SimplexCategory),
  SimplexCategory.toCat.obj X =
    CategoryTheory.Cat.of
      ↑((CategoryTheory.forget₂ PartOrd Preord).obj
          ((CategoryTheory.forget₂ Lat PartOrd).obj
            ((CategoryTheory.forget₂ LinOrd Lat).obj
              ((CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).obj (NonemptyFinLinOrd.of (Fin (X.len + 1)))))))
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_mul_aleph0 : Cardinal.aleph0 * Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.toDual_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → α),
  OrderDual.toDual (s.sup f) = s.inf (⇑OrderDual.toDual ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelZeroIsoSource_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.kernelZeroIsoSource.hom = CategoryTheory.Limits.kernel.ι 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).size =
    if k ∈ t ∧ (f (Std.ExtDTreeMap.Const.get? t k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then t.size + 1 else t.size
-- Aesop.Tree.State
_private.Aesop.Tree.State.0.Aesop.markProvenCore : Aesop.TreeRef → BaseIO Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {a : α} {fallback : β},
      m.contains a = true → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.getD m a fallback)
-- Mathlib.Order.Lex
/-- `ofColex` is the identity function from the `Colex` of a type.  -/
ofColex : {α : Type u_1} → Colex α ≃ α
-- Mathlib.CategoryTheory.Equivalence
/-- The composition `functor ⋙ inverse` is isomorphic to the identity.  -/
CategoryTheory.Equivalence.unitIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (self : C ≌ D) → CategoryTheory.Functor.id C ≅ self.functor.comp self.inverse
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.sup : ∀ {G : Type u_3} [inst : AddGroup G] {P Q : AddSubgroup G}, P.FG → Q.FG → (P ⊔ Q).FG
-- Lean.ToExpr
_private.Lean.ToExpr.0.Lean.Name.toExprAux.go : Lean.Name → Lean.Expr
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_zero`. -/
ProbabilityTheory.Kernel.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.galActionAux : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → MulAction p.Gal ↑(p.rootSet p.SplittingField)
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Lints against overlaps between instances in the local contexts of declarations.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.linter.overlappingInstances : Lean.Option Bool
-- Mathlib.Order.RelSeries
SetRel.InfiniteDimensional.mk : ∀ {α : Type u_1} {r : SetRel α α}, (∀ (n : ℕ), ∃ x, x.length = n) → r.InfiniteDimensional
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.instDecidableEqLiteral.decEq : (x x_1 : BitVec.Literal✝) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : X ⟶ Y) (hf : W f),
  CategoryTheory.Localization.Construction.wInv f hf = (CategoryTheory.Localization.isoOfHom W.Q W f hf).inv
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.algebraMap₀.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorPower.algebraMap₀ = (PiTensorProduct.isEmptyEquiv (Fin 0)).symm
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N),
  Submonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Tactic.ExtractGoal
/-- `extract_goal` formats the current goal as a stand-alone theorem or definition after
cleaning up the local context of irrelevant variables.

A variable is *relevant* if (1) it occurs in the target type, (2) there is a relevant variable
that depends on it, or (3) the type of the variable is a proposition that depends on a
relevant variable.
If the target is `False`, then for convenience `extract_goal` includes all variables.

The tactic tries to produce an output that can be copy-pasted and just work,
but its success depends on whether the expressions are amenable
to being unambiguously pretty printed.
The tactic responds to pretty printing options.
For example, `set_option pp.all true in extract_goal` gives the `pp.all` form.

* `extract_goal *` formats the current goal without cleaning up the local context.
* `extract_goal a b c ...` formats the current goal after removing everything that the given
  variables `a`, `b`, `c`, ... do not depend on.
* `extract_goal ... using name` uses the name `name` for the theorem or definition rather than
  the autogenerated name.
 -/
Mathlib.Tactic.ExtractGoal.extractGoal : Lean.ParserDescr
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.toStringWithToken.maybePseudoSyntax : Lean.Name → Bool
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.smul_left` -/
Function.HasFiniteSupport.fun_smul_left : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : Zero R] [inst_2 : SMulWithZero R M]
  {f : α → R}, Function.HasFiniteSupport f → ∀ (g : α → M), Function.HasFiniteSupport fun i => f i • g i
-- Lean.Elab.Do.Legacy
/-- Create a new join point that takes `rs` and `val` as arguments. `val` must be syntax representing a pure value.
The body of the join point is created using `mkJPBody yFresh`, where `yFresh`
is a fresh variable created by this method.  -/
Lean.Elab.Term.Do.mkJmp : Lean.Syntax →
  Lean.Elab.Term.Do.VarSet →
    Lean.Syntax →
      (Lean.Syntax → Lean.MacroM Lean.Elab.Term.Do.Code) →
        StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.emultiplicity_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a : α},
  FiniteMultiplicity a a → emultiplicity a a = 1
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
coeff_addMonoidAlgebraAddEquivDirectSum_symm_apply_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : DirectSum ι fun x => M), (addMonoidAlgebraAddEquivDirectSum.symm f).coeff.support = DFinsupp.support f
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, s /ₛ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.mk.injEq : ∀ (kinds : Array Lean.Json.CompressWorkItemKind✝) (values : Array Lean.Json) (objectFieldKeys : Array String)
  (kinds_1 : Array Lean.Json.CompressWorkItemKind✝) (values_1 : Array Lean.Json) (objectFieldKeys_1 : Array String),
  ({ kinds := kinds, values := values, objectFieldKeys := objectFieldKeys } =
      { kinds := kinds_1, values := values_1, objectFieldKeys := objectFieldKeys_1 }) =
    (kinds = kinds_1 ∧ values = values_1 ∧ objectFieldKeys = objectFieldKeys_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.mk.sizeOf_spec : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  [inst_4 : SizeOf G] [inst_5 : SizeOf H] (toMulEquiv : G ≃* H)
  (continuous_toFun : autoParam (Continuous toMulEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toMulEquiv.invFun) Homeomorph.continuous_invFun._autoParam),
  sizeOf { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toMulEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Std.Data.TreeMap.Iterator
Std.TreeMap.keysIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeMap α β cmp), m.keysIter.toList = m.keys
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.createsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {R : CategoryTheory.Sheaf J RingCat} →
            (F : CategoryTheory.Functor D (SheafOfModules R)) →
              [∀ (X : Cᵒᵖ),
                    Small.{v, max u₂ v}
                      ↑((F.comp (SheafOfModules.evaluation R X)).comp
                            (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections] →
                [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] →
                  CategoryTheory.CreatesLimit F (SheafOfModules.forget R)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.lift_ord : ∀ (c : Cardinal.{v}), Ordinal.lift.{u, v} c.ord = (Cardinal.lift.{u, v} c).ord
-- Mathlib.LinearAlgebra.Matrix.CharP
Matrix.charP : ∀ {n : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : DecidableEq n] [Nonempty n] (p : ℕ) [CharP R p],
  CharP (Matrix n n R) p
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Let `p : Y ⟶ X` be an effective epimorphism, `p₁ : Z ⟶ Y` and `p₂ : Z ⟶ Y` two
morphisms which make `Z` the pullback of two copies of `Y` over `X`.
Then, `Y ⟶ X` is the coequalizer of `p₁` and `p₂`.  -/
CategoryTheory.EffectiveEpiStruct.isColimitCoforkOfIsPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {p : Y ⟶ X} →
        CategoryTheory.EffectiveEpiStruct p →
          {p₁ p₂ : Z ⟶ Y} →
            (sq : CategoryTheory.IsPullback p₁ p₂ p p) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ p ⋯)
-- Init.Data.SInt.Bitwise
Int64.toInt16_or : ∀ (a b : Int64), (a ||| b).toInt16 = a.toInt16 ||| b.toInt16
-- Init.Control.MonadAttach
/-- For every `x : m α`, this type class provides a predicate `MonadAttach.CanReturn x`
and a way to attach a proof of this predicate to the return values of `x` by providing
an element `MonadAttach.attach x` of `m { a : α // MonadAttach.CanReturn x a }`.

Instances should abide the law `Subtype.val <$> MonadAttach.attach x = x`, which is encoded by
the `WeaklyLawfulMonadAttach` type class. The stronger type class `LawfulMonadAttach`
ensures that `MonadAttach.CanReturn x` is the *unique* strongest possible predicate.

Similarly to `List.attach`, the purpose of
`MonadAttach` is to attach proof terms necessary for well-founded termination proofs.
The iterator library relies on `MonadAttach` for combinators such as
`Std.Iter.filterM` in order to automatically attach
information about the monadic predicate's behavior that could be relevant for the termination
behavior of the iterator.

**Limitations**:

For many monads, there is a strongly lawful `MonadAttach` instance, but there are exceptions.
For example, there is no way to provide a computable `MonadAttach` instance for the CPS monad
transformers
`StateCpsT` and
`ExceptCpsT` with a predicate that is not always
`True`. Therefore, such CPS monads only provide the trivial `MonadAttach` instance
`MonadAttach.trivial` together with `WeaklyLawfulMonadAttach`, but without
`LawfulMonadAttach`.

For most monads with side effects, `MonadAttach` is too weak to fully capture the behavior of
computations because the postcondition represented by `MonadAttach.CanReturn` neither depends
on the prior internal state of the monad, nor does it contain information about how the state of the
monad changes with the computation.
 -/
MonadAttach : (Type u → Type v) → Type (max (u + 1) v)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint8 : UInt8 → Lean.Compiler.LCNF.LitValue
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindRing.toIsIntegralClosure : ∀ {A : Type u_2} {inst : CommRing A} [self : IsDedekindRing A], IsIntegralClosure A A (FractionRing A)
-- Mathlib.Algebra.Lie.TraceForm
/-- The trace form of a Lie module is compatible with the action of the Lie algebra.

See also `LieModule.traceForm_apply_lie_apply'`.  -/
LieModule.traceForm_apply_lie_apply : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y z : L),
  ((LieModule.traceForm R L M) ⁅x, y⁆) z = ((LieModule.traceForm R L M) x) ⁅y, z⁆
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.reachable_iff_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.IsBridge s(u, v) → (G.Reachable u v ↔ G.Adj u v)
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.hasDerivAt_neg_exp_mul_exp : ∀ {r x : ℝ}, HasDerivAt (fun a => -Real.exp (-(r * a))) (r * Real.exp (-(r * x))) x
-- Lean.Parser.Syntax
Lean.Parser.Syntax.binary.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Lemmas
List.head?_replace : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a b : α},
  (l.replace a b).head? =
    match l.head? with
    | none => none
    | some x => some (if (a == x) = true then b else x)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The multilinear version of `LinearMap.subtype_comp_codRestrict`  -/
LinearMap.subtype_compMultilinearMap_codRestrict : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p),
  p.subtype.compMultilinearMap (f.codRestrict p h) = f
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limit_pre_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [inst_4 : CategoryTheory.Limits.HasLimit G],
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.pre G F)
-- Init.Data.Vector.Basic
Vector.replace : {α : Type u_1} → {n : ℕ} → [BEq α] → Vector α n → α → α → Vector α n
-- Lean.Util.Trace
Lean.TraceState.mk.sizeOf_spec : ∀ (tid : UInt64) (traces : Lean.PersistentArray Lean.TraceElem),
  sizeOf { tid := tid, traces := traces } = 1 + sizeOf tid + sizeOf traces
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X},
  x ∈ I.supportSet ↔ ∀ (U : ↑X.affineOpens), x ∈ X.zeroLocus ↑(I.ideal U)
-- Mathlib.Data.List.Nodup
List.not_nodup_cons_of_mem : ∀ {α : Type u} {l : List α} {a : α}, a ∈ l → ¬(a :: l).Nodup
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The morphism `R ⟶ S` in `𝒮` obtained by projecting a morphism
`φ : (ι R).obj a ⟶ (ι S).obj b`.  -/
HasFibers.projMap : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            {R S : 𝒮} →
              {a : HasFibers.Fib p R} →
                {b : HasFibers.Fib p S} → ((HasFibers.ι R).obj a ⟶ (HasFibers.ι S).obj b) → (R ⟶ S)
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.mk : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Bool → Bool → ℕ → Lean.Elab.GoalsAtResult
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.lintegral_lintegral_mul_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
  (f : G → G → ENNReal),
  AEMeasurable (Function.uncurry f) (μ.prod ν) →
    ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
-- Init.Data.Option.Lemmas
Option.or_eq_none_iff : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = none ↔ o = none ∧ o' = none
-- Init.Data.ByteArray.Basic
ByteArray.append_eq : ∀ {a b : ByteArray}, a.append b = a ++ b
-- Mathlib.RingTheory.PolynomialAlgebra
/-- (Implementation detail).
The function underlying `A ⊗[R] R[X] →ₐ[R] A[X]`,
as a bilinear function of two arguments.
 -/
PolyEquivTensor.toFunBilinear : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₗ[A] Polynomial R →ₗ[R] Polynomial A
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.coeff_expand_smul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) (m : σ →₀ ℕ),
  (MvPowerSeries.coeff (p • m)) ((MvPowerSeries.expand p hp) φ) = (MvPowerSeries.coeff m) φ
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toNormedAlgebra : {A : Type u_1} → [self : CStarAlgebra A] → NormedAlgebra ℂ A
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_cons : ∀ {α : Type u_1} (a : α) (m : Multiset α), (a ::ₘ m).sym2 = Multiset.map (fun b => s(a, b)) (a ::ₘ m) + m.sym2
-- Init.Data.Vector.Lemmas
Vector.not_mem_empty : ∀ {α : Type u_1} (a : α), a ∉ #v[]
-- Mathlib.Analysis.SumIntegralComparisons
MonotoneOn.sum_le_integral : ∀ {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ},
  MonotoneOn f (Set.Icc x₀ (x₀ + ↑a)) → ∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x