mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Range
/-- The inclusion of `ValueGroup₀ f` into `WithZero Bˣ` as a homomorphism of monoids with zero.  -/
MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHom : {A : Type u_1} →
  {B : Type u_2} →
    [inst : MonoidWithZero A] →
      [inst_1 : LinearOrderedCommGroupWithZero B] → (f : A →*₀ B) → f.ValueGroup₀ →*₀o WithZero Bˣ
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_erase_attach : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} (f : ι → M) (i : ↥s),
  ∑ j ∈ s.attach.erase i, f ↑j = ∑ j ∈ s.erase ↑i, f j
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C)
  (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D) {X Y : B} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.append_assoc : ∀ {α : Type u} (s t u : Stream'.WSeq α), (s.append t).append u = s.append (t.append u)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A convex combination of a point with itself is that point.  -/
Convexity.convexCombPair_same : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M},
  Convexity.convexCombPair s t hs ht h x x = x
-- Batteries.Data.Vector.Lemmas
Vector.toArray_scanrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β} {as : Vector α n}, Vector.toArray <$> Vector.scanrM f init as = Array.scanrM f init as.toArray
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_C_zero : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).coeff 0 = a
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_of_det_ne_zero : ∀ {M₂ : Type u_4} [inst : AddCommGroup M₂] {A : Type u_5} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Module A M₂]
  (B₃ : LinearMap.BilinForm A M₂) {ι : Type u_6} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (b : Module.Basis ι A M₂), ((LinearMap.BilinForm.toMatrix b) B₃).det ≠ 0 → B₃.Nondegenerate
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.IsBimonHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.BimonObj M]
  [inst_4 : CategoryTheory.BimonObj N] {f : M ⟶ N} [toIsMonHom : CategoryTheory.IsMonHom f]
  [toIsComonHom : CategoryTheory.IsComonHom f], CategoryTheory.IsBimonHom f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `minIndexable := false`  -/
Lean.Meta.Grind.MinIndexableMode.no : Lean.Meta.Grind.MinIndexableMode
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.comp_left_injective : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (e : M ≃+ N), Function.Injective fun f => f.comp ↑e
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} [inst_1 : SizeOf C]
  (pullback : C) (p₁ : pullback ⟶ X₁) (p₂ : pullback ⟶ X₂)
  (condition : CategoryTheory.CategoryStruct.comp p₁ f₁ = CategoryTheory.CategoryStruct.comp p₂ f₂)
  (isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁ p₂ condition)) (p : pullback ⟶ S)
  (hp₁ : autoParam (CategoryTheory.CategoryStruct.comp p₁ f₁ = p) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam),
  sizeOf { pullback := pullback, p₁ := p₁, p₂ := p₂, condition := condition, isLimit := isLimit, p := p, hp₁ := hp₁ } =
    1 + sizeOf pullback + sizeOf p₁ + sizeOf p₂ + sizeOf condition + sizeOf isLimit + sizeOf p + sizeOf hp₁
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ρ_sq : ↑UpperHalfPlane.ρ ^ 2 = -↑UpperHalfPlane.ρ - 1
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint16.sizeOf_spec : sizeOf Lean.IR.IRType.uint16 = 1
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- When `ϕ` is a continuous alternating map
between the fibers `E₁ x` and `E₂ y` of two vector bundles `E` and `E'`,
`ContinuousAlternatingMap.inCoordinates F E F' E' x₀ x y₀ y ϕ`
is a coordinate change of this continuous linear map
w.r.t. the chart around `x₀` and the chart around `y₀`.

It is defined by composing `ϕ` with appropriate coordinate changes
given by the vector bundles `E₁` and `E₂`.
We use the operations `Bundle.Trivialization.continuousLinearMapAt` and
`Bundle.Trivialization.symmL` in the definition, instead of
`Bundle.Trivialization.continuousLinearEquivAt`, so that
`ContinuousAlternatingMap.inCoordinates` is defined everywhere.
See also `ContinuousAlternatingMap.inCoordinates_eq`.

This is the (second component of the) underlying function
of a trivialization of the bundle of continuous alternating maps,
see `FiberBundle.trivializationAt_continuousAlternatingMap_apply`.

However, note that `ContinuousAlternatingMap.inCoordinates` is
defined even when `x` and `y` live in different base sets.
Therefore, it is also convenient when working with the bundle of continuous alternating maps
between pulled back bundles.
 -/
ContinuousAlternatingMap.inCoordinates : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      {B₁ : Type u_3} →
        (F₁ : Type u_4) →
          [inst_1 : NormedAddCommGroup F₁] →
            [inst_2 : NormedSpace 𝕜 F₁] →
              {E₁ : B₁ → Type u_5} →
                [inst_3 : (x : B₁) → AddCommGroup (E₁ x)] →
                  [inst_4 : (x : B₁) → Module 𝕜 (E₁ x)] →
                    [inst_5 : TopologicalSpace B₁] →
                      [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                        [inst_7 : (x : B₁) → TopologicalSpace (E₁ x)] →
                          [inst_8 : FiberBundle F₁ E₁] →
                            [VectorBundle 𝕜 F₁ E₁] →
                              {B₂ : Type u_6} →
                                (F₂ : Type u_7) →
                                  [inst_10 : NormedAddCommGroup F₂] →
                                    [inst_11 : NormedSpace 𝕜 F₂] →
                                      {E₂ : B₂ → Type u_8} →
                                        [inst_12 : (x : B₂) → AddCommGroup (E₂ x)] →
                                          [inst_13 : (x : B₂) → Module 𝕜 (E₂ x)] →
                                            [inst_14 : TopologicalSpace B₂] →
                                              [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                                [inst_16 : (x : B₂) → TopologicalSpace (E₂ x)] →
                                                  [inst_17 : FiberBundle F₂ E₂] →
                                                    [VectorBundle 𝕜 F₂ E₂] →
                                                      B₁ →
                                                        (x : B₁) →
                                                          B₂ → (y : B₂) → E₁ x [⋀^ι]→L[𝕜] E₂ y → F₁ [⋀^ι]→L[𝕜] F₂
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.restrictScalars : ∀ {𝕜 : 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] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜' E F} {x : E} {s : Set E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    HasFPowerSeriesWithinOnBall f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x r
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_natCast_add_one : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (n : ℕ), ↑(↑n + 1) = ↑n + 1
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The type of the lemma  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.lemmaType : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Lean.Expr
-- Init.Data.SInt.Lemmas
Int16.toInt8_toInt32 : ∀ (n : Int16), n.toInt32.toInt8 = n.toInt8
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.comp_localizationAway_ker : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι) (f : P.Ring),
  (algebraMap P.Ring S) f = g →
    ((Algebra.Generators.localizationAway T g).comp P).ker =
      Ideal.map ((Algebra.Generators.localizationAway T g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(MvPolynomial.rename Sum.inr) f * MvPolynomial.X (Sum.inl ()) - 1}
-- Mathlib.Logic.Encodable.Basic
Encodable.nonempty_encodable : ∀ {α : Type u_1}, Nonempty (Encodable α) ↔ Countable α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toList_node : ∀ {α : Type u_1} {c : RBTree.RBColor} {a : RBTree.RBNode α} {x : α} {b : RBTree.RBNode α},
  (RBTree.RBNode.node c a x b).toList = a.toList ++ x :: b.toList
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuot_ext'_iff : ∀ {S : Type uS} [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u₄}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop} {f g : RingQuot s →ₐ[S] B},
  f = g ↔ f.comp (RingQuot.mkAlgHom S s) = g.comp (RingQuot.mkAlgHom S s)
-- Mathlib.Topology.Sets.VietorisTopology
/-- Given a basis `B` on a topological space `α`, the topology of `Compacts α` has a basis
consisting of sets of the form `{K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}`, where
`U₁, …, Uₙ ∈ B`.  -/
TopologicalSpace.IsTopologicalBasis.compacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    TopologicalSpace.IsTopologicalBasis
      ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B})
-- Init.Data.Repr
instReprString : Repr String
-- Mathlib.Algebra.Group.Units.Defs
Units.val_mul : ∀ {α : Type u} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑b
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toNonUnitalSubsemiring_injective : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Function.Injective NonUnitalSubring.toNonUnitalSubsemiring
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], Dilation.ratio 1 = 1
-- Mathlib.Algebra.Star.Rat
NNRat.instTrivialStar : TrivialStar ℚ≥0
-- Mathlib.GroupTheory.Sylow
Sylow.coe_mapSurjective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Finite G] {G' : Type u_2} [inst_2 : Group G'] {f : G →* G'}
  (hf : Function.Surjective ⇑f) [inst_3 : Fact (Nat.Prime p)] (P : Sylow p G),
  ↑(Sylow.mapSurjective hf P) = Subgroup.map f ↑P
-- Mathlib.Logic.Relation
/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`.  -/
Std.Refl.ne_imp_iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {x y : α}, x ≠ y → r x y ↔ r x y
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
the base is nonnegative and positive when the base is positive.  -/
Mathlib.Meta.Positivity.evalRpow : Mathlib.Meta.Positivity.PositivityExt
-- Std.Http.Data.Body.Stream
/-- Buffered partial chunk data accumulated from `Stream.send ... (incomplete := true)`.
These partial pieces are collapsed and emitted as a single chunk on the next complete send.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.pendingIncompleteChunk : Std.Http.Body.Channel.State✝ → Option Std.Http.Chunk
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i)
  [inst_6 : DecidableEq ι], HasFDerivAt (⇑f) (f.linearDeriv x) x
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_sup : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M)
  (S T : Subsemiring R), a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsDeterministicId : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsDeterministic ProbabilityTheory.Kernel.id
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.homEquiv.eq_1 : ∀ (G : GrpCat) (P : ProfiniteGrp.{u}),
  ProfiniteGrp.ProfiniteCompletion.homEquiv G P =
    {
      toFun := fun f =>
        CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
          ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map f),
      invFun := fun f => ProfiniteGrp.ProfiniteCompletion.lift f, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take.eq_1 : ∀ {α : Type u} (x : Stream'.Seq α), Stream'.Seq.take 0 x = []
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Constant to use for field completion terminfo. The root of the trie has this set.
Collected from `EvalConfigItemHandler.struct?`.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.struct? : Lean.Elab.ConfigEval.HandlerTrie✝ → Option Lean.Name
-- Init.Data.List.Lemmas
List.getLast?_singleton : ∀ {α : Type u_1} {a : α}, [a].getLast? = some a
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is right-regular if and only if `R` is trivial.  -/
isRightRegular_zero_iff_subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRightRegular 0 ↔ Subsingleton R
-- Mathlib.Probability.Distributions.Pareto
/-- CDF of the Pareto distribution equals the integral of the PDF.  -/
ProbabilityTheory.cdf_paretoMeasure_eq_integral : ∀ {t r : ℝ},
  0 < t →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x =
          ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.paretoPDFReal t r x
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.card_le_one_iff_eq_bot : ∀ {M : Type u_1} [inst : Monoid M] {S : Submonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S ≤ 1 ↔ S = ⊥
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.argNames : Lean.Elab.Deriving.Header → Array Lean.Name
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofDataValue? : Lean.DataValue → Option Lean.LeanOptionValue
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.get? : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → Option (β a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f m[k]?).isNone)
-- Lean.Parser.Extension
Lean.Parser.AliasValue.unary.inj : ∀ {α : Type} {p p_1 : α → α}, Lean.Parser.AliasValue.unary p = Lean.Parser.AliasValue.unary p_1 → p = p_1
-- Init.SizeOf
Lean.ParserDescr.nonReservedSymbol.sizeOf_spec : ∀ (val : String) (includeIdent : Bool),
  sizeOf (Lean.ParserDescr.nonReservedSymbol val includeIdent) = 1 + sizeOf val + sizeOf includeIdent
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_toArray : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool}, it.toArray.all p = Std.Iter.all p it
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_toNat : ∀ (n : USize), USize.ofNatClamp n.toNat = n
-- Mathlib.Algebra.Polynomial.Basic
/-- The finset of nonzero coefficients of a polynomial.  -/
Polynomial.coeffs : {R : Type u} → [inst : Semiring R] → Polynomial R → Finset R
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_add : ∀ {n : ℕ} (x y : ℤ), BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_map_ofDual`. -/
List.SortedGE.of_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, l.SortedGE → (List.map (⇑OrderDual.ofDual) l).SortedLE
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↑X.toTopCat) (hxx' : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (X.presheaf.stalkSpecializes ⋯) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x')
-- Mathlib.Data.List.Lemmas
List.mapAccumr₂.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : List α) (x_1 : γ),
  (x = [] → False) → List.mapAccumr₂ f x [] x_1 = (x_1, [])
-- Mathlib.Order.Bounds.Basic
bddBelow_iff_exists_le : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] {s : Set γ} (x₀ : γ), BddBelow s ↔ ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y
-- Mathlib.MeasureTheory.Integral.Gamma
Complex.integral_exp_neg_mul_rpow : ∀ {p b : ℝ}, 1 ≤ p → 0 < b → ∫ (x : ℂ), Real.exp (-b * ‖x‖ ^ p) = Real.pi * b ^ (-2 / p) * Real.Gamma (2 / p + 1)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_mul_dvd_mul_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (k m n : α), gcd k (m * n) ∣ gcd k m * gcd k n
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListₘ.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (l : List ((a : α) × β a)),
  m.insertListₘ l =
    match l with
    | [] => m
    | hd :: tl => (m.insert hd.fst hd.snd).insertListₘ tl
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableEqOffset : DecidableEq Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- The evaluation morphism is given by the contraction map.  -/
FGModuleCat.FGModuleCatEvaluation : (K : Type u) →
  [inst : Field K] →
    (V : FGModuleCat K) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (FGModuleCat.FGModuleCatDual K V) V ⟶
        CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat K)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.map_mk : ∀ (f : Type u → Type v) (hf : (α β : Type u) → α ≃ β → f α ≃ f β) (α : Type u),
  Cardinal.map f hf (Cardinal.mk α) = Cardinal.mk (f α)
-- Lean.Meta.Tactic.Grind.Action
/-- Appends a new tactic syntax to a successful result.
Used by leaf actions to record the tactic that produced progress.
If `(← getConfig).trace` is `false`, it just returns `r`.
 -/
Lean.Meta.Grind.Action.concatTactic : Lean.Meta.Grind.ActionResult →
  Lean.Meta.Grind.GrindM Lean.Meta.Grind.TGrind → Lean.Meta.Grind.GrindM Lean.Meta.Grind.ActionResult
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.id_toFun : ∀ (A : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A] (x : A), (ContinuousAddMonoidHom.id A) x = x
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsPrestackFor_generate_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Presieve S), F.IsPrestackFor (CategoryTheory.Sieve.generate R).arrows ↔ F.IsPrestackFor R
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.toList.match_1.splitter : {α : Type u_1} →
  (motive : Lists α → Sort u_2) → (x : Lists α) → ((fst : Bool) → (l : Lists' α fst) → motive ⟨fst, l⟩) → motive x
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_add : ∀ (x y : ℝ), Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ) (h : t.Balanced),
  t.insertManyIfNew l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have hr := ⋯;
              have r := ⟨(Std.DTreeMap.Internal.Impl.insertIfNew a b (↑r) hr).impl, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedNewInsertionInto := __s
      pure r).run
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- Adding a new zero to a canonically ordered additive monoid produces another one.  -/
WithZero.instCanonicallyOrderedAdd : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α],
  CanonicallyOrderedAdd (WithZero α)
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofIntClamp : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.Data.Sign.Defs
SignType.le_one : ∀ (a : SignType), a ≤ 1
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.eq_one_of_pow : ∀ {x n : ℕ}, Nat.Prime (x ^ n) → n = 1
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.falsum.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {n : ℕ},
  sizeOf FirstOrder.Language.BoundedFormula.falsum = 1 + sizeOf n
-- Mathlib.Data.Set.SymmDiff
Set.symmDiff_nonempty : ∀ {α : Type u} {s t : Set α}, (symmDiff s t).Nonempty ↔ s ≠ t
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.map` as a `MonoidHom`.  -/
LocallyConstant.mapMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        [inst_1 : MulOneClass Y] → [inst_2 : MulOneClass Z] → (Y →* Z) → LocallyConstant X Y →* LocallyConstant X Z
-- Mathlib.Topology.Algebra.UniformField
_private.Mathlib.Topology.Algebra.UniformField.0.termHat : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t[a]?.isSome = true ↔ a ∈ t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_toReal_eq_two_mul : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsGLB.mem_of_nonempty_of_not_isPredPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {x : α},
  IsGLB s x → s.Nonempty → ¬Order.IsPredPrelimit x → x ∈ s
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.functor_map_app : ∀ {n m : Type uᵒᵖ} (i : n ⟶ m) (S : AlgebraicGeometry.Scheme),
  (AlgebraicGeometry.AffineSpace.functor.map i).app S =
    AlgebraicGeometry.AffineSpace.reindex (⇑(CategoryTheory.ConcreteCategory.hom i.unop)) S
-- Mathlib.LinearAlgebra.Ray
/-- If a vector `v₁` is on the same ray as a nonzero vector `v₂`, then it is equal to `c • v₂` for
some nonnegative `c`.  -/
SameRay.exists_nonneg_right : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R x y → y ≠ 0 → ∃ r, 0 ≤ r ∧ x = r • y