mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.of_pow : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, (f ^ n).SameCycle x y → f.SameCycle x y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 →
            P 1 * Q 2 ≠ W.negY Q * P 2 →
              W.dblY P / W.dblZ P =
                W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                  (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMonoid : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Monoid R] → [BoundedMul R] → [ContinuousMul R] → Monoid (BoundedContinuousFunction α R)
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRccIterIteratorOfUpwardEnumerable : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.ToStream (Std.Rcc α) (Std.Iter α)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_one : ∀ {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], FractionalIdeal.spanSingleton S 1 = 1
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalSemiring.toSeparatelyContinuousMul : ∀ {R : Type u_2} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocSemiring R}
  [self : IsSemitopologicalSemiring R], SeparatelyContinuousMul R
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.jacobiTheta₂''.eq_1 : ∀ (z τ : ℂ),
  HurwitzZeta.jacobiTheta₂'' z τ =
    Complex.exp (↑Real.pi * Complex.I * z ^ 2 * τ) *
      (jacobiTheta₂' (z * τ) τ / (2 * ↑Real.pi * Complex.I) + z * jacobiTheta₂ (z * τ) τ)
-- Mathlib.RingTheory.Ideal.Prod
Ideal.map_prodComm_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  Ideal.map (↑RingEquiv.prodComm) (I.prod J) = J.prod I
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instEssFiniteTypeResidueField : ∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsPrime], Algebra.EssFiniteType R p.ResidueField
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_apply_eq_one_iff : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toMk₁ i)) j = 1 ↔ i ≤ j.castSucc
-- Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
CategoryTheory.instCreatesLimitsOfShapeGrpForget : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.Category.{u_2, w} J] →
          [CategoryTheory.Limits.HasLimitsOfShape J C] →
            CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.Grp.forget C)
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_mono : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : DivisionRing β] {a₁ a₂ : α},
  a₁ ≤ a₂ → LinearOrderedField.cutMap β a₁ ⊆ LinearOrderedField.cutMap β a₂
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmultiplesHom_bijective : ∀ {G : Type u_2} [Infinite G] [inst : AddGroup G] {g : G},
  AddSubgroup.zmultiples g = ⊤ → Function.Bijective ⇑((zmultiplesHom G) g)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_smul_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Semiring S] [IsDomain S]
  [inst_3 : Module S R] [Module.IsTorsionFree S R] {a : S},
  a ≠ 0 → ∀ (p : MvPolynomial σ R), (a • p).support = p.support
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.toPseudoMetricSpace : {E : Type u_8} → [self : SeminormedCommGroup E] → PseudoMetricSpace E
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- A ring homomorphism `R →+* S` is standard smooth of relative dimension `n` if
`S` is standard smooth of relative dimension `n` as `R`-algebra.  -/
RingHom.IsStandardSmoothOfRelativeDimension : ℕ → {R : Type u} → {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.nsmul_apply : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : M →+ N) (n : ℕ) (x : M),
  (n • f) x = n • f x
-- Mathlib.Analysis.Distribution.Distribution
/-- `lineDerivCLM 𝕜 v` is the continuous `𝕜`-linear-map sending a distribution
`T : 𝓓'^{k}_{K}(E, F)` to its derivative along the vector `v`, which is a
distribution in `𝓓^{n}_{K}(E, F)`. Because differentiating increases the order, this only makes
sense if `k + 1 ≤ n`, otherwise we define it as the zero map.

The parameters `n` and `k` are implicit as they can often be inferred from context, or
specified by a type ascription. For `n = k = ⊤`, we also provide instances of the `LineDeriv`
notation typeclass.  -/
Distribution.lineDerivCLM : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_2} →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module ℝ F] →
              [inst_4 : TopologicalSpace F] →
                {n k : ℕ∞} →
                  [inst_5 : IsTopologicalAddGroup F] →
                    [inst_6 : ContinuousSMul ℝ F] → E → Distribution Ω F k →L[ℝ] Distribution Ω F n
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide
            ((Finset.affineCombination R Finset.univ s.points) w₁)
            ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
          SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0
-- Init.Data.Ord.Array
Array.compare_eq_compareLex : ∀ {α : Type u_1} [inst : Ord α], compare = Array.compareLex compare
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_inverse_obj_mon_one : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon Cᴹᵒᵖ), CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.unmop
-- Mathlib.Algebra.Ring.Ext
Semiring.toNonUnitalSemiring_injective : ∀ {R : Type u}, Function.Injective (@Semiring.toNonUnitalSemiring R)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.of.inj : ∀ {carrier : Type u} {ring : Ring carrier} {carrier_1 : Type u} {ring_1 : Ring carrier_1},
  RingCat.of carrier = RingCat.of carrier_1 → carrier = carrier_1 ∧ ring ≍ ring_1
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.subtype_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] {s : S}
  (x : ↥s), (SubsemiringClass.subtype s) x = ↑x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.of_uncurry_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] {x : MeasurableSpace α}
  {x_1 : MeasurableSpace γ} {f : α → γ → β},
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {y : γ}, MeasureTheory.StronglyMeasurable fun x => f x y
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
minSmoothness_monotone : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜], Monotone (minSmoothness 𝕜)
-- Mathlib.Order.Filter.Pointwise
Filter.instNPow.eq_1 : ∀ {α : Type u_2} [inst : One α] [inst_1 : Mul α], Filter.instNPow = { pow := fun s n => npowRec n s }
-- Init.Data.Rat.Lemmas
Rat.mul_le_mul_of_nonneg_right : ∀ {a b c : ℚ}, a ≤ b → 0 ≤ c → a * c ≤ b * c
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) →
      (x y : CategoryTheory.WithTerminal Cᵒᵖ) →
        (f : x ⟶ y) →
          ((x y : C) →
              (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
                motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y))
                  f) →
            ((unop : C) →
                (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive x y f
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofQuotient_isPresentation : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  (Module.Relations.Solution.ofQuotient relations).IsPresentation
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux.congr_simp : ∀ {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] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J J_1 : CategoryTheory.GrothendieckTopology C} (e_J : J = J_1)
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α α_1 : G.op.comp R ⟶ F),
  α = α_1 →
    ∀ {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f f_1 : G.obj Y ⟶ X),
      f = f_1 →
        CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f =
          CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux ⋯ α_1 s f_1
-- Lean.Elab.SyntheticMVars
/-- Generate an nicer error message for stuck universe constraints.
 -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.throwStuckAtUniverseCnstr : Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- A path object for `A` can be obtained from a factorization of the obvious
map `A ⟶ A ⨯ A` as a trivial cofibration followed by a fibration.  -/
HomotopicalAlgebra.PathObject.ofFactorizationData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {A : C} →
        (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
            (CategoryTheory.Limits.diag A) →
          HomotopicalAlgebra.PathObject A
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_biInf_of_directed' : ∀ {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {dom : Set ι},
  dom.Nonempty →
    ∀ {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop),
      (∀ i ∈ dom, (l i).HasBasis (p i) (s i)) →
        DirectedOn (l ⁻¹'o GE.ge) dom →
          (⨅ i ∈ dom, l i).HasBasis (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `get!_filterMap` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.get!_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filterMap f m) k = ((Std.ExtDHashMap.Const.get? m k).bind (f k)).get!
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_lt_lift : ∀ {c : Cardinal.{u}}, Cardinal.continuum < Cardinal.lift.{v, u} c ↔ Cardinal.continuum < c
-- Mathlib.Dynamics.Minimal
eq_empty_or_univ_of_smul_invariant_closed : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] {s : Set α}, IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = Set.univ
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_smulRightL : ∀ {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E)
  [Nontrivial Fₗ], ‖(ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c‖ = ‖c‖
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.processVar : Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instIteratorLoop : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          {n : Type u_1 → Type u_2} →
            [inst_2 : Monad m] → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.Zip α₁ m α₂ β₂) m n
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.bi : Lean.Elab.Term.BinderView → Lean.BinderInfo
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_prod_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (l : List (Equiv.Perm α)),
  l.prod.support ⊆ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map Equiv.Perm.support l)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.liftFromUnder_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (X_1 : CategoryTheory.Functor J (CategoryTheory.Under X)) {X_2 Y : CategoryTheory.WithInitial J}
  (f : X_2 ⟶ Y),
  (CategoryTheory.WithInitial.liftFromUnder.obj X_1).map f =
    match X_2, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f =>
      CategoryTheory.Under.Hom.right (X_1.map (CategoryTheory.WithInitial.down f))
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => (X_1.obj a).hom
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id X
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.get : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α fun x => β) → (a : α) → m.contains a = true → β
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- An oplax functor `F` between bicategories `B` and `C` consists of a function between objects
`F.obj`, a function between 1-morphisms `F.map`, and a function between 2-morphisms `F.map₂`.

Unlike functors between categories, `F.map` does not need to strictly commute with composition,
and does not need to strictly preserve the identity. Instead, there are specified 2-morphisms
`F.map (𝟙 a) ⟶ 𝟙 (F.obj a)` and `F.map (f ≫ g) ⟶ F.map f ≫ F.map g`.

`F.map₂` strictly commutes with compositions and preserves the identity. It also preserves the
associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains
of 2-morphisms.
 -/
CategoryTheory.OplaxFunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_p_comp_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C}
  (h : Q.X.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (f.f.app X) h) =
    CategoryTheory.CategoryStruct.comp (f.f.app X) h
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_succ_left : ∀ (S : Type u) [inst : Semiring S] (n : ℕ),
  ascPochhammer S (n + 1) = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- If one controls the seminorm for every `x`, then one controls the seminorm.  -/
SchwartzMap.seminorm_le_bound : ∀ (𝕜 : 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] (k n : ℕ) (f : SchwartzMap E F) {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) → (SchwartzMap.seminorm 𝕜 k n) f ≤ M
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.const.injEq : ∀ (c c_1 : Lean.Name), (Mathlib.Tactic.Push.Head.const c = Mathlib.Tactic.Push.Head.const c_1) = (c = c_1)
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_mul : ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {n : ℕ} (v w : Fin n → α),
  Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)
-- Mathlib.GroupTheory.OrderOfElement
mem_multiples_iff_mem_range_addOrderOf : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [Finite G] {x y : G} [inst_2 : DecidableEq G],
  y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `closure_sdiff_intrinsicFrontier`. -/
closure_diff_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [inst_5 : MetricSpace P]
  [inst_6 : NormedAddTorsor V P] (s : Set P), closure s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
-- Mathlib.GroupTheory.Perm.Cycle.Type
exists_prime_addOrderOf_dvd_card' : ∀ {G : Type u_3} [inst : AddGroup G] [Finite G] (p : ℕ) [hp : Fact (Nat.Prime p)],
  p ∣ Nat.card G → ∃ x, addOrderOf x = p
-- Mathlib.Util.Superscript
/-- Map over the strings in a `Format`.  -/
Std.Format.mapStringsM : {m : Type → Type u_1} → [Monad m] → Std.Format → (String → m String) → m Std.Format
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.measure.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (z' : Lean.PersistentHashMap.Zipper α β),
  (Lean.PersistentHashMap.Zipper.consEntries es z').measure = Lean.PersistentHashMap.subarrayMeasure es + z'.measure + 1
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.overEquivOfIsInitial_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).functor = CategoryTheory.Functor.star (CategoryTheory.Over X)
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → l.Perm l' → (Std.Internal.List.eraseKey k l).Perm (Std.Internal.List.eraseKey k l')
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support.eq_1 : ∀ {β : Type u_2} (L : SummationFilter β), L.support = {b | ∀ᶠ (s : Finset β) in L.filter, b ∈ s}
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.restrictScalarsLI_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (𝕜' : Type u_1) [inst_6 : NontriviallyNormedField 𝕜']
  [inst_7 : NormedAlgebra 𝕜' 𝕜] [inst_8 : NormedSpace 𝕜' F] [inst_9 : IsScalarTower 𝕜' 𝕜 F] [inst_10 : NormedSpace 𝕜' E]
  [inst_11 : IsScalarTower 𝕜' 𝕜 E] (f : E [⋀^ι]→L[𝕜] F),
  (ContinuousAlternatingMap.restrictScalarsLI 𝕜') f = ContinuousAlternatingMap.restrictScalars 𝕜' f
-- Mathlib.Algebra.Group.Units.Basic
Units.eq_inv_of_mul_eq_one_left : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u * a = 1 → a = ↑u⁻¹
-- Mathlib.Algebra.CharP.Basic
/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`.  -/
Ring.two_ne_zero : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [Nontrivial R], ringChar R ≠ 2 → 2 ≠ 0
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subLeft.eq_1 : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x : G),
  Homeomorph.subLeft x = { toEquiv := Equiv.subLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformGroup.cauchy_map_iff_tendsto_swapped : ∀ {ι : Type u_3} {G : Type u_4} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G] (𝓕 : Filter ι)
  (f : ι → G), Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (nhds 1)
-- Mathlib.ModelTheory.Syntax
/-- Relabels a formula's variables along a particular function.  -/
FirstOrder.Language.Formula.relabel : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → (α → β) → L.Formula α → L.Formula β
-- Lean.Expr
Lean.Expr.isHaveEx : Lean.Expr → Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.other.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchDiagSource.other = 1
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.iUnion_le_mem : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C → ∀ {s : ℕ → Set α}, (∀ (n : ℕ), s n ∈ C) → ∀ (n : ℕ), ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from an additive monoid to itself.  -/
AddMonoidHom.id : (M : Type u_10) → [inst : AddZero M] → M →+ M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp h.isoPullback.inv (CategoryTheory.CategoryStruct.comp snd h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h_1
-- Mathlib.CategoryTheory.Monoidal.Limits.Basic
CategoryTheory.Limits.lim_μ_π : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F G : CategoryTheory.Functor J C) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G)
      (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.limit.π F j)
      (CategoryTheory.Limits.limit.π G j)
-- Mathlib.Order.OrderIsoNat
/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
Bolzano-Weierstrass for `ℝ`.  -/
exists_increasing_or_nonincreasing_subseq : ∀ {α : Type u_1} (r : α → α → Prop) [IsTrans α r] (f : ℕ → α),
  ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadCommRing.modifyCommRing : {m : Type → Type} →
  [self : Lean.Meta.Grind.Arith.CommRing.MonadCommRing m] →
    (Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.CommRing) → m Unit