mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Comon (CategoryTheory.Functor C D)) (x : C),
  (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso✝.inv.app X).hom.app x =
    CategoryTheory.CategoryStruct.id (X.X.obj x)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.w : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (self : CategoryTheory.BasedFunctor 𝒳 𝒴), self.comp 𝒴.p = 𝒳.p
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- The identity function is an equidecomposition of the space with itself.  -/
Equidecomp.refl : (X : Type u_1) → (G : Type u_2) → [inst : Monoid G] → [inst_1 : MulAction G X] → Equidecomp X G
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.ofList l)[k']! = v
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- Given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is
mutually singular with respect to `μ` and `s = t + μ.withDensityᵥ f`, we have
`f = rnDeriv s μ`, i.e. `f` is the Radon-Nikodym derivative of `s` and `μ`.  -/
MeasureTheory.SignedMeasure.eq_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
  (t : MeasureTheory.SignedMeasure α) (f : α → ℝ),
  MeasureTheory.Integrable f μ →
    MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
      s = t + μ.withDensityᵥ f → f =ᵐ[μ] s.rnDeriv μ
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.ofNat_sub : ∀ {α : Type u} [inst : Lean.Grind.Ring α] {x y : ℕ}, y ≤ x → OfNat.ofNat (x - y) = OfNat.ofNat x - OfNat.ofNat y
-- Mathlib.Data.Quot
Quot.lift.decidablePred : {α : Sort u_1} →
  (r : α → α → Prop) →
    (f : α → Prop) → (h : ∀ (a b : α), r a b → f a = f b) → [hf : DecidablePred f] → DecidablePred (Quot.lift f h)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.ext_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M},
  s₁ = s₂ ↔ s₁.toAddSubmonoid = s₂.toAddSubmonoid
-- Mathlib.Data.Set.Operations
Set.mem_prod : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Data.QPF.Univariate.Basic
QPF.recF_eq : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (g : F α → α) (x : (QPF.P F).W),
  QPF.recF g x = g (QPF.abs ((QPF.P F).map (QPF.recF g) x.dest))
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.map_contDiff : ∀ {B : Type u_5} {E : outParam (Type u_6)} {F : outParam (Type u_7)} {inst : NormedAddCommGroup E}
  {inst_1 : NormedAddCommGroup F} {inst_2 : NormedSpace ℝ E} {inst_3 : NormedSpace ℝ F} {n : outParam ℕ∞}
  {K : outParam (TopologicalSpace.Compacts E)} [self : ContDiffMapSupportedInClass B E F n K] (f : B), ContDiff ℝ ↑n ⇑f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isMatch_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos ↔ String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceTo pos).copy
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.one_lt_card_support_of_ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f ≠ 1 → 1 < f.support.card
-- Mathlib.RepresentationTheory.Character
Representation.char_dual : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Group G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (g : G), ρ.dual.character g = ρ.character g⁻¹
-- Mathlib.Order.Hom.Set
OrderIso.image_symm_image : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set β), ⇑e '' ⇑e.symm '' s = s
-- Mathlib.Tactic.CongrExclamation
/-- Whether the given number of arguments is allowed to be considered.  -/
Congr!.Config.numArgsOk : Congr!.Config → ℕ → Bool
-- Mathlib.Order.Atoms
IsSimpleOrder.equivBool.congr_simp : ∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : LE α] [inst_2 : BoundedOrder α] [inst_3 : IsSimpleOrder α],
  IsSimpleOrder.equivBool = IsSimpleOrder.equivBool
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- The submodule with every element negated. Note if `R` is a ring and not just a semiring, this
is a no-op, as shown by `Submodule.neg_eq_self`.

Recall that When `R` is the semiring corresponding to the nonnegative elements of `R'`,
`Submodule R' M` is the type of cones of `M`. This instance reflects such cones about `0`.

This is available as an instance in the `Pointwise` locale.  -/
Submodule.pointwiseNeg : {R : Type u_2} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Neg (Submodule R M)
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.ofList.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (Lists α) → Sort u_2) (a : Lists α) (l : List (Lists α)) (h_1 : Unit → motive [])
  (h_2 : (a : Lists α) → (l : List (Lists α)) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.zero_apply : ∀ (G H : AddCommGrpCat) (g : ↑G), (CategoryTheory.ConcreteCategory.hom 0) g = 0
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `f : ℕ → F` is multiplicative on coprime arguments, `p ∉ s` is a prime and `m`
is `s`-factored, then `f (p^e * m) = f (p^e) * f m`.  -/
Nat.factoredNumbers.map_prime_pow_mul : ∀ {F : Type u_1} [inst : Mul F] {f : ℕ → F},
  (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
    ∀ {s : Finset ℕ} {p : ℕ},
      Nat.Prime p → p ∉ s → ∀ (e : ℕ) {m : ↑(Nat.factoredNumbers s)}, f (p ^ e * ↑m) = f (p ^ e) * f ↑m
-- Mathlib.Order.Monotone.Basic
StrictMono.injective : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → Function.Injective f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_eq_intCast : ∀ {R : Type u} [inst : Ring R] (n : ℤ), Polynomial.C ↑n = ↑n
-- Mathlib.Data.FunLike.Equiv
EquivLike.comp_surjective : ∀ {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike F β γ] (f : α → β) (e : F),
  Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
-- Mathlib.Algebra.Order.Module.Archimedean
/-- A closed ball defined by `ArchimedeanClass.submodule` of `UpperSet.Ici c`.

This has the same carrier as `ArchimedeanClass.closedBallAddSubgroup`'s.  -/
FiniteArchimedeanClass.closedBall : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        (K : Type u_2) →
          [inst_3 : Ring K] →
            [inst_4 : LinearOrder K] →
              [IsOrderedRing K] →
                [Archimedean K] → [inst_7 : Module K M] → [PosSMulMono K M] → FiniteArchimedeanClass M → Submodule K M
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.const_inv_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Neg β]
  [inst_2 : Group γ] [inst_3 : DistribMulAction γ α],
  Function.Antiperiodic f c → ∀ (a : γ), Function.Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
-- Mathlib.Data.PNat.Xgcd
/-- `wp` is a variable which changes through the algorithm.  -/
PNat.XgcdType.wp : PNat.XgcdType → ℕ
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Chooses an element of each associate class, by multiplying by `normUnit`  -/
normalize : {α : Type u_1} → [inst : MonoidWithZero α] → [NormalizationMonoid α] → α → α
-- Init.Grind.ToInt
/-- The embedding takes exponentiation to exponentiation, wrapped into the range interval.  -/
Lean.Grind.ToInt.Pow.toInt_pow : ∀ {α : Type u} {inst : HPow α ℕ α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Pow α I] (x : α) (n : ℕ), ↑(x ^ n) = I.wrap (↑x ^ n)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv_right`. -/
Monovary.of_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Monovary f g⁻¹ → Antivary f g
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.iterToSum_C_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₂),
  (MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.X c)) = MvPolynomial.X (Sum.inr c)
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_le_ringKrullDim : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.supportDim R M ≤ ringKrullDim R
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.op_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) (a : M),
  (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_eq_of_eq : ∀ {a b : UInt64}, a = b → a.toBitVec = b.toBitVec
-- Mathlib.CategoryTheory.Subobject.WellPowered
/-- A category (with morphisms in `Type v`) is well-powered relative to a universe `w`
if it is locally small and `Subobject X` is `w`-small for every `X`.

We show in `wellPowered_of_essentiallySmall_monoOver` and `essentiallySmall_monoOver`
that this is the case if and only if `MonoOver X` is `w`-essentially small for every `X`.
 -/
CategoryTheory.WellPowered : (C : Type u₁) → [inst : CategoryTheory.Category.{v, u₁} C] → [CategoryTheory.LocallySmall.{w, v, u₁} C] → Prop
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_insidePart_add_semilength_outsidePart_add_one : ∀ {p : DyckWord}, p ≠ 0 → p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local extremum equals zero.  -/
IsLocalExtr.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalExtr f a → deriv f a = 0
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.zero : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], Function.HasTemperateGrowth fun x => 0
-- Lean.Parser.Syntax
Lean.Parser.Command.namedName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a : α},
  nhdsSet (Set.Iic a) = nhds a ⊔ Filter.principal (Set.Iio a)
-- Mathlib.Algebra.Quaternion
/-- Second imaginary part (j) of a quaternion.  -/
QuaternionAlgebra.imJ : {R : Type u_1} → {a b c : R} → QuaternionAlgebra R a b c → R
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, G.CliqueFree n ↔ IsEmpty ((SimpleGraph.completeGraph (Fin n)).Copy G)
-- Mathlib.Algebra.Group.Action.Defs
op_vadd_eq_add : ∀ {α : Type u_9} [inst : Add α] (a b : α), AddOpposite.op a +ᵥ b = b + a
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Φ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), (W.Φ n).coeff (n.natAbs ^ 2) = 1
-- Mathlib.Order.SuccPred.Archimedean
exists_pred_iterate_or : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {a b : α},
  (∃ n, Order.pred^[n] a = b) ∨ ∃ n, Order.pred^[n] b = a
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite' : ∀ {w : ℕ} (c0 c1 : Bool) {a b : BitVec w},
  (bif c0 then ~~~bif c1 then ~~~a else b else a) = bif c0 && !c1 then ~~~b else a
-- Mathlib.Data.Set.Function
/-- This lemma is a special case of `rightInvOn_invFunOn.image_image`; it may make more sense
to use the other lemma directly in an application.  -/
Set.SurjOn.image_invFunOn_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → f '' Function.invFunOn f s '' t = t
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toListRev_keysIter : ∀ {α β : Type u} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.keysIter.toListRev = m.keys.reverse
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) [inst_2 : p.IsCartesian f φ] {a' : 𝒳} (φ' φ'_1 : a' ⟶ b) (e_φ' : φ' = φ'_1)
  [inst_3 : p.IsCartesian f φ'],
  CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ' =
    CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p_1 f_1 φ_1 φ'_1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then
`f ^ n * x = 0` for some `n`.  -/
AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens},
  IsCompact U.carrier →
    ∀ (x f : ↑(X.presheaf.obj (Opposite.op U))),
      TopCat.Presheaf.restrictOpen x (X.basicOpen f) ⋯ = 0 → ∃ n, f ^ n * x = 0
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.of_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {v v' : Valuation R Γ₀},
  v = v' → v.IsEquiv v'
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comap_injective_of_surjective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Surjective ⇑f → Function.Injective (PrimeSpectrum.comap f)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.surj : ∀ {R : Type u_1} {inst : CommSemiring R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M}
  {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} (S : Submonoid R) (f : M →ₗ[R] M')
  [self : IsLocalizedModule S f] (y : M'), ∃ x, x.2 • y = f x.1
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod_coe_eq_self : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A] {r : Polynomial A},
  r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → H.mod ↑r = r
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  (X_1 : C),
  (CategoryTheory.WithTerminal.equivComma.counitIso.hom.app X).left.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithTerminal.incl.obj X_1 with
      | CategoryTheory.WithTerminal.of x => X.left.obj x
      | CategoryTheory.WithTerminal.star => X.right)
-- Batteries.Data.AssocList
/-- `O(n)`. Map a function `f` over the keys of the list.  -/
Batteries.AssocList.mapKey : {α : Type u_1} → {δ : Type u_2} → {β : Type u_3} → (α → δ) → Batteries.AssocList α β → Batteries.AssocList δ β
-- Mathlib.Topology.UniformSpace.Ultra.Basic
UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity : ∀ {X : Type u_1} [inst : UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans],
  V ∈ uniformity X → IsClosed (UniformSpace.ball x V)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionSemiHomClass.toDistribMulActionHom.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B] {F : Type u_10}
  [inst_6 : FunLike F A B] [inst_7 : DistribMulActionSemiHomClass F (⇑φ) A B] (f : F),
  ↑f = { toFun := (↑↑f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Array.Lemmas
Array.setIfInBounds_def : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (a : α), xs.setIfInBounds i a = if h : i < xs.size then xs.set i a h else xs
-- Batteries.Data.String.Lemmas
String.utf8Len_le_of_suffix : ∀ {cs₁ cs₂ : List Char}, cs₁ <:+ cs₂ → String.utf8Len cs₁ ≤ String.utf8Len cs₂
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommSemigroup : {M : Type u_1} →
  [inst : TopologicalSpace M] →
    [inst_1 : AddCommSemigroup M] → [ContinuousAdd M] → AddCommSemigroup (SeparationQuotient M)
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
_private.Mathlib.Analysis.CStarAlgebra.ApproximateUnit.0.termσ : Lean.ParserDescr
-- Lean.Meta.Basic
/-- Similar to `abstractM` but consider only the first `min n xs.size` entries in `xs`

It is also similar to `Expr.abstractRange`, but handles metavariables correctly.
It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
 -/
Lean.Expr.abstractRangeM : Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Smooth.IntegralClosure
TensorProduct.toIntegralClosure_bijective_of_smooth : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Smooth R S],
  Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.memAddSubmonoid : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddMonoid Y]
  (D : Function.locallyFinsuppWithin U Y), ⇑D ∈ Function.locallyFinsuppWithin.addSubmonoid U
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.contDiff_exp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {n : WithTop ℕ∞},
  ContDiff 𝕜 n Complex.exp
-- Init.Data.RArray
Lean.RArray.get_eq_getImpl : @Lean.RArray.get = @Lean.RArray.getImpl
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- `nonPrincipals R` is the set of all ideals of `R` that are not principal ideals.  -/
Ideal.nonPrincipals : (R : Type u) → [inst : Semiring R] → Set (Ideal R)
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
 -/
Lean.Core.CoreM.parIter : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (Std.IterM Lean.CoreM (Except Lean.Exception α))
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.mulActionWithZero : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      [inst : MonoidWithZero α] →
        [inst_1 : (i : I) → Zero (f i)] → [(i : I) → MulActionWithZero α (f i)] → MulActionWithZero α ((i : I) → f i)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.map_bot : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Subalgebra.map f ⊥ = ⊥
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {b : α} {n : ℕ},
  n • a +ᵥ b = b ↔ Function.minimalPeriod (fun x => a +ᵥ x) b ∣ n
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A), P.symm.ι = P.ι
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_le_card : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V], G.chromaticNumber ≤ ↑(Fintype.card V)
-- Mathlib.Data.Rat.Lemmas
Rat.inv_natCast_num_of_pos : ∀ {a : ℕ}, 0 < a → (↑a)⁻¹.num = 1
-- Mathlib.Order.SetNotation
/-- Delaborator for indexed intersections.  -/
Set.sInter_delab : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Nat.GCD.Basic
Nat.gcd_right_comm : ∀ (a b c : ℕ), (a.gcd b).gcd c = (a.gcd c).gcd b
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mk.sizeOf_spec : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] [inst_7 : SizeOf k] [inst_8 : SizeOf P₁] [inst_9 : SizeOf P₂]
  [inst_10 : SizeOf V₁] [inst_11 : SizeOf V₂] (toEquiv : P₁ ≃ P₂) (linear : V₁ ≃ₗ[k] V₂)
  (map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p),
  sizeOf { toEquiv := toEquiv, linear := linear, map_vadd' := map_vadd' } = 1 + sizeOf toEquiv + sizeOf linear
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_pos : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 < z⁻¹ ↔ 0 < z
-- Init.Data.Array.MapIdx
List.mapIdxM.go.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : ℕ → α → m β) (a : Array β),
  List.mapIdxM.go f [] a = pure a.toList
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.Balanced.isIso_of_mono_of_epi : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Balanced C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Mono f] [CategoryTheory.Epi f], CategoryTheory.IsIso f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.entryAtIdxD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.nonempty_dart_top : ∀ {V : Type u_1} [Nontrivial V], Nonempty ⊤.Dart
-- Mathlib.RingTheory.Teichmuller
/-- Given an `I`-adically complete ring `R`, and a prime number `p` with `p ∈ I`, this is the
multiplicative map from `Perfection (R ⧸ I) p` to `R` itself. Specifically, it is defined as the
limit of `p^n`-th powers of arbitrary lifts in `R` of the `n`-th component from the perfection of
`R ⧸ I`.

The simp NF is `teichmuller₀`.  -/
Perfection.teichmuller : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommRing R] →
        (I : Ideal R) → [inst_2 : CharP (R ⧸ I) p] → [IsAdicComplete I R] → Perfection (R ⧸ I) p →* R
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)]
  (X : CategoryTheory.Grothendieck F) {Z : H}
  (h : CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base) h)
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRocIterIteratorOfUpwardEnumerable : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.ToStream (Std.Roc α) (Std.Iter α)