mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.NumberField
NumberField.prod_nonarchAbsVal_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : CommMonoid M]
  (f : AbsoluteValue K ℝ → M),
  ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), f ↑v = ∏ᶠ (v : NumberField.FinitePlace K), f ↑v
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- The rank of a finite flat locally finitely presented morphism is locally constant.  -/
AlgebraicGeometry.Scheme.Hom.isLocallyConstant_finrank : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f], IsLocallyConstant (AlgebraicGeometry.Scheme.Hom.finrank f)
-- Init.Data.Array.Lemmas
Array.mem_of_back? : ∀ {α : Type u_1} {xs : Array α} {a : α}, xs.back? = some a → a ∈ xs
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable.  -/
nullMeasurableSet_regionBetween : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion.0.IsCovariantDerivativeOn.torsionAux_tensorial₁ : ∀ {𝕜 : 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] [inst_6 : IsManifold I 2 M] [CompleteSpace E]
  {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x},
  IsCovariantDerivativeOn E cov →
    ∀ (x : M) (Y : (x : M) → TangentSpace I x),
      TensorialAt I E (fun x_1 => IsCovariantDerivativeOn.torsionAux✝ cov x_1 Y x) x
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Client.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.TCP.Socket), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Lean.Environment
Lean.debug.skipKernelTC : Lean.Option Bool
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.identString : Lean.Syntax → String
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.emultiplicity_eq_multiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → emultiplicity a b = ↑(multiplicity a b)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  (m : Std.DHashMap.Raw α fun x => β) (l : ρ),
  Std.DHashMap.Raw.Const.insertMany m l =
    if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m, h⟩ l) else m
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Finset.uniformContinuous_prod : ∀ {α : Type u_3} {β : Type u_4} {ι : Type u_5} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α]
  [inst_3 : UniformSpace β] {f : ι → β → α} (s : Finset ι),
  (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x => ∏ i ∈ s, f i x
-- Mathlib.Order.Filter.Bases.Basic
/-- Constructs a filter basis from an indexed family of sets satisfying `IsBasis`.  -/
Filter.IsBasis.filterBasis : {α : Type u_1} → {ι : Sort u_4} → {p : ι → Prop} → {s : ι → Set α} → Filter.IsBasis p s → FilterBasis α
-- Lean.Meta.Tactic.Grind.Arith.Util
_private.Lean.Meta.Tactic.Grind.Arith.Util.0.Lean.Meta.Grind.Arith.CollectDecVars.alreadyVisited.unsafe_1 : {α : Type u_1} → α → UInt64
-- Mathlib.Data.Nat.Find
_private.Mathlib.Data.Nat.Find.0.Nat.findGreatest.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.sup_toSubalgebra_of_left : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1], (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
-- Mathlib.Analysis.Complex.Hadamard
/-- The transformation on ℂ that is used for `scale` maps the strip ``re ⁻¹' (l, u)``
to the strip ``re ⁻¹' (0, 1)``.  -/
Complex.HadamardThreeLines.scale_id_mem_verticalStrip_of_mem_verticalStrip : ∀ {l u : ℝ},
  l < u →
    ∀ {z : ℂ},
      z ∈ Complex.HadamardThreeLines.verticalStrip 0 1 →
        ↑l + z * (↑u - ↑l) ∈ Complex.HadamardThreeLines.verticalStrip l u
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.mk.sizeOf_spec : ∀ {ι : Type u_1} [inst : SizeOf ι] (faces : Set (Finset ι)) (isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty),
  sizeOf { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces } = 1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.Epi φ.τ₁ →
    CategoryTheory.IsIso φ.τ₂ →
      CategoryTheory.Mono φ.τ₃ → CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Order.Category.LinOrd
OrderHomClass.toLatticeHom.congr_simp : ∀ {F : Type u_1} (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : LinearOrder α] [inst_2 : Lattice β]
  [inst_3 : OrderHomClass F α β] (f f_1 : F),
  f = f_1 → OrderHomClass.toLatticeHom α β f = OrderHomClass.toLatticeHom α β f_1
-- Mathlib.Lean.Json
Lean.instFromJsonPUnit_mathlib : Lean.FromJson PUnit.{u_1 + 1}
-- Mathlib.Analysis.CStarAlgebra.Projection
isStarProjection_iff_quasispectrum_subset_and_isStarNormal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  {p : A}, IsStarProjection p ↔ quasispectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.image.eqToIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f'] (h : f = f'),
  CategoryTheory.Limits.image.eqToIso h = CategoryTheory.Limits.image.eqToIso h
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_emod_of_nonneg : ∀ (a : ℤ) {b : ℤ}, 0 ≤ b → a.fmod b = a % b
-- Std.Data.HashMap.Basic
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.HashMap.toList : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → List (α × β)
-- Mathlib.Order.InitialSeg
PrincipalSeg.subrelIso_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a : α),
  f.subrelIso.symm a = (Equiv.subtypeEquivProp ⋯) ⟨f.toRelEmbedding a, ⋯⟩
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.hom_hom_comp : ∀ (R : Type u) [inst : Ring R] {A B C : FGModuleCat R} (f : A ⟶ B) (g : B ⟶ C),
  ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = ModuleCat.Hom.hom g.hom ∘ₗ ModuleCat.Hom.hom f.hom
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.eq_of_mem_ordConnectedSection_of_uIcc_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : α},
  x ∈ s.ordConnectedSection → y ∈ s.ordConnectedSection → Set.uIcc x y ⊆ s → x = y
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_inj : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c.toSetoid = d.toSetoid ↔ c = d
-- Init.Data.String.Bootstrap
String.Pos.Raw.Internal.min : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.ModelTheory.Fraisse
/-- Any countable infinite structure in the empty language is a Fraïssé limit of the class of finite
structures.  -/
FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite : ∀ (M : Type u_1) [inst : Countable M] [Infinite M] [inst_2 : FirstOrder.Language.empty.Structure M],
  FirstOrder.Language.IsFraisseLimit {S | Finite ↑S} M
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The nilradical of a scheme.  -/
AlgebraicGeometry.Scheme.nilradical : (X : AlgebraicGeometry.Scheme) → X.IdealSheafData
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      compare k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l →
              Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k' = some v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).fst = b.π CategoryTheory.Limits.WalkingPair.left
-- Mathlib.Data.Set.Lattice
Set.union_distrib_iInter₂_right : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_of_measurable_exp : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ}, (Measurable fun x => Real.exp (f x)) → Measurable f
-- Mathlib.Topology.Filter
Filter.nhds_iInf : ∀ {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α), nhds (⨅ i, f i) = ⨅ i, nhds (f i)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.lift_base : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K)
  (hf : ∀ (i : ι), (f i).comp (φ i) = k) (g : H), (Monoid.PushoutI.lift f k hf) ((Monoid.PushoutI.base φ) g) = k g
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCoinitialFor s t → s.Nonempty → t.Nonempty
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdLocallyUniformly_of_forall_compact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [LocallyCompactSpace β],
  (∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K) → HasProdLocallyUniformly f g
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.const_smul` -/
DifferentiableAt.fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableAt 𝕜 f x → ∀ (c : R), DifferentiableAt 𝕜 (fun i => c • f i) x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.congr`  -/
TensorProduct.AlgebraTensorModule.congr : {R : Type uR} →
  {A : Type uA} →
    {M : Type uM} →
      {N : Type uN} →
        {P : Type uP} →
          {Q : Type uQ} →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Algebra R A] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module A M] →
                        [inst_6 : IsScalarTower R A M] →
                          [inst_7 : AddCommMonoid N] →
                            [inst_8 : Module R N] →
                              [inst_9 : AddCommMonoid P] →
                                [inst_10 : Module R P] →
                                  [inst_11 : Module A P] →
                                    [inst_12 : IsScalarTower R A P] →
                                      [inst_13 : AddCommMonoid Q] →
                                        [inst_14 : Module R Q] →
                                          (M ≃ₗ[A] P) → (N ≃ₗ[R] Q) → TensorProduct R M N ≃ₗ[A] TensorProduct R P Q
-- Mathlib.Data.Matrix.Block
/-- Let `b` map rows and columns of a square matrix `M` to blocks. Then
`toSquareBlock M b k` is the block `k` matrix.  -/
Matrix.toSquareBlock : {m : Type u_2} →
  {α : Type u_12} → {β : Type u_13} → Matrix m m α → (b : m → β) → (k : β) → Matrix { a // b a = k } { a // b a = k } α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag.ofNat : ℕ → Lean.Lsp.CompletionItemTag
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.ext_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s s' : S.Splitting), s.r = s'.r → s = s'
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
hom_chart : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {HB : Type u_9}
  [inst_13 : TopologicalSpace HB] [inst_14 : TopologicalSpace B] [inst_15 : ChartedSpace HB B]
  [inst_16 : FiberBundle F₁ E₁] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : FiberBundle F₂ E₂]
  [inst_19 : VectorBundle 𝕜 F₂ E₂] [inst_20 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_21 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (y₀ y : Bundle.TotalSpace (F₁ →L[𝕜] F₂) fun b => E₁ b →L[𝕜] E₂ b),
  ↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y =
    (↑(chartAt HB y₀.proj) y.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
-- Init.Core
Eq.substr : ∀ {α : Sort u} {p : α → Prop} {a b : α}, b = a → p a → p b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_id : ∀ {k H : Type u} [inst : CommRing k] [inst_1 : Group H] {A : Rep.{max u u_1, u, u} k H},
  groupCohomology.mapShortComplexH1 (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupCohomology.shortComplexH1 A)
-- Mathlib.Algebra.Homology.QuasiIso
HomotopyEquiv.quasiIsoAt_inv : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) (n : ι) [inst_2 : K.HasHomology n]
  [inst_3 : L.HasHomology n], QuasiIsoAt e.inv n
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
/-- The isomorphism between the zeroth continuous cohomology group and
the invariants of a representation.  -/
ContinuousCohomology.zeroIso : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              (A : TopRep k G) → continuousCohomology 0 A ≅ TopModuleCat.of k ↥A.ρ.invariants
-- Mathlib.Algebra.Lie.IdealOperations
/-- This is a very useful result; it allows us to use the fact that inclusion distributes over the
Lie bracket operation on ideals, subject to the conditions shown.  -/
LieIdeal.comap_bracket_incl_of_le : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  {I₁ I₂ : LieIdeal R L},
  I₁ ≤ I → I₂ ≤ I → ⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I₁, I₂⁆
-- Init.Omega.IntList
Lean.Omega.IntList.dot_distrib_left : ∀ (xs ys zs : Lean.Omega.IntList), (xs + ys).dot zs = xs.dot zs + ys.dot zs
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_ofObj : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {ι : Type u'} (X : ι → C) (F : CategoryTheory.Functor C D),
  (CategoryTheory.ObjectProperty.ofObj X).strictMap F = CategoryTheory.ObjectProperty.ofObj (F.obj ∘ X)
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.Context.env : Lean.Meta.Sym.AlphaShareCommon.Context → Lean.Environment
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- First version of the limit formula, with a limit over real numbers tending to 1 from above.  -/
ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right : Filter.Tendsto (fun s => riemannZeta ↑s - 1 / (↑s - 1)) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑Real.eulerMascheroniConstant)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- An exact pairing is a pair of objects `X Y : C` which admit
a coevaluation and evaluation morphism which fulfill two triangle equalities.  -/
CategoryTheory.ExactPairing : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → C → Type v₁
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr : Lean.Expr → Lean.Meta.Simp.Arith.Nat.ToLinear.M Lean.Meta.Simp.Arith.Nat.LinearExpr
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.SurjectiveOnStalks f] (x : ↥X),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.setIntegral_piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {η : ProbabilityTheory.Kernel α β} {s : Set α}
  {hs : MeasurableSet s} [inst_2 : DecidablePred fun x => x ∈ s] (a : α) (g : β → E) (t : Set β),
  ∫ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a =
    if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a
-- Mathlib.Topology.Algebra.Order.Field
IsStrictOrderedRing.toIsTopologicalDivisionRing : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], IsTopologicalDivisionRing 𝕜
-- Init.Data.List.Monadic
List.allM_nil : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool}, List.allM p [] = pure true
-- Mathlib.Algebra.Group.Units.Defs
/-- `inv` is the right inverse of `val` in the base `Monoid`.  -/
Units.val_inv : ∀ {α : Type u} [inst : Monoid α] (self : αˣ), ↑self * self.inv = 1
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_invOf : ∀ {α : Type u} [inst : Monoid α] (a : α) [inst_1 : Invertible a] [inst_2 : Invertible ⅟a], ⅟⅟a = a
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_inf_le : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {p q : Submodule R M},
  Submodule.map f (p ⊓ q) ≤ Submodule.map f p ⊓ Submodule.map f q
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ),
      HasDerivAt (iteratedDeriv n (ProbabilityTheory.mgf X μ))
        (∫ (x : Ω), (fun ω => X ω ^ (n + 1) * Real.exp (t * X ω)) x ∂μ) t
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `PredOrder.hasBasis_nhds_Ico`. -/
PredOrder.hasBasis_nhds_Ioc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [PredOrder α] {a : α}
  [NoMaxOrder α], (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioi_zero : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∏ i > 0, f i = ∏ j, f j.succ
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.Normal.addConj_mem' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → ∀ n ∈ H, ∀ (g : G), -g + n + g ∈ H
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isoMk_hom : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N)
  (hφ :
    ∀ (r : R),
      CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom),
  (ModuleCat.isoMk φ hφ).hom = ModuleCat.homMk φ.hom hφ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∈ m → (m.insertManyIfNewUnit l).getKey! k = m.getKey! k
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr'Aux_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
  (m : M) (x_fx : CliffordAlgebra Q × N),
  ((CliffordAlgebra.foldr'Aux Q f) m) x_fx = ((CliffordAlgebra.ι Q) m * x_fx.1, (f m) x_fx)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- A pair of `ℝ`-linearly independent complex numbers.
They span the period lattice in `lattice`,
and are the periods of the elliptic functions we shall construct.  -/
PeriodPair : Type
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.mem_of_superset : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} {i : ι},
  l.HasBasis p s → p i → s i ⊆ t → t ∈ l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.mk : String → Lean.Lsp.Range → Lean.Lsp.Range → Lean.Lsp.InsertReplaceEdit
-- Mathlib.Data.Sigma.Lex
Sigma.instAntisymmLexOfAsymm : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [Std.Asymm r]
  [∀ (i : ι), Std.Antisymm (s i)], Std.Antisymm (Sigma.Lex r s)
-- Lean.Meta.Tactic.Grind.Action
/-- Repeats `x` up to `n` times while it remains applicable.
 -/
Lean.Meta.Grind.Action.loop : ℕ → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Init.Data.Int.Order
Int.neg_max_neg : ∀ (a b : ℤ), max (-a) (-b) = -min a b
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperSheaf_obj_map : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
  (skyscraperSheaf p₀ A).obj.map i =
    if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯
    else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- The translation of a finset `s` by a vector `a`: `a +ᵥ s = {a +ᵥ x | x ∈ s}`.  -/
Finset.vaddFinset : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [VAdd α β] → VAdd α (Finset β)