mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instPreservesFiniteColimitsObjFunctorExactFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₑ D), CategoryTheory.Limits.PreservesFiniteColimits F.obj
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.inf_le_of_left_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {l : Filter α} {f g h : α → β}, f ≤ᶠ[l] h → f ⊓ g ≤ᶠ[l] h
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.uliftFunctorCompForgetIso_inv_app_hom_apply : ∀ (X : TopCat) (a : (TopCat.uliftFunctor.comp (CategoryTheory.forget TopCat)).obj X),
  (CategoryTheory.ConcreteCategory.hom (TopCat.uliftFunctorCompForgetIso.inv.app X)) a = a
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_left_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → Set.Ico (Order.succ a) b = Set.Ioo a b
-- Std.Time.Date.Unit.Week
/-- Convert `Second.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Week.Offset
-- Lean.Expr
Lean.Expr.mkDataForBinder : UInt64 → ℕ → UInt32 → Bool → Bool → Bool → Bool → Lean.Expr.Data
-- Lean.Meta.Instances
Lean.Meta.instBEqInstanceEntry : BEq Lean.Meta.InstanceEntry
-- Lean.Expr
Lean.Expr.data : Lean.Expr → Lean.Expr.Data
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} [inst : Inhabited β] {f : β → β},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.modify m k f) k' =
    if (k == k') = true then (Option.map f (Std.DHashMap.Const.get? m k)).get! else Std.DHashMap.Const.get! m k'
-- Mathlib.GroupTheory.Submonoid.Center
unitsCenterToCenterUnits_injective : ∀ (M : Type u_1) [inst : Monoid M], Function.Injective ⇑(unitsCenterToCenterUnits M)
-- Mathlib.Order.Category.BddDistLat
/-- `OrderDual` as a functor.  -/
BddDistLat.dual : CategoryTheory.Functor BddDistLat BddDistLat
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.mk.injEq : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (toContinuousMultilinearMap : ContinuousMultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap.toFun v = 0)
  (toContinuousMultilinearMap_1 : ContinuousMultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq'_1 : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap_1.toFun v = 0),
  ({ toContinuousMultilinearMap := toContinuousMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
      { toContinuousMultilinearMap := toContinuousMultilinearMap_1, map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 }) =
    (toContinuousMultilinearMap = toContinuousMultilinearMap_1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_semiconj : ∀ {f g₁ g₂ : CircleDeg1Lift}, Function.Semiconj ⇑f ⇑g₁ ⇑g₂ → g₁.translationNumber = g₂.translationNumber
-- Mathlib.Order.Hom.BoundedLattice
/-- Composition of `BoundedLatticeHom`s as a `BoundedLatticeHom`.  -/
BoundedLatticeHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Lattice α] →
        [inst_1 : Lattice β] →
          [inst_2 : Lattice γ] →
            [inst_3 : BoundedOrder α] →
              [inst_4 : BoundedOrder β] →
                [inst_5 : BoundedOrder γ] → BoundedLatticeHom β γ → BoundedLatticeHom α β → BoundedLatticeHom α γ
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R`
and their actions on all involved modules agree with the action of `R` on `A`.  -/
ContinuousMultilinearMap.restrictScalars : (R : Type u) →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      {A : Type u_1} →
                        [inst_7 : Semiring A] →
                          [inst_8 : SMul R A] →
                            [inst_9 : (i : ι) → Module A (M₁ i)] →
                              [inst_10 : Module A M₂] →
                                [∀ (i : ι), IsScalarTower R A (M₁ i)] →
                                  [IsScalarTower R A M₂] →
                                    ContinuousMultilinearMap A M₁ M₂ → ContinuousMultilinearMap R M₁ M₂
-- Mathlib.SetTheory.ZFC.Basic
/-- A subset of pairs `{(a, b) ∈ x × y | p a b}`  -/
ZFSet.pairSep : (ZFSet.{u} → ZFSet.{u} → Prop) → ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_ne_zero_of_finite : ∀ {G : Type u} [inst : LeftCancelMonoid G] [Finite G], Monoid.exponent G ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Z`-coordinate of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Projective.dblZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → R
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.closeBody.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Event.closeBody = 1
-- Mathlib.Order.CompleteBooleanAlgebra
himp_iInf_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α}, a ⇨ ⨅ x, f x = ⨅ x, a ⇨ f x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).minKey?.isSome = true
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_intCast : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Ring M] (z : ℤ),
  (↑z).toDirectSum = ↑z
-- Init.Grind.Ordered.Order
Lean.Grind.LinearOrder.lt_of_not_le : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {a b : α}, ¬a ≤ b → b < a
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- If a compact interval `[a, b]` is covered by a union of open interval `(c i, d i)`, then
`f b - f a ≤ ∑ f (d i) - f (c i)`. This is an auxiliary technical statement to prove the same
statement for half-open intervals, the point of the current statement being that one can use
compactness to reduce it to a finite sum, and argue by induction on the size of the covering set.

To be able to handle also the top element if there is one, we use `Iotop` instead of `Ioo` in the
statement. As these intervals are all open, this does not change the proof.  -/
StieltjesFunction.length_subadditive_Icc_Ioo : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R]
  [CompactIccSpace R] {a b : R} {c d : ℕ → R},
  Set.Icc a b ⊆ ⋃ i, Iotop (c i) (d i) → ENNReal.ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ENNReal.ofReal (↑f (d i) - ↑f (c i))
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iio_mul_Iic_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iio a * Finset.Iic b ⊆ Finset.Iio (a * b)
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instRepr : {α : ℚ} → Repr (Std.Time.Internal.UnitVal α)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.uniqueProd_symm_apply_snd : ∀ (X : Type u_7) (Y : Type u_8) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X] (a : Y),
  ((Homeomorph.uniqueProd X Y).symm a).2 = ((Homeomorph.prodUnique Y X).symm a).1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : N ≃+ P} (x : M),
  k.symm ((f.ofAddEquivOfLocalizations k) x) = f x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.total_le : ∀ {α : Type u_1} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_eq_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} (H : s.Nonempty)
  (f : β → α), s.inf' H f = s.inf f
-- Lean.Meta.AbstractNestedProofs
/-- Replace proofs nested in `e` with new lemmas. The new lemmas are named using `getDeclNGen`.  -/
Lean.Meta.abstractNestedProofs : Lean.Expr → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- The range of a finite monoid under a monoid homomorphism is finite.
Note: this instance can form a diamond with `Subtype.fintype` in the
presence of `Fintype N`.  -/
MonoidHom.fintypeMrange : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] → [Fintype M] → [DecidableEq N] → (f : M →* N) → Fintype ↥(MonoidHom.mrange f)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.nil : Tactic.ComputeAsymptotics.WellFormedBasis []
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `AddHomClass F M N` into an actual
`AddHom`. This is declared as the default coercion from `F` to `M →ₙ+ N`.  -/
AddHomClass.toAddHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : FunLike F M N] → [AddHomClass F M N] → F → M →ₙ+ N
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_lt : ∀ {a b : UInt16}, a.toUInt32 < b.toUInt32 ↔ a < b
-- Mathlib.Data.FunLike.Graded
GradedEquivLike.toGradedFunLike : ∀ (E : Type u_1) {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [inst_2 : EquivLike E A B] [GradedEquivLike E 𝒜 ℬ], GradedFunLike E 𝒜 ℬ
-- Mathlib.Data.Finset.Card
Finset.card_image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β],
  Set.InjOn f ↑s → (Finset.image f s).card = s.card
-- Mathlib.Data.Num.ZNum
ZNum.cast_zero' : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α], ↑ZNum.zero = 0
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] (k : A)
  (j : Cᵒᵖ), (Φ.skyscraperPresheafFunctor.obj k).obj j = ∏ᶜ fun t => k
-- Lean.Compiler.IR.CompilerM
Lean.IR.declMapExt : Lean.SimplePersistentEnvExtension Lean.IR.Decl Lean.IR.DeclMap
-- Mathlib.Data.List.Infix
List.suffix_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), l <:+ List.insert a l
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_left_inv : ∀ {n : ℕ} {G : Type u_3} [inst : Group G] (f : Fin (n + 1) → G),
  (f 0 • Fin.partialProd fun i => (f i.castSucc)⁻¹ * f i.succ) = f
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- An isocrystal is a vector space over the field `K(p, k)` additionally equipped with a
Frobenius-linear automorphism.
 -/
WittVector.Isocrystal : (p : ℕ) →
  [Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst : CommRing k] → [CharP k p] → [PerfectRing k p] → (V : Type u_2) → [AddCommGroup V] → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.ofNat_fin_two : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo],
  OfNat.ofNat n = !![OfNat.ofNat n, 0; 0, OfNat.ofNat n]
-- Aesop.Search.RuleSelection
Aesop.preprocessRule : Aesop.SafeRule
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H]
  [inst_4 : CategoryTheory.IsMonHom e.hom],
  CategoryTheory.Grp.mkIso' e = (CategoryTheory.Grp.fullyFaithfulForget₂Mon C).preimageIso (CategoryTheory.Mon.mkIso' e)
-- Mathlib.Topology.Bornology.Basic
/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions.  -/
Bornology.ofBounded' : {α : Type u_4} →
  (B : Set (Set α)) →
    ∅ ∈ B → (∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B) → (∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) → ⋃₀ B = Set.univ → Bornology α
-- Mathlib.Data.Nat.Prime.Int
/-- Version of `Nat.Prime.pow_inj` with an explicit nonzero assumption on the exponents.  -/
Nat.Prime.pow_inj' : ∀ {p q m n : ℕ}, Nat.Prime p → Nat.Prime q → m ≠ 0 → n ≠ 0 → p ^ m = q ^ n → p = q ∧ m = n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getKeyGT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.getKeyGTD k l ky
      else Std.DTreeMap.Internal.Impl.getKeyGT k r ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.instSmallColimitType : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J] (F : CategoryTheory.Functor J (Type u)),
  Small.{u, max u v} F.ColimitType
-- Init.Data.Nat.Lemmas
Nat.succ_le : ∀ {n m : ℕ}, n.succ ≤ m ↔ n < m
-- Mathlib.Analysis.Normed.Module.Convex
/-- Given a point `x` in the convex hull of `s` and a point `y`, there exists a point
of `s` at distance at least `dist x y` from `y`.  -/
convexHull_exists_dist_ge : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x : E},
  x ∈ (convexHull ℝ) s → ∀ (y : E), ∃ x' ∈ s, dist x y ≤ dist x' y
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaCongrRight_trans : ∀ {α : Sort u_4} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} {β₃ : α → Sort u_3} (F : (a : α) → β₁ a ≃ β₂ a)
  (G : (a : α) → β₂ a ≃ β₃ a),
  (Equiv.psigmaCongrRight F).trans (Equiv.psigmaCongrRight G) = Equiv.psigmaCongrRight fun a => (F a).trans (G a)
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] (G : Type u_1) [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [inst_4 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [inst_8 : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G],
  IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAutMulEquiv F G)
-- Init.Data.Order.Ord
Std.OrientedCmp.not_lt_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.lt → cmp b a ≠ Ordering.lt
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The equivalence of categories `SelfLERadical J ≌ SelfLERadical K`
when `J.radical = K.radical`.  -/
localCohomology.SelfLERadical.castEquivalence : {R : Type u} →
  [inst : CommRing R] →
    {J K : Ideal R} → J.radical = K.radical → (localCohomology.SelfLERadical J ≌ localCohomology.SelfLERadical K)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y)
  (c : AddCon N), AddCon.comap f H c = { toSetoid := Setoid.comap f c.toSetoid, add' := ⋯ }
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.eq_1 : ∀ {α : Type u} {β : Type v}, Std.Internal.List.values [] = []
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk.sizeOf_spec : ∀ {R : Type u_1} {a b c : R} [inst : SizeOf R] (re imI imJ imK : R),
  sizeOf { re := re, imI := imI, imJ := imJ, imK := imK } = 1 + sizeOf re + sizeOf imI + sizeOf imJ + sizeOf imK
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.toMessageData : Lean.Meta.Grind.SplitSource → Lean.MessageData
-- Lean.Elab.DocString
Lean.Doc.Context.mk.inj : ∀ {suggestionMode suggestionMode_1 : Lean.Doc.SuggestionMode},
  { suggestionMode := suggestionMode } = { suggestionMode := suggestionMode_1 } → suggestionMode = suggestionMode_1
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_pow_image_iterateFrobenius_subset : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p n : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R],
  Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical map `pullback f g ⟶ X ⊞ Y` is a kernel of the map induced by
`(f, -g)`.  -/
CategoryTheory.Abelian.PullbackToBiproductIsKernel.isLimitPullbackToBiproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y Z : C} →
          (f : X ⟶ Z) →
            (g : Y ⟶ Z) →
              CategoryTheory.Limits.IsLimit
                (CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductFork f g)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instRightDistribClass : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Mul R] [inst_2 : Add R] [RightDistribClass R]
  [inst_4 : ContinuousMul R] [inst_5 : ContinuousAdd R], RightDistribClass (SeparationQuotient R)
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.mk.injEq : ∀ (goals goals_1 : Array Lean.Widget.InteractiveGoal), ({ goals := goals } = { goals := goals_1 }) = (goals = goals_1)
-- Mathlib.Computability.Primrec.List
Primrec.list_map : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → β → σ}, Primrec f → Primrec₂ g → Primrec fun a => List.map (g a) (f a)
-- Init.Data.Repr
/-- Converts a natural number to the list of Unicode superscript digit characters that corresponds to
its decimal representation.

Examples:
 * `Nat.toSuperDigits 0 = ['⁰']`
 * `Nat.toSuperDigits 35 = ['³', '⁵']`
 -/
Nat.toSuperDigits : ℕ → List Char
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHomClass.toAddHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : AddZero M} {inst_1 : AddZero N}
  {inst_2 : FunLike F M N} [self : AddMonoidHomClass F M N], AddHomClass F M N
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R], Matrix.toMvPolynomial 0 = 0
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is a ring homomorphism of characteristic `p` rings, then it is called
`p`-radical if the following conditions are satisfied:

- For any element `x` of `L` there is `n : ℕ` such that `x ^ (p ^ n)` is contained in `K`.
- The kernel of `i` is contained in the `p`-nilradical of `K`.

It is a generalization of purely inseparable extension for fields.  -/
IsPRadical : {K : Type u_1} → {L : Type u_2} → [inst : CommSemiring K] → [inst_1 : CommSemiring L] → (K →+* L) → ℕ → Prop
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.elabGrindPattern : Lean.Elab.Command.CommandElab
-- Init.Data.List.SplitOn.Lemmas
List.splitOn_eq_splitOnP : ∀ {α : Type u_1} [inst : BEq α] {x : α} {xs : List α}, List.splitOn x xs = List.splitOnP (fun x_1 => x_1 == x) xs
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_comp_eq : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : α → M₁) (g : α → M₂), ⇑e₁₂.symm ∘ g = f ↔ g = ⇑e₁₂ ∘ f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_sum : ∀ {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ ℕ} (s : Finset ι),
  Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i)
-- Lean.Declaration
Lean.instBEqRecursorRule : BEq Lean.RecursorRule
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.X_smul_of : ∀ {R : Type u_2} {A : Type u_3} {M : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (m : M), Polynomial.X • (Module.AEval.of R M a) m = (Module.AEval.of R M a) (a • m)
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.finTwoArrow_symm_apply : ∀ (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M], ⇑(ContinuousLinearEquiv.finTwoArrow R M).symm = fun x => ![x.1, x.2]
-- Aesop.Index.Basic
Aesop.IndexMatchResult.mk : {α : Type} → α → Array Aesop.IndexMatchLocation → Option (Array Aesop.Substitution) → Aesop.IndexMatchResult α
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.darts_bypass_subset_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.darts ⊆ p.darts
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_X_pow_mul : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.X ^ n * p).reverse = p.reverse
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_pow : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (n : ℕ),
  0 < n → AlgebraicGeometry.Proj.basicOpen 𝒜 (f ^ n) = AlgebraicGeometry.Proj.basicOpen 𝒜 f
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.congr_fun : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {f g : X →ₑ[φ] Y}, f = g → ∀ (x : X), f x = g x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- a choice of kernel of `S.g : S.X₂ ⟶ S.X₃`  -/
CategoryTheory.ShortComplex.LeftHomologyData.K : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {S : CategoryTheory.ShortComplex C} → S.LeftHomologyData → C
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.strictPeriods],
  𝒢.strictPeriods = AddSubgroup.zmultiples 𝒢.strictWidthInfty