mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.maxKey? = none
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.range_mapAlgHom : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : Algebra R S₁] [inst_4 : Algebra R S₂] (f : S₁ →ₐ[R] S₂),
  Subalgebra.toSubmodule (MvPolynomial.mapAlgHom f).range = MvPolynomial.coeffsIn σ (Subalgebra.toSubmodule f.range)
-- Mathlib.SetTheory.Lists
Lists.isList_toList : ∀ {α : Type u_1} (l : List (Lists α)), (Lists.ofList l).IsList
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.continuousOn : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → ContinuousOn f s
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `SemilinearEquivClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear equivs
`M → M₂`.

See also `LinearEquivClass F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`.  -/
SemilinearEquivClass : (F : Type u_14) →
  {R : outParam (Type u_15)} →
    {S : outParam (Type u_16)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          (σ : outParam (R →+* S)) →
            {σ' : outParam (S →+* R)} →
              [RingHomInvPair σ σ'] →
                [RingHomInvPair σ' σ] →
                  (M : outParam (Type u_17)) →
                    (M₂ : outParam (Type u_18)) →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → [EquivLike F M M₂] → Prop
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_X_pow_add_C : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] {n : ℕ},
  0 < n → ∀ (a : R), (Polynomial.X ^ n + Polynomial.C a).degree = ↑n
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskering_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c)
  {X Y : CategoryTheory.Bicategory.RightLift f g} (η : X ⟶ Y),
  (CategoryTheory.Bicategory.RightLift.whiskering h).map η =
    CategoryTheory.Bicategory.RightLift.homMk (CategoryTheory.Bicategory.whiskerLeft h η.left) ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toAddMonoidHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : AddZeroClass α] → [inst_3 : AddZeroClass β] → (α →+o β) → α →+ β
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (dom : L.Substructure M) → (cod : L.Substructure N) → L.Equiv ↥dom ↥cod → L.PartialEquiv M N
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.reduceBin : Lean.Name → ℕ → ({n : ℕ} → Fin n → Fin n → Fin n) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Subring.isIntegrallyClosedIn_iff : ∀ {A : Type u_2} [inst : CommRing A] {C : Type u_5} [inst_1 : SetLike C A] [inst_2 : SubringClass C A] {S : C},
  IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
-- Init.System.IO
/-- Directories don't have contents, but may contain other files.  -/
IO.FS.FileType.dir : IO.FS.FileType
-- Init.Data.UInt.Basic
instShiftRightUInt8 : ShiftRight UInt8
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_inverse_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) {X Y : CategoryTheory.ComposableArrows Cᵒᵖ n}
  (f : X ⟶ Y),
  (CategoryTheory.ComposableArrows.opEquivalence C n).inverse.map f =
    ((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft
        (CategoryTheory.NatTrans.leftOp f)).op
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).π = CategoryTheory.Limits.cokernel.π S.f
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Iic` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderBot.ofIic`, this one requires `DecidableLE` but
only `Preorder`.  -/
LocallyFiniteOrderBot.ofIic' : (α : Type u_1) →
  [inst : Preorder α] →
    [DecidableLE α] → (finsetIic : α → Finset α) → (∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a) → LocallyFiniteOrderBot α
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C], U.mapPower id = CategoryTheory.CategoryStruct.id (U.power α)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app : ∀ (X : AlgebraicGeometry.Scheme) (X_1 : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec X).inv.app X_1 = ⋯.isoSpec.inv
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- Specialisation of `Nat.ofNat_nonneg'`, which seems to be easier for Lean to use.  -/
Nat.ofNat_nonneg : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (n : ℕ) [inst_3 : n.AtLeastTwo],
  0 ≤ OfNat.ofNat n
-- Lean.Compiler.IR.CompilerM
Lean.IR.CompilerM : Type → Type
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.forgetReflectsIsos : (CategoryTheory.forget AddMagmaCat).ReflectsIsomorphisms
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.contains : {α : Type u} → {β : α → Type v} → [inst : Ord α] → {k : α → Ordering} → Std.DTreeMap.Internal.Cell α β k → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasFDerivAt c c' x → HasFDerivAt d d' x → HasFDerivAt (c * d) (c x • d' + d x • c') x
-- Mathlib.Data.Set.Lattice
/-- This rather trivial consequence of `subset_iUnion` is convenient with `apply`, and has `i`
explicit for this purpose.  -/
Set.subset_iUnion_of_subset : ∀ {α : Type u_1} {ι : Sort u_5} {s : Set α} {t : ι → Set α} (i : ι), s ⊆ t i → s ⊆ ⋃ i, t i
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.quotDualCoannihilatorToDual_nondegenerate : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (W : Submodule R (Module.Dual R M)), W.quotDualCoannihilatorToDual.Nondegenerate
-- Mathlib.Analysis.SpecialFunctions.Choose
/-- `n.choose k` is asymptotically equivalent to `n^k / k!`.  -/
isEquivalent_choose : ∀ (k : ℕ), Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(n.choose k)) fun n => ↑n ^ k / ↑k.factorial
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.projRight_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
  (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂),
  Path.Homotopic.projRight (Path.Homotopic.prod q₁ q₂) = q₂
-- Mathlib.Analysis.InnerProductSpace.Symmetric
_private.Mathlib.Analysis.InnerProductSpace.Symmetric.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
While it is most natural to give the recursive formula for `I (n + 2) θ`, as well as give the second
base case of `I 1 θ`, it is in fact more convenient to give the recursive formula for `I (n + 1) θ`
in terms of `I n θ` and `I (n - 1) θ` (note the natural subtraction!).
Despite the usually inconvenient subtraction, this in fact allows deducing both of the above facts
with significantly fewer analysis computations.
In addition, note the `0 ^ n` on the right-hand side - this is intentional, and again allows
combining the proof of the "usual" recursion formula and the base case `I 1 θ`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.recursion' : ∀ {θ : ℝ} (n : ℕ),
  I✝ (n + 1) θ * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * Real.cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I✝ n θ -
      4 * (↑n + 1) * ↑n * I✝ (n - 1) θ
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.id_apply : ∀ (M : Type u_10) [inst : AddZero M] (x : M), (AddMonoidHom.id M) x = x
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_zero : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ↑0 = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.regexp : Lean.Lsp.SemanticTokenType
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.adapt_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [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}
  {epost : EPred} (f : ρ → ρ') (x : ReaderT ρ' m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp x (fun a x => post a r) epost (f r) ⦄ ReaderT.adapt f x ⦃ post; epost ⦄
-- Mathlib.Order.CompleteLatticeIntervals
subset_sSup_def : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s],
  sSup = fun t =>
    if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ s then ⟨sSup (Subtype.val '' t), ⋯⟩ else default
-- Mathlib.Data.Fintype.Prod
Finset.univ_product_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β], Finset.univ ×ˢ Finset.univ = Finset.univ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.nnreal_cfcₙ_eq_cfc_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : A)
  (f : NNReal → NNReal), autoParam (f 0 = 0) Unitization.nnreal_cfcₙ_eq_cfc_inr._auto_1 → ↑(cfcₙ f a) = cfc f ↑a
-- Std.Async.UDP
/-- Sets the membership for joining or leaving a multicast group.
 -/
Std.Async.UDP.Socket.setMembership : Std.Async.UDP.Socket → Std.Net.IPAddr → Option Std.Net.IPAddr → Std.Async.UDP.Membership → IO Unit
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- The cover of the glued `Xᵢ` given by the `Xᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) →
          [inst_2 : Small.{u, u_1} 𝒰.I₀] → [inst_3 : Quiver.IsThin 𝒰.I₀] → d.glued.OpenCover
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformAddGroup.mk : ∀ {G : Type u_7} [inst : UniformSpace G] [inst_1 : AddGroup G] [toIsTopologicalAddGroup : IsTopologicalAddGroup G],
  uniformity G = Filter.comap (fun x => x.2 + -x.1) (nhds 0) → IsRightUniformAddGroup G
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_faithful : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.Faithful],
  (CategoryTheory.Limits.BinaryBicones.functoriality P Q F).Faithful
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- A reformulation of `CategoryTheory.Paths.induction` in terms of `MorphismProperty`.  -/
CategoryTheory.Paths.morphismProperty_eq_top : ∀ (V : Type u₁) [inst : Quiver V] (P : CategoryTheory.MorphismProperty (CategoryTheory.Paths V)),
  (∀ {v : V}, P (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of V).obj v))) →
    (∀ {u v w : V} (p : (CategoryTheory.Paths.of V).obj u ⟶ (CategoryTheory.Paths.of V).obj v) (q : v ⟶ w),
        P p → P (CategoryTheory.CategoryStruct.comp p ((CategoryTheory.Paths.of V).map q))) →
      P = ⊤
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `edist_zero_right`. -/
edist_zero_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), edist a 0 = ‖a‖ₑ
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.mul_delta : ∀ {f : ℕ → ℂ}, f 1 = 1 → f * LSeries.delta = LSeries.delta
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.coe_triangle_down_toOrderHom : ∀ {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c),
  ⇑(SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.triangle a b c hab hbc).down) = ![a, b, c]
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  -Set.Icc a b = Set.Icc (-b) (-a)
-- Mathlib.Data.Fintype.Defs
Fintype.decidableExistsFintype : {α : Type u_1} → {p : α → Prop} → [DecidablePred p] → [Fintype α] → Decidable (∃ a, p a)
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `f` is an antitone function and `g` tends to `atBot` 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.upperBounds_range_comp_tendsto_atBot : ∀ {α : 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.atBot → upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.copy_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom d =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d).hom
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom)
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.decomposedTo_map : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J]
  {X Y : (i : CategoryTheory.ConnectedComponents J) × i.Component} (g : X ⟶ Y),
  (CategoryTheory.decomposedTo J).map g = CategoryTheory.Sigma.descMap CategoryTheory.ConnectedComponents.ι X Y g
-- Std.Data.TreeSet.Basic
/-- Erases multiple items from the tree set by iterating over the given collection and calling erase.
 -/
Std.TreeSet.eraseMany : {α : Type u} → {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeSet α cmp → ρ → Std.TreeSet α cmp
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mk.sizeOf_spec : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst_1 : SizeOf X]
  (setsAt : X → Set (Set X)) (measurableSet : ∀ (x : X), ∀ s ∈ setsAt x, MeasurableSet s)
  (nonempty_interior : ∀ (x : X), ∀ s ∈ setsAt x, (interior s).Nonempty)
  (nontrivial : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt x, s ⊆ Metric.closedBall x ε)
  (covering :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0),
  sizeOf
      { setsAt := setsAt, measurableSet := measurableSet, nonempty_interior := nonempty_interior,
        nontrivial := nontrivial, covering := covering } =
    1
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_mul : ∀ (m n : ℕ∞), ↑(m * n) = ↑m * ↑n
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformlyOn f g s ↔ TendstoLocallyUniformlyOn (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop s
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {η : ProbabilityTheory.Kernel α γ},
  ¬ProbabilityTheory.IsSFiniteKernel η → κ.prod η = 0
-- Mathlib.Data.List.MinMax
List.maximum_cons : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (l : List α), (a :: l).maximum = max (↑a) l.maximum
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → Group (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsMulLeftInvariant],
  MeasureTheory.volume.IsMulLeftInvariant
-- Mathlib.Topology.Convenient.Category
/-- The isomorphism between
`fromGeneratedByTopCat ⋙ toTopCat X ≅ GeneratedByTopCat.toTopCat`.  -/
ContinuousGeneratedByCat.equivalenceFunctorIso : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      ContinuousGeneratedByCat.fromGeneratedByTopCat.comp (ContinuousGeneratedByCat.toTopCat X) ≅
        GeneratedByTopCat.toTopCat
-- Mathlib.Algebra.Star.Center
Set.star_mem_centralizer' : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {a : R} {s : Set R},
  (∀ a ∈ s, star a ∈ s) → a ∈ s.centralizer → star a ∈ s.centralizer
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.contains ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ => Std.DHashMap.Internal.AssocList.contains a buckets[i]
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → α × β → α × β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.iff_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasPushouts D] {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃}
  {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  CategoryTheory.IsPushout f₁ f₂ f₃ f₄ ↔ ∀ (X : C), CategoryTheory.IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instIsEquivalenceOppositeSymmOpInverse : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V], (HomologicalComplex.opInverse V c).IsEquivalence
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_compNeg : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [Nontrivial E]
  (p : FormalMultilinearSeries 𝕜 E F), (p.compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E)).radius = p.radius
-- Init.Data.List.Lemmas
List.mem_filter : ∀ {α : Type u_1} {p : α → Bool} {as : List α} {x : α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_mul_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coe_map : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (x : AddUnits M),
  ↑((AddUnits.map f) x) = f ↑x
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_add_right_eq_add_addConj : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅a, b + c⁆ = ⁅a, b⁆ + b + ⁅a, c⁆ + -b
-- Mathlib.Order.SupClosed
supClosed_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, SupClosed (supClosure s)
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_frobeniusEquiv_symm : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (n : ℕ)
  (x : PreTilt O p), (PreTilt.coeff n) ((frobeniusEquiv (PreTilt O p) p).symm x) = (PreTilt.coeff (n + 1)) x
-- Mathlib.Topology.Sheaves.Alexandrov
/-- Given a structured arrow `f` with domain `iSup Us` over `principals X`,
where `Us` is a family of `Opens X`, this functor sends `f` to the principal open
associated with it, considered as an object in the full subcategory of all `V : Opens X`
such that `V ≤ Us i` for some `i`.

This definition is primarily meant to be used in `lowerCone`, and `isLimit` below.
 -/
Alexandrov.projSup : {X : Type v} →
  [inst : TopologicalSpace X] →
    [inst_1 : Preorder X] →
      [inst_2 : Topology.IsUpperSet X] →
        {ι : Type v} →
          (Us : ι → TopologicalSpace.Opens X) →
            CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X))
              (TopCat.Presheaf.SheafCondition.OpensLeCover Us)ᵒᵖ
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.coe_mapAddMonoidHom : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), ⇑(Multiset.mapAddMonoidHom f) = Multiset.map f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.propagateDown : Lean.Meta.Grind.Methods → Lean.Meta.Grind.Propagator
-- Mathlib.Data.Finset.Powerset
Finset.powerset_card_disjiUnion : ∀ {α : Type u_1} (s : Finset α),
  s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) ⋯
-- Init.Data.Float.Model.Unpacked.Round
/-- The approximation is exactly equal to the infinitely precise value.
 -/
Float.Model.UnpackedFloat.Accuracy.exact : Float.Model.UnpackedFloat.Accuracy
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β),
  (SupBotHom.id β).comp f = f