mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.norm_natCast_le_one : ∀ (R : Type u_1) [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (n : ℕ), ‖↑n‖ ≤ 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_pi_div_two_sub : ∀ (θ : Real.Angle), (↑(Real.pi / 2) - θ).sin = θ.cos
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_adaptExcept_EStateM_apply_eq : ∀ {ε ε' σ α : Type} {post : α → σ → Prop} {epost : ε' → σ → Prop} (f : ε → ε') (x : EStateM ε σ α),
  Std.Internal.Do.wp (EStateM.adaptExcept f x) post epost = Std.Internal.Do.wp x post fun e => epost (f e)
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The modular discriminant `Δ` as a cusp form of weight 12 and level 1.  -/
CuspForm.discriminant : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_def : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.contentIdeal = Ideal.span ↑p.coeffs
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf),
  (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).i = CategoryTheory.Limits.Fork.ι kf
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instRigidCategoryFunctorSingleObj : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) →
        [inst_2 : Group H] →
          [CategoryTheory.RigidCategory V] →
            CategoryTheory.RigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] (i j : ι), P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Given a short exact short complex `S` in an abelian category `C` and an object `X : C`,
this is the long exact sequence
`Ext X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁`
when `n₀ + 1 = n₁`  -/
CategoryTheory.Abelian.Ext.covariantSequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.HasExt C] →
        C →
          {S : CategoryTheory.ShortComplex C} →
            S.ShortExact → (n₀ n₁ : ℕ) → n₀ + 1 = n₁ → CategoryTheory.ComposableArrows AddCommGrpCat 5
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.homeomorph_symm_apply : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X],
  ⇑Metric.Snowflaking.homeomorph.symm = ⇑Metric.Snowflaking.toSnowflaking
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
          CategoryTheory.MonObj.one))
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.MonObj.one
-- Init.Grind.Ring.Basic
/-- Multiplication is associative.  -/
Lean.Grind.Semiring.mul_assoc : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a b c : α), a * b * c = a * (b * c)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
zsmulRec.eq_1 : ∀ {G : Type u_1} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (nsmul : ℕ → G → G) (x : G) (n : ℕ),
  zsmulRec nsmul (Int.ofNat n) x = nsmul n x
-- Batteries.Data.List.Count
List.sigmaCountToIdx_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α} {i : Fin xs.length},
  xs.sigmaCountToIdx (xs.idxToSigmaCount i) = i
-- Mathlib.Algebra.Group.ULift
ULift.addCommGroup.eq_1 : ∀ {α : Type u} [inst : AddCommGroup α], ULift.addCommGroup = Function.Injective.addCommGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The sheaf of sections guaranteed by the sheaf condition.  -/
CategoryTheory.sheafOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {J : CategoryTheory.GrothendieckTopology C} → CategoryTheory.Sheaf J A → A → CategoryTheory.Sheaf J (Type v₂)
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_of_one_lt_oneLePart : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α}, 1 < a⁺ᵐ → a⁺ᵐ = a
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of adding a point to a set with a finite-dimensional `vectorSpan` is
finite-dimensional.  -/
finiteDimensional_vectorSpan_insert_set : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P) [FiniteDimensional k ↥(vectorSpan k s)] (p : P),
  FiniteDimensional k ↥(vectorSpan k (insert p s))
-- Mathlib.Data.List.AList
/-- The predicate `a ∈ s` means that `s` has a value associated to the key `a`.  -/
AList.instMembership : {α : Type u} → {β : α → Type v} → Membership α (AList β)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapGrp_one_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.Grp C) {Z : E} (h : ((F.comp G).mapGrp.obj A).X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
        (G.map (F.map CategoryTheory.MonObj.one)))
      h
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.induction₂ : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  {C : DirectLimit F f → DirectLimit F f → Prop},
  (∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧) → ∀ (x y : DirectLimit F f), C x y
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictFDerivAt.const_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {c : ℝ}, HasStrictFDerivAt f f' x → 0 < c → HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mk_smul_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (r : R) (x : M), (Ideal.Quotient.mk (I • ⊤)) r • Submodule.Quotient.mk x = r • Submodule.Quotient.mk x
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_fst_assoc : ∀ (X Y : TopCat) {Z : TopCat} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp TopCat.prodFst h
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- We can always derive `HasFiniteLimits C` by providing limits at an
arbitrary universe.  -/
CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J),
      CategoryTheory.Limits.HasLimitsOfShape J C) →
    CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Algebra.Ring.Prod
/-- Given non-unital semirings `R`, `S`, the natural projection homomorphism from `R × S` to `R`.  -/
NonUnitalRingHom.fst : (R : Type u_1) →
  (S : Type u_3) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R × S →ₙ+* R
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.exists_frequently_lt_of_liminf_ne_top : ∀ {ι : Type u_4} {l : Filter ι} {x : ι → ℝ},
  Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤ → ∃ R, ∃ᶠ (n : ι) in l, x n < R
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.readBody.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (a : Std.Http.Protocol.H1.Reader.BodyState),
  sizeOf (Std.Http.Protocol.H1.Reader.State.readBody a) = 1 + sizeOf a
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_of_subsingleton : ∀ {V : Type u_1} {G : SimpleGraph V} [Subsingleton V], G.vertexCoverNum = 0
-- Mathlib.Order.KrullDimension
Order.krullDim_pos_iff_of_orderBot : ∀ {α : Type u_3} [inst : PartialOrder α] [OrderBot α], 0 < Order.krullDim α ↔ Nontrivial α
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map.
See `Module.Flat.iff_rTensor_preserves_injective_linearMap'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`.  -/
Module.Flat.iff_rTensor_preserves_injective_linearMap : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
      [inst_6 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.mk : {M : Type u_8} →
  {N : Type u_9} →
    {φ : M → N} →
      {X : Type u_10} →
        [inst : VAdd M X] →
          {Y : Type u_11} →
            [inst_1 : VAdd N Y] → (toFun : X → Y) → (∀ (m : M) (x : X), toFun (m +ᵥ x) = φ m +ᵥ toFun x) → X →ₑ[φ] Y
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : SMulCommClass 𝕜 𝕝 F] {c : 𝕝},
  curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  t.WF → ((Std.DTreeMap.Raw.filterMap f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), (f k (t.get k h)).isSome = true)
-- Mathlib.Topology.Algebra.Group.Basic
discreteTopology_iff_isOpen_singleton_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G],
  DiscreteTopology G ↔ IsOpen {1}
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.rfl : ∀ {M : Type u_1} [inst : Monoid M] {x : M}, Associated x x
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on connected spaces.  -/
mem_range_of_exists_le_of_exists_ge : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] {c : α} {f : X → α},
  Continuous f → (∃ a, f a ≤ c) → (∃ b, c ≤ f b) → c ∈ Set.range f
-- Batteries.Data.List.Basic
List.dropSlice.eq_2 : ∀ {α : Type u_1} (x : ℕ) (x_1 : List α), (x_1 = [] → False) → List.dropSlice 0 x x_1 = List.drop x x_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.smulZeroClass.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R],
  AddMonoidAlgebra.smulZeroClass =
    { smul := fun a a_1 => AddMonoidAlgebra.coeffEquiv.2 (a • AddMonoidAlgebra.coeffEquiv.toFun a_1), smul_zero := ⋯ }
-- Lean.Parser.Term
Lean.Parser.Term.num.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.mul_lt_floor : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a b : K},
  0 < b → b < 1 → ↑⌈b / (1 - b)⌉₊ ≤ a → b * a < ↑⌊a⌋₊
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm : ∀ {k : ℕ},
  1 ≤ k →
    SummableLocallyUniformlyOn (fun n => iteratedDerivWithin k (fun z => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet)
      UpperHalfPlane.upperHalfPlaneSet
-- Std.Http.Data.Chunk
/-- Folds over all key-value pairs in the trailer headers.
 -/
Std.Http.Trailer.fold : {α : Type u_1} → Std.Http.Trailer → α → (α → Std.Http.Header.Name → Std.Http.Header.Value → α) → α
-- Mathlib.Algebra.MvPolynomial.Basic
/-- The finite set of all `m : σ →₀ ℕ` such that `X^m` has a non-zero coefficient.  -/
MvPolynomial.support : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → Finset (σ →₀ ℕ)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The second factor of `p` in the universal coprime factorization ring of `p`.  -/
Polynomial.UniversalCoprimeFactorizationRing.factor₂ : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Polynomial.MonicDegreeEq (Polynomial.UniversalCoprimeFactorizationRing m k hn p) k
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Sums of circle integrable functions are circle integrable.  -/
CircleIntegrable.sum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} (s : Finset ι) {f : ι → ℂ → E},
  (∀ i ∈ s, CircleIntegrable (f i) c R) → CircleIntegrable (∑ i ∈ s, f i) c R
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.hom_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L)
  {Z : C} (h : I.left j ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (K₂.ι j) h) =
    CategoryTheory.CategoryStruct.comp (K₁.ι j) h
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- `adicCompletion.toCompletion` as a ring isomorphism onto the underlying completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+*
                  (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.decidableCodisjoint : {α : Type u_1} → {s t : Finset α} → [inst : Fintype α] → [inst_1 : DecidableEq α] → Decidable (Codisjoint s t)
-- Std.Http.Data.URI.Encoding
ByteArray.push.eq_1 : ∀ (x : UInt8) (bs : Array UInt8), { data := bs }.push x = { data := bs.push x }
-- Mathlib.Data.Nat.GCD.Prime
Nat.Prime.not_dvd_lcm : ∀ {p a b : ℕ}, Nat.Prime p → ¬p ∣ a → ¬p ∣ b → ¬p ∣ a.lcm b
-- Mathlib.Data.Matrix.Mul
Matrix.diagonal_const_mulVec : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : α)
  (v : m → α), (Matrix.diagonal fun x_1 => x).mulVec v = x • v
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.quasispectrum_abs : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A]
  [inst_2 : TopologicalSpace A] [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : SMulCommClass 𝕜 A A]
  [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [inst_10 : Module ℝ A] [inst_11 : SMulCommClass ℝ A A]
  [inst_12 : IsScalarTower ℝ A A] [inst_13 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (p a) CFC.quasispectrum_abs._auto_1 → quasispectrum 𝕜 (CFC.abs a) = (fun z => ↑‖z‖) '' quasispectrum 𝕜 a
-- Mathlib.Data.WSeq.Defs
/-- Get the list corresponding to a finite weak sequence.  -/
Stream'.WSeq.get : {α : Type u} → (s : Stream'.WSeq α) → [s.IsFinite] → List α
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.contMDiffCovariantDerivativeOn_univ_iff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] {cov : CovariantDerivative I F V} {k : WithTop ℕ∞},
  ContMDiffCovariantDerivativeOn F k (↑cov) Set.univ ↔ cov.ContMDiffCovariantDerivative k
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [inst_2 : NormedSpace ℝ E]
  ⦃f : β → α → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) →
    MeasureTheory.StronglyMeasurable fun y => ∫ (x : β), f x y ∂κ y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerRight_id : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ'),
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (CategoryTheory.Limits.CatCospanTransform.id F' G') =
    CategoryTheory.CategoryStruct.comp ψ.rightUnitor.hom (CategoryTheory.CategoryStruct.comp η ψ'.rightUnitor.inv)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_inter_eq_inter_closure : ∀ {α : Type u_2} {M : Matroid α} {I J : Set α}, M.Indep (I ∪ J) → M.closure (I ∩ J) = M.closure I ∩ M.closure J
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_xor : ∀ (a b : UInt32), (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
-- Mathlib.CategoryTheory.GlueData
/-- The pullback cone spanned by `V i j ⟶ U i` and `V i j ⟶ U j`.
This will often be a pullback diagram.  -/
CategoryTheory.GlueData.vPullbackCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] →
        (i j : D.J) → CategoryTheory.Limits.PullbackCone (D.ι i) (D.ι j)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k a : α} {v : β}, (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.Data.Matrix.Mul
Matrix.add_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : Add α] [RightDistribClass α] (w₁ w₂ : m → α)
  (v : n → α), Matrix.vecMulVec (w₁ + w₂) v = Matrix.vecMulVec w₁ v + Matrix.vecMulVec w₂ v
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.continuousWithinAt : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : Set P} {x : P},
  ContinuousWithinAt (⇑e) s x
-- Mathlib.Geometry.Manifold.Instances.Real
instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc : ChartedSpace (EuclideanHalfSpace 1) ↑(Set.Icc 0 1)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
CovariantDerivative.torsion_antisymm : ∀ {𝕜 : 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] {x : M} [inst_6 : CompleteSpace 𝕜]
  [inst_7 : CompleteSpace E] [inst_8 : FiniteDimensional 𝕜 E] [inst_9 : IsManifold I 2 M]
  (cov : CovariantDerivative I E (TangentSpace I)) (X₀ Y₀ : TangentSpace I x),
  ((cov.torsion x) X₀) Y₀ = -((cov.torsion x) Y₀) X₀
-- Aesop.Util.OrderedHashSet
Aesop.instInhabitedOrderedHashSet.default : {α : Type u_1} → {inst : BEq α} → {inst_1 : Hashable α} → Aesop.OrderedHashSet α
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.ControlStack.stateT.getσ : Lean.Elab.Do.MonadInfo → Array Lean.Elab.Do.MutVar → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Data.Matrix.Basic
Matrix.sum_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] (s : Finset ι) (x : ι → n → α) (y : Matrix n m α),
  Matrix.vecMul (∑ i ∈ s, x i) y = ∑ i ∈ s, Matrix.vecMul (x i) y
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z') {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f) h)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.comp : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ} {g : α → α},
  Function.Commute f g → Function.IsPeriodicPt f n x → Function.IsPeriodicPt g n x → Function.IsPeriodicPt (f ∘ g) n x