mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
This version assumes joint continuity of `f`, see `cfc_setIntegral'` for a statement
with weaker assumptions.  -/
cfc_setIntegral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : NormedSpace ℝ A]
  [inst_8 : TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
            autoParam (p a) cfc_setIntegral._auto_1 →
              cfc (fun r => ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfc (f x) a ∂μ
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.comp : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (self : CategoryTheory.Limits.DiagramOfCocones F)
  {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
  (self.map (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp (self.map f).hom (self.map g).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_right_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C), (X.homologyData₀ R).right.Q = ∐ fun x => R
-- Mathlib.Algebra.Order.Module.Defs
posSMulMono_iff_posSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] [inst_5 : PartialOrder α] [inst_6 : PartialOrder β],
  PosSMulMono α β ↔ PosSMulStrictMono α β
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.IsAffineOpen.of_subsingleton : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, (↑U).Subsingleton → AlgebraicGeometry.IsAffineOpen U
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.neg_smul : ∀ {α : 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)
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int8.ofInt 48 = 48`
* `Int8.ofInt (-115) = -115`
* `Int8.ofInt (-129) = 127`
* `Int8.ofInt (128) = -128`
 -/
Int8.ofInt : ℤ → Int8
-- Mathlib.Data.FunLike.IsApply
IsVAddApply.vadd_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : VAdd M β} {inst_2 : VAdd M F} [self : IsVAddApply M F α β] (f : F) (n : M) (x : α), (n +ᵥ f) x = n +ᵥ f x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `structureMapCLM 𝕜 n i` is the continuous `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to its
`i`-th iterated derivative as an element of `E →ᵇ (E [×i]→L[ℝ] F)`.
This only makes mathematical sense if `i ≤ n`, otherwise we define it as the zero map.

We call these "structure maps" because they define the topology on `𝓓^{n}_{K}(E, F)`.  -/
ContDiffMapSupportedIn.structureMapCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n : ℕ∞) →
                      {K : TopologicalSpace.Compacts E} →
                        (i : ℕ) → ContDiffMapSupportedIn E F n K →L[𝕜] BoundedContinuousFunction E (E [×i]→L[ℝ] F)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divCoeffs.eq_2 : ∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.divCoeffs k (Int.Internal.Linear.Poly.add k_1 v p_1) =
    (k_1 % k == 0 && Int.Internal.Linear.Poly.divCoeffs k p_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Init.Data.String.Lemmas.Order
String.Pos.le_sliceFrom_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p ≤ p₀.sliceFrom q h ↔ String.Pos.ofSliceFrom p ≤ q
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.IsLimit.binaryFanSwap_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (I : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Y X)),
  I.binaryFanSwap.lift t = I.lift (CategoryTheory.Limits.BinaryFan.swap t)
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the partial numerators `aᵢ` are equal to one.  -/
GenContFract.of_partNum_eq_one : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {a : K},
  (GenContFract.of v).partNums.get? n = some a → a = 1
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPStructureInstancesDefaults : Lean.Options → Bool
-- Mathlib.Computability.Primrec.List
/-- If `R a b` is decidable, then given `L : List α` and `b : β`, `g L b ↔ ∀ a L, R a b`
is a primitive recursive relation.  -/
PrimrecRel.forall_mem_list : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [inst : Primcodable α] [inst_1 : Primcodable β],
  PrimrecRel R → PrimrecRel fun L b => ∀ a ∈ L, R a b
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofPairwiseDisjoint_parts : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (parts : Finset α)
  (hdisjoint : (↑parts).PairwiseDisjoint id), (Finpartition.ofPairwiseDisjoint parts hdisjoint).parts = parts.erase ⊥
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, adding the angles between them in cyclic order results in 0.  -/
Orientation.oangle_add_cyc3 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V}, x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x y + o.oangle y z + o.oangle z x = 0
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} →
          {I₁ I₂ : S.Arrow} →
            (Z : C) →
              (g₁ : Z ⟶ I₁.Y) →
                (g₂ : Z ⟶ I₂.Y) →
                  autoParam (CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f)
                      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam →
                    I₁.Relation I₂
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_top : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : Monoid M] [inst_4 : DistribMulAction M V] [inst_5 : SMulCommClass M k V] {a : M}, IsUnit a → a • ⊤ = ⊤
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.snd_comp_inl : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ContinuousLinearMap.snd R M₁ M₂ ∘SL ContinuousLinearMap.inl R M₁ M₂ = 0
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.zero_mem_spectrum_inr : ∀ (R : Type u_3) (S : Type u_4) {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommRing S] [Nontrivial S]
  [inst_3 : NonUnitalRing A] [inst_4 : Algebra R S] [inst_5 : Module S A] [inst_6 : IsScalarTower S A A]
  [inst_7 : SMulCommClass S A A] [inst_8 : Module R A] [inst_9 : IsScalarTower R S A] (a : A), 0 ∈ spectrum R ↑a
-- Mathlib.Algebra.Lie.Basic
add_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L) (m : M),
  ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
-- Mathlib.Algebra.Polynomial.Basic
/-- See also `Polynomial.isCancelMulZero_iff`: in order for `R[X]` to have cancellative
multiplication (stronger than `NoZeroDivisors` in general, but equivalent if `R` is a ring),
`R` must have both cancellative multiplication and cancellative addition.  -/
Polynomial.noZeroDivisors_iff : ∀ {R : Type u} [inst : Semiring R], NoZeroDivisors (Polynomial R) ↔ NoZeroDivisors R
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup, then `p` divides the
index of `H` inside its normalizer.  -/
Sylow.prime_dvd_card_quotient_normalizer : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [Fact (Nat.Prime p)],
  p ^ (n + 1) ∣ Nat.card G →
    ∀ {H : Subgroup G},
      Nat.card ↥H = p ^ n → p ∣ Nat.card (↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.le_spanSingleton_mul_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x : P} {I J : FractionalIdeal S P},
  I ≤ FractionalIdeal.spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
-- Init.Data.Nat.Lemmas
Nat.add_eq_max_iff : ∀ {m n : ℕ}, m + n = max m n ↔ m = 0 ∨ n = 0
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Scalar multiplication by a group element as a continuous linear equivalence.  -/
ContinuousLinearEquiv.smulLeft : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] →
            {G : Type u_9} →
              [inst_4 : Group G] →
                [inst_5 : DistribMulAction G M₁] →
                  [ContinuousConstSMul G M₁] → [SMulCommClass G R₁ M₁] → G →* M₁ ≃L[R₁] M₁
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.instInhabitedMapping : Inhabited Mathlib.Tactic.Superscript.Mapping
-- Aesop.Saturate
Aesop.SaturateM.Context.mk.sizeOf_spec : ∀ (options : Aesop.Options'), sizeOf { options := options } = 1 + sizeOf options
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabNoMatch.loop : Lean.Syntax → List Lean.Term → Array Lean.Syntax → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Each element of the scalars defines a zero-preserving map.  -/
SMulZeroClass.toZeroHom : {M : Type u_1} → (A : Type u_7) → [inst : Zero A] → [SMulZeroClass M A] → M → ZeroHom A A
-- Batteries.Data.List.Perm
List.isSubperm_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isSubperm l₂ = true ↔ l₁.Subperm l₂
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.top_prod : ∀ {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β},
  lb.HasBasis pb sb → (⊤ ×ˢ lb).HasBasis pb fun x => Set.univ ×ˢ sb x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_zero : Real.Angle.toReal 0 = 0
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of a family uniformly equicontinuous on `S` is uniformly continuous on `S`.  -/
UniformEquicontinuousOn.uniformContinuousOn : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} {S : Set β},
  UniformEquicontinuousOn F S → ∀ (i : ι), UniformContinuousOn (F i) S
-- Init.Data.Array.Zip
Array.unzip_eq_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip = (Array.map Prod.fst xs, Array.map Prod.snd xs)
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstNatPowNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.FieldTheory.Separable
AlgHom.card_of_powerBasis : ∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} {L : Type u_5} [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K S] [inst_4 : Algebra K L] (pb : PowerBasis K S),
  IsSeparable K pb.gen → (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits → Fintype.card (S →ₐ[K] L) = pb.dim
-- Mathlib.Algebra.Order.Module.Defs
nonpos_of_smul_nonpos_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulReflectLE α β], a • b ≤ 0 → 0 < a → b ≤ 0
-- Mathlib.Probability.Martingale.OptionalSampling
/-- **Optional Sampling theorem**. If `τ` is a bounded stopping time and `σ` is another stopping
time, then the value of a martingale `f` at the stopping time `min τ σ` is almost everywhere equal
to the conditional expectation of `f` stopped at `τ` with respect to the σ-algebra generated
by `σ`.  -/
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [LocallyFiniteOrder ι]
  [inst_5 : OrderBot ι] [inst_6 : TopologicalSpace ι] [DiscreteTopology ι] [inst_8 : MeasurableSpace ι] [BorelSpace ι]
  [inst_10 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : MeasureTheory.Filtration ι m}
  {τ σ : Ω → WithTop ι} {f : ι → Ω → E} [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hσ : MeasureTheory.IsStoppingTime ℱ σ) {n : ι},
      (∀ (x : Ω), τ x ≤ ↑n) →
        ∀ [h_sf_min : MeasureTheory.SigmaFinite (μ.trim ⋯)],
          (MeasureTheory.stoppedValue f fun x => min (σ x) (τ x)) =ᵐ[μ]
            μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace]
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_adj' : ∀ {n : ℕ} {u v : Fin n}, (SimpleGraph.cycleGraph n).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial.eq_def : ∀ (x : ℕ),
  x.superFactorial =
    match x with
    | 0 => 1
    | n.succ => n.succ.factorial * n.superFactorial
-- Plausible.Random
/-- Generate one more `Nat`  -/
Plausible.Rand.next : {g : Type} → {m : Type → Type u_1} → [RandomGen g] → [Monad m] → Plausible.RandGT g m ℕ
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.eq_def : ∀ {σs : List (Type u)} (P Q : Std.Do.SPred σs),
  (P ⊣⊢ₛ Q) =
    match σs, P, Q with
    | [], P, Q => P.down ↔ Q.down
    | σ :: tail, P, Q => ∀ (s : σ), P s ⊣⊢ₛ Q s
-- Mathlib.Topology.GDelta.Basic
/-- Dense open sets are residual.  -/
residual_of_dense_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → Dense s → s ∈ residual X
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_iff_not_exists_mul_eq : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
instPosMulStrictMonoWithZeroOfMulLeftStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftStrictMono α], PosMulStrictMono (WithZero α)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.isSubwalk_dropUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  (p.dropUntil w h).IsSubwalk p
-- Mathlib.Order.Hom.Basic
/-- Composition of two order embeddings is an order embedding  -/
OrderEmbedding.comp : {α : Type u_2} →
  {β : Type u_3} → {γ : Type u_4} → [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → α ↪o β → β ↪o γ → α ↪o γ
-- Mathlib.CategoryTheory.Sites.Coverage
/-- The type `Coverage C` of coverages on `C`.
A coverage is a collection of *covering* presieves on every object `X : C`,
which satisfies a *pullback compatibility* condition.
Explicitly, this condition says that whenever `S` is a covering presieve for `X` and
`f : Y ⟶ X` is a morphism, then there exists some covering presieve `T` for `Y`
such that `T` factors through `S` along `f`.
 -/
CategoryTheory.Coverage : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)
-- Mathlib.Data.Matrix.Diagonal
Matrix.one : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [Zero α] → [One α] → One (Matrix n n α)
-- Mathlib.Data.Multiset.AddSub
Multiset.card_erase_lt_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (s.erase a).card < s.card
-- Lean.Compiler.Specialize
Lean.Compiler.hasNospecializeAttribute : Lean.Environment → Lean.Name → Bool
-- Std.Do.SPred.SVal
Std.Do.SVal.instGetTyCons_1 : {σ₁ : Type u_1} → {σs : List (Type u_1)} → {σ₂ : Type u_1} → [Std.Do.SVal.GetTy σ₁ σs] → Std.Do.SVal.GetTy σ₁ (σ₂ :: σs)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_measure_zero : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.eLpNormEssSup f 0 = 0
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_natCast_iff : ∀ {n : ℕ}, Irrational √↑n ↔ ¬IsSquare n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.ofList l cmp).getKey? k' = some k
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.coneOpEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op c.unop, map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => (Opposite.unop c).op, map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ })
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sum : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {s : Finset ι}, (∀ i ∈ s, A i =O[l] g) → (∑ i ∈ s, A i) =O[l] g
-- Init.Data.Array.Extract
Array.extract_add_left : ∀ {α : Type u_1} {as : Array α} {i j k : ℕ}, as.extract (i + j) k = (as.extract i k).extract j (k - i)
-- Mathlib.Topology.MetricSpace.Completion
/-- The embedding of a metric space in its completion is an isometry.  -/
UniformSpace.Completion.coe_isometry : ∀ {α : Type u} [inst : PseudoMetricSpace α], Isometry UniformSpace.Completion.coe'
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nndist_eq_add : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β],
  p ≠ ⊤ →
    ∀ (x y : WithLp p (α × β)),
      nndist x y = (nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_comp_of_preimage_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'},
  MDiffAt[u] g (f x) →
    MDiffAt[s] f x →
      f ⁻¹' u ∈ nhdsWithin x s → UniqueMDiffAt[s] x → mfderiv[s] (g ∘ f) x = mfderiv[u] g (f x) ∘SL mfderiv[s] f x
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.mem_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (x : R),
  x ∈ IsLocalRing.maximalIdeal R ↔ x ∈ nonunits R
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], Additive.ofMul ⊤ = ⊤
-- Lean.Elab.Attributes
Lean.Elab.elabAttrs : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadResolveName m] →
        [Lean.MonadError m] →
          [Lean.Elab.MonadMacroAdapter m] →
            [Lean.MonadRecDepth m] →
              [Lean.MonadTrace m] →
                [Lean.MonadOptions m] →
                  [Lean.AddMessageContext m] →
                    [Lean.MonadLog m] →
                      [MonadLiftT IO m] → [MonadFinally m] → Array Lean.Syntax → m (Array Lean.Elab.Attribute)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The Lebesgue measure associated to an alternating map. It gives measure `|ω v|` to the
parallelepiped spanned by the vectors `v₁, ..., vₙ`. Note that it is not always a Haar measure,
as it can be zero, but it is always locally finite and translation invariant.  -/
AlternatingMap.measure : {G : Type u_4} →
  [inst : NormedAddCommGroup G] →
    [inst_1 : NormedSpace ℝ G] →
      [inst_2 : MeasurableSpace G] →
        [BorelSpace G] →
          [FiniteDimensional ℝ G] →
            {n : ℕ} → [_i : Fact (Module.finrank ℝ G = n)] → G [⋀^Fin n]→ₗ[ℝ] ℝ → MeasureTheory.Measure G
-- Mathlib.Algebra.Torsor.Defs
/-- Torsor addition and subtraction with the same element cancels out.  -/
AddTorsor.vadd_vsub' : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : AddGroup G} [self : AddTorsor G P] (g : G) (p : P), (g +ᵥ p) -ᵥ p = g
-- Mathlib.MeasureTheory.SetAlgebra
/-- If a set belongs to the algebra of sets generated by `𝒜` then it can be written as a finite
union of finite intersections of sets which are in `𝒜` or have their complement in `𝒜`.  -/
MeasureTheory.mem_generateSetAlgebra_elim : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {s : Set α},
  s ∈ MeasureTheory.generateSetAlgebra 𝒜 →
    ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_cons : ∀ (exp : ℝ) (tl : Tactic.ComputeAsymptotics.UnitMonomial) (basis_hd : ℝ → ℝ)
  (basis_tl : Tactic.ComputeAsymptotics.Basis),
  Tactic.ComputeAsymptotics.UnitMonomial.toFun (exp :: tl) (basis_hd :: basis_tl) = basis_hd ^ exp * tl.toFun basis_tl
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
_private.Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt.0.termTsze : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Moving to the opposite additive commutative monoid commutes with summing.  -/
Finset.op_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.neg` -/
MeromorphicOn.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → MeromorphicOn (fun i => -f i) U