mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_const_mul : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 →
    f c ≠ 0 →
      IsPowMul ⇑f → ∀ (x : R), seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'.sizeOf_spec : ∀ {X : SSet} (toS : X.S) (nonDegenerate : toS.simplex ∈ X.nonDegenerate toS.dim),
  sizeOf { toS := toS, nonDegenerate := nonDegenerate } = 1 + sizeOf toS
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.mk : {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} →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                W.IsInvertedBy L →
                  (lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E) →
                    (∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift F hF) = F) →
                      (∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂) →
                        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.findCommonPrefix.go : Lean.Name → List Lean.Name → Lean.Name
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.resolution.π.eq_1 : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G),
  Rep.FiniteCyclicGroup.resolution.π k g =
    (((Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj (Rep.leftRegular k G)).toSingle₀Equiv
          (Rep.trivial k G k)).symm
      ⟨(Rep.trivial k G k).leftRegularHom 1, ⋯⟩
-- Init.Data.Fin.Lemmas
Fin.coe_natAdd : ∀ (n : ℕ) {m : ℕ} (i : Fin m), ↑(Fin.natAdd n i) = n + ↑i
-- Mathlib.Data.ZMod.Basic
ZMod.val_two_eq_two_mod : ∀ (n : ℕ), ZMod.val 2 = 2 % n
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- `AbsolutelyContinuousOnInterval f a b`: A function `f` is *absolutely continuous* on `uIcc a b`
if the function which (intuitively) maps `uIoc (a i) (b i)`, `i < n` to
`∑ i ∈ Finset.range n, dist (f (a i)) (f (b i))` tendsto `𝓝 0` wrt `totalLengthFilter` restricted
to `disjWithin a b`. This is equivalent to the traditional `ε`-`δ` definition: for any `ε > 0`,
there is `δ > 0` such that for any finite disjoint collection of intervals `uIoc (a i) (b i)` for
`i < n` where `a i`, `b i` are all in `uIcc a b` for `i < n`, if
`∑ i ∈ range n, dist (a i) (b i) < δ`, then `∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε`.  -/
AbsolutelyContinuousOnInterval : {X : Type u_1} → [PseudoMetricSpace X] → (ℝ → X) → ℝ → ℝ → Prop
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coeCLM_injective : ∀ {𝕜 : outParam (Type u_1)} {H : Type u_2} {X : outParam (Type u_3)} {V : outParam (Type u_4)} {inst : RCLike 𝕜}
  {inst_1 : NormedAddCommGroup V} {inst_2 : InnerProductSpace 𝕜 V} {inst_3 : NormedAddCommGroup H}
  {inst_4 : InnerProductSpace 𝕜 H} [self : RKHS 𝕜 H X V], Function.Injective ⇑(RKHS.coeCLM 𝕜)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.zeroHom_id : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M], Finsupp.mapRange.zeroHom (ZeroHom.id M) = ZeroHom.id (ι →₀ M)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If for every cell either `A ∩ openCell n j` is empty or `A ∩ closedCell n j` is closed then
`A` is closed.  -/
Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {A : Set X},
  A ⊆ C →
    IsClosed (A ∩ D) →
      (∀ (n : ℕ),
          0 < n →
            ∀ (j : Topology.RelCWComplex.cell C n),
              Disjoint A (Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) →
        IsClosed A
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- The cardinals are well-ordered. We express it here by the fact that in any set of cardinals
there is an element that injects into the others.
See `Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice instances.  -/
Function.Embedding.min_injective : ∀ {ι : Type u} (β : ι → Type v) [I : Nonempty ι], ∃ i, Nonempty ((j : ι) → β i ↪ β j)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.tensorObj_comul : ∀ {R : Type u} [inst : CommRing R] (K L : CoalgCat R),
  CoalgebraStruct.comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
-- Mathlib.Algebra.Lie.LieTheorem
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.T.eq_1 : ∀ {R : Type u_1} {A : Type u_3} {V : Type u_4} [inst : CommRing R] [inst_1 : LieRing A] [inst_2 : LieAlgebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : LieRingModule A V] [inst_6 : LieModule R A V] (χ : A → R)
  (w : A), LieModule.T✝ χ w = (LieModule.toEnd R A V) w - χ w • 1
-- Mathlib.RingTheory.Smooth.Basic
/-- **Alias** of `Algebra.instFormallySmoothMvPolynomial`. -/
Algebra.mvPolynomial : ∀ {R : Type u} [inst : CommRing R] (σ : Type u_4), Algebra.FormallySmooth R (MvPolynomial σ R)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  Std.DHashMap.Const.get? (m₁.union m₂) k = (Std.DHashMap.Const.get? m₂ k).or (Std.DHashMap.Const.get? m₁ k)
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.multipliableUniformlyOn_one_add : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R]
  [CompleteSpace R] [inst_3 : TopologicalSpace α] {f : ι → α → R},
  IsCompact K →
    Summable u →
      (∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) →
        (∀ (i : ι), ContinuousOn (f i) K) → MultipliableUniformlyOn (fun i x => 1 + f i x) K
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.exists_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (s : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)),
  ∀ x ∈ U,
    ∃ g,
      ∃ (_ : x ∈ PrimeSpectrum.basicOpen g) (i : PrimeSpectrum.basicOpen g ≤ U),
        ∃ f,
          AlgebraicGeometry.StructureSheaf.const f g (PrimeSpectrum.basicOpen g) ⋯ =
            (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structureSheafInType R M).obj.map i.hom.op)) s
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_eq_none_iff : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.findRev? p = none ↔ ∀ (i : Fin n), p i = false
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_monomial : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (g : σ → S₁) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.aeval g) ((MvPolynomial.monomial d) r) = (algebraMap R S₁) r * d.prod fun i k => g i ^ k
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_univ_two : ∀ (a b : ℕ), Nat.multinomial Finset.univ ![a, b] = (a + b).factorial / (a.factorial * b.factorial)
-- Mathlib.Combinatorics.Graph.Basic
Graph.Adj.symm : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β}, G.Adj x y → G.Adj y x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instIsScalarTower : ∀ {M : Type u_2} {N : Type u_3} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : DistribMulAction M α] [inst_4 : SMulCommClass M α α] [inst_5 : IsScalarTower M α α]
  [inst_6 : DistribMulAction N α] [inst_7 : SMulCommClass N α α] [inst_8 : IsScalarTower N α α] [inst_9 : SMul M N]
  [IsScalarTower M N α], IsScalarTower M N (CentroidHom α)
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences.eq_1 : ∀ (x y : NNReal) (n : ℕ), x.agmSequences y n = (fun p => (NNReal.sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The second projection functor.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.snd : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X → CategoryTheory.Functor X C
-- Mathlib.Order.UpperLower.Closure
UpperSet.erase.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (a : α),
  s.erase a = { carrier := ↑s \ ↑(LowerSet.Iic a), upper' := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_adjoinIntegral_self : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P) (hx : IsIntegral R x), x ∈ FractionalIdeal.adjoinIntegral S x hx
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_self_sub_right : ∀ {m n : ℕ}, m ≤ n → (n.Coprime (n - m) ↔ n.Coprime m)
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.of_keys_eq : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)},
  Std.Internal.List.keys l = Std.Internal.List.keys l' →
    Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys l'
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.mem_supported_support : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : α →₀ M), p ∈ Finsupp.supported M R ↑p.support
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint x y
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ι_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory}
  {f : X ⟶ Y}, P.ι.map f = f.hom
-- Mathlib.RingTheory.PicardGroup
/-- An invertible module over a commutative semiring is Zariski-locally free of rank 1.
Theorem 10.7 in [BorgerJun2024].

More precisely, there is a finite set of elements of `R` that generate the unit ideal,
and localizing `M` at any one of them yields a free module.

Finite projective modules over a local commutative semiring may not be free,
see Remark 7.10, Example 9.6 and 9.8.  -/
Module.Invertible.exists_finset_free_localization : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M],
  ∃ s, Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, Module.Free (Localization.Away r) (LocalizedModule.Away r M)
-- Mathlib.Data.List.Cycle
Cycle.length_nontrivial : ∀ {α : Type u_1} {s : Cycle α}, s.Nontrivial → 2 ≤ s.length
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_spec'_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x y : R) (hy : y ∈ M),
  (algebraMap R S) y * IsLocalization.mk' S x ⟨y, hy⟩ = (algebraMap R S) x
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.continuous : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂] {M₁ : Type u_3} {M₂ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommGroup M₂] [inst_7 : Module 𝕜₁ M₁]
  [inst_8 : Module 𝕜₂ M₂] [IsTopologicalAddGroup M₁] [ContinuousConstSMul 𝕜₁ M₁] [IsTopologicalAddGroup M₂]
  [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → Continuous ⇑f
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {n : ℕ} [NeZero n]
  [inst_4 : IsDomain B] {ζ : B}, IsPrimitiveRoot ζ n → Algebra.adjoin A ((Polynomial.cyclotomic n A).rootSet B) = A[ζ]
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ),
  MvPowerSeries.X s = (MvPowerSeries.monomial fun₀ | s => 1) 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, a ∉ m → m.getD a fallback = fallback
-- Aesop.Tree.Data
Aesop.NodeState.toEmoji : Aesop.NodeState → String
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [inst_1 : Preorder E] [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E]
  (hm : m ≤ m₀), MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → f ≤ᵐ[μ] g → f ≤ᵐ[μ.trim hm] g
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBSet.isEmpty.match_1.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (motive : RBTree.RBSet α cmp → Sort u_2)
  (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil)
  (h_1 : (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil) → motive ⟨RBTree.RBNode.nil, property⟩)
  (h_2 : (x : RBTree.RBSet α cmp) → motive x),
  (match ⟨RBTree.RBNode.nil, property⟩ with
    | ⟨RBTree.RBNode.nil, property⟩ => h_1 property
    | x => h_2 x) =
    h_1 property
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.mem_iff_infEDist_zero_of_closed`.

---

Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes  -/
EMetric.mem_iff_infEdist_zero_of_closed : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, IsClosed s → (x ∈ s ↔ Metric.infEDist x s = 0)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.replaceEntry k v l).length = l.length
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x))
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functor_obj_obj_map : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : Type (max u w)) {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y),
  ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.map f =
    TypeCat.ofHom fun g => LocallyConstant.comap (TopCat.Hom.hom f.unop.hom) g
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_add_le : ∀ {p q : ℝ}, ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C0.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.C0 C ho = C ∩ {f | f (Profinite.NobelingProof.term I ho) = false}
-- Init.Data.Nat.ToString
Nat.digitChar_eq_seven : ∀ {n : ℕ}, n.digitChar = '7' ↔ n = 7
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.match_3.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ) (fuel_1 : ℕ),
  fuel = fuel_1.succ →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_2 fuel_1
-- Mathlib.Algebra.Order.Ring.WithTop
/-- A version of `WithTop.map` for `MonoidWithZeroHom`s.  -/
MonoidWithZeroHom.withTopMap : {R : Type u_2} →
  {S : Type u_3} →
    [inst : MulZeroOneClass R] →
      [inst_1 : DecidableEq R] →
        [inst_2 : Nontrivial R] →
          [inst_3 : MulZeroOneClass S] →
            [inst_4 : DecidableEq S] →
              [inst_5 : Nontrivial S] → (f : R →*₀ S) → Function.Injective ⇑f → WithTop R →*₀ WithTop S
-- Lean.Meta.Sym.Simp.SimpM
/-- Cache for generated funext theorems  -/
Lean.Meta.Sym.Simp.State.funext : Lean.Meta.Sym.Simp.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr
-- Mathlib.Data.Num.Bitwise
/-- Alternative representation of integers using a sign bit at the end.
The convention on sign here is to have the argument to `msb` denote
the sign of the MSB itself, with all higher bits set to the negation
of this sign. The result is interpreted in two's complement.

```
13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true))))
-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))
```

  As with `Num`, a special case must be added for zero, which has no msb,
but by two's complement symmetry there is a second special case for -1.
Here the `Bool` field indicates the sign of the number.

```
0  = ..0000000(base 2) = zero false
-1 = ..1111111(base 2) = zero true
```  -/
SNum : Type
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  Finset.image MulOpposite.op (s * t) = Finset.image MulOpposite.op t * Finset.image MulOpposite.op s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.neg.match_1.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (motive : W'.Point → Sort u_2) (x y : R)
  (h : W'.Nonsingular x y) (h_1 : Unit → motive WeierstrassCurve.Affine.Point.zero)
  (h_2 : (x y : R) → (h : W'.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)),
  (match WeierstrassCurve.Affine.Point.some x y h with
    | WeierstrassCurve.Affine.Point.zero => h_1 ()
    | WeierstrassCurve.Affine.Point.some x y h => h_2 x y h) =
    h_2 x y h
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_neg : ∀ (f : ℕ → ℂ) (s : ℂ), LSeries.term (-f) s = -LSeries.term f s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow (S, S') (T.prod T')} (η : X ⟶ Y),
  (CategoryTheory.StructuredArrow.prodFunctor S S' T T').map η =
    (CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right η).1 ⋯,
      CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right η).2 ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_hom_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : A),
  (φ.associator φ' φ'').hom.left.app x = CategoryTheory.CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x)))
-- Mathlib.Computability.DFA
DFA.evalFrom_reindex : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ') (s : σ') (x : List α),
  ((DFA.reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)
-- Mathlib.Topology.Order.DenselyOrdered
closure_uIoc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.uIoc a b) = Set.uIcc a b
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalNonAssocRing : {R : Type u} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing (ULift.{u_1, u} R)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.keysArray.toList = t.keys
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_monotone_time : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X), Monotone fun n => Dynamics.netMaxcard T F U n
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_single_one : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) (r : k) (x : G), (f * SkewMonoidAlgebra.single 1 r).coeff x = f.coeff x * x • r
-- Init.Data.Float.Float32
/-- Rounds to the nearest integer, rounding away from zero at half-way points.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`roundf`.
 -/
Float32.round : Float32 → Float32
-- Mathlib.GroupTheory.Exponent
Monoid.neZero_exponent_of_finite : ∀ {G : Type u} [inst : LeftCancelMonoid G] [Finite G], NeZero (Monoid.exponent G)
-- Mathlib.Algebra.DirectSum.Module
/-- If a direct sum of submodules is internal then the submodules span the module.  -/
DirectSum.IsInternal.submodule_iSup_eq_top : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M}, DirectSum.IsInternal A → iSup A = ⊤
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_C_tmul_C : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (r : R) (s : S),
  (MvPolynomial.tensorEquivSum R σ ι S) (MvPolynomial.C s ⊗ₜ[R] MvPolynomial.C r) = MvPolynomial.C (r • s)
-- Init.Data.SInt.Lemmas
instCommutativeInt16HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Control.Monad.Cont
run_callCC : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadCont m] {α β : Type u}
  (f : MonadCont.Label α (OptionT m) β → OptionT m α),
  (OptionT.callCC f).run = MonadCont.callCC fun x => (f (OptionT.mkLabel x)).run
-- Init.Data.List.Perm
List.perm_middle : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (l₁ ++ a :: l₂).Perm (a :: (l₁ ++ l₂))
-- Mathlib.Topology.IndicatorConstPointwise
tendsto_ite : ∀ {ι : Type u_3} (L : Filter ι) {β : Type u_4} {p : ι → Prop} [inst : DecidablePred p] {q : Prop} [inst_1 : Decidable q]
  {a b : β} {F G : Filter β},
  {a}ᶜ ∈ G →
    {b}ᶜ ∈ F →
      Filter.principal {a} ≤ F →
        Filter.principal {b} ≤ G →
          (Filter.Tendsto (fun i => if p i then a else b) L (if q then F else G) ↔ ∀ᶠ (i : ι) in L, p i ↔ q)