mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_eval : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (x : R),
  Polynomial.eval x (Polynomial.derivative p) = p.sum fun n a => a * ↑n * x ^ (n - 1)
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.DaylightSavingRule.mk.sizeOf_spec : ∀ (name : String) (offset : Std.Time.TimeZone.Offset) (start end_ : Option Std.Time.TimeZone.TransitionRule),
  sizeOf { name := name, offset := offset, start := start, end_ := end_ } =
    1 + sizeOf name + sizeOf offset + sizeOf start + sizeOf end_
-- Init.GrindInstances.ToInt
Lean.Grind.instLTUInt16UintOfNatNat : Lean.Grind.ToInt.LT UInt16 (Lean.Grind.IntInterval.uint 16)
-- Plausible.Gen
/-- Generate a `Nat` example between `lo` and `hi` (exclusively).  -/
Plausible.Gen.chooseNatLt : (lo hi : ℕ) → lo < hi → Plausible.Gen { a // lo ≤ a ∧ a < hi }
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_sup_le : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α},
  Coheyting.boundary (a ⊔ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.mk_neg_add_mk_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits),
  ⟨(AddUnits.coeHom M) (-x), ⋯⟩ + ⟨(AddUnits.coeHom M) x, ⋯⟩ = 0
-- Mathlib.Order.RelIso.Basic
/-- Copy of a `RelIso` with a new `toFun` and `invFun` equal to the old ones.
Useful to fix definitional equalities.  -/
RelIso.copy : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → (e : r ≃r s) → (f : α → β) → (g : β → α) → f = ⇑e → g = ⇑e.symm → r ≃r s
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.exists_isMinOn_Gamma_Ioi : ∃ x ∈ Set.Ioo 1 2, IsMinOn Real.Gamma (Set.Ioi 0) x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ext : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] {f g : A ≃⋆ₐ[R] B},
  (∀ (a : A), f a = g a) → f = g
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The first morphism of triangles given by an `Octahedron'`.  -/
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            (h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles) →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  (h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        (h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                          CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃ →
                                            (CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ⟶
                                              CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃)
-- Mathlib.RingTheory.Flat.Domain
/-- Tensor product of linearly independent families is linearly independent over domains.
This is true over non-domains if one of the modules is flat.
See `LinearIndependent.tmul_of_flat_left`.  -/
LinearIndependent.tmul_of_isDomain : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N}, LinearIndependent R v → LinearIndependent R w → LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
-- Mathlib.Logic.Denumerable
Nat.Subtype.lt_succ_self : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] (x : ↑s), x < Nat.Subtype.succ x
-- Std.Data.HashMap.Lemmas
/-- Variant of `getElem_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.map f m},
  (Std.HashMap.map f m)[k] = f (m.getKey k ⋯) m[k]
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariantClass_le_of_lt : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N] [CovariantClass M N μ fun x1 x2 => x1 < x2],
  CovariantClass M N μ fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_left_inverse : ∀ {M : Type u_1} [inst : Monoid M], Function.LeftInverse Submonoid.units Subgroup.ofUnits
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr).Balanced
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid is normal if it is wide and satisfies the expected stability under conjugacy.  -/
CategoryTheory.Subgroupoid.IsNormal : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Prop
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of extended pseudometric spaces,
one may put an extended distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`.  -/
PiCountable.pseudoEMetricSpace : {ι : Type u_2} →
  [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → PseudoEMetricSpace (F i)] → PseudoEMetricSpace ((i : ι) → F i)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_nc.go.induct_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k_1 : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k_1) acc (Lean.Grind.CommRing.Poly.insert (k * k_1) m acc)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (Lean.Grind.CommRing.Poly.insert (k * k_1) (m.mul_nc m_1) acc)
            (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p
              (Lean.Grind.CommRing.Poly.insert (k * k_1) (m.mul_nc m_1) acc)) →
          motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) acc
            (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p
              (Lean.Grind.CommRing.Poly.insert (k * k_1) (m.mul_nc m_1) acc))) →
      ∀ (p acc : Lean.Grind.CommRing.Poly), motive p acc (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p acc)
-- Mathlib.RingTheory.Etale.Descent
RingHom.Etale.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.Etale) fun {R S} [CommRing R] [CommRing S] =>
  RingHom.FaithfullyFlat
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_set : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s t : Set H} {x : H} {f : H → H'}, s =ᶠ[nhds x] t → (P f s x ↔ P f t x)
-- Aesop.Stats.Basic
Aesop.instToJsonForwardClusterStateStats : Lean.ToJson Aesop.ForwardClusterStateStats
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.isMulCommutative_iSup : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} [Nonempty ι] {S : ι → Subring R}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_union_inter : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  ∑ x ∈ s₁ ∪ s₂, f x + ∑ x ∈ s₁ ∩ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBase.encard_compl_eq : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → (M.E \ B).encard = M✶.eRank
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.goodδ_lt_one : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  Besicovitch.goodδ E < 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : β k → β k)
  (l : List ((a : α) × β a)), (Std.Internal.List.modifyKey k f l).isEmpty = l.isEmpty
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.zero_smul_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero α] [inst_2 : Zero β] [inst_3 : SMulWithZero α β]
  (t : Finset β), 0 • t ⊆ 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  CategoryTheory.IsIso g →
    ∀ (n₀ n₁ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂._auto_1),
      X.δ f g n₀ n₁ hn₁ = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise addition of finsets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in
scope `Pointwise`.  -/
Finset.add : {α : Type u_2} → [DecidableEq α] → [Add α] → Add (Finset α)
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωSupImpl_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α × β)),
  (Prod.ωSupImpl c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Cast for modular forms, which is useful for avoiding `Heq`s. Optionally transports along
an equality of subgroups.  -/
ModularForm.mcast : {a b : ℤ} →
  {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} →
    a = b → ModularForm Γ a → autoParam (Γ' = Γ) ModularForm.mcast._auto_1 → ModularForm Γ' b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, (m.erase k).getD k fallback = fallback
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Variant with `fun x => x` rather than `id`  -/
derivWithin_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜),
  UniqueDiffWithinAt 𝕜 s x → derivWithin (fun x => x) s x = 1
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The underlying set of a non-empty directed sSup of subrings is just a union of the subrings.
Note that this fails without the directedness assumption (the union of two subrings is
typically not a subring)  -/
Subring.mem_iSup_of_directed : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.RingTheory.Perfection
/-- The perfection of a monoid `α`, defined to be the projective limit of `α` using the `p`-th
power maps `α → α` indexed by the natural numbers, implemented as
`{ f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }`.

If `α` is a ring with characteristic `p` and `p` is prime, `Perfection α p` is also a ring.  -/
Perfection : (α : Type u₁) → [Pow α ℕ] → ℕ → Type u₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLED k fallback = t₂.getEntryLED k fallback
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes : ∀ {w : ℕ} (a b : BitVec w), (a &&& b == -1#w) = (a == -1#w && b == -1#w)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.equivBoundedOfCompact.congr_simp : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ContinuousMap.equivBoundedOfCompact α β = ContinuousMap.equivBoundedOfCompact α β
-- Mathlib.Data.Fin.Tuple.Sort
/-- The sorted versions of a tuple `f` and of any permutation of `f` agree.  -/
Tuple.comp_perm_comp_sort_eq_comp_sort : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
  (f ∘ ⇑σ) ∘ ⇑(Tuple.sort (f ∘ ⇑σ)) = f ∘ ⇑(Tuple.sort f)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (AlgebraicGeometry.SheafedSpace.forget C)
-- Batteries.Data.List.Lemmas
List.filter.match_1.congr_eq_2 : ∀ (motive : Bool → Sort u_1) (x : Bool) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  x = false →
    (match x with
      | true => h_1 ()
      | false => h_2 ()) ≍
      h_2 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Fork.ofι ι w` is a limit cone in `Cᵒᵖ` if and only if `Cofork.ofπ ι.unop w.unop` in `C` is
a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (ι ι' : P ⟶ X) →
          (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) →
            (w' :
                CategoryTheory.CategoryStruct.comp f.unop ι'.unop = CategoryTheory.CategoryStruct.comp g.unop ι'.unop) →
              ι = ι' →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι ι w) ≃
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ ι'.unop w')
-- Mathlib.Order.SetDissipate
Set.dissipate_subset_dissipate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] {x y : α},
  y ≤ x → Set.dissipate s x ⊆ Set.dissipate s y
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV2.mk.injEq : ∀ (toTZifV1 : Std.Time.TimeZone.TZif.TZifV1) (footer : Option String) (toTZifV1_1 : Std.Time.TimeZone.TZif.TZifV1)
  (footer_1 : Option String),
  ({ toTZifV1 := toTZifV1, footer := footer } = { toTZifV1 := toTZifV1_1, footer := footer_1 }) =
    (toTZifV1 = toTZifV1_1 ∧ footer = footer_1)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabRawNatLit : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instIsScalarTower'' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower M N (Lex α)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimageIso.congr_simp : ∀ {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 Y : C} [inst_2 : F.Full] [inst_3 : F.Faithful] (f f_1 : F.obj X ≅ F.obj Y),
  f = f_1 → F.preimageIso f = F.preimageIso f_1
-- Mathlib.Analysis.SpecificLimits.Basic
geom_lt : ∀ {u : ℕ → ℝ} {c : ℝ}, 0 ≤ c → ∀ {n : ℕ}, 0 < n → (∀ k < n, c * u k < u (k + 1)) → c ^ n * u 0 < u n
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.instDirectedSystemCoeLinearMapIdLTensor : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  (M : Type u_4) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)],
  DirectedSystem (fun x => TensorProduct R M (G x)) fun i j h => ⇑(LinearMap.lTensor M (f i j h))
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.toNNReal_apply_of_tsum_ne_top : ∀ {α : Type u_4} {f : α → ENNReal}, ∑' (i : α), f i ≠ ⊤ → ∀ (x : α), ↑((ENNReal.toNNReal ∘ f) x) = f x
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mk.inj : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {inst : NontriviallyNormedField R} {inst_1 : NormedAddCommGroup F}
  {inst_2 : NormedSpace R F} {inst_3 : TopologicalSpace B} {ι : Type u_5} {baseSet : ι → Set B}
  {isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)} {indexAt : B → ι}
  {mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)} {coordChange : ι → ι → B → F →L[R] F}
  {coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), (coordChange i i x) v = v}
  {continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (coordChange i j) (baseSet i ∩ baseSet j)}
  {coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
        ∀ (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v}
  {baseSet_1 : ι → Set B} {isOpen_baseSet_1 : ∀ (i : ι), IsOpen (baseSet_1 i)} {indexAt_1 : B → ι}
  {mem_baseSet_at_1 : ∀ (x : B), x ∈ baseSet_1 (indexAt_1 x)} {coordChange_1 : ι → ι → B → F →L[R] F}
  {coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), (coordChange_1 i i x) v = v}
  {continuousOn_coordChange_1 : ∀ (i j : ι), ContinuousOn (coordChange_1 i j) (baseSet_1 i ∩ baseSet_1 j)}
  {coordChange_comp_1 :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet_1 i ∩ baseSet_1 j ∩ baseSet_1 k,
        ∀ (v : F), (coordChange_1 j k x) ((coordChange_1 i j x) v) = (coordChange_1 i k x) v},
  { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
      { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1,
        mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1,
        continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 } →
    baseSet = baseSet_1 ∧ indexAt = indexAt_1 ∧ coordChange = coordChange_1
-- Mathlib.Topology.UniformSpace.Basic
/-- A version of `UniformContinuous.inf_dom_right` for binary functions  -/
uniformContinuous_inf_dom_right₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β}
  {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.IsDeterministic.parallelComp_self_comp_copy' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [self : ProbabilityTheory.IsDeterministic κ],
  (κ.parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) = (ProbabilityTheory.Kernel.copy β).comp κ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The packing number of a set `A` for radius `ε` is the maximal cardinality (in `ℕ∞`)
of an `ε`-separated set in `A`.  -/
Metric.packingNumber : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → ℕ∞
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_add_le_of_le : ∀ {R : Type u} {n m : ℕ} [inst : Semiring R] {p q : Polynomial R},
  p.natDegree ≤ m → q.natDegree ≤ n → (p + q).natDegree ≤ max m n
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_sub : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (f g : M →ₗ[R] N), LinearMap.baseChange A (f - g) = LinearMap.baseChange A f - LinearMap.baseChange A g
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_const_le_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  (∃ C, ∀ (x : α), C ≤ f x) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_mul : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : ↥s), ↑(x * y) = ↑x * ↑y
-- Mathlib.GroupTheory.Finiteness
/-- A submonoid of `M` is finitely generated if it is the closure of a finite subset of `M`.  -/
Submonoid.FG : {M : Type u_1} → [inst : Monoid M] → Submonoid M → Prop
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.isLocalRing : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (P : Ideal R)
  [hp : P.IsPrime] [IsLocalization.AtPrime S P], IsLocalRing S
-- Lean.Meta.Basic
Lean.Meta.instNonemptySavedState : Nonempty Lean.Meta.SavedState
-- Mathlib.Order.Minimal
exists_minimal_of_wellFoundedLT : ∀ {α : Type u_2} [inst : Preorder α] [WellFoundedLT α] (P : α → Prop), (∃ a, P a) → ∃ a, Minimal P a
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- **Alias** of the forward direction of `Submodule.linearDisjoint_op`.

---

Linear disjointness is preserved by taking multiplicative opposite.  -/
Submodule.LinearDisjoint.op : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_mk' : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁)
  (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p), ⇑(AffineEquiv.mk' (⇑e) e' p h) = ⇑e
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofExact_map_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G),
  ((CategoryTheory.AdditiveFunctor.ofExact C D).map α).hom = α.hom
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The remainder map `PowerSeries.IsWeierstrassDivisorAt.mod` induces a linear map
`A⟦X⟧ / (g) →ₗ[A] A[X]`.  -/
PowerSeries.IsWeierstrassDivisorAt.mod' : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} →
        g.IsWeierstrassDivisorAt I → [IsAdicComplete I A] → PowerSeries A ⧸ Ideal.span {g} →ₗ[A] Polynomial A