mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun m n ↦ g (f m n)` as a `MonoidHom`.  -/
MonoidHom.compr₂ : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      {Q : Type uQ} →
        [inst : MulOneClass M] →
          [inst_1 : MulOneClass N] →
            [inst_2 : CommMonoid P] → [inst_3 : CommMonoid Q] → (M →* N →* P) → (P →* Q) → M →* N →* Q
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_StateT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε : Type u_1} {σ α : Type u} {x : StateT σ m α} {h : ε → StateT σ m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ sh)} [inst : Std.Do.WP m sh] [inst_1 : Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q = fun s =>
    (Std.Do.wp (MonadExceptOf.tryCatch (x.run s) fun e => (h e).run s)).apply (fun xs => Q.1 xs.1 xs.2, Q.2)
-- Lean.Meta.Tactic.Grind.Types
/-- Model-based theory combination equality coming from the i-th argument of applications `a` and `b`  -/
Lean.Meta.Grind.SplitSource.mbtc : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.SplitSource
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.mk'.inj : ∀ {α : Type v} {small : Std.Internal.Small α} {inner inner_1 : Std.Internal.ComputableSmall.Target α},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Init.Data.List.Basic
/-- Computes the product of the elements of a list.

Examples:
* `[a, b, c].prod = a * (b * (c * 1))`
* `[1, 2, 5].prod = 10`
 -/
List.prod : {α : Type u_1} → [Mul α] → [One α] → List α → α
-- Mathlib.NumberTheory.NumberField.CMField
/-- The complex conjugation is an automorphism of degree `2`.
 -/
NumberField.IsCMField.orderOf_complexConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K], orderOf (NumberField.IsCMField.complexConj K) = 2
-- Init.Data.UInt.Lemmas
UInt8.le_rfl : ∀ {a : UInt8}, a ≤ a
-- Lean.CoreM
/-- Context for the CoreM monad.  -/
Lean.Core.Context : Type
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Given an `a : A` where `A` is an `R`-algebra, the *resolvent* is
a map `R → A` which sends `r : R` to `(algebraMap R A r - a)⁻¹` when
`r ∈ resolvent R A` and `0` when `r ∈ spectrum R A`.  -/
resolvent : {R : Type u} → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Ring A] → [Algebra R A] → A → R → A
-- Std.Data.DTreeMap.Internal.Operations
/-- Constructs the tree `l ++ r`.  -/
Std.DTreeMap.Internal.Impl.glue : {α : Type u} →
  {β : α → Type v} →
    (l r : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Std.DTreeMap.Internal.Impl α β
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.trivial_grp_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_zero_ae : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → f x = 0) → ∫ (x : ℝ) in a..b, f x ∂μ = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.mk.injEq : ∀ (name : Lean.Name) (cidx size usize ssize : ℕ) (name_1 : Lean.Name) (cidx_1 size_1 usize_1 ssize_1 : ℕ),
  ({ name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
      { name := name_1, cidx := cidx_1, size := size_1, usize := usize_1, ssize := ssize_1 }) =
    (name = name_1 ∧ cidx = cidx_1 ∧ size = size_1 ∧ usize = usize_1 ∧ ssize = ssize_1)
-- Mathlib.Probability.Kernel.Irreducible
/-- A kernel `κ : Kernel α α` is `φ`-irreducible (w.r.t. a given measure `φ` on `α`),
if for every measurable set `A` with positive measure under `φ`,
and for every `a : α`, there exists an integer `n` such that `(κ ^ n) a A > 0`.
Ref. *Meyn-Tweedie* Proposition 4.2.1(ii), page 89  -/
ProbabilityTheory.Kernel.IsIrreducible : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → ProbabilityTheory.Kernel α α → Prop
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.scMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMapIso._auto_1),
  (CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i hi).hom = CategoryTheory.ComposableArrows.scMap e.hom h₁ h₂ i hi
-- Mathlib.NumberTheory.LucasLehmer
/-- There are strictly fewer than `q^2` units, since `0` is not a unit.  -/
LucasLehmer.X.card_units_lt : ∀ {q : ℕ} [inst : NeZero q], 1 < q → Fintype.card (LucasLehmer.X q)ˣ < q ^ 2
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_bot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Ideal S},
  ⊥.ramificationIdx' P = 0
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat : Std.Roo.HasRcoIntersection ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter!_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.inter! m₂).Equiv (m₃.inter! m₄)
-- Mathlib.Topology.Convenient.Category
/-- The functor `ContinuousGeneratedByCat.toTopCat : ContinuousGeneratedByCat X ⥤ TopCat`
is fully faithful.  -/
ContinuousGeneratedByCat.fullyFaithfulToTopCat : {ι : Type t} →
  (X : ι → Type u) → [inst : (i : ι) → TopologicalSpace (X i)] → (ContinuousGeneratedByCat.toTopCat X).FullyFaithful
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} [inst : Inhabited β] {f : Option β → Option β}, (t.alter k f)[k]! = (f t[k]?).get!
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap.Raw α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Mathlib.Data.List.AList
AList.lookup_to_alist : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} (s : List (Sigma β)),
  AList.lookup a s.toAList = List.dlookup a s
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.instGroup : {R : Type u_1} →
  {E : Type u_5} →
    [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → Group (E ≃ₗᵢ[R] E)
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs
the values emitted by `it` until one of those values is rejected by `P`.
If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

In situations where `P` is monadic, use `takeWhileM` instead.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it               ---a----b---c--d-e--⊥
it.takeWhile P   ---a----b---⊥

it               ---a----⊥
it.takeWhile P   ---a----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not.
In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
it terminates.
 -/
Std.IterM.takeWhile : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst : Monad m] → (P : β → Bool) → Std.IterM m β → Std.IterM m β
-- Aesop.Stats.Basic
Aesop.instToJsonForwardRuleStateStats : Lean.ToJson Aesop.ForwardRuleStateStats
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The glue data of ringed spaces associated to a family of glue data of locally ringed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData : AlgebraicGeometry.LocallyRingedSpace.GlueData → AlgebraicGeometry.SheafedSpace.GlueData CommRingCat
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isCofibrant_of_cofibration : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] {X Y : C}
  (i : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [hX : HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.IsCofibrant Y
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) {r : ℝ}, 0 < r → ⨆ x, T.rayleighQuotient ↑x = ⨆ x, T.rayleighQuotient ↑x
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertZoneId : Std.Time.ZoneId → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_ne_bot : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a b : WithBot α}, a ≠ ⊥ → b ≠ ⊥ → a * b ≠ ⊥
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) '' Set.Iio b = Set.Ioi (a / b)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso.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)
  [inst_5 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Localization.Monoidal.braidingNatIso L W ε =
    CategoryTheory.Localization.lift₂NatIso (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)
      (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) W W
      ((CategoryTheory.MonoidalCategory.curriedTensor C).comp
        ((CategoryTheory.Functor.whiskeringRight C C (CategoryTheory.LocalizedMonoidal L W ε)).obj
          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
      ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.comp
        ((CategoryTheory.Functor.whiskeringRight C C (CategoryTheory.LocalizedMonoidal L W ε)).obj
          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
      (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε)
      (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).flip
      (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.BraidedCategory.curriedBraidingNatIso C)
        ((CategoryTheory.Functor.whiskeringRight C C (CategoryTheory.LocalizedMonoidal L W ε)).obj
          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapIso_inv : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (i : J),
  (CategoryTheory.GradedObject.mapIso e p).inv i = CategoryTheory.GradedObject.mapMap e.inv p i
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.uncurry_bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (s : CategoryTheory.Presieve X)
  (t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → CategoryTheory.Presieve Y),
  (s.bind t).uncurry =
    ⋃ i,
      ⋃ (h : i ∈ s.uncurry), (Sigma.map id fun Z g => CategoryTheory.CategoryStruct.comp g i.snd) '' (t i.snd h).uncurry
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousMultilinear_apply : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
  [inst_6 : Fintype ι] [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)]
  (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
  (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖)
  (m : (i : ι) → E i), ⇑((f.mkContinuousMultilinear C H) m) = ⇑(f m)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Class `ContinuousConstVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.

Note that both `ContinuousConstVAdd α α` and `ContinuousConstVAdd αᵐᵒᵖ α` are
weaker versions of `ContinuousVAdd α`.  -/
ContinuousConstVAdd : (Γ : Type u_1) → (T : Type u_2) → [TopologicalSpace T] → [VAdd Γ T] → Prop
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofAlgHom_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁), (AlgEquiv.ofAlgHom f g h₁ h₂).symm = AlgEquiv.ofAlgHom g f h₂ h₁
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.syncKind : Lean.Lsp.TextDocumentChangeRegistrationOptions → Lean.Lsp.TextDocumentSyncKind
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between the chosen initial object and the chosen zero object.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → [inst_2 : CategoryTheory.Limits.HasInitial C] → 0 ≅ ⊥_ C
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- the coercion to `Matrix ι ι R` as a monoid homomorphism  -/
Matrix.SpecialLinearGroup.coeMonoidHom : {ι : Type u_2} →
  {R : Type u_3} →
    [inst : Fintype ι] →
      [inst_1 : DecidableEq ι] → [inst_2 : CommRing R] → Matrix.SpecialLinearGroup ι R →* Matrix ι ι R
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [Small.{w, u₁} I] [CategoryTheory.Limits.HasLimitsOfShape I C]
  [CategoryTheory.Limits.PreservesLimitsOfShape I A], CategoryTheory.Limits.HasLimitsOfShape I A.Elements
-- Mathlib.Order.WithBot
WithBot.toDual_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithBot α),
  WithBot.toDual (WithBot.map f a) = WithTop.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithBot.toDual a)
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.initCache : Lean.Expr.ReplaceLevelImpl.State
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul_C_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R],
  IsUnit a → ∀ (p : Polynomial R), (p * Polynomial.C a).leadingCoeff = p.leadingCoeff * a
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
/-- If `K` is a coverage, it generates the smallest Grothendieck topology containing `K`.  -/
CategoryTheory.Coverage.generates_toGrothendieck : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Coverage C), K.Generates K.toGrothendieck
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.subsingleton_iff : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  Subsingleton (OreLocalization S R) ↔ 0 ∈ S
-- Mathlib.Data.Nat.Choose.Multinomial
Finsupp.multinomial_eq_of_support_subset : ∀ {α : Type u_1} {f : α →₀ ℕ} {s : Finset α}, f.support ⊆ s → f.multinomial = Nat.multinomial s ⇑f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableOn_empty : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}, MDiff[∅] f
-- Init.Data.String.Decode
List.utf8DecodeChar_utf8Encode_cons : ∀ {l : List Char} {c : Char} {h : ((c :: l).utf8Encode.utf8DecodeChar? 0).isSome = true},
  (c :: l).utf8Encode.utf8DecodeChar 0 h = c
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `f : ℕ → F` is multiplicative on coprime arguments, `p` is a prime and `m` is `p`-smooth,
then `f (p^e * m) = f (p^e) * f m`.  -/
Nat.map_prime_pow_mul : ∀ {F : Type u_1} [inst : Mul F] {f : ℕ → F},
  (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
    ∀ {p : ℕ}, Nat.Prime p → ∀ (e : ℕ) {m : ↑p.smoothNumbers}, f (p ^ e * ↑m) = f (p ^ e) * f ↑m
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.pow : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} [NormOneClass S] {f : α → R} {g : α → S},
  f =O[l] g → ∀ (n : ℕ), (fun x => f x ^ n) =O[l] fun x => g x ^ n
-- Mathlib.Util.Delaborators
/-- Override the Lean 4 pi notation delaborator with one that prints cute binders
such as `∀ ε > 0`.  -/
PiNotation.delabPi : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Async.Select
Std.Async.Selector.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (tryFn : Std.Async.Async (Option α))
  (registerFn : Std.Async.Waiter α → Std.Async.Async Unit) (unregisterFn : Std.Async.Async Unit),
  sizeOf { tryFn := tryFn, registerFn := registerFn, unregisterFn := unregisterFn } = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_of_isCofinal : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α}, IsCofinal s → Order.cof ↑s = Order.cof α
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- For any `y < 1` and any positive `x`, there exists `n : ℕ` with `y ^ n < x`.  -/
exists_pow_lt_of_lt_one : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K}
  [ExistsAddOfLE K], 0 < x → y < 1 → ∃ n, y ^ n < x
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The topology of a `NormedSpace 𝕜 E` is induced by the seminorm `normSeminorm 𝕜 E`.  -/
norm_withSeminorms : ∀ (𝕜 : Type u_11) (E : Type u_12) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  WithSeminorms fun x => normSeminorm 𝕜 E
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.norm_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_6} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜' 𝕜] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜' 𝕜 E] [inst_9 : NormedSpace 𝕜' Fₗ] [inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ] (f : E →L[𝕜] Fₗ),
  ‖ContinuousLinearMap.restrictScalars 𝕜' f‖ = ‖f‖
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If `f` is a surjective uniform inducing map,
then its domain is a complete space iff its codomain is a complete space.
See also `_root_.completeSpace_congr` for a version that assumes `f` to be an equivalence.  -/
IsUniformInducing.completeSpace_congr : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → Function.Surjective f → (CompleteSpace α ↔ CompleteSpace β)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cdiv_le : ∀ {a d k : ℤ}, d > 0 → a ≤ k * d → Int.Internal.Linear.cdiv a d ≤ k
-- Lean.Compiler.IR.Basic
Lean.IR.Alt : Type
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_snd_dvd_addOrderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {x : α × β}, addOrderOf x.2 ∣ addOrderOf x
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_ne_zero : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L], Algebra.trace K L ≠ 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.comp_cokerπ : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp φ (TopModuleCat.cokerπ φ) = 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} (val val_1 : X.val ⟶ Y.val),
  ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.Order.SupIndep
/-- See also `iSupIndep.disjoint_biSup_biSup` where it is shown that the hypothesis `s.Finite` may
be omitted if the lattice is compactly-generated.  -/
iSupIndep.disjoint_biSup_biSup' : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [IsModularLattice α] {f : ι → α} {s t : Set ι},
  iSupIndep f → Disjoint s t → s.Finite → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKey? k =
    (t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.Functor.isFinitelyAccessible_iff_preservesFilteredColimits : ∀ {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.IsFinitelyAccessible ↔ CategoryTheory.Limits.PreservesFilteredColimits F
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toOpens_top : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], ↑⊤ = ⊤
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_comp_inr : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L'),
  (ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInr = ψ
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.natDegree_restriction : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.restriction.natDegree = p.natDegree
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- the objects in the covering of `S`  -/
CategoryTheory.PreZeroHypercover.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (self : CategoryTheory.PreZeroHypercover S) → self.I₀ → C
-- Init.MetaTypes
Lean.Meta.instInhabitedOccurrences.default : Lean.Meta.Occurrences
-- Mathlib.MeasureTheory.Measure.Hausdorff
Isometry.hausdorffMeasure_preimage : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℝ},
  Isometry f →
    0 ≤ d ∨ Function.Surjective f →
      ∀ (s : Set Y),
        (MeasureTheory.Measure.hausdorffMeasure d) (f ⁻¹' s) =
          (MeasureTheory.Measure.hausdorffMeasure d) (s ∩ Set.range f)