mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg : Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Subfields of a ring form a complete lattice.  -/
Subfield.instCompleteLattice : {K : Type u} → [inst : DivisionRing K] → CompleteLattice (Subfield K)
-- Init.Data.UInt.Lemmas
USize.ofNat_size : USize.ofNat USize.size = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_null_of_null_right : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (S : Set α) {T : Set α},
  μ T = 0 → μ (S ∩ T) = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_6 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.udiv with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_6 ()
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instCanLiftCoeLtRealNormOfNat : CanLift ℂ Complex.UnitDisc Complex.UnitDisc.coe fun x => ‖x‖ < 1
-- Init.Data.Array.Lemmas
Array.append_eq_filterMap_iff : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array β} {zs : Array α} {f : α → Option β},
  xs ++ ys = Array.filterMap f zs ↔ ∃ as bs, zs = as ++ bs ∧ Array.filterMap f as = xs ∧ Array.filterMap f bs = ys
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
BoundedContinuousFunction.instCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : CStarAlgebra A] → CStarAlgebra (BoundedContinuousFunction α A)
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_5 : Std.Rci.LawfulRcoIntersection ℕ
-- Mathlib.CategoryTheory.Core
/-- Construct an isomorphism in `Core C` from an isomorphism in `C`.  -/
CategoryTheory.Core.isoMk : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {x y : CategoryTheory.Core C} → (x.of ≅ y.of) → (x ≅ y)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A coequalizer of `f` and `g` is a cokernel of `f - g`.  -/
CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          {c : CategoryTheory.Limits.Cofork f g} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.cokernelCoforkOfCofork c)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `- ⊗ unmop X = unmop (X ⊗ mop -)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorRightUnmopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : Cᴹᵒᵖ) →
        CategoryTheory.MonoidalCategory.tensorRight X.unmop ≅
          (CategoryTheory.mopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorLeft X).comp (CategoryTheory.unmopFunctor C))
-- Mathlib.Topology.MetricSpace.Similarity
/-- Scales pairwise distance with positive ratio. Forward of
`similar_iff_exists_pos_pairwise_dist_eq`.  -/
Similar.exists_pos_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Tactic.Simps.Basic
/-- Function elaborating `initialize_simps_projections`.  -/
Simps.elabInitializeSimpsProjections : Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cocone F} (e : K ≌ J),
  CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv e =
    { toFun := fun h => h.whiskerEquivalence e, invFun := CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence e,
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatchThe_apply_eq : ∀ {Pred : Type u_2} {EPred : Type u_3} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1} {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadExceptOf ε m] (x : m α) (h : ε → m α),
  Std.Internal.Do.wp (tryCatchThe ε x h) post epost = Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_add : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f : M → N) (x y : M),
  f (x + y) = f x + f y + QuadraticMap.polar f x y
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- For any `f : Arrow C` and `j : κ.ord.ToType`, the object
`(((iterationFunctor I κ).obj j).obj f).right` identifies to `f.right`.  -/
CategoryTheory.SmallObject.iterationFunctorObjObjRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              (f : CategoryTheory.Arrow C) →
                (j : κ.ord.ToType) → (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj f).right ≅ f.right
-- Lean.Compiler.LCNF.Basic
/-- Constructor information.

   - `name` is the Name of the Constructor in Lean.
   - `cidx` is the Constructor index (aka tag).
   - `size` is the number of arguments of type `object/tobject`.
   - `usize` is the number of arguments of type `usize`.
   - `ssize` is the number of bytes used to store scalar values.

Recall that a Constructor object contains a header, then a sequence of
pointers to other Lean objects, a sequence of `USize` (i.e., `size_t`)
scalar values, and a sequence of other scalar values.  -/
Lean.Compiler.LCNF.CtorInfo : Type
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_isMultiplicative : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) [F.Faithful] [F.Full] [P.IsMultiplicative]
  [P.RespectsIso], (CategoryTheory.MorphismProperty.relative F P).IsMultiplicative
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.logEquiv_symm : ∀ {G : Type u_5} [inst : AddGroup G], WithZero.logEquiv.symm = WithZero.expEquiv
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- The kind of match this handler is looking for.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.kind : Lean.Elab.ConfigEval.EvalConfigItemHandler → Lean.Elab.ConfigEval.EvalConfigItemHandlerKind
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_minKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {fallback : α},
  cmp ((Std.ExtDTreeMap.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : Lean.ToJson Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  {f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_hom_toFunctor_map_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  {F₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C),
  ((CategoryTheory.flippingIso.hom.toFunctor.map φ).app Y).app X = (φ.app X).app Y
-- Init.Data.Int.Lemmas
Int.ofNat_add_negSucc_of_lt : ∀ {m n : ℕ}, m < n.succ → Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)
-- Mathlib.Algebra.Quandle
Rack.self_act_act_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Shelf.act (Shelf.act x x) y = Shelf.act x y
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.exists_upperCrossingTime_eq : ∀ {Ω : Type u_1} {a b : ℝ} (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω), a < b → ∃ n, MeasureTheory.upperCrossingTime a b f N n ω = N
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_insert : ∀ {α : Type u_1} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (x : α) (t : Ordnode α),
  (Ordnode.insert x t).dual = Ordnode.insert x t.dual
-- Mathlib.Util.Notation3
Mathlib.Notation3.expandFoldr : Lean.ParserDescr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_sum : ∀ {R : Type u} (M : Type v) {ι : Type u_3} [inst : AddCommMonoid R] [inst_1 : AddCommMonoid M] (s : Finset ι)
  (f : ι → R), TrivSqZeroExt.inl (∑ i ∈ s, f i) = ∑ i ∈ s, TrivSqZeroExt.inl (f i)
-- Init.Data.Array.Count
Array.countP_filterMap : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {xs : Array α},
  Array.countP p (Array.filterMap f xs) = Array.countP (fun a => (Option.map p (f a)).getD false) xs
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.coe_toMonoidHom : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (x : R),
  χ.toMonoidHom x = χ x
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toListRev_valuesIter : ∀ {α β : Type u} {m : Std.DHashMap.Raw α fun x => β}, m.valuesIter.toListRev = (List.map Sigma.snd m.toList).reverse
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and right homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced right homology map `h₁.H ⟶ h₁.H`.  -/
CategoryTheory.ShortComplex.rightHomologyMap' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → (h₁ : S₁.RightHomologyData) → (h₂ : S₂.RightHomologyData) → h₁.H ⟶ h₂.H
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_isLongestMatchAt_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos : s.Pos},
  ¬String.Slice.Pattern.Model.IsLongestMatchAt pat startPos startPos
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.IsSkewAdjoint.eq_1 : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ : Matrix n n R),
  J.IsSkewAdjoint A₁ = J.IsAdjointPair J A₁ (-A₁)
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn.eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1}
  {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1}
  (t : Lean.PrefixTreeNode α β cmp) (F_1 : (t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t)
  (F_2 : (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_1 t → motive_2 t)
  (F_3 :
    (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_2 t → motive_3 t)
  (F_4 :
    (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
      Lean.PrefixTreeNode.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.PrefixTreeNode.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Order.RelSeries
RelSeries.smash.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (p p_1 : RelSeries r) (e_p : p = p_1) (q q_1 : RelSeries r) (e_q : q = q_1)
  (connect : p.last = q.head), p.smash q connect = p_1.smash q_1 ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Raw α (fun x => β) compare}
  [inst_2 : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (Std.DTreeMap.Raw.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.empty : Lean.NameGenerator → Lean.Meta.LazyDiscrTree.Cache
-- Mathlib.Algebra.Category.Semigrp.Basic
mulEquivIsoMagmaIso.eq_1 : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y],
  mulEquivIsoMagmaIso =
    { hom := TypeCat.ofHom fun e => e.toMagmaCatIso, inv := TypeCat.ofHom fun i => i.magmaCatIsoToMulEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Order.WithBot
WithTop.coe_lt_top : ∀ {α : Type u_1} [inst : LT α] (a : α), ↑a < ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Set.measurable_restrict : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (s : Set δ), Measurable s.domRestrict
-- Std.Do.WP.SimpLemmas
Std.Do.WP.pure : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (a : α)
  (Q : Std.Do.PostCond α ps), (Std.Do.wp (pure a)).apply Q = Q.1 a
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- This says `{(u, y) | α(u, F(u, y))} ⊆ {(u, y) | β(f(u), y)}` using subobject pullbacks  -/
CategoryTheory.Dial.Hom.le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (self : X.Hom Y),
  (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst self.F)).obj
      X.rel ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.prod.map self.f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
      Y.rel
-- Lean.Expr
_private.Lean.Expr.0.Lean.intSubFn : Lean.Expr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} {k : α} {v : β},
  Std.DTreeMap.Raw.Const.insertMany t [(k, v)] = t.insert k v
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij)
      (HomologicalComplex.homotopyCofiber.d φ i j) =
    -CategoryTheory.CategoryStruct.comp (F.d j k) (HomologicalComplex.homotopyCofiber.inlX φ k j hjk) +
      CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)
-- Init.Data.List.Nat.Range
List.pairwise_le_range : ∀ {n : ℕ}, List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.range n)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Right unitor for the vertical composition of lax natural transformations.  -/
CategoryTheory.Lax.LaxTrans.rightUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.ForwardSliceSearcher.skipPrefix?.eq_def : ∀ (pat s : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.skipPrefix? pat s =
    if String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s = true then
      some (s.pos! (pat.rawEndPos.offsetBy s.startPos.offset))
    else none
-- Mathlib.Analysis.Normed.Group.Tannery
/-- **Tannery's theorem**: topological sums commute with termwise limits, when the norms of the
summands are eventually uniformly bounded by a summable function.

(This is the special case of the Lebesgue dominated convergence theorem for the counting measure
on a discrete set. However, we prove it under somewhat weaker assumptions than the general
measure-theoretic result, e.g. `G` is not assumed to be an `ℝ`-vector space or second countable,
and the limit is along an arbitrary filter rather than `atTop ℕ`.)

See also:
* `MeasureTheory.tendsto_integral_of_dominated_convergence` (for general integrals, but
  with more assumptions on `G`)
* `continuous_tsum` (continuity of infinite sums in a parameter)
 -/
tendsto_tsum_of_dominated_convergence : ∀ {α : Type u_1} {β : Type u_2} {G : Type u_3} {𝓕 : Filter α} [inst : NormedAddCommGroup G] [CompleteSpace G]
  {f : α → β → G} {g : β → G} {bound : β → ℝ},
  Summable bound →
    (∀ (k : β), Filter.Tendsto (fun x => f x k) 𝓕 (nhds (g k))) →
      (∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k) →
        Filter.Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (nhds (∑' (k : β), g k))
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.eq_1 : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  CyclotomicRing n A K = ↥(Algebra.adjoin A {b | b ^ n = 1})
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} (X_1 : CategoryTheory.Limits.Cone K),
  (CategoryTheory.WithTerminal.coneEquiv.unitIso.inv.app X_1).hom.left = CategoryTheory.CategoryStruct.id X_1.pt.left
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSemigroupOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Semigroup β] → [ContinuousMul β] → Semigroup C(α, β)
-- Mathlib.Order.SuccPred.Basic
Order.Iio_succ_eq_insert_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α},
  ¬IsMax a → Set.Iio (Order.succ a) = insert a (Set.Iio a)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_eventually_monotone : ∀ {u v : ℕ → ENNReal}, u ≤ᶠ[Filter.atTop] v → ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup v
-- Mathlib.Analysis.Seminorm
Seminorm.ball_subset_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.ball x r ⊆ p.closedBall x r
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherAppCore : Lean.Environment → Lean.Expr → Bool
-- Mathlib.Order.Hom.Order
OrderHom.instCompleteLattice : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : CompleteLattice β] → CompleteLattice (α →o β)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Negation of a monomial.  -/
Tactic.ComputeAsymptotics.Monomial.neg : Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.Monomial
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Subsingleton.conformalAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] [Subsingleton X] (f : X → Y) (x : X), ConformalAt f x
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_one_add_ordered : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : LinearOrder ι] (s : Finset ι) (f : ι → R),
  ∏ i ∈ s, (1 + f i) = 1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C CategoryTheory.Cat} {base : C}
  {fiber : ↑(F.obj base)} {base_1 : C} {fiber_1 : ↑(F.obj base_1)},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- Version of `PowerSeries.IsWeierstrassDivisorAt` for local rings with respect to
its maximal ideal.  -/
PowerSeries.IsWeierstrassDivisor : {A : Type u_1} → [inst : CommRing A] → PowerSeries A → [IsLocalRing A] → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsSchemeTheoreticallyDominant f],
  AlgebraicGeometry.Scheme.Hom.ker f = ⊥
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClass_closedBall_right : SMulCommClass Complex.UnitDisc Complex.UnitClosedDisc Complex.UnitDisc
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.fst =
    F.map CategoryTheory.Limits.prod.fst
-- Mathlib.Geometry.Manifold.StructureGroupoid
idRestrGroupoid_mem : ∀ {H : Type u_1} [inst : TopologicalSpace H] {s : Set H} (hs : IsOpen s),
  OpenPartialHomeomorph.ofSet s hs ∈ idRestrGroupoid
-- Mathlib.Topology.Order
continuous_sup_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
  Continuous f ↔ Continuous f ∧ Continuous f
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.is_model : ∀ {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType), ↑self ⊨ T
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F.unop] → CategoryTheory.CreatesLimitsOfShape J F
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.lowerSemicontinuousOn_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → y ≤ 0 → LowerSemicontinuousOn (s.indicator fun _x => y) t
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, panicking if no such element exists.
 -/
Std.TreeSet.Raw.getLE! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.TrailingMonic.decidable : {R : Type u} → [inst : Semiring R] → {p : Polynomial R} → [DecidableEq R] → Decidable p.TrailingMonic