mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.differentiableWithinAt_iff_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {x : E} {s : Set E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → x ∈ s → (DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G j)
      (CategoryTheory.CategoryStruct.comp (w.inv.app j) h)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_carrier : ∀ (R : CommRingCat), ↥(AlgebraicGeometry.Spec R) = PrimeSpectrum ↑R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertMany_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {l : List (α × β)} {k : α} {v : β},
  t.insertMany ((k, v) :: l) = (t.insert k v).insertMany l
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModule : Lean.FromJson Lean.Lsp.LeanModule
-- Lean.MetavarContext
Lean.MetavarDecl.mk.inj : ∀ {userName : Lean.Name} {lctx : Lean.LocalContext} {type : Lean.Expr} {depth : ℕ}
  {localInstances : Lean.LocalInstances} {kind : Lean.MetavarKind} {numScopeArgs index : ℕ} {userName_1 : Lean.Name}
  {lctx_1 : Lean.LocalContext} {type_1 : Lean.Expr} {depth_1 : ℕ} {localInstances_1 : Lean.LocalInstances}
  {kind_1 : Lean.MetavarKind} {numScopeArgs_1 index_1 : ℕ},
  { userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind,
        numScopeArgs := numScopeArgs, index := index } =
      { userName := userName_1, lctx := lctx_1, type := type_1, depth := depth_1, localInstances := localInstances_1,
        kind := kind_1, numScopeArgs := numScopeArgs_1, index := index_1 } →
    userName = userName_1 ∧
      lctx = lctx_1 ∧
        type = type_1 ∧
          depth = depth_1 ∧
            localInstances = localInstances_1 ∧ kind = kind_1 ∧ numScopeArgs = numScopeArgs_1 ∧ index = index_1
-- Mathlib.Analysis.Normed.Module.Ball.Action
ne_neg_of_mem_unit_sphere : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CharZero 𝕜] (x : ↑(Metric.sphere 0 1)), x ≠ -x
-- Lean.Exception
/-- Throw an unknown constant error message.
The end position of the range of the current reference should point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
 -/
Lean.throwUnknownConstant : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m α
-- Init.Data.SInt.Lemmas
Int8.sub_self : ∀ (a : Int8), a - a = 0
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A more general version of `ZLattice.volume_image_eq_volume_div_covolume`;
see the `Naming conventions` section in the introduction.  -/
ZLattice.volume_image_eq_volume_div_covolume' : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L]
  [inst_6 : IsZLattice ℝ L] {ι : Type u_3} [inst_7 : Fintype ι] (b : Module.Basis ι ℤ ↥L) {s : Set E},
  MeasureTheory.NullMeasurableSet s MeasureTheory.volume →
    MeasureTheory.volume (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
      MeasureTheory.volume s / ENNReal.ofReal (ZLattice.covolume L MeasureTheory.volume)
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAt_sub_const_iff`. -/
HasDerivAt.sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt f f' x → HasDerivAt (fun x => f x - c) f' x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {l : List ι} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ l, DifferentiableWithinAt 𝕜 (fun x => f i x) s x) →
      fderivWithin 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) s x =
        ∑ i,
          (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
            MulOpposite.op (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod •
              fderivWithin 𝕜 (fun x => f l[i] x) s x
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_sum_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R),
  MvPolynomial.degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => MvPolynomial.degreeOf i (f j)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.closure_range_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  closure (Set.range (PrimeSpectrum.comap f)) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.LawfulMapOperator.chainable : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α}
  {f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  {inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f} [self : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (aig : Std.Sat.AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size ≤ (f aig input1).aig.decls.size)
  (assign : α → Bool), ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.unshift : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → E →L[𝕜] F}
  {pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {s : Set E} {x : E} {r : ENNReal} {z : F},
  HasFPowerSeriesWithinOnBall f pf s x r → HasFPowerSeriesWithinOnBall (fun y => z + (f y) (y - x)) (pf.unshift z) s x r
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  H.mapCocone c = (CategoryTheory.Limits.Cocone.functoriality F H).obj c
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.go.eq_def : ∀ (n a x x_1 : ℕ),
  Nat.nthRoot.go n a x x_1 =
    match x, x_1 with
    | 0, guess => guess
    | fuel.succ, guess =>
      have next := (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2);
      if next < guess then Nat.nthRoot.go n a fuel next else guess
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instFullDecomposedDecomposedTo : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], (CategoryTheory.decomposedTo J).Full
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.instToJsonMethod.toJson : Aesop.ScriptGenerated.Method → Lean.Json
-- Mathlib.Data.Complex.Basic
Complex.ratCast_im : ∀ (q : ℚ), (↑q).im = 0
-- Mathlib.Analysis.Calculus.TangentCone.Prod
/-- The product of two sets of unique differentiability is a set of unique differentiability.  -/
UniqueDiffOn.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {s : Set E}
  {t : Set F}, UniqueDiffOn 𝕜 s → UniqueDiffOn 𝕜 t → UniqueDiffOn 𝕜 (s ×ˢ t)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Topology.IsEmbedding.isSimplyConnected_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → ∀ {s : Set X}, IsSimplyConnected (f '' s) ↔ IsSimplyConnected s
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Int.instMeasurableSingletonClass : MeasurableSingletonClass ℤ
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_le_toColex_iff_max'_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α},
  toColex s ≤ toColex t ↔ ∀ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t
-- Mathlib.Order.Lattice
Pi.instMaxForall_mathlib.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Max (α' i)],
  Pi.instMaxForall_mathlib = { max := fun f g i => f i ⊔ g i }
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_div_lt_mk_right_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk (a / b) < MulArchimedeanClass.mk b ↔ MulArchimedeanClass.mk a < MulArchimedeanClass.mk b
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableLocallyUniformly_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], (∀ (x : β), ∃ t ∈ nhds x, MultipliableUniformlyOn f t) → MultipliableLocallyUniformly f
-- Mathlib.Algebra.Module.Presentation.Tensor
_private.Mathlib.Algebra.Module.Presentation.Tensor.0.Module.Relations.tensor.match_1.splitter : {A : Type u_5} →
  [inst : CommRing A] →
    (relations₁ : Module.Relations A) →
      (relations₂ : Module.Relations A) →
        (motive : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R → Sort u_6) →
          (x : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R) →
            ((r₁ : relations₁.R) → (g₂ : relations₂.G) → motive (Sum.inl (r₁, g₂))) →
              ((g₁ : relations₁.G) → (r₂ : relations₂.R) → motive (Sum.inr (g₁, r₂))) → motive x
-- Aesop.Percent
Aesop.Percent.instBEq : BEq Aesop.Percent
-- Mathlib.RingTheory.Lasker
Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {t : Finset (Ideal R)},
  Submodule.IsMinimalPrimaryDecomposition I t → I.minimalPrimes ⊆ Ideal.radical '' ↑t
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizer_mul_eq_left : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Group α] [IsScalarTower G α α]
  (a b : α), MulAction.stabilizer G (a * b) = MulAction.stabilizer G a
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The product of topological modules is associative up to continuous linear isomorphism.
This is `LinearEquiv.prodAssoc` prodAssoc as a continuous linear equivalence.  -/
ContinuousLinearEquiv.prodAssoc : (R : Type u_8) →
  (M₁ : Type u_9) →
    (M₂ : Type u_10) →
      (M₃ : Type u_11) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M₃] →
                      [inst_7 : TopologicalSpace M₁] →
                        [inst_8 : TopologicalSpace M₂] →
                          [inst_9 : TopologicalSpace M₃] → ((M₁ × M₂) × M₃) ≃L[R] M₁ × M₂ × M₃
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instIsUniformAddGroup : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F], IsUniformAddGroup (E [⋀^ι]→L[𝕜] F)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.iUnion_of_monotone : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_5} [inst_1 : Preorder ι] [IsDirectedOrder ι]
  [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  Monotone s → (∀ (i : ι), MeasurableSet (s i)) → MeasurableSet (⋃ i, s i)
-- ImportGraph.Imports.ImportGraph
/-- Construct the import graph of the current file.
 -/
Lean.Environment.importGraph : Lean.Environment → Lean.NameMap (Array Lean.Name)
-- Batteries.Data.AssocList
Batteries.AssocList.length_cons : ∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β} {t : Batteries.AssocList α β},
  (Batteries.AssocList.cons a b t).length = t.length + 1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s : NonUnitalSubalgebra R A),
  NonUnitalAlgebra.adjoin R ↑s = s
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.Subgroup.exists_neg_generator : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G)
  [Nontrivial ↥H] [hH : IsAddCyclic ↥H], ∃ a < 0, AddSubgroup.zmultiples a = H
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap.eq_1 : ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap =
  {
    forget₂ :=
      { obj := fun G => G.toProfinite,
        map := fun {X Y} f =>
          CompHausLike.ofHom (fun X => TotallyDisconnectedSpace ↑X)
            { toFun := ⇑(ProfiniteAddGrp.Hom.hom f), continuous_toFun := ⋯ },
        map_id :=
          ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_2,
        map_comp :=
          @ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_3 },
    forget_comp :=
      ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_5 }
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsTerminal.uniqueUpToIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (hT' : CategoryTheory.Limits.IsTerminal T'), (hT.uniqueUpToIso hT').inv = hT.from T'
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_inf : ∀ {G : Type u_2} [inst : AddGroup G] (S₁ S₂ : AddSubgroup G), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns an element in the tree equivalent to `x` if one exists.  -/
RBTree.RBSet.find? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → α → Option α
-- Init.Data.List.Nat.Modify
List.eraseIdx_eq_modifyTailIdx : ∀ {α : Type u_1} (i : ℕ) (l : List α), l.eraseIdx i = l.modifyTailIdx i List.tail
-- Mathlib.Order.Bounds.Basic
IsLUB.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} {a : α} {b : β},
  s.Nonempty → t.Nonempty → IsLUB s a → IsLUB t b → IsLUB (s ×ˢ t) (a, b)
-- Mathlib.Order.GaloisConnection.Basic
isGLB_image2_of_isLUB_isGLB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (u₂ a) (u a)) → IsLUB s a₀ → IsGLB t b₀ → IsGLB (Set.image2 u s t) (u a₀ b₀)
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.le_slope_of_hasDerivWithinAt_Iio : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Iio y) y → f' ≤ slope f x y
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.dvdNotUnit_of_lt : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {a b : Associates M}, a < b → DvdNotUnit a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- **Alias** of `summable_cotTerm`. -/
Summable_cotTerm : ∀ {x : ℂ}, x ∈ Complex.integerComplement → Summable fun n => cotTerm x n
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.sum_mul_smul : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • Polynomial.X ^ 2
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuousWithinAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α},
  SemicontinuousWithinAt r s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, ¬r x' y) → ¬r x y
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.toInt? : Lean.FuzzyMatching.Score✝ → Option ℤ
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The constant sheaf functor is left adjoint to evaluation at a terminal object.  -/
CategoryTheory.constantSheafAdj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {T : C} →
              CategoryTheory.Limits.IsTerminal T →
                (CategoryTheory.constantSheaf J D ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivWithinAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') s x
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- `f` is a left inverse of `algebraMap R S`.  -/
QuasispectrumRestricts.left_inv : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalRing A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  QuasispectrumRestricts a f → Function.LeftInverse f ⇑(algebraMap R S)
-- Mathlib.Data.EReal.Operations
EReal.bot_add : ∀ (x : EReal), ⊥ + x = ⊥
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.category_comp_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {Z Y X : CategoryTheory.Limits.Cocone F}
  (g : CategoryTheory.Limits.CoconeMorphism Z Y) (f : CategoryTheory.Limits.CoconeMorphism Y X),
  (CategoryTheory.CategoryStruct.comp g f).hom = CategoryTheory.CategoryStruct.comp g.hom f.hom
-- Lean.Parser.Command
Lean.Parser.Command.definition.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instIntCast : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [IntCast Y] → IntCast (LocallyConstant X Y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α}
  [inst : Inhabited β],
  (List.map Prod.fst l).contains k = false → Std.DHashMap.Const.get! (Std.DHashMap.Const.ofList l) k = default
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`.  -/
HomologicalComplex.sc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → ι → ι → ι → CategoryTheory.ShortComplex C
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
dotProduct_star_self_eq_zero : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R}, star v ⬝ᵥ v = 0 ↔ v = 0
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioc_bot : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Ioc ⊥ ↑y = Set.Iic y
-- Mathlib.Data.Finsupp.Notation
/-- Display `Finsupp` using `fun₀` notation.  -/
Finsupp.instRepr : {α : Type u_1} → {β : Type u_2} → [Repr α] → [Repr β] → [inst : Zero β] → Repr (α →₀ β)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.minD fallback = fallback
-- Init.Data.Nat.Lemmas
Nat.dvd_iff_div_mul_eq : ∀ (n d : ℕ), d ∣ n ↔ n / d * d = n
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
then `F` preserves colimits for `K`.  -/
CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesColimit K (F.comp G)] [CategoryTheory.Limits.ReflectsColimit (K.comp F) G],
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) ⁻¹' Set.Ioi b = Set.Iio (a / b)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The tautological action by `M ≃ₗ[R] M` on `M`.

This generalizes `Function.End.applyMulAction`.  -/
LinearEquiv.applyDistribMulAction : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → DistribMulAction (M ≃ₗ[R] M) M
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsPretransitiveVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X]
  [AddAction.IsPretransitive M X], AddAction.IsPretransitive M (SeparationQuotient X)
-- Mathlib.CategoryTheory.EpiMono
/-- The retraction of a split monomorphism is itself a split epimorphism.  -/
CategoryTheory.retraction_isSplitEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.IsSplitMono f], CategoryTheory.IsSplitEpi (CategoryTheory.retraction f)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.neg_lt_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddRightStrictMono α] {a : α}, 0 < a → -a < a
-- Mathlib.RingTheory.Support
/-- If `M` is `R`-finite, then `Supp M = Z(Ann(M))`.  -/
Module.support_eq_zeroLocus : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M],
  Module.support R M = PrimeSpectrum.zeroLocus ↑(Module.annihilator R M)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffDist_singleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Metric.hausdorffDist {x} {y} = dist x y
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_bot_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.IsComplement' ⊥ ↔ H = ⊤
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_ceil_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R], Nat.ceil ⁻¹' {0} = Set.Iic 0