mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A `FamilyOfElements` associated to an explicit family of elements.
 -/
CategoryTheory.Presieve.Arrows.Compatible.familyOfElements : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {B : C} →
        {I : Type u_1} →
          {X : I → C} →
            {π : (i : I) → X i ⟶ B} →
              {x : (i : I) → P.obj (Opposite.op (X i))} →
                CategoryTheory.Presieve.Arrows.Compatible P π x →
                  CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)
-- Init.Data.SInt.Bitwise
Int32.toInt8_not : ∀ (a : Int32), (~~~a).toInt8 = ~~~a.toInt8
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₁_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.π₁.obj S = S.X₁
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The cotangent space on `P = R[X]`.
This is isomorphic to `Sⁿ` with `n` being the number of variables of `P`.
 -/
Algebra.Extension.CotangentSpace : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Type (max w v)
-- Mathlib.Order.Concept
Concept.intent_top : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, ⊤.intent = upperPolar r Set.univ
-- Mathlib.Topology.VectorBundle.Basic
/-- A fiberwise linear inverse to `e`.  -/
Bundle.Pretrivialization.symmₗ : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module R F] →
                  [inst_5 : (x : B) → AddCommMonoid (E x)] →
                    [inst_6 : (x : B) → Module R (E x)] →
                      (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) →
                        [Bundle.Pretrivialization.IsLinear R e] → (b : B) → F →ₗ[R] E b
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_filterMap' : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α]
  {f : (a : α) × β a → Option ((a : α) × γ a)},
  (∀ (p : (a : α) × β a), Option.all (fun x => x.fst == p.fst) (f p) = true) →
    ∀ {l : List ((a : α) × β a)} {k : α},
      Std.Internal.List.DistinctKeys l →
        Std.Internal.List.containsKey k (List.filterMap f l) = true → Std.Internal.List.containsKey k l = true
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- `C n` is the `n`th rescaled Chebyshev polynomial of the first kind (also known as a Vieta–Lucas
polynomial), given by $C_n(2x) = 2T_n(x)$. See `Polynomial.Chebyshev.C_comp_two_mul_X`.  -/
Polynomial.Chebyshev.C : (R : Type u_1) → [inst : CommRing R] → ℤ → Polynomial R
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mul_mk'_one_eq_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f x * f.mk' 1 y = f.mk' x y
-- Init.Data.SInt.Lemmas
ISize.pow_zero : ∀ (x : ISize), x ^ 0 = 1
-- Lean.Parser.Do
Lean.Parser.doElemParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Multiseries representing a given function `f : ℝ → ℝ`.
`MultiseriesExpansion []` is just `ℝ`: multiseries representing constant functions.
Otherwise it is a pair of a `Multiseries basis_hd basis_tl` and a function `ℝ → ℝ`. We call
the former an expansion of the latter.

Note: most of the theory can be formulated in terms of `Multiseries`, but we need to explicitly
store the approximated function to be able to use the eventual zeroness oracle at the trimming step.
 -/
Tactic.ComputeAsymptotics.MultiseriesExpansion : Tactic.ComputeAsymptotics.Basis → Type
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.sheafInhabited : (X : TopCat) → Inhabited (TopCat.Sheaf (CategoryTheory.Discrete PUnit.{1}) X)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.support : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (self : ContDiffBumpBase E) (R : ℝ),
  1 < R → Function.support (self.toFun R) = Metric.ball 0 R
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittSub.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittSub p a = WittVector.wittSub p_1 a_1
-- Batteries.Recycling.RBTree.Basic
RBTree.instInhabitedRBMap : (α : Type u) → (β : Type v) → (cmp : α → α → Ordering) → Inhabited (RBTree.RBMap α β cmp)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
  I.glueDataObjMap h = I.glueDataObjMap h
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.ofNat_eq_coe : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo] (m : α),
  OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.obj_ext_of_isDiscrete : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsDiscrete C] {X Y : C} (f : X ⟶ Y),
  X = Y
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Given a collection of maps between corresponding summands of a pair of biproducts
indexed by the same type, we obtain a map between the biproducts.  -/
CategoryTheory.Limits.biproduct.map : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f g : J → C} →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            [inst_3 : CategoryTheory.Limits.HasBiproduct g] → ((b : J) → f b ⟶ g b) → (⨁ f ⟶ ⨁ g)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_subset_Icc_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a c ⊆ Set.Icc a b ∪ Set.Ioo b c
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHomClass.toOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [inst_4 : FunLike F α β] [ContinuousOrderHomClass F α β], OrderHomClass F α β
-- Batteries.Classes.Order
Batteries.compareOfLessAndEq_eq_lt : ∀ {α : Type u_1} {x y : α} [inst : LT α] [inst_1 : Decidable (x < y)] [inst_2 : DecidableEq α],
  compareOfLessAndEq x y = Ordering.lt ↔ x < y
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_iInf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} {S : ι → NonUnitalSubring R} {x : R},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).unitIso.inv.app X).hom.app X_1 =
    X.obj.map (e.unitIso.hom.app (Opposite.unop X_1)).op
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.G₂_diag : ∀ (i : Fin 2), CartanMatrix.G₂ i i = 2
-- Init.Data.List.Erase
List.Sublist.eraseP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁.Sublist l₂ → (List.eraseP p l₁).Sublist (List.eraseP p l₂)
-- Mathlib.Data.List.Sigma
List.mem_dlookup_kunion : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)},
  b ∈ List.dlookup a (l₁.kunion l₂) ↔ b ∈ List.dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ List.dlookup a l₂
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.rootsOfUnityAddChar.congr_simp : ∀ (n : ℕ) [inst : NeZero n], ZMod.rootsOfUnityAddChar n = ZMod.rootsOfUnityAddChar n
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C} {i : CategoryTheory.Arrow.leftFunc ⟶ Z}
  {p : Z ⟶ CategoryTheory.Arrow.rightFunc}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam}
  {hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)} {hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)}
  {Z_1 : CategoryTheory.Functor (CategoryTheory.Arrow C) C} {i_1 : CategoryTheory.Arrow.leftFunc ⟶ Z_1}
  {p_1 : Z_1 ⟶ CategoryTheory.Arrow.rightFunc}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 p_1 = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam}
  {hi_1 : ∀ (f : CategoryTheory.Arrow C), W₁ (i_1.app f)} {hp_1 : ∀ (f : CategoryTheory.Arrow C), W₂ (p_1.app f)},
  { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
      { Z := Z_1, i := i_1, p := p_1, fac := fac_1, hi := hi_1, hp := hp_1 } →
    Z = Z_1 ∧ i ≍ i_1 ∧ p ≍ p_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.diam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E), Metric.diam (⇑f '' s) = Metric.diam s
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.eq_1 : ∀ {𝕜 : 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'] (f : M → M') (s : Set M) (x : M)
  (f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)),
  HasMFDerivAt[s] f x f' =
    (ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
        (↑(extChartAt I x) x))
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (X : C) →
            (Y : F.op.LeftExtension (CategoryTheory.yoneda.obj X)) →
              Unique
                (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.yoneda.obj (F.obj X))
                    (CategoryTheory.yonedaMap F X) ⟶
                  Y)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) The intersections `Spec Γ(𝒪ₓ/I, U) ∩ V` useful for gluing.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjPullback : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → ↑X.affineOpens → ↑X.affineOpens → AlgebraicGeometry.Scheme
-- Std.Time.Zoned.Database.TzIf
/-- Parses a TZif file, which may be in either version 1 or version 2 format.
 -/
Std.Time.TimeZone.TZif.parse : Std.Internal.Parsec.ByteArray.Parser Std.Time.TimeZone.TZif.TZif
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G)
  (x : ↑(groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H1Iso A).inv)
      ((groupHomology.shortComplexH1 A).moduleCatToCycles.range.mkQ x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Poly.denote' ctx p = 0)
-- Mathlib.Algebra.Group.Action.Defs
/-- A scalar multiplication is left-cancellative if it is pointwise injective on the left.  -/
IsLeftCancelSMul : (G : Type u_9) → (P : Type u_10) → [SMul G P] → Prop
-- Mathlib.LinearAlgebra.Prod
/-- `M` as a submodule of `M × N` is isomorphic to `M`.  -/
Submodule.fstEquiv : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → ↥(Submodule.fst R M M₂) ≃ₗ[R] M
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.erase.injEq : ∀ (toErase toErase_1 : Lean.Meta.Origin),
  (Lean.Elab.Tactic.ElabSimpArgResult.erase toErase = Lean.Elab.Tactic.ElabSimpArgResult.erase toErase_1) =
    (toErase = toErase_1)
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget CommGrpCat)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.coe_sInf' : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set α}, BddBelow s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)
-- Mathlib.Data.Set.Monotone
/-- **Alias** of `StrictMonoOn.domRestrict`.

---

**Alias** of the reverse direction of `strictMono_domRestrict`. -/
StrictMonoOn.restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → StrictMono (s.domRestrict f)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.fstIdx.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M),
  w.fstIdx = Option.map Sigma.fst w.toList.head?
-- Mathlib.Topology.Order.Basic
/-- A version of `isOpen_Iio` that doesn't require a `LinearOrder`.  -/
isOpen_Iio' : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α), IsOpen (Set.Iio a)
-- Init.Data.Vector.Lemmas
Vector.mem_singleton : ∀ {α : Type u_1} {a b : α}, a ∈ #v[b] ↔ a = b
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat}
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- Given a sequences of objects `N : ℕ → C` in a category `C`, this is
a family of objects indexed by the elements `A : Splitting.IndexSet Δ`.
The `Δ`-simplices of a split simplicial objects shall identify to the
coproduct of objects in such a family.  -/
CategoryTheory.SimplicialObject.Splitting.summand : {C : Type u_1} → (ℕ → C) → (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ → C
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Rcc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Rcc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Order.Hom.Lattice
InfHom.const.eq_1 : ∀ (α : Type u_2) {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (b : β),
  InfHom.const α b = { toFun := fun x => b, map_inf' := ⋯ }
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instModuleCotangentOfAlgebra : {R : Type u_2} →
  {S : Type u_1} →
    [inst : CommRing R] → [inst_1 : CommSemiring S] → [Algebra S R] → (I : Ideal R) → Module S I.Cotangent
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_mem_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) (y : F),
  y ∈ B.polar s ↔ ∀ x ∈ s, ‖(B x) y‖ ≤ 1
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eval_unique : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (φ : Polynomial R →ₐ[R] A) (p : Polynomial R), φ p = Polynomial.eval₂ (algebraMap R A) (φ Polynomial.X) p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  Array.find? (fun x_2 => x_2.1 == k) (Std.DHashMap.Const.toArray m) = none ↔ m.contains k = false
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.tsum_subtype_add_tsum_subtype_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α]
  [CompleteSpace α] [T2Space α] {f : β → α},
  Summable f → ∀ (s : Set β), ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- A fiber bundle `E` over a base `B` with model fiber `F` is naturally a charted space modelled on
`B × F`.  -/
FiberBundle.chartedSpace' : {B : Type u_2} →
  {F : Type u_4} →
    {E : B → Type u_6} →
      [inst : TopologicalSpace F] →
        [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            [inst_3 : TopologicalSpace B] → [FiberBundle F E] → ChartedSpace (B × F) (Bundle.TotalSpace F E)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a₁`, `a₂` and any
real `b₁ < b₂`, we have `(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`.  -/
Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp : ∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
  Complex.IsExpCmpFilter l →
    b₁ < b₂ → ∀ (a₁ a₂ : ℂ), (fun z => z ^ a₁ * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ a₂ * Complex.exp (↑b₂ * z)