mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coeFn_injective : ∀ {𝕜 : 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₂], Function.Injective fun f => ⇑f
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabTypeOf : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
instInhabitedCliffordAlgebra : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Inhabited (CliffordAlgebra Q)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDeleteFile.fromJson : Lean.Json → Except String Lean.Lsp.DeleteFile
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.coconePtToShrinkYoneda_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  (c : CategoryTheory.Limits.Cone F)
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc' : CategoryTheory.Limits.IsColimit c') {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (x : P.obj c.pt)
  {Z : CategoryTheory.Functor Cᵒᵖ (Type w)} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.coconePtToShrinkYoneda c hc')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaEquiv.symm x) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv hc').symm
        (CategoryTheory.Limits.Types.sectionOfCone (P.mapCone c) x))
      h
-- Std.Data.TreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.Raw.getKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : Small.{u, max u v} ↑F.sections] (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Types.Small.limitConeIsLimit F).lift s =
    TypeCat.ofHom fun v => (equivShrink ↑F.sections) ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform from `L1` functions to bounded continuous functions as a continuous linear
map.  -/
Real.Lp.fourierTransformCLM : (V : Type u_1) →
  (E : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℂ E] →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [inst_4 : MeasurableSpace V] →
              [inst_5 : BorelSpace V] →
                [inst_6 : FiniteDimensional ℝ V] →
                  ↥(MeasureTheory.Lp E 1 MeasureTheory.volume) →L[ℂ] BoundedContinuousFunction V E
-- Mathlib.Order.Hom.CompleteLattice
/-- `id` as a `FrameHom`.  -/
FrameHom.id : (α : Type u_2) → [inst : CompleteLattice α] → FrameHom α α
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
lt_iff_exists_pos_add : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftStrictMono α]
  [AddLeftReflectLT α], a < b ↔ ∃ c, 0 < c ∧ a + c = b
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is differentiable, and has two derivatives at `x`, then the second
derivative is symmetric.  -/
second_derivative_symmetric : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  [IsRCLikeNormedField 𝕜] {f' : E → E →L[𝕜] F} {f'' : E →L[𝕜] E →L[𝕜] F} {x : E},
  (∀ (y : E), HasFDerivAt f (f' y) y) → HasFDerivAt f' f'' x → ∀ (v w : E), (f'' v) w = (f'' w) v
-- Batteries.Data.List.Basic
/-- `takeList as ns` extracts successive sublists from `as`. For `ns = n₁ ... nₘ`,
it first takes the `n₁` initial elements from `as`, then the next `n₂` ones,
etc. It returns the sublists of `as` -- one for each `nᵢ` -- and the remaining
elements of `as`. If `as` does not have at least as many elements as the sum of
the `nᵢ`, the corresponding sublists will have less than `nᵢ` elements.
```
takeList ['a', 'b', 'c', 'd', 'e'] [2, 1, 1] = ([['a', 'b'], ['c'], ['d']], ['e'])
takeList ['a', 'b'] [3, 1] = ([['a', 'b'], []], [])
```
 -/
List.takeList : {α : Type u_1} → List α → List ℕ → List (List α) × List α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Iso.isZero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y),
  CategoryTheory.Limits.IsZero X ↔ CategoryTheory.Limits.IsZero Y
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂).inv.right =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right W).inv
-- Mathlib.Algebra.Ring.BooleanRing
instBooleanRingBool : BooleanRing Bool
-- Mathlib.RingTheory.Valuation.Minpoly
/-- For `x ∈ K` the valuation of the zeroth coefficient of the minimal polynomial
of `algebraMap K L x` over `K` is equal to the valuation of `x`.  -/
Valuation.coeff_zero_minpoly : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L] (x : K), v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.exists_radius_le : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a : ENNReal} (t : T) (V : Finset T),
  1 < a → ∀ (c : ENNReal), ∃ r, 1 ≤ r ∧ ↑{x ∈ V | edist t x ≤ ↑r * c}.card ≤ a ^ r
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.toCommSemigroup.eq_1 : ∀ {M : Type u_5} [inst : CommSemigroup M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : MulMemClass A M] (S : A),
  MulMemClass.toCommSemigroup S = { toSemigroup := MulMemClass.toSemigroup S, mul_comm := ⋯ }
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.of : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)}, ∀ x ∈ S, Projectivization.Subspace.spanCarrier S x
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.jointly_surjective : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (F : CategoryTheory.Functor J FintypeCat) (t : CategoryTheory.Limits.Cocone F) (h : CategoryTheory.Limits.IsColimit t)
  (x : t.pt.obj), ∃ j y, (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) y = x
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.elabs' : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Elab.Command.InductiveElabStep2
-- Lean.Util.MonadBacktrack
Lean.withoutModifyingState : {m : Type → Type} → {s α : Type} → [Monad m] → [MonadFinally m] → [Lean.MonadBacktrack s m] → m α → m α
-- Init.Data.List.Impl
List.zipIdx.eq_2 : ∀ {α : Type u} (x : ℕ) (a : α) (l : List α), (a :: l).zipIdx x = (a, x) :: l.zipIdx (x + 1)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.monoid : {α : Type u} → [h : AddMonoid α] → Monoid (Multiplicative α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C}
  {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F), E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.CochainComplex.augment.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (x x_1 : ℕ) (h_1 : Unit → motive 0 1) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_2 : ℕ) → motive x x_2),
  (x = 0 → x_1 = 1 → False) →
    (∀ (i j : ℕ), x = i.succ → x_1 = j.succ → False) →
      (match x, x_1 with
        | 0, 1 => h_1 ()
        | i.succ, j.succ => h_2 i j
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Init.Data.BitVec.Lemmas
BitVec.not_cast : ∀ {w w' : ℕ} {x : BitVec w} (h : w = w'), ~~~BitVec.cast h x = BitVec.cast h (~~~x)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.set_EStateM : ∀ {σ ε : Type} (s : σ) (post : PUnit.{1} → σ → Prop) (epost : ε → σ → Prop),
  ⦃ fun x => post PUnit.unit s ⦄ set s ⦃ post; epost ⦄
-- Init.Data.Vector.Find
Vector.findFinIdx?_congr : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs ys : Vector α n},
  xs = ys → Vector.findFinIdx? p xs = Vector.findFinIdx? p ys
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).hom =
    CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} [inst_1 : SizeOf C] [inst_2 : SizeOf I] (toOneCochain : CategoryTheory.PresheafOfGroups.OneCochain G U)
  (ev_trans :
    autoParam
      (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
        toOneCochain.ev i j a b * toOneCochain.ev j k b c = toOneCochain.ev i k a c)
      CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam),
  sizeOf { toOneCochain := toOneCochain, ev_trans := ev_trans } = 1 + sizeOf toOneCochain
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_eq_get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {a : α} {h' : a ∈ t}, t.get a h' = (t.get? a).get ⋯
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackCongr.eq_1 : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] {g : X ⟶ Y} (h : f = g),
  CategoryTheory.MorphismProperty.Over.pullbackCongr h =
    CategoryTheory.NatIso.ofComponents
      (fun X_1 => CategoryTheory.MorphismProperty.Over.isoMk (CategoryTheory.Limits.pullback.congrHom ⋯ h) ⋯) ⋯
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) [inst_5 : Module.FinitePresentation R M]
  (f : M →ₗ[R] N),
  (Module.FinitePresentation.linearEquivMapExtendScalars S).symm
      ((IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
          (Localization S))
        f) =
    (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f
-- Mathlib.Order.Disjoint
Prod.isCompl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {x y : α × β}, IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_add : ∀ {i : Lean.Grind.IntInterval}, i.isFinite = true → ∀ (x y : ℤ), i.wrap (x + y) = i.wrap (i.wrap x + i.wrap y)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] [inst_3 : DecidableEq G] (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (A : Rep.{u, u, u} k G) (i : ℕ) (hi : Odd i)
  (x y : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) x =
      (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ LinearMap.range A.ρ.norm
-- Mathlib.RingTheory.Polynomial.Quotient
/-- Given any ring `R` and an ideal `I` of `R[X]`, we get a map `R → R[x] → R[x]/I`.
If we let `R` be the image of `R` in `R[x]/I` then we also have a map `R[x] → R'[x]`.
In particular we can map `I` across this map, to get `I'` and a new map `R' → R'[x] → R'[x]/I`.
This theorem shows `I'` will not contain any non-zero constant polynomials.  -/
Ideal.eq_zero_of_polynomial_mem_map_range : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal (Polynomial R)) (x : ↥((Ideal.Quotient.mk I).comp Polynomial.C).range),
  Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom ((Ideal.Quotient.mk I).comp Polynomial.C).rangeRestrict) I → x = 0
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B),
  w.GuitartExact ↔
    ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition_go_step : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] {k : α → Ordering} {init : δ} (l₁ l₂ : List ((a : α) × β a))
  (l l' : Std.DTreeMap.Internal.Impl α β)
  (h : Std.DTreeMap.Internal.Impl.contains' k l' = true → Std.DTreeMap.Internal.Impl.contains' k l = true)
  (f : δ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → δ),
  Std.DTreeMap.Internal.Impl.applyPartition.go k l'
      (fun l'_1 c x r' => f init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq l'_1 c r')) l₁ l h l₂ =
    Std.DTreeMap.Internal.Impl.applyPartition.go k l'
      (fun l'_1 c x r' => f init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq (l₁ ++ l'_1) c (r' ++ l₂))) [] l h []
-- Mathlib.Probability.Process.HittingTime
/-- `hittingAfter` is monotone with respect to the minimal time.  -/
MeasureTheory.hittingAfter_mono : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (s : Set β),
  Monotone (MeasureTheory.hittingAfter u s)
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instInhabited : {α : Type u} → {cmp : α → α → Ordering} → Inhabited (Std.TreeSet.Raw α cmp)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {n : Type x → Type x'} →
          (((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
              (γ : Type x) →
                (plausible_forInStep : β → γ → ForInStep γ → Prop) →
                  (it : Std.IterM m β) →
                    γ →
                      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) →
                        n γ) →
            Std.IteratorLoop α m n
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.ne_bot_iff : ∀ {α : Type u_1} {f : Filter α} (F : f.Realizer), f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty
-- Mathlib.CategoryTheory.MorphismProperty.RetractArgument
CategoryTheory.MorphismProperty.rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [W₁.HasFactorization W₂] [W₂.IsStableUnderRetracts], W₂ ≤ W₁.rlp → W₁.rlp = W₂
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The partial Dirichlet series $\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}$.  -/
NumberField.Set.primeIdealZetaSum : {K : Type u_1} →
  [inst : Field K] → [NumberField K] → Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → ℝ → ℝ
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearIsometry.extend.eq_1 : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {V : Type u_7} [inst_1 : NormedAddCommGroup V] [inst_2 : InnerProductSpace 𝕜 V]
  [inst_3 : FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V),
  L.extend =
    {
      toLinearMap :=
        L.toLinearMap ∘ₗ ↑S.orthogonalProjectionOnto +
          (L.rangeᗮ.subtypeₗᵢ.comp
                (have dim_LS_perp := ⋯;
                  (stdOrthonormalBasis 𝕜 ↥Sᗮ).repr.trans
                    ((stdOrthonormalBasis 𝕜 ↥L.rangeᗮ).reindex
                          (finCongr dim_LS_perp)).repr.symm).toLinearIsometry).toLinearMap ∘ₗ
            ↑Sᗮ.orthogonalProjectionOnto,
      norm_map' := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t ≠ ∅ → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.splitMany.eq_1 : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)),
  BoxIntegral.Prepartition.splitMany I s = s.inf fun p => BoxIntegral.Prepartition.split I p.1 p.2
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- Given a sequence of continuous linear maps which converges pointwise and for which the
domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map
is a *continuous* linear map as well.

This actually works for any *countably generated* filter instead of `atTop : Filter ℕ`,
but the proof ultimately goes back to sequences.  -/
continuousLinearMapOfTendsto : {α : Type u_1} →
  {𝕜₁ : Type u_4} →
    {𝕜₂ : Type u_5} →
      {E : Type u_6} →
        {F : Type u_7} →
          [inst : NontriviallyNormedField 𝕜₁] →
            [inst_1 : NontriviallyNormedField 𝕜₂] →
              {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                [RingHomIsometric σ₁₂] →
                  [inst_3 : AddCommGroup E] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : Module 𝕜₁ E] →
                        [inst_6 : Module 𝕜₂ F] →
                          [inst_7 : UniformSpace E] →
                            [inst_8 : UniformSpace F] →
                              [IsUniformAddGroup E] →
                                [IsUniformAddGroup F] →
                                  [ContinuousSMul 𝕜₁ E] →
                                    [BarrelledSpace 𝕜₁ E] →
                                      [PolynormableSpace 𝕜₂ F] →
                                        [ContinuousSMul 𝕜₂ F] →
                                          [T2Space F] →
                                            {l : Filter α} →
                                              [l.IsCountablyGenerated] →
                                                [l.NeBot] →
                                                  (g : α → E →SL[σ₁₂] F) →
                                                    {f : E → F} →
                                                      Filter.Tendsto (fun n x => (g n) x) l (nhds f) → E →SL[σ₁₂] F
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddCon.instInhabited = { default := addConGen emptyRelation }
-- Lean.Message
Lean.MessageData.toString : Lean.MessageData → BaseIO String
-- Lean.Environment
Lean.AsyncConstantInfo.mk.sizeOf_spec : ∀ (name : Lean.Name) (kind : Lean.ConstantKind) (sig : Task Lean.ConstantVal) (constInfo : Task Lean.ConstantInfo),
  sizeOf { name := name, kind := kind, sig := sig, constInfo := constInfo } =
    1 + sizeOf name + sizeOf kind + sizeOf sig + sizeOf constInfo
-- Lean.Meta.ArgsPacker
/-- Unpacks a unary packed argument created with `Unary.pack`.

Throws an error if the expression is not of that form.
 -/
Lean.Meta.ArgsPacker.Unary.unpack : ℕ → Lean.Expr → Option (Array Lean.Expr)
-- Lean.Declaration
Lean.instInhabitedRecursorRule.default : Lean.RecursorRule
-- Mathlib.Data.ZMod.Basic
ZMod.cast_sub : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (a b : ZMod n), (a - b).cast = a.cast - b.cast
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, k ∈ t.alter k f ↔ (f (t.get? k)).isSome = true
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExists.add_distrib : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f f' : M → E} {g : M → E'} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExists L f g →
    DiscreteConvolution.ConvolutionExists L f' g →
      DiscreteConvolution.convolution L (f + f') g =
        DiscreteConvolution.convolution L f g + DiscreteConvolution.convolution L f' g
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddMonoid.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.instAddMonoid =
    { toAdd := BoundedContinuousFunction.instAdd, add_assoc := ⋯, toZero := BoundedContinuousFunction.instZero,
      zero_add := ⋯, add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Given a Fredholm decomposition `dec` of the space `E`, `dec.proj` is the (continuous linear)
projection onto the "essential part" `dec.X₁` along the "inessential part" `dec.X₀`.
This is a Fredholm operator.  -/
FredholmDecomposition.proj : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace E] → (dec : FredholmDecomposition 𝕜 E) → E →L[𝕜] ↥dec.X₁
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t t_1 : Std.DTreeMap.Internal.Impl α β)
  (e_t : t = t_1) (k : α) (hlk : k ∈ t), t.get k hlk = t_1.get k ⋯
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular],
  μ ≠ 0 → ∀ {s : Set G}, IsOpen s → (μ s ≠ 0 ↔ s.Nonempty)