mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurrySum_add : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)]
  (g₁ g₂ : MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)),
  (g₁ + g₂).uncurrySum = g₁.uncurrySum + g₂.uncurrySum
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`.  -/
MulEquiv.toAdditiveLeft : {G : Type u_2} →
  {H : Type u_3} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → G ≃* Multiplicative H ≃ (Additive G ≃+ H)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.calc_norm_le_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ∀ {n : ℕ} {z : ℤ_[p]},
      ih_gen✝ n z → ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
-- Mathlib.NumberTheory.LSeries.RiemannZeta
completedRiemannZeta_eq : ∀ (s : ℂ), completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget₂_map_homMk : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ :
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶
      (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N)
  (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ),
  (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map (ModuleCat.homMk φ hφ) = φ
-- Mathlib.Analysis.Complex.OpenMapping
Complex.isOpenQuotientMap_zpow_compl_zero : ∀ (n : ℤ) [NeZero n], IsOpenQuotientMap fun z => ⟨↑z ^ n, ⋯⟩
-- Mathlib.RingTheory.TensorProduct.Basic
SemiconjBy.tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B},
  SemiconjBy a₁ a₂ a₃ → SemiconjBy b₁ b₂ b₃ → SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.isNilpotent_of_finite_tfae`.

---

A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are
normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow
groups.  -/
isNilpotent_of_finite_tfae : ∀ {G : Type u_1} [hG : Group G] [Finite G],
  [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
-- Init.Data.SInt.Lemmas
ISize.le_antisymm : ∀ {a b : ISize}, a ≤ b → b ≤ a → a = b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- Let `t i` be a countable covering of `α` by measurable sets. Let `f i : t i → β` be a family of
functions that agree on the intersections `t i ∩ t j`. Then the function `Set.liftCover t f _ _`,
defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable.  -/
measurable_liftCover : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι]
  (t : ι → Set α),
  (∀ (i : ι), MeasurableSet (t i)) →
    ∀ (f : (i : ι) → ↑(t i) → β),
      (∀ (i : ι), Measurable (f i)) →
        ∀ (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
          (htU : ⋃ i, t i = Set.univ), Measurable (Set.liftCover t f hf htU)
-- Batteries.Data.String.Lemmas
String.utf8GetAux?_of_valid : ∀ (cs cs' : List Char) {i p : ℕ},
  i + String.utf8Len cs = p → String.Pos.Raw.utf8GetAux? (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.head?
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
/-- An approximate subgroup in a group is a symmetric set `A` containing the identity and such that
`A + A` can be covered by a small number of translates of `A`.

In practice, we will take `K` fixed and `A` large but finite.
 -/
IsApproximateAddSubgroup : {G : Type u_2} → [AddGroup G] → ℝ → Set G → Prop
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top : ∀ {ι : Type u_1} [inst : Fintype ι] {I J : BoxIntegral.Box ι} (l : BoxIntegral.IntegrationParams) (h : I ≤ J),
  Filter.Tendsto (⇑(BoxIntegral.TaggedPrepartition.embedBox I J h)) (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤)
    (BoxIntegral.IntegrationParams.toFilteriUnion J (BoxIntegral.Prepartition.single J I h))
-- Init.Prelude
/-- The only element of the unit type.

It can be written as an empty tuple: `()`.
 -/
Unit.unit : Unit
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The action of `alternatingGroup α` on `Set.powersetCard α n` is preprimitive
provided `1 ≤ n < Nat.card α` and `Nat.card α ≠ 2 * n`.  -/
Set.powersetCard.isPreprimitive_alternatingGroup : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ},
  3 ≤ n → n < Nat.card α → Nat.card α ≠ 2 * n → MulAction.IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α n)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isBigO_logb_mul_const_log_atTop : ∀ {b : ℝ} (c : ℝ), (fun x => Real.logb b (x * c)) =O[Filter.atTop] Real.log
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousOn.isBigO_rev_principal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace α] {s : Set α} {f : α → E}
  [inst_1 : NormedAddGroup E] [inst_2 : SeminormedAddGroup F],
  ContinuousOn f s → IsCompact s → (∀ i ∈ s, f i ≠ 0) → ∀ (c : F), (fun x => c) =O[Filter.principal s] f
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} →
          (toNatTrans : CategoryTheory.NatTrans F.toFunctor G.toFunctor) →
            autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a))
                CategoryTheory.BasedNatTrans.isHomLift'._autoParam →
              CategoryTheory.BasedNatTrans F G
-- Mathlib.Data.Nat.Nth
Nat.filter_range_nth_eq_insert : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {k : ℕ},
  (∀ (hf : (Set.ofPred p).Finite), k + 1 < hf.toFinset.card) →
    {n ∈ Finset.range (Nat.nth p (k + 1)) | p n} = insert (Nat.nth p k) ({n ∈ Finset.range (Nat.nth p k) | p n})
-- Mathlib.Algebra.Divisibility.Basic
pow_dvd_pow_of_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ n
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Closed immersions are locally of finite type.  -/
AlgebraicGeometry.instLocallyOfFiniteTypeOfIsClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Lean.Structure
/-- Returns the name of the auxiliary definition that defines a default value for the field, if any such definition exists.
This is *not* an inherited default. We need to store provided defaults so that it is possible to resolve defaults according to the resolution order.
 -/
Lean.getDefaultFnForField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cycles_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {A : C} (f₁ f₂ : A ⟶ S.cycles),
  CategoryTheory.CategoryStruct.comp f₁ S.iCycles = CategoryTheory.CategoryStruct.comp f₂ S.iCycles → f₁ = f₂
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instNonemptyElemForall : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X] [IsOrderedRing S]
  [Nonempty X], Nonempty ↑(stdSimplex S X)
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.smul : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : Zero β]
  [inst_2 : SMulZeroClass 𝕜 β] [ContinuousConstSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜),
  l.ZeroAtFilter f → l.ZeroAtFilter (c • f)
-- Init.Data.Array.Int
Array.min_le_sum_div_length_int : ∀ {xs : Array ℤ} (h : xs ≠ #[]), xs.min h ≤ xs.sum / ↑xs.size
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The short complex `(G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A)` is isomorphic to the 2nd
short complex associated to the complex of inhomogeneous chains of `A`.  -/
groupHomology.isoShortComplexH2 : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 2 ≅ groupHomology.shortComplexH2 A
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Given an equivalence `e : L ≃ₐ[K] L'` of `K`-field extensions and an intermediate
field `E` of `L/K`, `intermediateFieldMap e E` is the induced equivalence
between `E` and `E.map e`.  -/
IntermediateField.intermediateFieldMap : {K : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] →
            [inst_3 : Algebra K L] →
              [inst_4 : Algebra K L'] →
                (e : L ≃ₐ[K] L') → (E : IntermediateField K L) → ↥E ≃ₐ[K] ↥(IntermediateField.map (↑e) E)
-- Mathlib.Probability.Independence.Kernel.Indep
/-- Two measurable space structures (or σ-algebras) `m₁, m₂` are independent with respect to a
kernel `κ` and a measure `μ` if for any sets `t₁ ∈ m₁, t₂ ∈ m₂`,
`∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)`  -/
ProbabilityTheory.Kernel.Indep : {α : Type u_1} →
  {Ω : Type u_2} →
    {_mα : MeasurableSpace α} →
      MeasurableSpace Ω →
        MeasurableSpace Ω →
          {_mΩ : MeasurableSpace Ω} →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.Indep._auto_1 → Prop
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioc_disjoint_Ioc_of_le : ∀ {α : Type v} [inst : Preorder α] {a b c d : α}, b ≤ c → Disjoint (Set.Ioc a b) (Set.Ioc c d)
-- Mathlib.Logic.Relation
Relation.EqvGen.reflTransGen_symmGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.ReflTransGen (Relation.SymmGen r) = Relation.EqvGen r
-- Mathlib.Topology.Defs.Basic
IsClosed.mk : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen sᶜ → IsClosed s
-- Init.NotationExtra
unexpandGetElem? : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitorEquivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.leftUnitorEquivalence C).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.prod.leftInverseUnitor C).comp (CategoryTheory.prod.leftUnitor C))
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → ∀ {g₁ g₂ : β → δ}, g₁ =ᵐ[μb] g₂ → g₁ ∘ f =ᵐ[μa] g₂ ∘ f
-- Mathlib.Order.Heyting.Basic
hnot_hnot_sdiff_distrib : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : α), ￢￢(b \ a) = ￢￢b \ ￢￢a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : Option β → Option β) (l : List ((_ : α) × β)),
  Std.Internal.List.Const.alterKey k f l =
    match f (Std.Internal.List.getValue? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Raw.Const.modify t k f},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.modify t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then f (Std.DTreeMap.Raw.Const.get t k ⋯) else Std.DTreeMap.Raw.Const.get t k' ⋯
-- Std.Internal.Parsec.String
/-- Convert a byte representing `'0'..'9'` to a `Nat`.
 -/
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.digitToNat : Char → ℕ
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- If a net of upper hemicontinuous set-valued functions converges uniformly
(along a filter `l`) in the Hausdorff uniformity to a set-valued function `f` with
compact values, then `f` is upper hemicontinuous  -/
TendstoUniformly.upperHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {ι : Type u_3} {F : ι → α → Set β}
  {l : Filter ι} [l.NeBot] [inst_2 : UniformSpace β],
  TendstoUniformly F f l → (∀ (n : ι), UpperHemicontinuous (F n)) → (∀ (x : α), IsCompact (f x)) → UpperHemicontinuous f
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- If a monic polynomial `p : R[X]` factors into a product of coprime monic polynomials `p = f * g`
in the residue field `κ(P)` of some `P : Spec R`,
then there exists `Q : Spec R_univ` in the universal coprime factorization ring lying over `P`,
such that `κ(P) = κ(Q)` and `f` and `g` are the image of the universal factors.  -/
Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n) (P : Ideal R)
  [inst_1 : P.IsPrime] (f : Polynomial.MonicDegreeEq P.ResidueField m) (g : Polynomial.MonicDegreeEq P.ResidueField k),
  Polynomial.map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g →
    IsCoprime ↑f ↑g →
      ∃ Q,
        ∃ (x : Q.IsPrime) (x_1 : Q.LiesOver P),
          Function.Bijective
              ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (Polynomial.UniversalCoprimeFactorizationRing m k hn p))
                  ⋯) ∧
            f.map
                  (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (Polynomial.UniversalCoprimeFactorizationRing m k hn p))
                      ⋯).toRingHom =
                (Polynomial.UniversalCoprimeFactorizationRing.factor₁ m k hn p).map
                  (algebraMap (Polynomial.UniversalCoprimeFactorizationRing m k hn p) Q.ResidueField) ∧
              g.map
                  (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (Polynomial.UniversalCoprimeFactorizationRing m k hn p))
                      ⋯).toRingHom =
                (Polynomial.UniversalCoprimeFactorizationRing.factor₂ m k hn p).map
                  (algebraMap (Polynomial.UniversalCoprimeFactorizationRing m k hn p) Q.ResidueField)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.mk : Lean.Meta.KExprMap ℕ → Array Lean.Expr → Lean.Meta.Simp.Arith.Nat.ToLinear.State
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  K.toSubmodule = ⊥ ↔ K = ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((a : α) × β a)} {x : (a : α) × β a}
  (h : x ∈ l), Std.Internal.List.DistinctKeys l → Std.Internal.List.getEntry x.fst l ⋯ = x
-- Init.Data.Array.MinMax
Array.max?_replicate_of_pos : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {n : ℕ} {a : α}, 0 < n → (Array.replicate n a).max? = some a
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.one_le_mul_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  (∀ (x : α), 1 ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Std.Http.Protocol.H1.Writer
/-- Waiting for the application to provide the outgoing message head via `send`.
 -/
Std.Http.Protocol.H1.Writer.State.waitingHeaders : Std.Http.Protocol.H1.Writer.State
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Iio : ∀ {n : ℕ} (i : Fin n), Finset.map (Fin.succEmb n) (Finset.Iio i) = Finset.Ioo 0 i.succ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsLieTowerSubtypeMem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {M : Type w} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M], IsLieTower (↥L') L M
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapId_inv_app : ∀ (I : Type w₀) (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I),
  (CategoryTheory.Pi.comapId I C).inv.app X i = CategoryTheory.CategoryStruct.id X i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a subtraction monoid under pointwise operations if `α` is.  -/
Finset.subtractionMonoid : {α : Type u_2} → [DecidableEq α] → [SubtractionMonoid α] → SubtractionMonoid (Finset α)
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s s_1 : AffineSubspace ℝ P) (e_s : s = s_1) [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] (p p_1 : P), p = p_1 → s.signedInfDist p = s_1.signedInfDist p_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT : ∀ (N : Type u_2) [inst : Mul N] [IsLeftCancelMul N] [inst_2 : PartialOrder N] [MulLeftReflectLT N], MulLeftReflectLE N
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A category with cofibrations is a category equipped with
a class of morphisms named "cofibrations".  -/
HomotopicalAlgebra.CategoryWithCofibrations : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Data.List.Sublists
List.sublists'_reverse : ∀ {α : Type u} (l : List α), l.reverse.sublists' = List.map List.reverse l.sublists
-- Mathlib.Tactic.Set
Mathlib.Tactic.setArgsRest : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.«term_⟶ᵐ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Dual to `Monad.CreatesColimitOfIsSplitPair`.  -/
CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Type (max (max u₁ u₂) v₁)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.add_right_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α},
  μ.MutuallySingular (ν₁ + ν₂) ↔ μ.MutuallySingular ν₁ ∧ μ.MutuallySingular ν₂
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.mixedEmbedding.covolume_integerLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ZLattice.covolume (NumberField.mixedEmbedding.integerLattice K) MeasureTheory.volume =
    2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.discr K)|
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions as continuous functions vanishing at infinity.  -/
SchwartzMap.toZeroAtInfty : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] → [ProperSpace E] → SchwartzMap E F → ZeroAtInftyContinuousMap E F
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.ordered : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'}, t.SameKeys t' → t.Ordered → t'.Ordered
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNatClamp_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.Data.List.MinMax
List.le_of_mem_argmin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {a m : α},
  a ∈ l → m ∈ List.argmin f l → f m ≤ f a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkEMatchEqBwdTheoremCore : Lean.Meta.Grind.Origin → Array Lean.Name → Lean.Expr → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Util.Export
Lean.Export.Entry.level.sizeOf_spec : ∀ (n : Lean.Level), sizeOf (Lean.Export.Entry.level n) = 1 + sizeOf n
-- Mathlib.Analysis.Analytic.Uniqueness
/-- The *identity principle* for analytic functions: If two analytic functions on a normed space
coincide in a neighborhood of a point `z₀`, then they coincide everywhere.
For a one-dimensional version assuming only that the functions coincide at some points
arbitrarily close to `z₀`, see `AnalyticOnNhd.eq_of_frequently_eq`.  -/
AnalyticOnNhd.eq_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  [PreconnectedSpace E], AnalyticOnNhd 𝕜 f Set.univ → AnalyticOnNhd 𝕜 g Set.univ → ∀ {z₀ : E}, f =ᶠ[nhds z₀] g → f = g
-- Mathlib.Tactic.DeriveTraversable
/-- derive the `traverse` definition of a `Traversable` instance  -/
Mathlib.Deriving.Traversable.mkTraverse : Lean.Name → Lean.MVarId → Lean.Elab.TermElabM Unit
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_modifyGet : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s : σ) (f : σ → α × σ),
  (do
      set s
      modifyGet f) =
    do
    set (f s).2
    pure (f s).1
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.hasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}
  [CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Subobject X)
-- Mathlib.Analysis.Convex.Join
convexJoin_subset : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t u : Set E}, s ⊆ u → t ⊆ u → Convex 𝕜 u → convexJoin 𝕜 s t ⊆ u
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.del : {β : Type u} → {α : Type v} → Array ℕ → Std.Tactic.BVDecide.LRAT.Action β α
-- Lean.Meta.Basic
/-- Zeta reduction: `let x := v; e[x]` and `have x := v; e[x]` reduce to `e[v]`.
We say a let-declaration `let x := v; e` is nondependent if it is equivalent to `(fun x => e) v`.
Recall that
```
fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
```
is type correct, but
```
fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
```
is not.
See also `zetaHave`, for disabling the reduction nondependent lets (`have` expressions).
 -/
Lean.Meta.Config.zeta : Lean.Meta.Config → Bool
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Consider the differential of the inclusion of the sphere in `E` at the point `v` as a continuous
linear map from `TangentSpace (𝓡 n) v` to `E`.  The range of this map is the orthogonal complement
of `v` in `E`.
 -/
range_mvfderiv_subtypeVal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), (↑(d% Subtype.val v)).range = (ℝ ∙ ↑v)ᗮ