mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For a graded ring `⨁ᵢ 𝒜ᵢ` graded by
`[AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι]`, the irrelevant ideal refers to
`⨁_{i>0} 𝒜ᵢ`, or equivalently `{a | a₀ = 0}`. This definition is used in `Proj` construction where
`ι` is always `ℕ` so the irrelevant ideal is simply elements with `0` as 0-th coordinate.
 -/
HomogeneousIdeal.irrelevant : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddCommMonoid ι] →
            [inst_3 : PartialOrder ι] →
              [CanonicallyOrderedAdd ι] →
                [inst_5 : SetLike σ A] →
                  [inst_6 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_7 : GradedRing 𝒜] → HomogeneousIdeal 𝒜
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I}
  (hK hK_1 : CategoryTheory.Limits.IsLimit K),
  hK = hK_1 →
    ∀ {T : C} (k k_1 : (a : J.L) → T ⟶ I.left a) (e_k : k = k_1)
      (hk :
        ∀ (b : J.R),
          CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
            CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)),
      CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk = CategoryTheory.Limits.Multifork.IsLimit.lift hK_1 k_1 ⋯
-- Lean.Compiler.IR.Basic
Lean.IR.mkIf : Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.tail =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Aesop.Forward.State
/-- Remove a hyp from `slot` and all later slots.  -/
Aesop.VariableMap.eraseHyp : Aesop.VariableMap → Lean.FVarId → Aesop.SlotIndex → Aesop.VariableMap
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnAddMonoidHom_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β] (f : C(α, β)) (a : α), ContinuousMap.coeFnAddMonoidHom f a = f a
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- For all `x : R`, `smoothingFun μ x ≤ μ x`.  -/
smoothingFun_le_self : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (x : R), smoothingFun μ x ≤ μ x
-- Mathlib.MeasureTheory.Function.Floor
Measurable.nat_ceil : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] [inst_1 : Semiring R] [inst_2 : LinearOrder R]
  [inst_3 : FloorSemiring R] [inst_4 : TopologicalSpace R] [OrderTopology R] [inst_6 : MeasurableSpace R]
  [OpensMeasurableSpace R] {f : α → R}, Measurable f → Measurable fun x => ⌈f x⌉₊
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.constCompPiIsoConst_inv_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1}
  [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X_1 : (i : α) → I i),
  (CategoryTheory.Limits.Pi.constCompPiIsoConst X).inv.app X_1 = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFilteredOrEmpty.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (X Y : C), ∃ Z x x, True) →
    (∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
        ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) →
      CategoryTheory.IsFilteredOrEmpty C
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- The square of `f.normDet` equals the determinant of the Gram matrix formed by vectors mapped from
an orthonormal basis.
 -/
LinearMap.normDet_sq_eq_det_gram : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {ι : Type u_5} [inst_6 : Fintype ι] [inst_7 : DecidableEq ι] (f : U →ₗ[𝕜] V)
  (b : OrthonormalBasis ι 𝕜 U), ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x => f (b x)).det
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.mk.inj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {obj obj_1 : B}, { obj := obj } = { obj := obj_1 } → obj = obj_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.P_δ.δ : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategoryGenRel.P_δ (SimplexCategoryGenRel.δ i)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.map_csInf_le_csInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : ConditionallyCompleteLattice α]
  {f : α → β} {s : Set α},
  s.Nonempty →
    Monotone f → autoParam (BddBelow s) Monotone.map_csInf_le_csInf_image._auto_1 → f (sInf s) ≤ sInf (f '' s)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.cancelVar'.induct_unfolding : ∀ (c : ℤ) (x : Lean.Grind.CommRing.Var)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ), motive (Lean.Grind.CommRing.Poly.num k) acc (acc.addConst k)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        have n := m.degreeOf x;
        (decide (n > 0) && decide (c ^ n ∣ k)) = true →
          motive p (Lean.Grind.CommRing.Poly.insert (k / c ^ n) (m.cancelVar x) acc)
              (Lean.Grind.CommRing.Poly.cancelVar' c x p
                (Lean.Grind.CommRing.Poly.insert (k / c ^ n) (m.cancelVar x) acc)) →
            motive (Lean.Grind.CommRing.Poly.add k m p) acc
              (Lean.Grind.CommRing.Poly.cancelVar' c x p
                (Lean.Grind.CommRing.Poly.insert (k / c ^ n) (m.cancelVar x) acc))) →
      (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          have n := m.degreeOf x;
          (decide (n > 0) && decide (c ^ n ∣ k)) = false →
            motive p (Lean.Grind.CommRing.Poly.insert k m acc)
                (Lean.Grind.CommRing.Poly.cancelVar' c x p (Lean.Grind.CommRing.Poly.insert k m acc)) →
              motive (Lean.Grind.CommRing.Poly.add k m p) acc
                (Lean.Grind.CommRing.Poly.cancelVar' c x p (Lean.Grind.CommRing.Poly.insert k m acc))) →
        ∀ (p acc : Lean.Grind.CommRing.Poly), motive p acc (Lean.Grind.CommRing.Poly.cancelVar' c x p acc)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The Cartesian product of `C^n` functions is `C^n`.  -/
ContDiff.prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} {g : E → G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => (f x, g x)
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleMapHomologicalComplex_inv_app_self : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] [inst_4 : CategoryTheory.Limits.HasZeroObject W₁]
  [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_6 : F.PreservesZeroMorphisms] (c : ComplexShape ι) [inst_7 : DecidableEq ι] (j : ι) (X : W₁),
  ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f j =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j (F.obj X)).hom
      (F.map (HomologicalComplex.singleObjXSelf c j X).inv)
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_inv_Ioi : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : CommGroup G] [IsOrderedMonoid G] [MeasurableInv G] [μ.IsInvInvariant] {c : G}
  {f : G → F}, MeasureTheory.IntegrableOn f (Set.Iio c⁻¹) μ → MeasureTheory.IntegrableOn (fun x => f x⁻¹) (Set.Ioi c) μ
-- Batteries.Data.Array.Scan
Array.scanl_empty : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β), Array.scanl f init #[] = #[init]
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.eq_zero_of_mem_of_neg_mem' : ∀ {G : Type u_1} [inst : AddCommGroup G] (self : AddGroupCone G) {a : G}, a ∈ self.carrier → -a ∈ self.carrier → a = 0
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.top_apply : ∀ {α : Type u_1} {s : Set α}, s.Nonempty → ⊤ s = ⊤
-- Init.Data.Nat.Basic
Nat.instLawfulIdentityHMulOfNat : Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
/-- Extension for the `positivity` tactic: `SimpleGraph.triangleRemovalBound ε` is positive
if `ε` is.

This exploits the positivity of the junk value of `triangleRemovalBound ε` for `ε ≥ 1`.  -/
Mathlib.Meta.Positivity.evalTriangleRemovalBound : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem : ∀ {𝕜 : 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] {f₀ f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → x ∈ s → (HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x)
-- Mathlib.LinearAlgebra.Ray
/-- A ray does not equal its own negation.  -/
Module.Ray.ne_neg_self : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsDomain R] [Module.IsTorsionFree R M] (x : Module.Ray R M), x ≠ -x
-- Mathlib.NumberTheory.Padics.Complex
/-- The underlying metric space of `ℂ_[p]` is ultrametric.  -/
PadicComplex.isUltrametricDist : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsUltrametricDist ℂ_[p]
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
Equiv.mulRight₀.congr_simp : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a a_1 : G₀) (e_a : a = a_1) (ha : a ≠ 0),
  Equiv.mulRight₀ a ha = Equiv.mulRight₀ a_1 ⋯
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.options : Lean.Elab.CommandContextInfo → Lean.Options
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).obj₁ = DerivedCategory.Q.obj S.X₁
-- Mathlib.Algebra.Order.Module.Pointwise
upperBounds_smul_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  {s : Set β} {a : α}, a < 0 → upperBounds (a • s) = a • lowerBounds s
-- Mathlib.Algebra.Module.NatInt
/-- All `ℤ`-module structures are equal. Not an instance since in mathlib all `AddCommGroup`
should normally have exactly one `ℤ`-module structure by design.  -/
AddCommGroup.uniqueIntModule : {M : Type u_3} → [inst : AddCommGroup M] → Unique (Module ℤ M)
-- Mathlib.CategoryTheory.Monad.Basic
/-- The comultiplication for the comonad.  -/
CategoryTheory.Comonad.δ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (self : CategoryTheory.Comonad C) → self.toFunctor ⟶ self.comp self.toFunctor
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- A terminal object is initial in the opposite category.  -/
CategoryTheory.Limits.initialOpOfTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsInitial (Opposite.op X)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_rio : ∀ {n : ℕ}, (*...n).toList.toArray = (*...n).toArray
-- Lean.Parser.Do
Lean.Parser.Term.doTry.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.of_ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) {a : A},
  Transcendental S (g a) →
    Function.Injective ⇑f → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Transcendental R a
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsIntegral.of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} [h : AlgebraicGeometry.IsIntegral X] (f : X ⟶ Y) [CategoryTheory.IsIso f],
  AlgebraicGeometry.IsIntegral Y
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_univ : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y}, e.restr Set.univ = e
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundariesOfIsCoboundary₂_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] {f : G × G → A} (hf : groupCohomology.IsCoboundary₂ f)
  (a : G × G), ↑(groupCohomology.coboundariesOfIsCoboundary₂ hf) a = f a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.ext.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j),
  CategoryTheory.Limits.Cocone.ext φ w = CategoryTheory.Limits.Cocone.extInv φ ⋯
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The family of Schwartz seminorms.  -/
schwartzSeminormFamily : (𝕜 : Type u_2) →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NormedField 𝕜] →
                [inst_5 : NormedSpace 𝕜 F] → [inst_6 : SMulCommClass ℝ 𝕜 F] → SeminormFamily 𝕜 (SchwartzMap E F) (ℕ × ℕ)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.isSimplyLaced_E₇ : CartanMatrix.E₇.IsSimplyLaced
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.comp_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] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- The degree `[E : K]` of the inertia field `E` over `K` equals the product of the number of
prime ideals of `B` lying over `p` and the inertia degree of `p` in `B`.
 -/
IsInertiaField.rank_right : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [FiniteDimensional K L] [inst_8 : MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal]
  (E : Type u_6) [inst_16 : Field E] [inst_17 : Algebra E L] [IsInertiaField K L P E] [IsGalois K L]
  [inst_20 : Algebra K E] [IsScalarTower K E L], p ≠ ⊥ → Module.finrank K E = (p.primesOver B).ncard * p.inertiaDegIn B
-- Mathlib.Data.Multiset.MapFold
Multiset.map_cons : ∀ {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α), Multiset.map f (a ::ₘ s) = f a ::ₘ Multiset.map f s
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.continuous_of_isContPerfPair : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) {x : M} [p.IsContPerfPair],
  Continuous ⇑(p x)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.coe_sup : ∀ {N : Type u_7} [inst : AddCommMonoid N] (H K : AddSubmonoid N), ↑(H ⊔ K) = ↑H + ↑K
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.foldlM.match_1.eq_1 : ∀ {δ : Type u_4} {α : Type u_1} {β : Type u_2} (motive : δ → Batteries.AssocList α β → Sort u_3) (d : δ)
  (h_1 : (d : δ) → motive d Batteries.AssocList.nil)
  (h_2 : (d : δ) → (a : α) → (b : β) → (es : Batteries.AssocList α β) → motive d (Batteries.AssocList.cons a b es)),
  (match d, Batteries.AssocList.nil with
    | d, Batteries.AssocList.nil => h_1 d
    | d, Batteries.AssocList.cons a b es => h_2 d a b es) =
    h_1 d
-- Mathlib.Order.CompleteLattice.Lemmas
biSup_inf_le_inf_biSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (s : Set β) (a : α),
  ⨆ i ∈ s, a ⊓ f i ≤ a ⊓ ⨆ i ∈ s, f i
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The restriction of a sheafed space along an open embedding into the space.
 -/
AlgebraicGeometry.SheafedSpace.restrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U : TopCat} →
      (X : AlgebraicGeometry.SheafedSpace C) →
        {f : U ⟶ ↑X.toPresheafedSpace} →
          Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → AlgebraicGeometry.SheafedSpace C
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mul_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.GrpObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.GrpObj.inv =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
        CategoryTheory.MonObj.mul)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Integral closures are all isomorphic to each other.  -/
IsIntegralClosure.equiv : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R B] →
              [inst_4 : Algebra A B] →
                [IsIntegralClosure A R B] →
                  (A' : Type u_4) →
                    [inst_6 : CommRing A'] →
                      [inst_7 : Algebra A' B] →
                        [IsIntegralClosure A' R B] →
                          [inst_9 : Algebra R A] →
                            [inst_10 : Algebra R A'] → [IsScalarTower R A B] → [IsScalarTower R A' B] → A ≃ₐ[R] A'
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- Alternative formulation of `MeasureTheory.SignedMeasure.exists_isCompl_positive_negative`
(the Hahn decomposition theorem) using set complements.  -/
MeasureTheory.SignedMeasure.exists_compl_positive_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  ∃ i,
    MeasurableSet i ∧
      MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
        MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.center.instNonUnitalCommRing : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      [inst_1 : NonUnitalNonAssocRing A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] → NonUnitalCommRing ↥(NonUnitalSubalgebra.center R A)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
/-- If `c ∈ [a, b]`, then the distance between `a` and `c` is less than or equal to
that of `a` and `b`  -/
Set.abs_sub_left_of_mem_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b c : α},
  c ∈ Set.uIcc a b → |c - a| ≤ |b - a|
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.mk.injEq : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (toDistribMulActionHom : R →ₑ+[φ] S) (map_one' : toDistribMulActionHom.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : R), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y)
  (toDistribMulActionHom_1 : R →ₑ+[φ] S) (map_one'_1 : toDistribMulActionHom_1.toFun 1 = 1)
  (map_mul'_1 :
    ∀ (x y : R),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y),
  ({ toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toDistribMulActionHom = toDistribMulActionHom_1)
-- Mathlib.Order.Hom.Set
OrderEmbedding.orderIso_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {f : α ↪o β} (a : α), OrderEmbedding.orderIso a = ⟨f a, ⋯⟩
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.hasEval_def : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] (a : σ → S),
  MvPowerSeries.HasEval a ↔ (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧ Filter.Tendsto a Filter.cofinite (nhds 0)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.nil.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural),
  sizeOf (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α) = 1 + sizeOf e + sizeOf α
-- Mathlib.Algebra.GCDMonoid.Basic
StrongNormalizationMonoid.mk : {α : Type u_2} →
  [inst : CommMonoidWithZero α] →
    [toNormalizationMonoid : NormalizationMonoid α] →
      (∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b) →
        (∀ (u : αˣ), normUnit ↑u = u⁻¹) → StrongNormalizationMonoid α
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_ite_self_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {N : Type u_16} [inst_1 : AddCommMonoid N] (f : α →₀ N) (a : α),
  (f.sum fun x v => if a = x then v else 0) = f a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sub_ne_pi_of_sign_eq_of_sign_ne_zero : ∀ (a b : Real.Angle), a.sign = b.sign → b.sign ≠ 0 → a - b ≠ ↑Real.pi
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousEval.toContinuousMapClass : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y], ContinuousMapClass F X Y