mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Termination
String.Pos.eq_prev_of_prev?_eq_some : ∀ {s : String} {p q : s.Pos} (h : p.prev? = some q), q = p.prev ⋯
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_eq_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  ⇑SemidirectProduct.rightHom = SemidirectProduct.right
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An auxiliary structure, used to define `S.index`.  -/
CategoryTheory.GrothendieckTopology.Cover.Relation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → J.Cover X → Type (max u v)
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Denest `p`, i.e. `(x)` becomes `x`, given that `p.IsNested`.  -/
DyckWord.denest : (p : DyckWord) → p.IsNested → DyckWord
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.degrees 1 = 0
-- Mathlib.Analysis.PSeries
/-- The harmonic series restricted to a residue class is not summable.  -/
Real.not_summable_indicator_one_div_natCast : ∀ {m : ℕ}, m ≠ 0 → ∀ (k : ZMod m), ¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonReferenceParams : Lean.FromJson Lean.Lsp.ReferenceParams
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of the reverse direction of `OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom`.

---

A monotone function `f : α →o β` is ωScott continuous if and only if it distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f : α →o β},
  (∀ (c : OmegaCompletePartialOrder.Chain α),
      f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)) →
    OmegaCompletePartialOrder.ωScottContinuous ⇑f
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.uliftFunctor.eq_1 : AddCommGrpCat.uliftFunctor =
  { obj := fun X => AddCommGrpCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      AddCommGrpCat.ofHom
        (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {k : α},
  Std.DHashMap.Const.insertManyIfNewUnit m [k] = m.insertIfNew k ()
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.union : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet t μ → MeasureTheory.NullMeasurableSet (s ∪ t) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `biproduct.bicone F` is a limit cone.  -/
CategoryTheory.Limits.biproduct.isLimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct F] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.biproduct.bicone F).toCone
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_zero : ∀ {M : Type u_2} [inst : AddMonoid M] {n : ℕ} (f : Fin n → M), Fin.partialSum f 0 = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- If the quasispectrum of an element restricts to a smaller scalar ring, then a non-unital
continuous functional calculus over the larger scalar ring descends to the smaller one.  -/
QuasispectrumRestricts.nonUnitalStarAlgHom : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      [inst : Semifield R] →
        [inst_1 : StarRing R] →
          [inst_2 : TopologicalSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : Field S] →
                  [inst_6 : StarRing S] →
                    [inst_7 : TopologicalSpace S] →
                      [inst_8 : IsTopologicalRing S] →
                        [inst_9 : ContinuousStar S] →
                          [inst_10 : NonUnitalRing A] →
                            [inst_11 : StarRing A] →
                              [inst_12 : Algebra R S] →
                                [inst_13 : Module R A] →
                                  [inst_14 : Module S A] →
                                    [IsScalarTower S A A] →
                                      [SMulCommClass S A A] →
                                        [IsScalarTower R S A] →
                                          [StarModule R S] →
                                            [ContinuousSMul R S] →
                                              {a : A} →
                                                (ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A) →
                                                  {f : C(S, R)} →
                                                    QuasispectrumRestricts a ⇑f →
                                                      ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] (k : ℕ),
  Disjoint ({t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k | t.1.card < k})
    ({t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k | t.1.card = k})
-- Batteries.Lean.EStateM
EStateM.Result.map_error : ∀ {ε σ α β : Type u_1} (f : α → β) (e : ε) (s : σ),
  EStateM.Result.map f (EStateM.Result.error e s) = EStateM.Result.error e s
-- Lean.Meta.Sym.Pattern
/-- Helper function for implementing `mkPatternFromDecl` and `mkEqPatternFromDecl`  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.preprocessDeclPattern : Lean.Name → optParam Bool false → Lean.MetaM (List Lean.Name × Lean.Expr)
-- Std.Time.Time.Unit.Second
/-- Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
 -/
Std.Time.Second.Ordinal.ofNat : {leap : Bool} → (data : ℕ) → (data ≤ if leap = true then 60 else 59) → Std.Time.Second.Ordinal leap
-- Mathlib.Order.Antichain
IsAntichain.to_dual : ∀ {α : Type u_1} {s : Set α} [inst : LE α], IsAntichain (fun x1 x2 => x1 ≤ x2) s → IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Data.DFinsupp.Defs
/-- If `s` is a subset of `ι` then `mk_addGroupHom s` is the canonical additive
group homomorphism from $\prod_{i\in s}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i$.  -/
DFinsupp.mkAddGroupHom : {ι : Type u} →
  {β : ι → Type v} →
    [DecidableEq ι] → [inst : (i : ι) → AddGroup (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ Π₀ (i : ι), β i
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  (hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)),
  MonoidHom.noncommPiCoprod ϕ hcomm =
    { toFun := fun f => Finset.univ.noncommProd (fun i => (ϕ i) (f i)) ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_sub_right : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, (f - g).NeBot → g.NeBot
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y), L.HasPointwiseRightKanExtensionAt F Y
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.mk.injEq : ∀ {R : Type u} [inst : Ring R] (toTopologicalSpace : TopologicalSpace R) (toIsTopologicalRing : IsTopologicalRing R)
  (toTopologicalSpace_1 : TopologicalSpace R) (toIsTopologicalRing_1 : IsTopologicalRing R),
  ({ toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 }) =
    (toTopologicalSpace = toTopologicalSpace_1)
-- Mathlib.Data.Set.Sups
Set.sups_inter_subset_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t₁ t₂ : Set α}, s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
-- Mathlib.Algebra.Order.Hom.Basic
map_eq_zero_iff_eq_zero : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupNormClass F α β] (f : F) {x : α}, f x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_eq_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| = |b| ↔ a = b ∨ a = -b
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp.congr_simp : ∀ {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)
  {X₂ X₂' : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (g' : R.obj X₂' ⟶ B.obj X₃) (γ γ_1 : X₂' ⟶ X₂) (e_γ : γ = γ_1)
  (hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g'),
  w.costructuredArrowDownwardsPrecomp g g' γ hγ = w.costructuredArrowDownwardsPrecomp g g' γ_1 ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.semiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.semiring =
    { toAddCommMonoid := AddMonoidAlgebra.instAddCommMonoid, toMul := AddMonoidAlgebra.nonUnitalSemiring.toMul,
      mul_assoc := ⋯, toOne := AddMonoidAlgebra.nonAssocSemiring.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, zero_mul := ⋯, mul_zero := ⋯, left_distrib := ⋯, right_distrib := ⋯,
      toNatCast := AddMonoidAlgebra.nonAssocSemiring.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯ }
-- Init.Data.UInt.Bitwise
UInt32.and_not_self : ∀ {a : UInt32}, a &&& ~~~a = 0
-- Mathlib.Algebra.Order.Hom.Ring
/-- `OrderRingHom α β`, denoted `α →+*o β`,
is the type of monotone semiring homomorphisms from `α` to `β`.

When possible, instead of parametrizing results over `(f : OrderRingHom α β)`,
you should parametrize over `(F : Type*) [OrderRingHomClass F α β] (f : F)`.

When you extend this structure, make sure to extend `OrderRingHomClass`.  -/
OrderRingHom : (α : Type u_6) →
  (β : Type u_7) → [NonAssocSemiring α] → [Preorder α] → [NonAssocSemiring β] → [Preorder β] → Type (max u_6 u_7)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced)
  (hl_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size),
  Std.DTreeMap.Internal.Impl.minView k v Std.DTreeMap.Internal.Impl.leaf r hl_2 hr hlr_2 =
    { k := k, v := v, tree := { impl := r, balanced_impl := hr, size_impl := ⋯ } }
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_lcm_mul_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), lcm m n ∣ lcm (k * m) n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_insert : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, insert a (Set.Ioi a) = Set.Ici a
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.mk.congr_simp : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f f_1 : X.obj ⟶ Y.obj) (e_f : f = f_1)
  (comm :
    CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
      CategoryTheory.CategoryStruct.comp f Y.d),
  { f := f, comm := comm } = { f := f_1, comm := ⋯ }
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey_cons_perm.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    {k : α} →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.extendFunctor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c),
  (e.extendFunctor C).obj K = K.extend e
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The entire function of `s` which agrees with
`1 / 2 * Gamma ((s + 1) / 2) * π ^ (-(s + 1) / 2) * ∑' (n : ℤ), sgn (n + a) / |n + a| ^ s`
for `1 < re s`.
 -/
HurwitzZeta.completedHurwitzZetaOdd : UnitAddCircle → ℂ → ℂ
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.algebraMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : DecidableEq ι] [inst_4 : AddCommMonoid ι] [inst_5 : CommSemiring A]
  [inst_6 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_7 : GradedAlgebra 𝒜] (x : ↥(Submodule.baseChange S (𝒜 0))),
  (algebraMap (↥(Submodule.baseChange S (𝒜 0))) (TensorProduct R S A)) x = ↑x
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is algebraic, then the `Field.finSepDegree F E` is equal to `Field.sepDegree F E`
as a natural number. This means that the cardinality of `Field.Emb F E` and the degree of
`(separableClosure F E) / F` are both finite or infinite, and when they are finite, they
coincide.  -/
Field.finSepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  Field.finSepDegree F E = Cardinal.toNat (Field.sepDegree F E)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_add : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.truncateFun n (x + y) = WittVector.truncateFun n x + WittVector.truncateFun n y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_union_of_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddAssocClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : VAdd M N] [inst_1 : (i : ι) → VAdd N (α i)]
  [inst_2 : (i : ι) → VAdd M (α i)] [∀ (i : ι), VAddAssocClass M N (α i)], VAddAssocClass M N ((i : ι) → α i)
-- Mathlib.Topology.EMetricSpace.Defs
instPseudoEMetricSpaceULift : {α : Type u} → [PseudoEMetricSpace α] → PseudoEMetricSpace (ULift.{u_2, u} α)
-- Mathlib.Tactic.ErwQuestion
/-- Check if two expressions are different at reducible transparency.
Attempt to log an info message for the first subexpressions which are different
(but agree at default transparency).

Also returns an array of messages for the `verbose` report.
 -/
Mathlib.Tactic.Erw?.logDiffs : Lean.Syntax → Lean.Expr → Lean.Expr → StateT (Array (Unit → Lean.MessageData)) Lean.MetaM Bool
-- Mathlib.Order.InitialSeg
/-- Principal segment from the empty relation on `PEmpty` to the empty relation on `PUnit`.  -/
PrincipalSeg.pemptyToPUnit : PrincipalSeg emptyRelation emptyRelation
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi_F : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive],
  Λ.karoubi.F = CategoryTheory.Abelian.LeftResolution.karoubi.F Λ
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `f` is an antitone function and `g` tends to `atTop` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`.  -/
Antitone.lowerBounds_range_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {l : Filter α} [l.NeBot]
  {f : β → γ},
  Antitone f →
    ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
-- Std.Http.Data.Body.Stream
Std.Http.Body.instNonemptyStream : Nonempty Std.Http.Body.Stream
-- Mathlib.Data.Int.Lemmas
Int.natAbs_inj_of_nonpos_of_nonneg : ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → (a.natAbs = b.natAbs ↔ -a = b)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α)
  (x : ℝ), (hf.stieltjesFunction a).measure (Set.Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_of_dvd' : ∀ {m n : ℕ}, (∀ (k : ℕ), Nat.Prime k → k ∣ m → k ∣ n → k ∣ 1) → m.Coprime n
-- Mathlib.Data.UInt
UInt16.toBitVec_nsmul : ∀ (n : ℕ) (a : UInt16), (n • a).toBitVec = n • a.toBitVec
-- Mathlib.Data.Set.Basic
Set.univ_inter : ∀ {α : Type u} (a : Set α), Set.univ ∩ a = a
-- Mathlib.Probability.Process.Filtration
/-- If the index type is a `SuccOrder`, then `𝓕₊ = 𝓕`.  -/
MeasureTheory.Filtration.rightCont_eq_self : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [SuccOrder ι]
  (𝓕 : MeasureTheory.Filtration ι m), 𝓕.rightCont = 𝓕
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `SplitMonoCategory`,
then `D` also is.  -/
CategoryTheory.Functor.splitMonoCategoryImpOfIsEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsEquivalence] [CategoryTheory.SplitMonoCategory C],
  CategoryTheory.SplitMonoCategory D
-- Mathlib.RingTheory.Perfectoid.Untilt
/-- The composition of the mod `p` map
with the untilt function equals taking the zeroth component of the perfection.
A variation of `PreTilt.mk_untilt_eq_coeff_zero`.
 -/
PreTilt.mk_comp_untilt_eq_coeff_zero : ∀ {O : Type u_1} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) O],
  ⇑(Ideal.Quotient.mk (Ideal.span {↑p})) ∘ ⇑PreTilt.untilt = ⇑(PreTilt.coeff 0)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.

```
Vᵢⱼ ⟶ Uᵢ
 |      |
 ↓      ↓
 Uⱼ ⟶ X
```
 -/
AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] → (i j : D.J) → CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithScott α)
-- Init.Data.Array.Lemmas
/-- Variant of `all_eq_false` in terms of membership rather than an array index.  -/
Array.all_eq_false' : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.all p = false ↔ ∃ x ∈ as, ¬p x = true
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- This is the splitting of a short complex `S` in a balanced category induced by
a section of the morphism `S.g : S.X₂ ⟶ S.X₃`  -/
CategoryTheory.ShortComplex.Splitting.ofExactOfSection : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        (S : CategoryTheory.ShortComplex C) →
          S.Exact →
            (s : S.X₃ ⟶ S.X₂) →
              CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃ →
                CategoryTheory.Mono S.f → S.Splitting
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.hasColimits_of_completeLattice : ∀ {α : Type u} [inst : CompleteLattice α], CategoryTheory.Limits.HasColimitsOfSize.{w, w', u, u} α
-- Mathlib.Topology.Order.Basic
nhds_bot_basis : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderBot α] [OrderTopology α]
  [Nontrivial α], (nhds ⊥).HasBasis (fun a => ⊥ < a) fun a => Set.Iio a
-- Mathlib.Order.RelClasses
Set.unbounded_of_isEmpty : ∀ {α : Type u} [IsEmpty α] {r : α → α → Prop} (s : Set α), Set.Unbounded r s
-- Mathlib.Data.Set.Lattice
Set.sInter_subset_of_mem : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, t ∈ S → ⋂₀ S ⊆ t
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv h) =
    CategoryTheory.CategoryStruct.comp (w.inv.app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instDecidableEq : {α : Type u_1} → [inst : LE α] → [DecidableEq α] → DecidableEq (NonemptyInterval α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_diff_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldrM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ) (x_1 : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldrM f x x_1 =
    match x, x_1 with
    | d, Std.DHashMap.Internal.AssocList.nil => pure d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => do
      let d ← Std.DHashMap.Internal.AssocList.foldrM f d es
      f a b d