mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray.congr_simp : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Rio α), r = r_1 → r.toArray = r_1.toArray
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_toAddSubmonoid_apply : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑(Submonoid.toAddSubmonoid S) = ⇑Additive.toMul ⁻¹' ↑S
-- Init.System.IO
IO.FS.instReprSystemTime.repr : IO.FS.SystemTime → ℕ → Std.Format
-- Batteries.Recycling.RBTree.Basic
/-- `lowerBound? cut` retrieves the largest entry smaller than or equal to `cut`, if it exists.  -/
RBTree.RBNode.lowerBound? : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → optParam (Option α) none → Option α
-- Mathlib.Algebra.Category.ModuleCat.Colimits
/-- The induced scalar multiplication on
`colimit (F ⋙ forget₂ _ AddCommGrpCat)`.  -/
ModuleCat.HasColimit.coconePointSMul : {R : Type w} →
  [inst : Ring R] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] →
            R →+*
              CategoryTheory.End
                (CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)))
-- Mathlib.Order.BoundedOrder.Basic
ne_top_of_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a ≠ ⊤
-- Std.Data.DTreeMap.Raw.Basic
/-- Well-formedness predicate for tree maps. Users of `DTreeMap` will not need to interact with
this. Users of `DTreeMap.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas
like `WF.empty` and `WF.insert` (which are always named exactly like the operations they are about)
to show that map operations preserve well-formedness. The constructors of this type are internal
implementation details and should not be accessed by users.
 -/
Std.DTreeMap.Raw.WF : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Prop
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation `𝟭 C ⟶ t.eTruncGE.obj i` for all `i : EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTruncGEπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (i : EInt) → CategoryTheory.Functor.id C ⟶ t.eTruncGE.obj i
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- If `F : J ⥤ C` is a functor that has a limit and is such that for all `j`,
`F.obj j` satisfies a property `P`, then this structure expresses that `limit F`
is indeed a limit of objects satisfying `P`.  -/
CategoryTheory.ObjectProperty.LimitOfShape.limit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          (F : CategoryTheory.Functor J C) →
            [inst_2 : CategoryTheory.Limits.HasLimit F] →
              (∀ (j : J), P (F.obj j)) → P.LimitOfShape J (CategoryTheory.Limits.limit F)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
ContDiffOn.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ n (fun x => Real.log (f x)) s
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- The coreflector `D ⥤ C` when `L : C ⥤ D` is coreflective.  -/
CategoryTheory.coreflector : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (j : CategoryTheory.Functor C D) → [CategoryTheory.Coreflective j] → CategoryTheory.Functor D C
-- Mathlib.Logic.Encodable.Basic
Encodable.instTotalPreimageNatCoeEmbeddingEncode'Le : ∀ {α : Type u_1} [inst : Encodable α], Std.Total (⇑(Encodable.encode' α) ⁻¹'o fun x1 x2 => x1 ≤ x2)
-- Mathlib.Data.List.Duplicate
List.Duplicate.brecOn : ∀ {α : Type u_1} {x : α} {motive : (a : List α) → List.Duplicate x a → Prop} {a : List α} (t : List.Duplicate x a),
  (∀ (a : List α) (t : List.Duplicate x a), List.Duplicate.below t → motive a t) → motive a t
-- Mathlib.Algebra.Algebra.Opposite
/-- The 'unopposite' of an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. Inverse to `RingHom.op`.  -/
AlgHom.unop : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B)
-- Lean.Elab.PreDefinition.MkInhabitant
_private.Lean.Elab.PreDefinition.MkInhabitant.0.Lean.Elab.withInhabitedInstances : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (-f) μ
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_zero_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E),
  Metric.closedBall 0 δ - {x} = Metric.closedBall (-x) δ
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_span : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → Set R),
  ∏ i ∈ s, Ideal.span (I i) = Ideal.span (∏ i ∈ s, I i)
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of `x - y` is at most `totalWeight K * log 2`
plus the sum of the logarithmic heights of `x` and `y`.  -/
Height.logHeight₁_sub_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.logHeight₁ (x - y) ≤ ↑(Height.totalWeight K) * Real.log 2 + Height.logHeight₁ x + Height.logHeight₁ y
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The power series expansion of `℘[L - l₀]` at `x`.
See `PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept`.  -/
PeriodPair.weierstrassPExceptSeries : PeriodPair → ℂ → ℂ → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.Combinatorics.Graph.Basic
Graph.not_isNonloopAt_bouquet : ∀ {α : Type u_1} {β : Type u_2} {x v : α} {e : β} {edgeSet : Set β}, ¬(Graph.bouquet v edgeSet).IsNonloopAt e x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_le_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (H : G.Subgraph) (h : H.Adj v w), G.subgraphOfAdj ⋯ ≤ H
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite coproducts, then `F.unop : C ⥤ D` reflects finite
products.  -/
CategoryTheory.Limits.reflectsFiniteProducts_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteCoproducts F],
  CategoryTheory.Limits.ReflectsFiniteProducts F.unop
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.toLinearEquiv_apply : ∀ {n : Type u_1} [inst : Fintype n] {R : Type u_2} {M : Type u_3} [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (b : Module.Basis n R M) [inst_4 : DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det)
  (a : M), (Matrix.toLinearEquiv b A hA) a = ((Matrix.toLin b b) A) a
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The ring hom `R/I →+* S/J` induced by a ring hom `f : R →+* S` with `I ≤ f⁻¹(J)`  -/
Ideal.quotientMap : {R : Type u} →
  [inst : Ring R] →
    {S : Type v} →
      [inst_1 : Ring S] →
        {I : Ideal R} →
          (J : Ideal S) →
            [inst_2 : I.IsTwoSided] → [inst_3 : J.IsTwoSided] → (f : R →+* S) → I ≤ Ideal.comap f J → R ⧸ I →+* S ⧸ J
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.of_subring : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B} (T : Subring R),
  IsIntegral (↥T) x → IsIntegral R x
-- Mathlib.Data.PFunctor.Univariate.M
/-- An `n`-th level approximation, for each depth `n`  -/
PFunctor.MIntl.approx : {F : PFunctor.{uA, uB}} → F.MIntl → (n : ℕ) → PFunctor.Approx.CofixA F n
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.withSeminorms : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], WithSeminorms (WeakDual.seminormFamily 𝕜 E)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_injective : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {f : A →⋆ₐ[R] B},
  Function.Injective ⇑f → Function.Injective (StarSubalgebra.map f)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint16 : Lean.IR.IRType
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.objX_add_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1) =
    Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)
-- Mathlib.LinearAlgebra.Ray
/-- **Alias** of the forward direction of `sameRay_neg_iff`.

---

`SameRay.neg` as an `iff`.  -/
SameRay.of_neg : ∀ {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] {x y : M}, SameRay R (-x) (-y) → SameRay R x y
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomain_algebraMap : ∀ {R : Type u_1} (A : Type u_4) {M : Type u_7} {N : Type u_8} {F : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] [inst_5 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) (r : R),
  MonoidAlgebra.mapDomain (⇑f) ((algebraMap R (MonoidAlgebra A M)) r) = (algebraMap R (MonoidAlgebra A N)) r
-- Mathlib.Topology.UnitInterval
unitInterval.symm_eq_one : ∀ {i : ↑unitInterval}, unitInterval.symm i = 1 ↔ i = 0
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.TSyntax.isHexNum? : Lean.Syntax → Option ℕ
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_logb : ∀ {b x y : ℝ}, 1 < b → 0 < x → x < y → Real.logb b x < Real.logb b y
-- Lean.Elab.Do.Legacy
/-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not  -/
Lean.Elab.Term.Do.Code.joinpoint : Lean.Name →
  Array (Lean.Elab.Term.Do.Var × Bool) → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_map : ∀ {α : Type u} {β : Type v} {α' : Type u'} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f₁ : α → α')
  (f₂ : β → β'), (Stream'.Seq.map f₁ s₁).zip (Stream'.Seq.map f₂ s₂) = Stream'.Seq.map (Prod.map f₁ f₂) (s₁.zip s₂)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instZero : {α : Type u_1} → Zero (MeasureTheory.OuterMeasure α)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartite.subgraph : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsBipartite → ∀ (H : G.Subgraph), H.coe.IsBipartite
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.le_sInf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasWidePullbacks C] {A : C}
  (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A),
  (∀ g ∈ s, f ≤ g) → f ≤ CategoryTheory.Subobject.sInf s
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
CategoryTheory.Limits.colimit.cocone.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit.cocone F = CategoryTheory.Limits.colimit.cocone F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
/-- The yoneda embedding of `RingObjCat C` into presheaves of rings.  -/
CategoryTheory.yonedaRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.RingObjCat C) (CategoryTheory.Functor Cᵒᵖ RingCat)
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodProdProdComm_toEquiv : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : AddZeroClass N'] [inst_3 : AddZeroClass M'],
  ↑(AddEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (τ₁ : S₁.X₁ ⟶ S₂.X₁) →
          (τ₂ : S₁.X₂ ⟶ S₂.X₂) →
            (τ₃ : S₁.X₃ ⟶ S₂.X₃) →
              autoParam (CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
                  CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam →
                autoParam (CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃)
                    CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam →
                  S₁.Hom S₂
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYonedaHomEquiv_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A}
  (α : CategoryTheory.Presheaf.freeYoneda X M ⟶ F) (f : F ⟶ G) {Z : A} (h : G.obj (Opposite.op X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Presheaf.freeYonedaHomEquiv (CategoryTheory.CategoryStruct.comp α f)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.freeYonedaHomEquiv α)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op X)) h)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.id A.X)
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_eq_sum_finrank_nsmul_mul : ∀ (K : Type u_2) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M]
  [inst_7 : FiniteDimensional K M] [inst_8 : LieRing.IsNilpotent L] [LieModule.LinearWeights K L M]
  [LieModule.IsTriangularizable K L M] (x y : L),
  ((LieModule.traceForm K L M) x) y = ∑ χ, Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ) • (χ x * χ y)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.zero_ne_one_iff : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R}, 0 ≠ 1 ↔ I ≠ ⊤
-- Mathlib.CategoryTheory.Monoidal.Opposite
Quiver.Hom.mop_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} {f : X ⟶ Y}, f.unmop.mop = f
-- Lean.Elab.Command.Scope
/-- Attributes that should be applied to all matching declaration in the section. Inherited from
parent scopes.
 -/
Lean.Elab.Command.Scope.attrs : Lean.Elab.Command.Scope → List (Lean.TSyntax `Lean.Parser.Term.attrInstance)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⇑H.subtype = Subtype.val
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t[k]? = some v ↔ ∃ (h : k ∈ t), t[k] = v
-- Mathlib.Tactic.Translate.Core
/-- Unfold `simp`, `gcongr` and `hcongr`/`congr_simp` auxlemmas in the type and value.
The reason why we can't just translate them is that they are generated by the `@[simp]` attribute,
so it would require a change in the implementation of `@[simp]` to add these translations.
Additionally, these lemmas have very short proofs, so unfolding them is not costly.  -/
Mathlib.Tactic.Translate.declUnfoldSimpAuxLemmas : Lean.ConstantInfo → Lean.MetaM Lean.ConstantInfo
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_self_sub_one_pos_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : LinearOrder Γ] [inst_1 : Zero Γ] [inst_2 : NonAssocRing R] [Nontrivial R]
  (x : HahnSeries Γ R), 0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1
-- Batteries.Data.List.Basic
/-- Split a list at an index. Ensures the left list always has the specified length
by right padding with the provided default element.
```
splitAtD 2 [a, b, c] x = ([a, b], [c])
splitAtD 4 [a, b, c] x = ([a, b, c, x], [])
```
 -/
List.splitAtD : {α : Type u_1} → ℕ → List α → α → List α × List α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Raw α (fun x => β) compare},
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      compare ((Std.DTreeMap.Raw.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.toEquiv_symm_eq_codRestrict_restrict : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β),
  ⇑e.toEquiv.symm = Set.codRestrict (e.target.domRestrict e.invFun) e.source ⋯
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func] [chainable : Std.Sat.AIG.RefVec.LawfulMapOperator α func]
  (vec_1 : aig.RefVec len) (func_1 : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  (lawful_1 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func_1)
  (chainable_1 : Std.Sat.AIG.RefVec.LawfulMapOperator α func_1),
  ({ vec := vec, func := func, lawful := lawful, chainable := chainable } =
      { vec := vec_1, func := func_1, lawful := lawful_1, chainable := chainable_1 }) =
    (vec = vec_1 ∧ func = func_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.to_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P Q : C}
  (f : P ⟶ Q) {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to P) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to Q) h
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.instHasPropTotallyDisconnectedSpaceCarrier : ∀ (X : Type u_1) [inst : TopologicalSpace X] [TotallyDisconnectedSpace X],
  CompHausLike.HasProp (fun Y => TotallyDisconnectedSpace ↑Y) X
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- Decomposing `fourierPowSMulRight L f v n` as a composition of continuous bilinear and
multilinear maps, to deduce easily its continuity and differentiability properties.  -/
VectorFourier.fourierPowSMulRight_eq_comp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {v : V} {n : ℕ},
  VectorFourier.fourierPowSMulRight L f v n =
    (-(2 * ↑Real.pi * Complex.I)) ^ n •
      ((ContinuousMultilinearMap.smulRightL ℝ (fun x => W) E)
          ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v))
        (f v)
-- Mathlib.RingTheory.Radical.NatInt
Int.two_le_radical_iff : ∀ {z : ℤ}, 2 ≤ UniqueFactorizationMonoid.radical z ↔ 2 ≤ z.natAbs
-- Init.Data.UInt.Bitwise
UInt32.shiftRight_and : ∀ {a b c : UInt32}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.Tactic.TFAE
/-- See `haveIdDecl`. E.g. `h : 1 → 3 := term`.  -/
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdDecl : Lean.Parser.Parser
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_left_ball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ),
  (fun x => a * x) ⁻¹' Metric.ball b r = Metric.ball (a⁻¹ * b) r
-- Mathlib.Analysis.CStarAlgebra.lpSpace
instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial : {I : Type u_1} →
  {A : I → Type u_2} → [∀ (i : I), Nontrivial (A i)] → [inst : (i : I) → CStarAlgebra (A i)] → NormedRing ↥(lp A ⊤)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Canonical map from the stalk of `smoothSheaf IM I M N` at `x` to `N`, given by evaluating
sections at `x`.  -/
smoothSheaf.eval : {𝕜 : 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] →
                                  (N : Type u) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H N] →
                                        (x : M) → (smoothSheaf IM I M N).presheaf.stalk x → N
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.documentation : Lean.Lsp.SemanticTokenModifier
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.match_1.splitter : {α : Type u_1} →
  (xs : Array α) →
    (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) →
      (x : ℕ) →
        (x_1 : x ≤ xs.size) →
          ((x : 0 ≤ xs.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h) → motive x x_1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.self_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (cmp k (t.insert k).max!).isLE = true
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.class_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCocycle G U), γ₁.class = γ₂.class ↔ γ₁.IsCohomologous γ₂
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_ofNat_le_lift : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.omega (OfNat.ofNat n) ≤ Ordinal.lift.{v, u} o ↔ Ordinal.omega (OfNat.ofNat n) ≤ o
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing : ∀ (K : Type u_1) (A : Type u_2) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A]
  [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A],
  Function.Bijective ⇑(algebraMap K A)