mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ZMod.Units
/-- `unitsMap` is a group homomorphism that maps units of `ZMod m` to units of `ZMod n` when `n`
divides `m`.  -/
ZMod.unitsMap : {n m : ℕ} → n ∣ m → (ZMod m)ˣ →* (ZMod n)ˣ
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.instBEqSeq.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (a b : Lean.Grind.AC.Var)
  (h_1 : (a b : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b))
  (h_2 :
    (a : Lean.Grind.AC.Var) →
      (a_1 : Lean.Grind.AC.Seq) →
        (b : Lean.Grind.AC.Var) →
          (b_1 : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons a a_1) (Lean.Grind.AC.Seq.cons b b_1))
  (h_3 : (x x_1 : Lean.Grind.AC.Seq) → motive x x_1),
  (match Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b with
    | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => h_1 a b
    | Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 => h_2 a a_1 b b_1
    | x, x_1 => h_3 x x_1) =
    h_1 a b
-- Mathlib.Algebra.Field.Basic
div_sub' : ∀ {K : Type u_1} [inst : Field K] {a b c : K}, c ≠ 0 → a / c - b = (a - c * b) / c
-- Mathlib.Topology.Continuous
DenseRange.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} (f : α → X), DenseRange f = Dense (Set.range f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (p : ProjectiveSpectrum ℬ),
  ↑((TopCat.Hom.hom (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.base) p).asHomogeneousIdeal =
    ⇑f ⁻¹' ↑p.asHomogeneousIdeal
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.isSymmetric_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {e : σ ≃ τ},
  ((MvPolynomial.rename ⇑e) φ).IsSymmetric ↔ φ.IsSymmetric
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.eq_1 : ∀ {α : Type u} (L : List (α × Bool)), FreeGroup.IsReduced L = List.IsChain (fun a b => a.1 = b.1 → a.2 = b.2) L
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The composition of two continuous linear equivalences as a continuous linear equivalence.  -/
ContinuousLinearEquiv.trans : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : Semiring R₁] →
        [inst_1 : Semiring R₂] →
          [inst_2 : Semiring R₃] →
            {σ₁₂ : R₁ →+* R₂} →
              {σ₂₁ : R₂ →+* R₁} →
                [inst_3 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_4 : RingHomInvPair σ₂₁ σ₁₂] →
                    {σ₂₃ : R₂ →+* R₃} →
                      {σ₃₂ : R₃ →+* R₂} →
                        [inst_5 : RingHomInvPair σ₂₃ σ₃₂] →
                          [inst_6 : RingHomInvPair σ₃₂ σ₂₃] →
                            {σ₁₃ : R₁ →+* R₃} →
                              {σ₃₁ : R₃ →+* R₁} →
                                [inst_7 : RingHomInvPair σ₁₃ σ₃₁] →
                                  [inst_8 : RingHomInvPair σ₃₁ σ₁₃] →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] →
                                        {M₁ : Type u_4} →
                                          [inst_11 : TopologicalSpace M₁] →
                                            [inst_12 : AddCommMonoid M₁] →
                                              {M₂ : Type u_5} →
                                                [inst_13 : TopologicalSpace M₂] →
                                                  [inst_14 : AddCommMonoid M₂] →
                                                    {M₃ : Type u_6} →
                                                      [inst_15 : TopologicalSpace M₃] →
                                                        [inst_16 : AddCommMonoid M₃] →
                                                          [inst_17 : Module R₁ M₁] →
                                                            [inst_18 : Module R₂ M₂] →
                                                              [inst_19 : Module R₃ M₃] →
                                                                (M₁ ≃SL[σ₁₂] M₂) → (M₂ ≃SL[σ₂₃] M₃) → M₁ ≃SL[σ₁₃] M₃
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertNumber : Std.Time.Number → Lean.MacroM (Lean.TSyntax `term)
-- Std.Time.Format.Modifier
/-- Hour, minute, and second with colon (e.g., "+01:30:15")
 -/
Std.Time.OffsetX.hourMinuteSecondColon : Std.Time.OffsetX
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α],
  r.toList = [] ↔ ¬r.lower < r.upper
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lift₂_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f : M → M → α)
  (h :
    ∀ (a₁ b₁ a₂ b₂ : M),
      MulArchimedeanClass.mk a₁ = MulArchimedeanClass.mk b₁ →
        MulArchimedeanClass.mk a₂ = MulArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂)
  (a b : M), MulArchimedeanClass.lift₂ f h (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b) = f a b
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.binaryCofan_inr : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R),
  (A.binaryCofan B).inr = CommAlgCat.ofHom Algebra.TensorProduct.includeRight
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mul_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G),
  (a * b).right = a.right * b.right
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson.eq_1 : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.jacobson R M = sInf {m | IsCoatom m}
-- Mathlib.Algebra.BigOperators.Finprod
AddEquiv.map_finsum_mem : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (g : M ≃+ N)
  (f : α → M) {s : Set α}, s.Finite → g (∑ᶠ (i : α) (_ : i ∈ s), f i) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNonUnitalRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : NonUnitalSeminormedRing R] → NonUnitalRing (BoundedContinuousFunction α R)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.examples : Lean.Meta.Match.Problem → List Lean.Meta.Match.Example
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Suffix of a Dyck word as a Dyck word, given that the count of `U`s and `D`s in the prefix
are equal.  -/
DyckWord.drop : (p : DyckWord) → (i : ℕ) → List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p) → DyckWord
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_add : ∀ {R : Type u_3} {A : Type u_4} [inst : Add R] [inst_1 : Add A] (x₁ x₂ : Unitization R A),
  (x₁ + x₂).toProd.2 = x₁.toProd.2 + x₂.toProd.2
-- Mathlib.GroupTheory.PushoutI
/-- All letters in the word are in the transversal.  -/
Monoid.PushoutI.NormalWord.Pair.normalized : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι}
  (self : Monoid.PushoutI.NormalWord.Pair d i) (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ self.tail.toList → g ∈ d.set i_1
-- Mathlib.Order.Extension.Well
instInhabitedWellOrderExtension : {α : Type u} → [Inhabited α] → Inhabited (WellOrderExtension α)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The state for the elimination monad.
* `maxVar`: the largest variable index that has not been eliminated.
* `comps`: a set of comparisons

The elimination procedure proceeds by eliminating variable `v` from `comps` progressively
in decreasing order.
 -/
Mathlib.Tactic.Linarith.LinarithData : Type
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.relations_liftable : ∀ {B : Type u_1} {M : CoxeterMatrix B} {G : Type u_5} [inst : Group G] {f : B → G},
  M.IsLiftable f → ∀ r ∈ M.relationsSet, (FreeGroup.lift f) r = 1
-- Mathlib.Algebra.Quaternion
Quaternion.instIsScalarTower : ∀ {S : Type u_1} {T : Type u_2} {R : Type u_3} [inst : CommRing R] [inst_1 : SMul S T] [inst_2 : SMul S R]
  [inst_3 : SMul T R] [IsScalarTower S T R], IsScalarTower S T (Quaternion R)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.val_inv_expOrderIso_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : G),
  ↑(WithZero.expOrderIso a)⁻¹ = (↑(Multiplicative.ofAdd a))⁻¹
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.equivSubZero_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ₁ φ₂ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₂) 0),
  (CategoryTheory.ShortComplex.Homotopy.equivSubZero φ₁ φ₂).symm h =
    ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans (h.add (CategoryTheory.ShortComplex.Homotopy.refl φ₂))).trans
      (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯)
-- Lean.Meta.Tactic.Simp.Arith.Util
/-- Quick filter for linear terms.  -/
Lean.Meta.Simp.Arith.isLinearTerm? : Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_coeff_of_ne : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} (i : ℕ), i ≠ f.natDegree → f.eraseLead.coeff i = f.coeff i
-- Mathlib.Data.Nat.Squarefree
_private.Mathlib.Data.Nat.Squarefree.0.Nat.MinSqFacProp.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → (Unit → motive none) → ((d : ℕ) → motive (some d)) → motive x
-- Init.Data.String.Pattern.Basic
/-- Provides a conversion from a pattern to an iterator of `SearchStep` that searches for matches
of the pattern from the start towards the end of a `Slice`.

While these operations can be implemented on top of `ForwardPattern`, some patterns allow
for more efficient implementations. For example, a searcher for `String` patterns derived
from the `ForwardPattern` instance on strings would try to match the pattern at every
position in the string, but more efficient string matching routines are known. Indeed, the Lean
standard library uses the Knuth-Morris-Pratt algorithm. See the module
`Init.Data.String.Pattern.String` for the implementation.

This class can be used to provide such an efficient implementation. If there is no
need to specialize in this fashion, then
`ToForwardSearcher.defaultImplementation` can be
used to automatically derive an instance.
 -/
String.Slice.Pattern.ToForwardSearcher : {ρ : Type} → ρ → outParam (String.Slice → Type) → Type
-- Mathlib.CategoryTheory.Monoidal.Center
/-- The family of isomorphisms `X ⊗ U ≅ U ⊗ X`  -/
CategoryTheory.HalfBraiding.β : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        CategoryTheory.HalfBraiding X →
          (U : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The group extension associated to the semidirect product  -/
SemidirectProduct.toGroupExtension : {N : Type u_1} →
  {G : Type u_3} → [inst : Group G] → [inst_1 : Group N] → (φ : G →* MulAut N) → GroupExtension N (N ⋊[φ] G) G
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity between indexed sets of vertices v₁ and v₂.
Use `open scoped Similar` to access the `v₁ ∼ v₂` notation.  -/
Similar : {ι : Type u_1} →
  {P₁ : Type u_3} → {P₂ : Type u_4} → [PseudoEMetricSpace P₁] → [PseudoEMetricSpace P₂] → (ι → P₁) → (ι → P₂) → Prop
-- Lean.Elab.Command.Scope
Lean.Elab.Command.instInhabitedScope : Inhabited Lean.Elab.Command.Scope
-- Init.Data.Nat.Fold
Nat.all_zero : ∀ {f : (i : ℕ) → i < 0 → Bool}, Nat.all 0 f = true
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.atIdxSlow?_appendSnd : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Productive α₁ Id]
  [Std.Iterators.Productive α₂ Id] {it₂ : Std.Iter β} {n : ℕ},
  Std.Iter.atIdxSlow? n (Std.Iter.Intermediate.appendSnd α₁ it₂) = Std.Iter.atIdxSlow? n it₂
-- Mathlib.Analysis.Normed.Algebra.Spectrum
upperHemicontinuous_spectrum : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NormedField 𝕜] [ProperSpace 𝕜] [inst_2 : NormedRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [CompleteSpace A], UpperHemicontinuous (spectrum 𝕜)
-- Mathlib.Order.Filter.Tendsto
Filter.map_eq_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α),
  φ ∘ ψ = id → Filter.Tendsto φ f g → Filter.Tendsto ψ g f → Filter.map φ f = g
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Synonym of `Matrix.IsParabolic`, for dot-notation.  -/
Matrix.GeneralLinearGroup.IsParabolic : {R : Type u_1} → [inst : CommRing R] → GL (Fin 2) R → Prop
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.find?_bool_eq_some_iff_splits : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ t c u, pos.Splits t (String.singleton c ++ u) ∧ p c = true ∧ ∀ d ∈ t.toList, p d = false
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.liftH_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : A ⟶ h.Q)
  (hk : CategoryTheory.CategoryStruct.comp k h.g' = 0), CategoryTheory.CategoryStruct.comp (h.liftH k hk) h.ι = k
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Equivalence.prun_step : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β γ : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [LawfulMonad m] {it : Std.IterM m β}
  {f : (step : Std.IterStep (Std.IterM m β) β) → it.stepAsHetT.Property step → m γ},
  it.stepAsHetT.prun f = do
    let step ← it.step
    f ↑step.inflate ⋯
-- Mathlib.Order.LatticeIntervals
Set.Iic.coe_sup : ∀ {α : Type u_1} {a : α} [inst : SemilatticeSup α] {x y : ↑(Set.Iic a)}, ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_roi : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t lowerBound<...*) =
        List.filter (fun e => (compare e.1 lowerBound).isGT) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Aesop.Stats.Basic
Aesop.instToJsonScriptGenerated.toJson : Aesop.ScriptGenerated → Lean.Json
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insert k v).isEmpty = false
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_top_of_le_card : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite G], Nat.card G ≤ Nat.card ↥H → H = ⊤
-- Init.Prelude
/-- Gets the current state that has the explicitly-provided type `σ`. When the current monad has
multiple state types available, this function selects one of them.
 -/
getThe : (σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → m σ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instUniqueHom : {J : CategoryTheory.Limits.MultispanShape} → (a : CategoryTheory.Limits.WalkingMultispan J) → Unique (a ⟶ a)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying `ContinuousAddMonoidHom`.  -/
ProfiniteAddGrp.Hom.hom' : {A B : ProfiniteAddGrp.{u}} → A.Hom B → ↑A.toProfinite.toTop →ₜ+ ↑B.toProfinite.toTop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.addHom_ext' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddZeroClass N]
  ⦃f g : SkewMonoidAlgebra k G →+ N⦄,
  (∀ (x : G), f.comp (SkewMonoidAlgebra.singleAddHom x) = g.comp (SkewMonoidAlgebra.singleAddHom x)) → f = g
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddLeftRegular_op`. -/
IsAddLeftRegular.op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddRightRegular a → IsAddLeftRegular (AddOpposite.op a)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.rightRel_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, (QuotientAddGroup.rightRel s) x y ↔ y + -x ∈ s
-- Mathlib.CategoryTheory.Limits.Filtered
/-- Class for having filtered colimits.  -/
CategoryTheory.Limits.HasFilteredColimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Sat.AIG.Basic
/-- Evaluate an `AIG.Entrypoint` using some assignment for atoms.
 -/
Std.Sat.AIG.denote : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → (α → Bool) → Std.Sat.AIG.Entrypoint α → Bool
-- Mathlib.Topology.Basic
/-- A constructor for topologies by specifying the closed sets,
and showing that they satisfy the appropriate conditions.  -/
TopologicalSpace.ofClosed : {X : Type u} → (T : Set (Set X)) → ∅ ∈ T → (∀ A ⊆ T, ⋂₀ A ∈ T) → (∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T) → TopologicalSpace X
-- Mathlib.Algebra.Group.Defs
NSMul.ofSMul : {M : Type u_2} → [SMul ℕ M] → NSMul M
-- Mathlib.MeasureTheory.Measure.GiryMonad
/-- Monadic bind on `Measure`, only works in the category of measurable spaces and measurable
functions. When the function `f` is not measurable the result is not well defined.  -/
MeasureTheory.Measure.bind : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} → MeasureTheory.Measure α → (α → MeasureTheory.Measure β) → MeasureTheory.Measure β
-- Mathlib.Data.List.Dedup
List.dedup_cons_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∉ l → (a :: l).dedup = a :: l.dedup
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- `RestrictedProduct.evalMonoidHom j` is the monoid homomorphism from the restricted
product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`.
 -/
RestrictedProduct.evalMonoidHom : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            (j : ι) →
              [inst_1 : (i : ι) → Monoid (R i)] →
                [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
                  RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕 →* R j
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.add_eq_max_of_ne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ_[p]}, ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖
-- Mathlib.Topology.Instances.ENat
ENat.nhds_eq_pure : ∀ {n : ℕ∞}, n ≠ ⊤ → nhds n = pure n
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
_private.Mathlib.Analysis.Fourier.RiemannLebesgueLemma.0.termI : Lean.ParserDescr
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLE_iff_smulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsDomain α] [Module.IsTorsionFree α β],
  SMulPosReflectLE α β ↔ SMulPosReflectLT α β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.constGetThenInsertIfNew? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α} {v : β} {h : t.WF},
  (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ⋯).2.WF
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- Negative part of the Jordan decomposition  -/
MeasureTheory.JordanDecomposition.negPart : {α : Type u_2} → [inst : MeasurableSpace α] → MeasureTheory.JordanDecomposition α → MeasureTheory.Measure α
-- Mathlib.Data.Fin.Embedding
Fin.castLEEmb_apply : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), (Fin.castLEEmb h) i = Fin.castLE h i
-- Mathlib.Order.Basic
/-- **Alias** of `ne_of_gt`. -/
LT.lt.ne' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → a ≠ b
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Makes an additive isomorphism from a bijection which preserves addition.  -/
AddEquiv.mk' : {M : Type u_4} →
  {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → (f : M ≃ N) → (∀ (x y : M), f (x + y) = f x + f y) → M ≃+ N
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ‖↑p‖ = (↑p)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.instPreservesLimitsOfShapeWalkingCospanOfDiscreteWalkingPair : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [Quiver.IsThin D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F
-- Mathlib.Logic.Equiv.Defs
/-- The dependent product of sorts is associative up to an equivalence.  -/
Equiv.pSigmaAssoc : {α : Sort u_1} →
  {β : α → Sort u_2} →
    (γ : (a : α) → β a → Sort u_3) → (ab : (a : α) ×' β a) ×' γ ab.fst ab.snd ≃ (a : α) ×' (b : β a) ×' γ a b
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The category of types has `X ⊕ Y`,
as the binary coproduct of `X` and `Y`.
 -/
CategoryTheory.Limits.Types.binaryCoproductColimitCocone : (X Y : Type u) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair X Y)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_add_mk_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {m1 m2 : M} {s : ℕ+},
  DivisibleHull.mk m1 s + DivisibleHull.mk m2 s = DivisibleHull.mk (m1 + m2) s
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_iInter : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {ι : Sort u_5} (a : α) (t : ι → Set β),
  a +ᵥ ⋂ i, t i = ⋂ i, a +ᵥ t i
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.toList.match_1.eq_3 : ∀ {α : Type u_1} (motive : (x : Bool) → Lists' α x → Sort u_2) (b : Bool) (a : Lists' α b) (l : Lists' α true)
  (h_1 : (a : α) → motive false (Lists'.atom a)) (h_2 : Unit → motive true Lists'.nil)
  (h_3 : (b : Bool) → (a : Lists' α b) → (l : Lists' α true) → motive true (a.cons' l)),
  (match true, a.cons' l with
    | .(false), Lists'.atom a => h_1 a
    | .(true), Lists'.nil => h_2 ()
    | .(true), a.cons' l => h_3 b a l) =
    h_3 b a l
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_eq_dropEndWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.dropEndWhile pat = s.toSlice.dropEndWhile pat
-- Mathlib.Control.Basic
Bind.kleisliRight.eq_1 : ∀ {α : Type u} {m : Type u_1 → Type u_2} {β γ : Type u_1} [inst : Bind m] (f₁ : α → m β) (f₂ : β → m γ) (a : α),
  (f₁ >=> f₂) a = f₁ a >>= f₂
-- Mathlib.Topology.Defs.Basic
/-- The intersection of two open sets is an open set. Use `IsOpen.inter` instead.  -/
TopologicalSpace.isOpen_inter : ∀ {X : Type u} [self : TopologicalSpace X] (s t : Set X),
  TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
-- Lean.Widget.InteractiveCode
/-- Pretty prints the expression `e` using delaborator `delab`, returning an object that represents
the pretty printed syntax paired with information needed to support hovers.
 -/
Lean.Widget.ppExprTagged : Lean.Expr →
  optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab →
    Lean.MetaM Lean.Widget.CodeWithInfos