mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeDiffLeft : {α : Type u} → (s t : Set α) → [Fintype ↑s] → [DecidablePred fun x => x ∈ t] → Fintype ↑(s \ t)
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- The category of `R`-bialgebras.  -/
BialgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.RingTheory.MvPowerSeries.Derivative
_private.Mathlib.RingTheory.MvPowerSeries.Derivative.0.MvPowerSeries.pderivFun_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (f : MvPolynomial σ R),
  MvPowerSeries.pderivFun i ↑f = ↑((MvPolynomial.pderiv i) f)
-- Batteries.Data.MLList.Basic
MLList.instMonadLiftOfMonad : {m : Type u_1 → Type u_1} → [Monad m] → MonadLift m (MLList m)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l → k ∈ List.map Prod.fst l → (m.insertMany l).getKey! k' = k
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instCommRingObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [ContMDiffRing I (↑⊤) R] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              CommRing ((smoothSheaf IM I M R).presheaf.obj U)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.range_preOmega : Set.range ⇑Ordinal.preOmega = {x | x.IsInitial}
-- Init.Data.Range.Polymorphic.Iterators
Std.Ric.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] [inst_2 : LE α]
  [inst_3 : DecidableLE α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] {r : Std.Ric α} {a : α},
  (Std.Ric.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.of_surjectiveOnStalks_of_liesOver : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (p : Ideal S)
  [inst_7 : p.IsPrime] [Algebra.QuasiFiniteAt R p],
  (algebraMap S T).SurjectiveOnStalks → ∀ (q : Ideal T) [inst_9 : q.IsPrime] [q.LiesOver p], Algebra.QuasiFiniteAt R q
-- Mathlib.Data.List.Nodup
List.nodup_mergeSort : ∀ {α : Type u} {l : List α} {le : α → α → Bool}, (l.mergeSort le).Nodup ↔ l.Nodup
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- A finite-product-preserving functor takes commutative group objects to commutative group
objects.  -/
CategoryTheory.Functor.mapCommGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) →
                  [F.Braided] → CategoryTheory.Functor (CategoryTheory.CommGrp C) (CategoryTheory.CommGrp D)
-- Mathlib.Data.Complex.Basic
Complex.conj_re : ∀ (z : ℂ), ((starRingEnd ℂ) z).re = z.re
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.toSubringClass : ∀ {S : Type u_1} {K : Type u_2} {inst : DivisionRing K} {inst_1 : SetLike S K} [self : SubfieldClass S K],
  SubringClass S K
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The convolution `g * f` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly
supported. Version where `g` depends on an additional parameter in an open subset `s` of a
parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
given in terms of composition with additional `C^n` functions.  -/
MeasureTheory.contDiffOn_convolution_left_with_param_comp : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : MeasurableSpace G]
  [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [inst_12 : NormedAddCommGroup P]
  [inst_13 : NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant]
  (L : E' →L[𝕜] E →L[𝕜] F) {s : Set P} {n : ℕ∞} {v : P → G},
  ContDiffOn 𝕜 (↑n) v s →
    ∀ {f : G → E} {g : P → G → E'} {k : Set G},
      IsOpen s →
        IsCompact k →
          (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
            MeasureTheory.LocallyIntegrable f μ →
              ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ) →
                ContDiffOn 𝕜 (↑n) (fun x => MeasureTheory.convolution (g x) f L μ (v x)) s
-- Batteries.Data.List.Lemmas
List.prod_one_cons : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] {l : List α},
  (1 :: l).prod = l.prod
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.mk.injEq : ∀ {A : Type u} [inst : Ring A] (G : Type w₀) (R : Type w₁) (relation : R → G →₀ A) (G_1 : Type w₀) (R_1 : Type w₁)
  (relation_1 : R_1 → G_1 →₀ A),
  ({ G := G, R := R, relation := relation } = { G := G_1, R := R_1, relation := relation_1 }) =
    (G = G_1 ∧ R = R_1 ∧ relation ≍ relation_1)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.deriv2_binEntropy : ∀ {p : ℝ}, deriv^[2] Real.binEntropy p = -1 / (p * (1 - p))
-- Mathlib.MeasureTheory.Measure.Prod
/-- The measurable equiv induced by the equiv `(α × β) × γ ≃ α × (β × γ)` is measure preserving.  -/
MeasureTheory.measurePreserving_prodAssoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] (μa : MeasureTheory.Measure α) (μb : MeasureTheory.Measure β)
  (μc : MeasureTheory.Measure γ) [MeasureTheory.SFinite μb] [MeasureTheory.SFinite μc],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.prodAssoc) ((μa.prod μb).prod μc) (μa.prod (μb.prod μc))
-- Mathlib.FieldTheory.Minpoly.Basic
/-- A minimal polynomial is nonzero.  -/
minpoly.ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial A],
  IsIntegral A x → minpoly A x ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.three_le_girth : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.IsAcyclic → 3 ≤ G.girth
-- Lean.Parser.Basic
Lean.Parser.trailingLoopStep : Lean.Parser.PrattParsingTables → Lean.Syntax → List (Lean.Parser.Parser × ℕ) → Lean.Parser.ParserFn
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.sectionsGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat),
  GrpCat.sectionsGroup F = (GrpCat.sectionsSubgroup F).toGroup
-- Init.Data.ByteArray.Basic
/-- Replaces the byte at the given index.

The array is modified in-place if there are no other references to it.

If the index is out of bounds, the array is returned unmodified.
 -/
ByteArray.set! : ByteArray → ℕ → UInt8 → ByteArray
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.const` as an `AddMonoidHom`.  -/
Pi.constAddMonoidHom : (α : Type u_5) → (β : Type u_6) → [inst : AddZeroClass β] → β →+ α → β
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} (n : ℕ) [inst_7 : OfNat F n], fderivWithin 𝕜 (OfNat.ofNat n) s = 0
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_half_period_eq : ∀ (p : ℝ), ‖↑(p / 2)‖ = |p| / 2
-- Init.Data.Array.Basic
/-- Returns the first non-`none` result of applying the function `f` to each element of the
array, in order. Returns `none` if `f` returns `none` for all elements.

Example:
```lean example
#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
  if i < 5 then
    some (i * 10)
  else
    none
```
```output
some 10
```
 -/
Array.findSome? : {α : Type u} → {β : Type v} → (α → Option β) → Array α → Option β
-- Mathlib.Tactic.FieldSimp
/-- Given `l` of type `qNF M`, i.e. a list of `(ℤ × Q($M)) × ℕ`s (two `Expr`s and a natural
number), build an `Expr` representing an object of type `NF M` (i.e. `List (ℤ × M)`) in the
in the obvious way: by forgetting the natural numbers and gluing together the integers and `Expr`s.
 -/
Mathlib.Tactic.FieldSimp.qNF.toNF : {v : Lean.Level} → {M : Q(Type v)} → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Q(Mathlib.Tactic.FieldSimp.NF «$M»)
-- Mathlib.Data.Finset.Card
/-- **Alias** of the reverse direction of `Finset.card_pos`. -/
Finset.Nonempty.card_pos : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → 0 < s.card
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint.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] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 →
    ∀ (signs signs_1 : Finset (Fin (n + 1))),
      signs = signs_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.touchpoint signs i = s_1.touchpoint signs_1 i_1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id : ∀ {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] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) =
    CategoryTheory.CategoryStruct.id (L.obj Y)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_le_of_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F},
  S ≤ Submonoid.comap f T → Submonoid.map f S ≤ T
-- Init.Control.Lawful.Instances
ReaderT.run_monadMap : ∀ {n : Type u → Type u_1} {m : Type u → Type u_2} {ρ α : Type u} [inst : MonadFunctorT n m]
  (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ), (monadMap f x).run ctx = monadMap f (x.run ctx)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive
homomorphism `AddHom Mᵐᵒᵖ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on
morphisms.  -/
AddHom.mulOp : {M : Type u_3} → {N : Type u_4} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) ≃ (Mᵐᵒᵖ →ₙ+ Nᵐᵒᵖ)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.baseOf.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : Monoid M] [inst_1 : LinearOrder S] [inst_2 : Monoid S]
  (v : ι → M) (f : M →* S), IsMulIndecomposable.baseOf v f = {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
-- Mathlib.RingTheory.PowerSeries.Basic
/-- First coefficient of the `n`-th power of a power series.  -/
PowerSeries.coeff_one_pow : ∀ {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff 1) (φ ^ n) = ↑n * (PowerSeries.coeff 1) φ * PowerSeries.constantCoeff φ ^ (n - 1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v` adic valuation of `a / b : K` is `≤ 1` if and only if `b ∉ v`, provided that `a` and
`b` are coprime at `v`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (a : R) {b : R},
  b ≠ 0 →
    (b ∈ v.asIdeal → a ∉ v.asIdeal) → ((IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑a / ↑b) ≤ 1 ↔ b ∉ v.asIdeal)
-- Mathlib.Data.Int.Log
Int.clog_zpow : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ (z : ℤ), Int.clog b (↑b ^ z) = z
-- Mathlib.RingTheory.Artinian.Defs
/-- A ring is Artinian if it is Artinian as a module over itself.

Strictly speaking, this should be called `IsLeftArtinianRing` but we omit the `Left` for
convenience in the commutative case. For a right Artinian ring, use `IsArtinian Rᵐᵒᵖ R`.

For equivalent definitions, see `Mathlib/RingTheory/Artinian/Ring.lean`.
 -/
IsArtinianRing : (R : Type u_1) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightId L R).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Finset.measurable_restrict : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (s : Finset δ), Measurable s.restrict
-- Init.Data.Vector.Basic
/-- Delete an element of a vector using a `Nat` index and a tactic provided proof.  -/
Vector.eraseIdx : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → autoParam (i < n) Vector.eraseIdx._auto_1 → Vector α (n - 1)
-- Mathlib.Topology.Order
IsClosed.mono : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α}, IsClosed s → t₁ ≤ t₂ → IsClosed s
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.mk.sizeOf_spec : ∀ (out : Lean.Widget.TaggedText (ℕ × ℕ)) (tagStack : List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))) (column : ℕ),
  sizeOf { out := out, tagStack := tagStack, column := column } = 1 + sizeOf out + sizeOf tagStack + sizeOf column
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTermInfo : Lean.Elab.TermInfo → Lean.Elab.Info
-- Init.Data.Option.Attach
Option.attach_congr : ∀ {α : Type u_1} {o₁ o₂ : Option α} (h : o₁ = o₂), o₁.attach = Option.map (fun x => ⟨↑x, ⋯⟩) o₂.attach
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  {J : Type u_3} (X : I → C) (ι : J → I),
  Function.Injective ι →
    ∀ (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι))
      (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁)
      (c₂ : CategoryTheory.Limits.Cofan fun k => X ↑k) (hc₂ : CategoryTheory.Limits.IsColimit c₂),
      CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
-- Mathlib.Algebra.Category.ModuleCat.Subobject
/-- The categorical subobjects of a module `M` are in one-to-one correspondence with its
submodules.  -/
ModuleCat.subobjectModule : {R : Type u} → [inst : Ring R] → (M : ModuleCat R) → CategoryTheory.Subobject M ≃o Submodule R ↑M
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Continuous f → Function.Injective f → IsOpenMap f → Topology.IsOpenEmbedding f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.hasStrictDerivAt_cosh : ∀ (x : ℝ), HasStrictDerivAt Real.cosh (Real.sinh x) x
-- Mathlib.Algebra.Group.Basic
natCast_sub_natCast_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (m n : ℕ), (↑m - ↑n) • a = m • a - n • a
-- Mathlib.Data.Matrix.Basic
Matrix.transposeLinearEquiv_symm : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α], (Matrix.transposeLinearEquiv m n R α).symm = Matrix.transposeLinearEquiv n m R α
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : ArithmeticFunction R},
  f.IsMultiplicative →
    g.IsMultiplicative →
      ∀ {n : ℕ}, Squarefree n → (ArithmeticFunction.prodPrimeFactors fun p => (f + g) p) n = (f * g) n
-- Mathlib.Data.Num.Lemmas
PosNum.mul_to_nat : ∀ (m n : PosNum), ↑(m * n) = ↑m * ↑n
-- Lean.Expr
/-- `getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
and performs pending beta reductions. It does **not** use whnf.
Examples:
- If `a` is `Nat`, `getForallArity a` returns `0`
- If `a` is `Nat → Bool`, `getForallArity a` returns `1`
 -/
Lean.Expr.getForallArity : Lean.Expr → ℕ
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_div : ∀ {K : Type u} [inst : Field K] {x y : RatFunc K}, x ≠ 0 → y ≠ 0 → (x / y).intDegree = x.intDegree - y.intDegree
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.realSize.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.HeapNode α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.HeapNode α) →
      (Unit → motive Batteries.BinomialHeap.Imp.HeapNode.nil) →
        ((a : α) →
            (c s : Batteries.BinomialHeap.Imp.HeapNode α) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s)) →
          motive x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk.injEq : ∀ {V : Type u} (Adj : V → V → Prop) (symm : autoParam (Std.Symm Adj) SimpleGraph.symm._autoParam)
  (loopless : autoParam (Std.Irrefl Adj) SimpleGraph.loopless._autoParam) (Adj_1 : V → V → Prop)
  (symm_1 : autoParam (Std.Symm Adj_1) SimpleGraph.symm._autoParam)
  (loopless_1 : autoParam (Std.Irrefl Adj_1) SimpleGraph.loopless._autoParam),
  ({ Adj := Adj, symm := symm, loopless := loopless } = { Adj := Adj_1, symm := symm_1, loopless := loopless_1 }) =
    (Adj = Adj_1)
-- Lean.Util.Diff
Lean.Diff.Histogram.Entry.mk : {α : Type u} →
  {lsize rsize : ℕ} →
    (leftCount : ℕ) →
      (leftIndex : Option (Fin lsize)) →
        (leftCount = 0 ↔ leftIndex = none) →
          (rightCount : ℕ) →
            (rightIndex : Option (Fin rsize)) →
              (rightCount = 0 ↔ rightIndex = none) → Lean.Diff.Histogram.Entry α lsize rsize
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.top_lowerCentralSeries_sum : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] (n : ℕ),
  ⊤.lowerCentralSeries n = (⊤.lowerCentralSeries n).prod (⊤.lowerCentralSeries n)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- **Alias** of `ProperSMul.isCompact_setOfPred_inter_nonempty`.

---

If `G` acts properly on `X`, then for each pair of compacts `U, V ⊆ X`,
the set of `g` such that `g • U` intersects `V` is compact.

See `MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty` for the two-way implication
under additional conditions on `G` and `X`.  -/
ProperSMul.isCompact_setOf_inter_nonempty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : TopologicalSpace G] [ProperSMul G X] {U V : Set X},
  IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_lt_of_forall_lt_of_nonempty : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [ProperSpace 𝕜] {a : A},
  (spectrum 𝕜 a).Nonempty → ∀ {r : NNReal}, (∀ k ∈ spectrum 𝕜 a, ‖k‖₊ < r) → spectralRadius 𝕜 a < ↑r
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Given a non-unital star `ℝ≥0`-algebra homomorphism `φ` from `C(X, ℝ≥0)₀` into a non-unital
`ℝ`-algebra `A`, this is the unique extension of `φ` from `C(X, ℝ)₀` to `A` as a non-unital
star `ℝ`-algebra homomorphism.  -/
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : Zero X] →
      {A : Type u_2} →
        [inst_2 : NonUnitalRing A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module ℝ A] → (ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A) → ContinuousMapZero X ℝ →⋆ₙₐ[ℝ] A
-- Init.Data.SInt.Lemmas
Int16.ofInt_tmod : ∀ {a b : ℤ},
  Int16.minValue.toInt ≤ a →
    a ≤ Int16.maxValue.toInt →
      Int16.minValue.toInt ≤ b → b ≤ Int16.maxValue.toInt → Int16.ofInt (a.tmod b) = Int16.ofInt a % Int16.ofInt b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ Std.DHashMap.Raw.ofList l}, (Std.DHashMap.Raw.ofList l).getKey k' h' = k
-- Init.Data.SInt.Lemmas
Int8.ofInt_iSizeToInt : ∀ (x : ISize), Int8.ofInt x.toInt = x.toInt8
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_le_add_lpNorm_add : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp g p μ →
    1 ≤ p → MeasureTheory.lpNorm f p μ ≤ MeasureTheory.lpNorm (f + g) p μ + MeasureTheory.lpNorm g p μ
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat_unsat_iff_of_NonEmpty : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {idx : ℕ} {invert : Bool} [Nonempty α] {aig : Std.Sat.AIG α}
  {hidx1 : idx < aig.relabelNat.decls.size} {hidx2 : idx < aig.decls.size},
  aig.relabelNat.UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (m : M) (r : R),
  MonoidAlgebra.single m ((algebraMap R A) r) = (algebraMap R (MonoidAlgebra A M)) r * (MonoidAlgebra.of A M) m
-- Mathlib.Data.List.Monad
List.instLawfulMonad : LawfulMonad List
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
/-- The data needed to induce a `MonoidalCategory` structure via
`CoalgCat.instMonoidalCategoryStruct` and the forgetful functor to modules.  -/
CoalgCat.MonoidalCategory.inducingFunctorData : (R : Type u) →
  [inst : CommRing R] → CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R))
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.alts : Lean.Elab.Term.ElabMatchTypeAndDiscrsResult → Array Lean.Elab.Term.TermMatchAltView