mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.convex_sdiff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {A B : Set E} [IsOrderedRing 𝕜], Convex 𝕜 A → IsExtreme 𝕜 A B → Convex 𝕜 (A \ B)
-- Mathlib.RingTheory.Smooth.Basic
LinearMap.extendScalarsOfSurjectiveEquiv.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  {N : Type u_4} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : IsScalarTower R S M] [inst_8 : Module R N] [inst_9 : Module S N] [inst_10 : IsScalarTower R S N]
  (h : Function.Surjective ⇑(algebraMap R S)),
  LinearMap.extendScalarsOfSurjectiveEquiv h = LinearMap.extendScalarsOfSurjectiveEquiv h
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_monomial : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (s : σ →₀ ℕ) (a : R), (MvPolynomial.map f) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial s) (f a)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressOptions.mk.inj : ∀ {workDoneProgress workDoneProgress_1 : Bool},
  { workDoneProgress := workDoneProgress } = { workDoneProgress := workDoneProgress_1 } →
    workDoneProgress = workDoneProgress_1