mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- Let `R → S → T` be algebras such that `T` is the localization of `S` away from one
element, where `S` is generated over `R` by `P` with kernel `I` and `Q` is the
canonical `S`-presentation of `T`. Denote by `J` the kernel of the composition
`R[X,Y] → T`. Then `T ⊗[S] (I/I²) → J/J²` is injective.
 -/
Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι),
  Function.Injective
    ⇑(LinearMap.liftBaseChange T
        (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom))
-- Lean.Environment
Lean.Kernel.Diagnostics : Type
-- Init.Data.Nat.Lemmas
Nat.div_mul_div_comm : ∀ {a b c d : ℕ}, b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_nonneg : ∀ {x : ℝ}, 1 ≤ x → 0 ≤ Real.log x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {X_1 Y : Cᵒᵖ}
  (f : X_1 ⟶ Y), S.functor.map f = TypeCat.ofHom fun g => ⟨CategoryTheory.CategoryStruct.comp f.unop ↑g, ⋯⟩
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_flatten : ∀ {α : Type u_1} (xs : List (List α)), FreeAddMonoid.ofList xs.flatten = (List.map (⇑FreeAddMonoid.ofList) xs).sum
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inv_mul_cancel : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero),
  f.inv hf * f ≈ 1
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lift₂.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : M → M → α)
  (h :
    ∀ (a₁ b₁ a₂ b₂ : M),
      ArchimedeanClass.mk a₁ = ArchimedeanClass.mk b₁ →
        ArchimedeanClass.mk a₂ = ArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂),
  ArchimedeanClass.lift₂ f h = Quotient.lift₂ f ⋯
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : DistribSMul S R] [IsScalarTower S R R] (x y : R) (s : S)
  (p : Polynomial (Polynomial R)), Polynomial.evalEval x y (s • p) = s • Polynomial.evalEval x y p
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.comp_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {γ : Type u_5} [inst_2 : TopologicalSpace γ] {f : α → γ},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun z => f z.1) (μ.prod ν)
-- Mathlib.Data.List.AList
/-- `s₁ ∪ s₂` is the key-based union of two association lists. It is
left-biased: if there exists an `a ∈ s₁`, `lookup a (s₁ ∪ s₂) = lookup a s₁`.
 -/
AList.union : {α : Type u} → {β : α → Type v} → [DecidableEq α] → AList β → AList β → AList β
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_right_inv : ∀ {n : ℕ} {G : Type u_3} [inst : Group G] (f : Fin n → G) (i : Fin n),
  (Fin.partialProd f i.castSucc)⁻¹ * Fin.partialProd f i.succ = f i
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_inf : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I), (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion
-- Mathlib.Order.GaloisConnection.Basic
sInf_image2_eq_sInf_sInf : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (u₂ a) (u a)) → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
-- Mathlib.Topology.Constructions
instTopologicalSpaceQuotient : {X : Type u} → {s : Setoid X} → [t : TopologicalSpace X] → TopologicalSpace (Quotient s)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_le_of_lt_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosMono α], a ≤ b → c < d → 0 < a → 0 ≤ d → a * c < b * d
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.mem_isPrincipalSubmonoid_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I ∈ Ideal.isPrincipalSubmonoid R ↔ Submodule.IsPrincipal I
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `neg_apply`. -/
CuspForm.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N') (x : N),
  (Monoid.Coprod.map f g) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (g x)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_eq_self : ∀ {α : Type u_1} [inst : LinearOrder α] {b x : α}, Set.projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] (y : ↥Y),
  IsDiscrete (⇑f ⁻¹' {y})
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace),
  AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) x) =
    x
-- Mathlib.Algebra.Star.Pointwise
Set.iInter_star : ∀ {α : Type u_1} {ι : Sort u_2} [inst : Star α] (s : ι → Set α), star (⋂ i, s i) = ⋂ i, star (s i)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.incl_obj : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i : I} (X : C i),
  (CategoryTheory.Sigma.incl i).obj X = ⟨i, X⟩
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, 0 ≤ ↑f x
-- Mathlib.Topology.Order
generateFrom_iUnion_isOpen : ∀ {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α), TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) = ⨅ i, f i
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- A variant of `isTerminalOfEmpty` that is easier to `apply`.  -/
TopCat.Sheaf.isTerminalOfEqEmpty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} →
      (F : TopCat.Sheaf C X) →
        {U : TopologicalSpace.Opens ↑X} → U = ⊥ → CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op U))
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.id_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), (EsakiaHom.id α) a = a
-- LeanSearchClient.LoogleSyntax
/-- a single `#find` filter. The `term` can also be an ident or a strlit,
these are distinguished in `parseFindFilters`  -/
LeanSearchClient.loogle_filter : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommMon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Ici : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b : M), (fun x => a + x) '' Set.Ici b = Set.Ici (a + b)
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_right_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.HopfObj.antipode)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `Filter.atBot` then `f * g` tends to `Filter.atTop`.  -/
Filter.Tendsto.neg_mul_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  C < 0 →
    Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.GroupTheory.Torsion
IsAddTorsion.torsionAddEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : AddCommMonoid G] (tG : IsAddTorsion G) (a : G), ↑(tG.torsionAddEquiv.symm a) = a
-- Init.Data.Int.Order
Int.mul_le_mul_of_nonneg_right : ∀ {a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.isoMkFunctor_hom_app : ∀ {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 (CategoryTheory.Join C D) E)
  (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.isoMkFunctor F).hom.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.Join.left x))
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.Join.right x))
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A section `s` of `V` is `C^k` at `x ∈ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffAt_iff_localFrameCoeff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  {x' : M} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  x' ∈ e.baseSet →
    (ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) x' ↔
      ∀ (i : ι),
        ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) k
          ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x')
-- Batteries.Data.PairingHeap
/-- An empty forest, which has depth `0`.  -/
Batteries.PairingHeapImp.Heap.nil : {α : Type u} → Batteries.PairingHeapImp.Heap α
-- Mathlib.GroupTheory.CosetCover
/-- Let the group `G` be the union of finitely many left cosets `g i • H i`. Then the
sum of the inverses of the indexes of the subgroups `H i` is greater than or equal to 1.  -/
Subgroup.one_le_sum_inv_index_of_leftCoset_cover : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ → 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹
-- Init.Control.Except
ExceptT.finally : {m : Type u → Type v} → {ε : Type u} → [MonadFinally m] → [Monad m] → MonadFinally (ExceptT ε m)
-- Mathlib.Computability.Encoding
/-- Deprecated: Use the encoding directly.  -/
Computability.FinEncoding.toEncoding : {α : Type u} → {Γ : Type v} → [Fintype Γ] → Computability.Encoding α Γ → Computability.Encoding α Γ
-- Mathlib.Order.Category.Frm
Frm.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : Order.Frame carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_of_isLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint], F.Initial
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.const_vadd : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable (c +ᵥ f)
-- Mathlib.Order.SuccPred.Relation
/-- For `n ≤ m`, `(n, m)` is in the reflexive-transitive closure of `~` if `pred i ~ i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_pred_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n ≤ m → Relation.ReflTransGen r n m
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeAction : Lean.FromJson Lean.Lsp.CodeAction
-- Mathlib.Data.Set.Basic
Set.inter_inter_distrib_right : ∀ {α : Type u} (s t u : Set α), s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropEndWhile_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, ((s.takeEndWhile pat).dropEndWhile pat).isEmpty = true
-- Mathlib.Order.Heyting.Basic
/-- Construct a Heyting algebra from the lattice structure and Heyting implication alone.  -/
HeytingAlgebra.ofHImp : {α : Type u_2} →
  [inst : DistribLattice α] →
    [BoundedOrder α] → (himp : α → α → α) → (∀ (a b c : α), a ≤ himp b c ↔ a ⊓ b ≤ c) → HeytingAlgebra α
-- Mathlib.Tactic.PPWithUniv
/-- `attribute [pp_with_univ] Ordinal` instructs the pretty-printer to
print `Ordinal.{u}` with universe parameters by default
(unless `pp.universes` is explicitly set to `false`).
 -/
Mathlib.PPWithUniv.ppWithUnivAttr : Lean.ParserDescr
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.cons_head : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  (HNNExtension.NormalWord.cons g u w h1 h2).head = g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mk.injEq : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  (toSubsemiring : Subsemiring A) (is_homogeneous' : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring)
  (toSubsemiring_1 : Subsemiring A) (is_homogeneous'_1 : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring_1),
  ({ toSubsemiring := toSubsemiring, is_homogeneous' := is_homogeneous' } =
      { toSubsemiring := toSubsemiring_1, is_homogeneous' := is_homogeneous'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_target' : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
/-- Given a polynomial with integer coefficients `p` and a complex constant `s`, there is a nonnegative
`c` such that for all nonzero `q ∈ ℕ`, `|P(X ^ (q - 1) * p ^ q, s)| ≤ c ^ q`.

Note: Jacobson writes `h(x)` for `x ^ (q - 1) * p(x) ^ q` and `bⱼ` for its coefficients.
 -/
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.exp_polynomial_approx_aux : ∀ (f : Polynomial ℤ) (s : ℂ),
  ∃ c ≥ 0,
    ∀ (p : ℕ),
      p ≠ 0 → ‖LindemannWeierstrass.P✝ (Polynomial.map (algebraMap ℤ ℂ) (Polynomial.X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).get? k = Option.filter (f k) (t.get? k)
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
forall_le_add_iff_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α]
  [AddLeftMono α] [IsLeftCancelAdd α], (∀ a ≤ b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing an alternating map twice with the same linear map in each argument is
the same as composing with their composition.  -/
AlternatingMap.compLinearMap_assoc : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_11} [inst_7 : AddCommMonoid M₃] [inst_8 : Module R M₃] (f : M [⋀^ι]→ₗ[R] N)
  (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂), (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorRxoIteratorIdSigma.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α],
  Std.DTreeMap.Internal.instIteratorRxoIteratorIdSigma =
    { IsPlausibleStep := fun it step => it.internalState.step = step,
      step := fun it => pure (Std.Shrink.deflate ⟨it.internalState.step, ⋯⟩) }
-- Mathlib.LinearAlgebra.Complex.Module
Complex.liftAux_apply_I : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : A) (hI' : I' * I' = -1),
  (Complex.liftAux I' hI') Complex.I = I'
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasColimitsIndOfHasFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasColimits (CategoryTheory.Ind C)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The archimedean class of a given element.  -/
ArchimedeanClass.mk : {M : Type u_1} →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → M → ArchimedeanClass M
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {a b : B'}
  {f g : a ⟶ b} (f_1 : f ⟶ g), ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).map₂ f_1).iso.hom = F.map₂ f_1
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.ext : ∀ {α : Type u} {x y : CategoryTheory.Codiscrete α}, x.as = y.as → x = y
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The only continuous `R`-alternating map from two or more copies of `R` is the zero map.  -/
ContinuousAlternatingMap.uniqueOfCommRing : {R : Type u_1} →
  {N : Type u_3} →
    {ι : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid N] →
          [inst_2 : Module R N] →
            [inst_3 : TopologicalSpace N] →
              [Finite ι] → [Nontrivial ι] → [inst_6 : TopologicalSpace R] → Unique (R [⋀^ι]→L[R] N)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- The measure of a segment is the distance between its endpoints.  -/
MeasureTheory.hausdorffMeasure_affineSegment : ∀ {E : Type u_5} {P : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace P]
  [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor E P] [inst_5 : BorelSpace P] (x y : P),
  (MeasureTheory.Measure.hausdorffMeasure 1) (affineSegment ℝ x y) = edist x y
-- Mathlib.Order.Completion
DedekindCut.image_right_subset_upperBounds : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ (A : DedekindCut α), f '' A.right ⊆ upperBounds (f '' A.left)
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.isWFRec : Lean.Name → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → a ∉ m
-- Mathlib.FieldTheory.SeparableDegree
/-- If `K / E / F` is a field extension tower, such that `K / E` is algebraic, then their
separable degrees satisfy the tower law
$[E:F]_s [K:E]_s = [K:F]_s$. See also `Module.finrank_mul_finrank`.  -/
Field.finSepDegree_mul_finSepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K],
  Field.finSepDegree F E * Field.finSepDegree E K = Field.finSepDegree F K
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.mk.inj : ∀ {B : Type u_1} {M : Matrix B B ℕ} {isSymm : autoParam M.IsSymm CoxeterMatrix.isSymm._autoParam}
  {diagonal : autoParam (∀ (i : B), M i i = 1) CoxeterMatrix.diagonal._autoParam}
  {off_diagonal : autoParam (∀ (i i' : B), i ≠ i' → M i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam}
  {M_1 : Matrix B B ℕ} {isSymm_1 : autoParam M_1.IsSymm CoxeterMatrix.isSymm._autoParam}
  {diagonal_1 : autoParam (∀ (i : B), M_1 i i = 1) CoxeterMatrix.diagonal._autoParam}
  {off_diagonal_1 : autoParam (∀ (i i' : B), i ≠ i' → M_1 i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam},
  { M := M, isSymm := isSymm, diagonal := diagonal, off_diagonal := off_diagonal } =
      { M := M_1, isSymm := isSymm_1, diagonal := diagonal_1, off_diagonal := off_diagonal_1 } →
    M = M_1
-- Aesop.Saturate
Aesop.SaturateM.run : {α : Type} → Aesop.Options' → Aesop.SaturateM α → Lean.MetaM (α × Aesop.Stats)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} [inst_3 : SizeOf C] (cocomplex : CochainComplex C ℕ)
  (injective :
    autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex.X n))
      CategoryTheory.InjectiveResolution.injective._autoParam)
  [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex i]
  (ι : (CochainComplex.single₀ C).obj Z ⟶ cocomplex)
  (quasiIso : autoParam (QuasiIso ι) CategoryTheory.InjectiveResolution.quasiIso._autoParam),
  sizeOf { cocomplex := cocomplex, injective := injective, hasHomology := hasHomology, ι := ι, quasiIso := quasiIso } =
    1 + sizeOf cocomplex + sizeOf ι + sizeOf quasiIso