mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNat_nnratCast : ∀ {R : Type u_1} [inst : DivisionSemiring R] {q : ℚ≥0} {n : ℕ},
  Mathlib.Meta.NormNum.IsNat q n → Mathlib.Meta.NormNum.IsNat (↑q) n
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.nontrivial_toCycle : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle),
  (f.toCycle hf).Nontrivial
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instLawfulForwardPatternChar : ∀ {c : Char}, String.Slice.Pattern.LawfulForwardPattern c
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- **Alias** of the reverse direction of `ProbabilityTheory.isGaussian_iff_charFunDual_eq`.

---

A finite measure is Gaussian iff its characteristic function has value
`exp (μ[L] * I - Var[L; μ] / 2)` for every `L : Dual ℝ E`.  -/
ProbabilityTheory.isGaussian_of_charFunDual_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (L : StrongDual ℝ E),
      MeasureTheory.charFunDual μ L =
        Complex.exp ((∫ (x : E), ↑(L x) ∂μ) * Complex.I - ↑(ProbabilityTheory.variance (⇑L) μ) / 2)) →
    ProbabilityTheory.IsGaussian μ
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.pseudofunctor_mapComp : ∀ {a b c : CategoryTheory.Cat} (x : a ⟶ b) (x_1 : b ⟶ c),
  CategoryTheory.WithInitial.pseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapComp x.toFunctor x_1.toFunctor)
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Normed commutative ring structure on the product of finitely many normed commutative rings,
using the sup norm.  -/
Pi.normedCommutativeRing : {ι : Type u_3} → {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedCommRing (R i)] → NormedCommRing ((i : ι) → R i)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_normalizer_of_normal_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [hK : (H.addSubgroupOf K).Normal],
  H ≤ K → K ≤ AddSubgroup.normalizer ↑H
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.start_mem_vertices : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), a ∈ p.vertices
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- Stirling's approximation gives a lower bound for `n!` for all `n`.
The left-hand side is formulated to mimic the usual informal description of the approximation.
See also `factorial_isEquivalent_stirling` which says these are asymptotically equivalent. That
statement gives an upper bound also, but requires sufficiently large `n`. In contrast, this one is
only a lower bound, but holds for all `n`.
See also `log_stirlingSeq_sdiff_le` for Robbins' sharp bound on successive differences in the
Stirling sequence.
 -/
Stirling.le_factorial_stirling : ∀ (n : ℕ), √(2 * Real.pi * ↑n) * (↑n / Real.exp 1) ^ n ≤ ↑n.factorial
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_pow : ∀ (a : USize) (n : ℕ) (h : System.Platform.numBits = 64), (a ^ n).toBitVec64 h = a.toBitVec64 h ^ n
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.prop_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  P.shift a X ↔ P ((CategoryTheory.shiftFunctor C a).obj X)
-- Mathlib.Algebra.Order.Field.Basic
one_le_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < b → (1 ≤ a / b ↔ b ≤ a)
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.neg_symm`. -/
AddAut.inv_symm : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), AddEquiv.symm (-e) = e
-- Init.Data.List.Lemmas
List.contains_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {as : List α}, as.contains a = true ↔ a ∈ as
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.keys.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → t.keys = t_1.keys
-- Std.Data.TreeMap.Raw.Basic
/-- Computes the intersection of the given tree maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map.
 -/
Std.TreeMap.Raw.inter : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp
-- Lean.Expr
_private.Lean.Expr.0.Lean.natEqPred : Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhOrderIso_apply : ⇑Real.sinhOrderIso = Real.sinh
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_preserves : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasLeftHomology]
  [F.PreservesLeftHomologyOf S], (S.map F).HasLeftHomology
-- Mathlib.Algebra.Homology.ModelCategory.Injective
/-- Let `sq` be a commutative square in the category of bounded below cochain complexes
in an abelian category. We assume that the left morphism `i` is a monomorphism,
and `p` an epimorphism with a degreewise injective kernel. Then, there exists
a lifting for `sq` if `i` or `p` is a quasi-isomorphism.  -/
_private.Mathlib.Algebra.Homology.ModelCategory.Injective.0.CochainComplex.Plus.modelCategoryQuillen.lifting : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex.Plus C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.Mono i] [HomotopicalAlgebra.Fibration p],
  HomotopicalAlgebra.WeakEquivalence i ∨ HomotopicalAlgebra.WeakEquivalence p → CategoryTheory.HasLiftingProperty i p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonHoverParams : Lean.ToJson Lean.Lsp.HoverParams
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.fourier_iteratedDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {N : ℕ∞} {n : ℕ},
  ContDiff ℝ (↑N) f →
    (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedDeriv n f) MeasureTheory.volume) →
      ↑n ≤ N →
        FourierTransform.fourier (iteratedDeriv n f) = fun x =>
          (2 * ↑Real.pi * Complex.I * ↑x) ^ n • FourierTransform.fourier f x
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.rankFinite : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → (M.restrict X).RankFinite
-- Mathlib.Data.Multiset.AddSub
Multiset.add_assoc : ∀ {α : Type u_1} (s t u : Multiset α), s + t + u = s + (t + u)
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_nonneg : ∀ {a : ℕ → ℂ} {n : ℕ}, 0 ≤ a n → ∀ (x : ℝ), 0 ≤ LSeries.term a (↑x) n
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.conj' : ∀ {A : Type u} {inst : AddGroup A} [self : AddGroupFilterBasis A] (x₀ : A) {U : Set A},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → {f g : a ⟶ b} → (f ≅ g) → CategoryTheory.BicategoricalCoherence f g
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁_D₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂),
  CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') =
    -CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.ofHom_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G),
  ↑(CochainComplex.HomComplex.Cocycle.ofHom φ) = CochainComplex.HomComplex.Cochain.ofHom φ
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_comp : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {M'' : Type u_1}
  [inst_8 : AddCommGroup M''] [inst_9 : Module R M''] [inst_10 : LieRingModule L M''] {g : M' →ₗ⁅R,L⁆ M''},
  LieSubmodule.map (g.comp f) N = LieSubmodule.map g (LieSubmodule.map f N)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instHashableRequestID : Hashable Lean.JsonRpc.RequestID
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.sum_fin : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → ∀ {n : ℕ} {p : Polynomial R}, p.degree < ↑n → ∑ i, f (↑i) (p.coeff ↑i) = p.sum f
-- Mathlib.Analysis.Complex.Basic
RCLike.im_eq_complex_im : ⇑RCLike.im = Complex.im
-- Init.Data.Array.Erase
Array.erase_eq_eraseP' : ∀ {α : Type u_1} [inst : BEq α] (a : α) (xs : Array α), xs.erase a = xs.eraseP fun x => x == a
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instReprError : Repr Std.Internal.Parsec.Error
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_ge_max : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  max (cs.length w₁ - cs.length w₂) (cs.length w₂ - cs.length w₁) ≤ cs.length (w₁ * w₂)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq.inj : ∀ {x : Int.Internal.Linear.Var} {c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {x_1 : Int.Internal.Linear.Var}
  {c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq x c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq x_1 c_1 →
    x = x_1 ∧ c = c_1
-- Mathlib.Order.Nucleus
Nucleus.instHeytingAlgebra : {X : Type u_1} → [inst : Order.Frame X] → HeytingAlgebra (Nucleus X)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_eq_sum_card_fiberwise : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq M] {f : ι → M} {s : Finset ι} {t : Finset M},
  Set.MapsTo f ↑s ↑t → s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α], LawfulSingleton (α × β) (Std.HashMap.Raw α β)
-- Init.Data.List.Basic
List.rotateRight_nil : ∀ {α : Type u} {n : ℕ}, [].rotateRight n = []
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → ∀ {h' : k' ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l).getKey k' h' = k
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_exp_log : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)}, x ≤ WithZero.exp x.log
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsBigOWith` over a `Homeomorph`.  -/
Homeomorph.isBigOWith_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ},
  Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppEquivDFinsupp_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.tensor_unit_d₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (i₁ i₂ j : I),
  HomologicalComplex.mapBifunctor.d₂ K (HomologicalComplex.tensorUnit C c)
      (CategoryTheory.MonoidalCategory.curriedTensor C) c i₁ i₂ j =
    0
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The inverse of an equivalence between measurable spaces.  -/
MeasurableEquiv.symm : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → α ≃ᵐ β → β ≃ᵐ α
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_mul_left_left : ∀ (a b c : ℤ), a.lcm b ∣ (c * a).lcm b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
one_le_zpow : ∀ {G : Type u_2} [inst : DivInvMonoid G] [inst_1 : Preorder G] [MulLeftMono G] {x : G},
  1 ≤ x → ∀ {n : ℤ}, 0 ≤ n → 1 ≤ x ^ n
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.isCoboundedUnder_ge : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι}
  {u : ι → α} {a : α} [f.NeBot], Filter.Tendsto u f (nhds a) → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_sup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] {s t : ClosedSubmodule R N},
  ↑(s ⊔ t) = closure (↑s ⊔ ↑t).carrier
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.takeWhile_prop_eq_takeWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.takeWhile p = s.takeWhile fun x => decide (p x)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_succ? : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
-- Mathlib.NumberTheory.MulChar.Basic
/-- When the domain has a zero, then the inverse of a multiplicative character `χ`,
applied to `a`, is `χ` applied to the inverse of `a`.  -/
MulChar.inv_apply' : ∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommGroupWithZero R] (χ : MulChar R R')
  (a : R), χ⁻¹ a = χ a⁻¹
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_True : Set.Iic True = Set.univ
-- Mathlib.Order.SuccPred.Basic
WithBot.orderSucc_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α], Order.succ ⊥ = ↑⊥
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).I₀) (j : (self.𝒰X i).I₀),
  AlgebraicGeometry.IsAffine ((self.𝒰X i).X j)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.norm.eq_1 : ∀ (e : Lean.Grind.Linarith.Expr), e.norm = e.toPoly'.norm
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.tactic.simp.user.exampleInt : Lean.Option ℤ
-- Mathlib.Order.SuccPred.Basic
OrderIso.map_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : PartialOrder β]
  [inst_3 : PredOrder β] (f : α ≃o β) (a : α), f (Order.pred a) = Order.pred (f a)
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
PiLp.contDiff_ofLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  {p : ENNReal} [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞}, ContDiff 𝕜 n WithLp.ofLp
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Note: the assumption `IsFiniteMeasureOnCompacts μ` cannot be removed. For example, if
`μ` is infinite on any nonempty set and `ν = 0`, then the hypotheses are satisfied.  -/
RealRMK.measure_le_of_isCompact_of_integral : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [BorelSpace X]
  {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [ν.OuterRegular] [MeasureTheory.IsFiniteMeasureOnCompacts ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  (∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν) →
    ∀ ⦃K : Set X⦄, IsCompact K → μ K ≤ ν K
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_ndunion : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (s₁ s₂ : Multiset α),
  (s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid (Lex α)
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.cdf_expMeasure_eq_lintegral : ∀ {r : ℝ},
  0 < r →
    ∀ (x : ℝ),
      ↑(ProbabilityTheory.cdf (ProbabilityTheory.expMeasure r)) x =
        (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDF r x).toReal
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WPMonad.toLawfulMonad : ∀ {m : Type u → Type v} {Pred : outParam (Type w)} {EPred : outParam (Type w')} {inst : Monad m}
  {inst_1 : Std.Internal.Do.Assertion Pred} {inst_2 : Std.Internal.Do.Assertion EPred}
  [self : Std.Internal.Do.WPMonad m Pred EPred], LawfulMonad m
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.jacobson_eq_nilradical_of_krullDimLE_zero : ∀ (R : Type u_3) [inst : CommRing R] [Ring.KrullDimLE 0 R], Ring.jacobson R = nilradical R
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An internal equivalence relation in the category of types gives rise to a standard equivalence
relation.  -/
TypeCat.equivalence_of_equivalenceRelation : ∀ {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.EquivalenceRelation p₁ p₂), Equivalence (TypeCat.Rel.ofPair p₁ p₂)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.uset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.FVarId) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9),
  sizeOf (Lean.Compiler.LCNF.Code.uset fvarId i y k h) = 1 + sizeOf fvarId + sizeOf i + sizeOf y + sizeOf k + sizeOf h
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B C_1 : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  (f : A ⟶ B) (g : B ⟶ C_1) {Z : C} (h : C_1.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h =
    CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h)
-- Mathlib.MeasureTheory.Measure.Real
/-- If two sets `s` and `t` are included in a set `u` of finite measure,
and `μ.real s + μ.real t > μ.real u`, then `s` intersects `t`.
Version assuming that `s` is measurable.  -/
MeasureTheory.nonempty_inter_of_measureReal_lt_add' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasurableSet s →
    s ⊆ u →
      t ⊆ u →
        μ.real u < μ.real s + μ.real t →
          autoParam (μ u ≠ ⊤) MeasureTheory.nonempty_inter_of_measureReal_lt_add'._auto_1 → (s ∩ t).Nonempty
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.instInhabitedOpenCover : {X : AlgebraicGeometry.Scheme} → Inhabited X.OpenCover
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.objMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  CategoryTheory.SmallObject.objMap I κ (CategoryTheory.CategoryStruct.id f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.obj I κ f.hom)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.right_inv : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)] {x : B × F₁ × F₂},
  x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ →
    Bundle.Trivialization.Prod.toFun' e₁ e₂ (Bundle.Trivialization.Prod.invFun' e₁ e₂ x) = x
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- The key lemma for Poisson summation: the `m`-th Fourier coefficient of the periodic function
`∑' n : ℤ, f (x + n)` is the value at `m` of the Fourier transform of `f`.  -/
Real.fourierCoeff_tsum_comp_add : ∀ {f : C(ℝ, ℂ)},
  (∀ (K : TopologicalSpace.Compacts ℝ),
      Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖) →
    ∀ (m : ℤ), fourierCoeff ⋯.lift m = FourierTransform.fourier ⇑f ↑m
-- Lean.DocString.Types
Lean.Doc.DescItem.mk : {α : Type u} → {β : Type v} → Array α → Array β → Lean.Doc.DescItem α β
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk.injEq : ∀ {ι : Type u_2} (lower upper : ι → ℝ) (lower_lt_upper : ∀ (i : ι), lower i < upper i) (lower_1 upper_1 : ι → ℝ)
  (lower_lt_upper_1 : ∀ (i : ι), lower_1 i < upper_1 i),
  ({ lower := lower, upper := upper, lower_lt_upper := lower_lt_upper } =
      { lower := lower_1, upper := upper_1, lower_lt_upper := lower_lt_upper_1 }) =
    (lower = lower_1 ∧ upper = upper_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- Let `F` be a functor from the category of sheaves of `R`-modules to sheaves of `S`-modules.
If `F` preserves coproducts and `unit S ≅ F.obj (unit R)`, then `F` preserves free sheaves of
modules.  -/
SheafOfModules.mapFreeIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                          (I : Type u) →
                            [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] →
                              (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) →
                                (SheafOfModules.free I ≅ F.obj (SheafOfModules.free I))
-- Init.Data.Nat.Lcm
Nat.lcm_eq_right : ∀ {m n : ℕ}, m ∣ n → m.lcm n = n
-- Lean.Server.ServerTask
Lean.Server.ServerTask.BaseIO.bindTaskCostly : {α : Type u_1} →
  {β : Type} → Lean.Server.ServerTask α → (α → BaseIO (Lean.Server.ServerTask β)) → BaseIO (Lean.Server.ServerTask β)