mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isEmbedding_toUniformOnFun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F], Topology.IsEmbedding ContinuousMultilinearMap.toUniformOnFun
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  (∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e) →
    HasFPowerSeriesAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
rank_lt_rank_dual' : ∀ {K : Type u} [inst : DivisionRing K] {V : Type u} [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2_T : EisensteinSeries.D2 ModularGroup.T = 0
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.modify₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {f : β a → β a} (a_1 : m.WF),
  Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The image of `m/s` under `liftOfLE` is `m/s`.  -/
IsLocalizedModule.liftOfLE_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_7}
  {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂] (m : M) (s : ↥S₁),
  (IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂) (IsLocalizedModule.mk' f₁ m s) = IsLocalizedModule.mk' f₂ m ⟨↑s, ⋯⟩
-- Init.Data.BitVec.Lemmas
BitVec.xor_assoc : ∀ {w : ℕ} (x y z : BitVec w), x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y Z T : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W X Z]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X T]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Z]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W Y T]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W Z T] (α : CategoryTheory.Localization.SmallHom W X Y)
  (β : CategoryTheory.Localization.SmallHom W Y Z) (γ : CategoryTheory.Localization.SmallHom W Z T),
  (α.comp β).comp γ = α.comp (β.comp γ)
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.nsmul_eq_nsmul_iff_modEq : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {x : G} {m n : ℕ}, n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_compl_left_iff_subset : ∀ {α : Type u_1} {s t : Set α}, Disjoint sᶜ t ↔ t ⊆ s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? (pref.size + 1) r.lower).get ⋯
-- Mathlib.NumberTheory.SiegelsLemma
Int.Matrix.exists_ne_zero_int_vec_norm_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ),
  Fintype.card α < Fintype.card β →
    0 < Fintype.card α →
      ∃ t,
        t ≠ 0 ∧
          A.mulVec t = 0 ∧
            ‖t‖ ≤ (↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.InstMap.pHashSetSize : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashSet α → ℕ
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.exists_cartanMatrix_diagaonal_mul_posDef : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [inst_9 : DecidableEq ι] [P.IsRootSystem],
  ∃ d, (∀ (i : ↥b.support), 0 < d i) ∧ (Matrix.diagonal d * b.cartanMatrix).PosDef
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is uniformly equicontinuous on a subset if the
family `(↑) : ↥H → (X → α)` is uniformly equicontinuous on that subset.  -/
Set.UniformEquicontinuousOn : {α : Type u_6} → {β : Type u_8} → [uα : UniformSpace α] → [uβ : UniformSpace β] → Set (β → α) → Set β → Prop
-- Mathlib.Data.Finset.Fin
Finset.map_valEmbedding_attachFin : ∀ {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n), Finset.map Fin.valEmbedding (s.attachFin h) = s
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- The `L`-series of a modular form (without its Archimedean `Γ`-factor).  -/
ModularForm.L : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.IsArithmetic] →
    {k : ℤ} → 0 < k → {F : Type u_1} → [inst : FunLike F UpperHalfPlane ℂ] → F → [ModularFormClass F Γ k] → ℂ → ℂ
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- If `μ` is an additive Haar measure on a normed space `E`,
then `μ.toSphere` is the measure on the unit sphere in `E`
such that `μ.toSphere s = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s)`.  -/
MeasureTheory.Measure.toSphere : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] → MeasureTheory.Measure E → MeasureTheory.Measure ↑(Metric.sphere 0 1)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_insert_of_notMem : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  a ∉ s → ((insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e),
  (CategoryTheory.CostructuredArrow.preEquivalence F f).functor =
    CategoryTheory.CostructuredArrow.preEquivalence.functor F f
-- Mathlib.Order.OrderDual
OrderDual.instUnique : {α : Type u_1} → [h : Unique α] → Unique αᵒᵈ
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.toGradedMonoid : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} {inst : DecidableEq ι} {inst_1 : AddMonoid ι} {inst_2 : Semiring A}
  {inst_3 : SetLike σ A} {inst_4 : AddSubmonoidClass σ A} {𝒜 : ι → σ} [self : GradedRing 𝒜], SetLike.GradedMonoid 𝒜
-- Mathlib.CategoryTheory.Shift.Pullback
/-- This expresses the compatibility between two `CommShift` structures by `A` on (synonyms of)
`𝟭 C`: the canonical `CommShift` structure on `𝟭 (PullbackShift C φ)`, and the `CommShift`
structure on `PullbackShift.functor (𝟭 C) φ` (i.e the pullback of the canonical `CommShift`
structure on `𝟭 C`).
 -/
CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B),
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.PullbackShift.natIsoId C φ).hom A
-- Mathlib.Topology.Order.LeftRightLim
rightLim_eq_of_not_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
  [h'α : OrderTopology α] (f : α → β) {a : α},
  (¬∃ y, Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds y)) → Function.rightLim f a = f a
-- Mathlib.Order.WithBot
WithTop.untop_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α} (hx : x ≠ ⊤), x.untop hx ≤ a ↔ x ≤ ↑a
-- Mathlib.Tactic.ReduceModChar
/-- A `TypeToCharPResult α` indicates if `α` can be determined to be a ring of characteristic `p`.
 -/
Tactic.ReduceModChar.TypeToCharPResult : {u : Lean.Level} → Q(Type u) → Type
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.mul.eq_4 : ∀ {n : ℕ} (a b : ZMod (2 * n)),
  QuaternionGroup.mul✝ (QuaternionGroup.xa a) (QuaternionGroup.xa b) = QuaternionGroup.a (↑n + b - a)
-- Mathlib.Analysis.InnerProductSpace.Calculus
differentiableWithinAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [Finite ι],
  DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (f x).ofLp i) t y
-- Mathlib.RingTheory.ClassGroup.Basic
/-- Send a nonzero fractional ideal to the corresponding class in the class group.  -/
ClassGroup.mk : {R : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] → [inst_4 : IsDomain R] → (FractionalIdeal (nonZeroDivisors R) K)ˣ →* ClassGroup R
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop' : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} {l : Filter β},
  Filter.Tendsto f Filter.atTop l ↔ ∀ s ∈ l, ∃ a, ∀ (b : α), a ≤ b → f b ∈ s
-- Mathlib.Order.SetDissipate
Set.dissipate_eq_biInter_lt : ∀ {β : Type u_2} {s : ℕ → Set β} {n : ℕ}, Set.dissipate s n = ⋂ k, ⋂ (_ : k < n + 1), s k
-- Mathlib.GroupTheory.GroupAction.Hom
Pi.evalAddActionHom.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → VAdd M (X i)] (i : ι),
  Pi.evalAddActionHom i = { toFun := Function.eval i, map_vadd' := ⋯ }
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.Embedding.toElementaryEmbedding_toFun : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N)
  (htv :
    ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
      φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b)))
  (a : M), (f.toElementaryEmbedding htv) a = f a
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {x y : D₁.Hom D₂}, x.hom = y.hom → x = y
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.isEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ≌ D), F.inverse.IsEquivalence
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.krullDimLE_one_iff_of_noZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R],
  Ring.KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getKeyArgs : Lean.Expr → Bool → Bool → Lean.MetaM (Lean.Meta.DiscrTree.Key × Array Lean.Expr)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
is in the `AddSubmonoid`.  -/
sum_mem : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : SetLike B M] [AddSubmonoidClass B M]
  {ι : Type u_5} {t : Finset ι} {f : ι → M}, (∀ c ∈ t, f c ∈ S) → ∑ c ∈ t, f c ∈ S
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite ν] {s : Set α}, MeasurableSet s → (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)
-- Batteries.Data.Nat.Lemmas
Nat.casesDiagOn_zero_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive (m + 1) (n + 1)),
  Nat.casesDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- A (limit) cokernel cofork of the differential on the `r`th page whose point
identifies to an object `X.E`  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq pq' : κ) →
                            (i₀ i₁ i₂ i₃ i₃' : ι) →
                              i₀ = data.i₀ r pq' ⋯ →
                                i₁ = data.i₁ pq' →
                                  i₂ = data.i₂ pq' →
                                    i₃ = data.i₃ r pq' ⋯ →
                                      i₃' = data.i₃ r' pq' ⋯ →
                                        (n₀ n₁ n₂ : ℤ) →
                                          n₁ = data.deg pq' →
                                            autoParam (n₀ + 1 = n₁)
                                                CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc._auto_1 →
                                              autoParam (n₁ + 1 = n₂)
                                                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc._auto_3 →
                                                CategoryTheory.Limits.CokernelCofork
                                                  ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r
                                                        hr).d
                                                    pq pq')
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
CategoryTheory.LocalizerMorphism.Derives.isRightDerivedFunctor_of_isIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₂ : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {F : CategoryTheory.Functor C₂ H},
  Φ.Derives F →
    ∀ [Φ.IsRightDerivabilityStructure] {L₂ : CategoryTheory.Functor C₂ D₂} [inst_5 : L₂.IsLocalization W₂]
      {RF : CategoryTheory.Functor D₂ H} (α : F ⟶ L₂.comp RF),
      (∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (Φ.functor.obj X₁))) → RF.IsRightDerivedFunctor α W₂
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.rename_isHomogeneous : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {f : σ → τ},
  φ.IsHomogeneous n → ((MvPolynomial.rename f) φ).IsHomogeneous n
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.inductionOn₃ : ∀ {motive : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2})
  (c₃ : Cardinal.{u_3}),
  (∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), motive (Cardinal.mk α) (Cardinal.mk β) (Cardinal.mk γ)) →
    motive c₁ c₂ c₃
-- Init.Data.Int.Lemmas
Int.natCast_one : ↑1 = 1
-- Lean.Parser.Term
/-- `let (eq := h) x := v; ...` adds the equality `h : x = v` to the context while elaborating the body.
 -/
Lean.Parser.Term.letOptEq : Lean.Parser.Parser
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.totalDegree_coeff_optionEquivLeft_le : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (p : MvPolynomial (Option S₁) R) (i : ℕ),
  (((MvPolynomial.optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree
-- Init.Grind.PP
Lean.Grind.NodeDef.unit : NodeDef
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.IsUniform.mono : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α} {ε' : 𝕜}, ε ≤ ε' → G.IsUniform ε s t → G.IsUniform ε' s t
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.M : Type → Type
-- Mathlib.Lean.Meta.KAbstractPositions
/-- Return the positions that `kabstract` would abstract for pattern `p` in expression `e`.
i.e. the positions that unify with `p`.  -/
Lean.Meta.kabstractPositions : Lean.Expr → Lean.Expr → Lean.MetaM (Array Lean.SubExpr.Pos)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cardinalMk_le_isBase : ∀ {α : Type u} {M : Matroid α} {I B : Set α} [M.InvariantCardinalRank],
  M.Indep I → M.IsBase B → Cardinal.mk ↑I ≤ Cardinal.mk ↑B
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- Quantitative result associated to the direct comparison test for series:  If, for all `i`,
`‖f i‖ₑ ≤ g i`, then `‖∑' i, f i‖ₑ ≤ ∑' i, g i`. Note that we do not assume that `∑' i, f i` is
summable, and it might not be the case if `α` is not a complete space.  -/
tsum_of_enorm_bounded : ∀ {ι : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] {f : ι → ε}
  {g : ι → ENNReal} {a : ENNReal}, HasSum g a → (∀ (i : ι), ‖f i‖ₑ ≤ g i) → ‖∑' (i : ι), f i‖ₑ ≤ a
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instContinuousAdd : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  ContinuousAdd (MeasureTheory.FiniteMeasure Ω)
-- Init.Data.List.Nat.Range
List.zipIdx_singleton : ∀ {α : Type u_1} {x : α} {k : ℕ}, [x].zipIdx k = [(x, k)]
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.id_comp : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G), ApplicativeTransformation.idTransformation.comp η = η
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (h : e.source = Set.univ) (h' : e.target = Set.univ), ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- morphisms  -/
CategoryTheory.CoreSmallCategoryOfSet.hom : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.CoreSmallCategoryOfSet Ω C) → ↑self.obj → ↑self.obj → Set Ω
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} {n : ℕ}, a ≡ b [PMOD p] → n • a ≡ n • b [PMOD n • p]
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_limRatio : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds (v.limRatio ρ x))
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.surjective_χ`. -/
CategoryTheory.Classifier.surjective_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω), ∃ Z i, ∃ (x : CategoryTheory.Mono i), φ = 𝒞.χ i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α},
  a ∈ m ↔ m.contains a = true
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.cycle_zpow_mem_support_iff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  g.IsCycle → ∀ {n : ℤ} {x : α}, g x ≠ x → ((g ^ n) x = x ↔ n % ↑g.support.card = 0)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.monoidalCategoryStruct.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit),
  CategoryTheory.Localization.Monoidal.monoidalCategoryStruct L W ε =
    { tensorObj := fun X Y => ((CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).obj X).obj Y,
      whiskerLeft := fun X x x_1 g => ((CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).obj X).map g,
      whiskerRight := fun {X₁ X₂} f Y => ((CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).map f).app Y,
      tensorUnit := unit,
      associator := fun X Y Z => (((CategoryTheory.Localization.Monoidal.associator L W ε).app X).app Y).app Z,
      leftUnitor := fun Y => (CategoryTheory.Localization.Monoidal.leftUnitor L W ε).app Y,
      rightUnitor := fun X => (CategoryTheory.Localization.Monoidal.rightUnitor L W ε).app X }
-- Mathlib.Analysis.Seminorm
Seminorm.ext_iff : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, p = q ↔ ∀ (x : E), p x = q x
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Sleep.ofNative : Std.Internal.UV.Timer → Std.Async.Sleep
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- A group-like element `a` satisfies `ε(a) = 1`.  -/
IsGroupLikeElem.counit_eq_one : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A}, IsGroupLikeElem R a → CoalgebraStruct.counit a = 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_pow : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (n : ℕ), n ≠ 0 → (I ^ n).support = I.support
-- Mathlib.AlgebraicGeometry.EllipticCurve.LFunction
/-- The local Euler factor associated to a Weierstrass curve over a nonarchimedean local field.  -/
WeierstrassCurve.localEulerFactor : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → ArithmeticFunction ℤ
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.close : {α : Type} → Std.CloseableChannel.Bounded✝ α → EIO Std.CloseableChannel.Error Unit