mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.color.eq_1 : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (x : Ordinal.{u}),
  p.color x =
    sInf
      (Set.univ \
        ⋃ j,
          ⋃ (_ :
            (Metric.closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩
                Metric.closedBall (p.c (p.index x)) (p.r (p.index x))).Nonempty),
            {p.color ↑j})
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.preimageSingletonHomeomorph_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : F),
  (e.preimageSingletonHomeomorph hb).symm p = ⟨↑e.symm (b, p), ⋯⟩
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribEquivOfBasis_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i))
  (a : Module.Dual R (PiTensorProduct R fun i => M i)),
  (PiTensorProduct.dualDistribEquivOfBasis b).symm a = (PiTensorProduct.dualDistribInvOfBasis b) a
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ne_zero_of_mul_eq_one : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  (I J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1 → I ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.isUnit_charpolyRev_of_isNilpotent : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R},
  IsNilpotent M → IsUnit M.charpolyRev
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
/-- Although not explicitly stated, the assumptions of lemma `natDegree_mul_C_eq_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
 -/
Polynomial.natDegree_mul_C_eq_of_mul_ne_zero : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
  p.leadingCoeff * a ≠ 0 → (p * Polynomial.C a).natDegree = p.natDegree
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forM_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {m : Type w → Type w'} [inst : Std.TransCmp cmp]
  [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → m PUnit.{w + 1}}, forM t f = t.toList.forM f
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.diag : Lean.Meta.Simp.Stats → Lean.Meta.Simp.Diagnostics
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.toEquiv_piCongrLeft : ∀ {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [inst : (j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι'),
  (Homeomorph.piCongrLeft e).toEquiv = Equiv.piCongrLeft Y e
-- Mathlib.Data.Stream.Init
Stream'.cons_injective2 : ∀ {α : Type u}, Function.Injective2 Stream'.cons
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.match_1.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.CommRing.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁_1 : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂_1 : Lean.Grind.CommRing.Poly),
  p₁ = Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_1 →
    p₂ = Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_1 →
      (match p₁, p₂ with
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) ≍
        h_4 k₁ m₁ p₁_1 k₂ m₂ p₂_1
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeLinearEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (m : M),
  (DirectSum.decomposeLinearEquiv ℳ) m = (DirectSum.decompose ℳ) m
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on
overflow.

Examples:
 * `Nat.toInt32 127 = 127`
 * `Nat.toInt32 32770 = 32770`
 * `Nat.toInt32 2_147_483_647 = 2_147_483_647`
 * `Nat.toInt32 2_147_483_648 = -2_147_483_648`
 -/
Nat.toInt32 : ℕ → Int32
-- Mathlib.RepresentationTheory.Rep.Res
Rep.instLinearResFunctor : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] (f : H →* G) {k : Type u} [inst_2 : CommSemiring k],
  CategoryTheory.Functor.Linear k (Rep.resFunctor f)
-- Std.Time.DateTime
/-- Creates a new `DateTime` out of a `PlainDateTime` and a `ZoneRules`. It assumes `PlainDateTime` is
the local time.
 -/
Std.Time.DateTime.ofPlainDateTime : Std.Time.PlainDateTime → Std.Time.TimeZone.ZoneRules → Std.Time.DateTime
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddSemigroup.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddSemigroup = { toAdd := SeparationQuotient.instAdd, add_assoc := ⋯ }
-- Mathlib.Dynamics.Flow
Flow.mk : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddZero τ] →
          (toFun : τ → α → α) →
            Continuous (Function.uncurry toFun) →
              (∀ (t₁ t₂ : τ) (x : α), toFun (t₁ + t₂) x = toFun t₁ (toFun t₂ x)) → (∀ (x : α), toFun 0 x = x) → Flow τ α
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_or : ∀ {w i : ℕ} {x y : BitVec w}, (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isoColimitCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  (t : CategoryTheory.Limits.ColimitCocone F),
  CategoryTheory.Limits.colimit.isoColimitCocone t =
    (CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso t.isColimit
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization map of a quotient module.  -/
Submodule.toLocalizedQuotient' : {R : Type u_5} →
  (S : Type u_6) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          (p : Submonoid R) →
                            [inst_9 : IsLocalization p S] →
                              (f : M →ₗ[R] N) →
                                [inst_10 : IsLocalizedModule p f] →
                                  (M' : Submodule R M) → M ⧸ M' →ₗ[R] N ⧸ Submodule.localized' S p f M'
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M),
  ∑ i, ∑ j > i, (f j i + f i j) = ∑ i, ∑ j ∈ {i}ᶜ, f j i
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.mk.inj : ∀ {R : Type u₀} {inst : CommSemiring R} {A : Type u₁} {inst_1 : Ring A} {inst_2 : Algebra R A} {B : Type u₂}
  {inst_3 : Ring B} {inst_4 : Algebra R B} {eqv : ModuleCat A ≌ ModuleCat B}
  {linear : autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam}
  {eqv_1 : ModuleCat A ≌ ModuleCat B}
  {linear_1 : autoParam (CategoryTheory.Functor.Linear R eqv_1.functor) MoritaEquivalence.linear._autoParam},
  { eqv := eqv, linear := linear } = { eqv := eqv_1, linear := linear_1 } → eqv = eqv_1
-- Mathlib.Data.NNReal.Basic
NNReal.natCast_iSup : ∀ {ι : Sort u_4} (f : ι → ℕ), ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Data.Set.Lattice.Image
Set.seq.eq_1 : ∀ {α : Type u} {β : Type v} (s : Set (α → β)) (t : Set α), s.seq t = Set.image2 (fun f => f) s t
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H))
  (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)),
  LieSubmodule.restr (LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q hq) H =
    ⨆ α, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.mulSingle_mem_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] [inst_1 : DecidableEq η] {I : Set η}
  {H : (i : η) → Subgroup (f i)} (i : η) (x : f i), Pi.mulSingle i x ∈ Subgroup.pi I H ↔ i ∈ I → x ∈ H i
-- Mathlib.Analysis.LConvolution
/-- The convolution of `AEMeasurable` functions is `AEMeasurable`.  -/
MeasureTheory.aemeasurable_mlconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {f g : G → ENNReal},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (MeasureTheory.mlconvolution f g μ) μ
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.chainComplexFunctor_map_f : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G)
  {X Y : Rep.{u_1, u, u} k G} (f : X ⟶ Y) (i : ℕ), ((Rep.FiniteCyclicGroup.chainComplexFunctor k g).map f).f i = f
-- Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
CategoryTheory.Monoidal.leftRigidFunctorCategory : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Groupoid C] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.LeftRigidCategory D] → CategoryTheory.LeftRigidCategory (CategoryTheory.Functor C D)
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.fixedParamPerms : Lean.Elab.Structural.EqnInfo → Lean.Elab.FixedParamPerms
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- If `K` admits an orthogonal projection, then the orthogonal complement of its orthogonal
complement is itself.  -/
Submodule.orthogonal_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection], Kᗮᗮ = K
-- Init.Data.Repr
instReprAtomBool : ReprAtom Bool
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.exists_supDegree_mem_support : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} (D : A → B), p ≠ 0 → ∃ a ∈ p.coeff.support, AddMonoidAlgebra.supDegree D p = D a
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
SubStarSemigroup.mk : {M : Type v} →
  [inst : Mul M] →
    [inst_1 : Star M] →
      (toSubsemigroup : Subsemigroup M) →
        (∀ {a : M}, a ∈ toSubsemigroup.carrier → star a ∈ toSubsemigroup.carrier) → SubStarSemigroup M
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Returns an integer value `i` for assigning to `e` s.t. adding `e := i` to `a` will not falsify any disequality
and `i` is not in `alreadyUsed`.
 -/
Lean.Meta.Grind.Arith.pickUnusedValue : Lean.Meta.Grind.Goal → Std.HashMap Lean.Expr ℚ → Lean.Expr → ℤ → Std.HashSet ℤ → ℤ
-- Mathlib.Topology.Algebra.Ring.Basic
instIsSemitopologicalSemiringMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [IsSemitopologicalSemiring R],
  IsSemitopologicalSemiring Rᵐᵒᵖ
-- Mathlib.Geometry.Manifold.DerivationBundle
smooth_functions_tower : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
  IsScalarTower 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuousOn_iff_restrict : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- The quasi-compact precoverage on the category of schemes is the precoverage
given by quasi-compact covers. The intersection of this precoverage
with the precoverage defined by jointly surjective families of flat morphisms is
the fpqc-precoverage.
 -/
AlgebraicGeometry.Scheme.qcPrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.Logic.Encodable.Pi
/-- If `α` and `β` are encodable and `α` is a fintype, then `α → β` is encodable as well.  -/
Encodable.fintypeArrowOfEncodable : {α : Type u_2} → {β : Type u_3} → [Encodable α] → [Fintype α] → [Encodable β] → Encodable (α → β)
-- Init.WFExtrinsicFix
/-- A 2-ary fixpoint combinator that can be used to construct recursive functions with an
**extrinsic, partial** proof of termination.

Given a relation `R` and a fixpoint functional `F` which must be decreasing with respect
to `R`, `partialExtrinsicFix₂ R F` is the recursive function obtained by having `F` call
itself recursively.

For each pair of inputs `a` and `b`, `partialExtrinsicFix₂ R F a b` can be verified
given a **partial** termination proof. The precise semantics are as follows.

If `Acc R ⟨a, b⟩ ` does not hold, `partialExtrinsicFix₂ R F a b` might run forever. In this
case, nothing interesting can be proved about the recursive function; it is opaque and behaves like
a recursive function with the `partial` modifier.

If `Acc R ⟨a, b⟩` *does* hold, `partialExtrinsicFix₂ R F a b` is equivalent to
`F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b')`, both logically and regarding its
termination behavior.

In particular, if `R` is well-founded, `partialExtrinsicFix₂ R F a b` is equivalent to
a well-foundesd fixpoint.
 -/
WellFounded.partialExtrinsicFix₂ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {C₂ : (a : α) → β a → Sort u_3} →
      [∀ (a : α) (b : β a), Nonempty (C₂ a b)] →
        (R : (a : α) ×' β a → (a : α) ×' β a → Prop) →
          ((a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) →
            (a : α) → (b : β a) → C₂ a b
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_associator_assoc : ∀ (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inr z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h) =
    CategoryTheory.CategoryStruct.comp (y.inr z)
      (CategoryTheory.CategoryStruct.comp (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h)
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is continuous on a set if each individual
function is.  -/
continuousOn_tsum : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
  [inst_2 : TopologicalSpace β] {f : α → β → F} {s : Set β},
  (∀ (i : α), ContinuousOn (f i) s) →
    Summable u → (∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) → ContinuousOn (fun x => ∑' (n : α), f n x) s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {m₁ m₂ : Std.HashMap.Raw α Unit},
  m₁.WF → m₂.WF → (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans.app X)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.dense_setOfPred_finite : ∀ {α : Type u_1} [inst : TopologicalSpace α], Dense {K | (↑K).Finite}
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- Main theorem of this section: if both `f` and `x ↦ ‖x‖ * ‖f x‖` are integrable, then the
Fourier transform of `f` has a Fréchet derivative (everywhere in its domain) and its derivative is
the Fourier transform of `smulRight L f`.  -/
VectorFourier.hasFDerivAt_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V]
  {μ : MeasureTheory.Measure V},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ →
      ∀ (w : W),
        HasFDerivAt (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
          (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
            (VectorFourier.fourierSMulRight L f) w)
          w
-- Init.Data.Bool
Bool.instDecidableLe : (x y : Bool) → Decidable (x ≤ y)
-- Lean.DocString.Syntax
/-- A footnote definition.
 -/
Lean.Doc.Syntax.footnote_ref : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSetIso_symm_apply : ∀ (x : { x // x.IsOrdinal }), (RelIso.symm Ordinal.toZFSetIso) x = (↑x).rank
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  {X_1 Y : CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2} (g : X_1 ⟶ Y),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).map g).left = CategoryTheory.Over.Hom.left g.left
-- Batteries.Tactic.Init
/-- `split_ands` applies `And.intro` on all goals until it does not make progress.  -/
Batteries.Tactic.tacticSplit_ands : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Constructions
/-- `AnalyticAt.comp_analyticWithinAt` for functions on product spaces  -/
AnalyticAt.comp₂_analyticWithinAt : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  {h : F × G → H} {f : E → F} {g : E → G} {x : E} {s : Set E},
  AnalyticAt 𝕜 h (f x, g x) →
    AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 g s x → AnalyticWithinAt 𝕜 (fun x => h (f x, g x)) s x
-- Batteries.Tactic.Init
/-- Deprecated variant of `trivial`.  -/
Batteries.Tactic.triv : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.PP
/-- Helper function for pretty printing the state for debugging purposes.  -/
Lean.Meta.Grind.Goal.ppENodeRef : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (f + f') (g + g') l s
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i),
  (∀ (i : ℕ) (hi : i < n),
      F.map' i (i + 1) ⋯ hi =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map' i (i + 1) ⋯ hi) (CategoryTheory.eqToHom ⋯))) →
    F = G
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalizer_eq_top : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [h : H.Normal], Subgroup.normalizer ↑H = ⊤
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_zpow : ∀ (n : ℤ) (R θ : ℝ), circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.intMul : ℤ → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr
-- Mathlib.CategoryTheory.Quotient
/-- The induced functor on the quotient category.  -/
CategoryTheory.Quotient.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            (∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
              CategoryTheory.Functor (CategoryTheory.Quotient r) D
-- Mathlib.Logic.Equiv.Defs
/-- The equivalence `(∀ i, β i) ≃ β ⋆` when the domain of `β` only contains `⋆`  -/
Equiv.piUnique : {α : Sort u} → [inst : Unique α] → (β : α → Sort u_1) → ((i : α) → β i) ≃ β default
-- Mathlib.Data.PNat.Defs
/-- We define `m % k` and `m / k` in the same way as for `ℕ`
except that when `m = n * k` we take `m % k = k` and
`m / k = n - 1`.  This ensures that `m % k` is always positive
and `m = (m % k) + k * (m / k)` in all cases.  Later we
define a function `div_exact` which gives the usual `m / k`
in the case where `k` divides `m`.
 -/
PNat.modDivAux : ℕ+ → ℕ → ℕ → ℕ+ × ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- the set of type (I) simplices  -/
SSet.Subcomplex.Pairing.I : {X : SSet} → {A : X.Subcomplex} → A.Pairing → Set A.N
-- Mathlib.Data.ENat.Basic
ENat.add_lt_add : ∀ {a b c d : ℕ∞}, a < c → b < d → a + b < c + d
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ}
  {Y : C} (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkCoyonedaObjObjEquiv
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y)) f))
      h =
    CategoryTheory.CategoryStruct.comp g.unop
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) h)